diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index e25e1f5ac..40acb45fe 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/crucible-llvm/crucible-llvm.cabal @@ -91,6 +91,7 @@ library Lang.Crucible.LLVM.QQ Lang.Crucible.LLVM.SymIO Lang.Crucible.LLVM.SimpleLoopFixpoint + Lang.Crucible.LLVM.SimpleLoopFixpointCHC Lang.Crucible.LLVM.SimpleLoopInvariant Lang.Crucible.LLVM.Translation Lang.Crucible.LLVM.Translation.Aliases diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index c271ff16f..95aec1285 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs @@ -94,6 +94,7 @@ module Lang.Crucible.LLVM.MemModel , unpackMemValue , packMemValue , loadRaw + , loadArrayConcreteSizeRaw , storeRaw , condStoreRaw , storeConstRaw @@ -161,6 +162,7 @@ module Lang.Crucible.LLVM.MemModel , G.pushStackFrameMem , G.popStackFrameMem , G.asMemAllocationArrayStore + , G.asMemMatchingArrayStore , SomeFnHandle(..) , G.SomeAlloc(..) , G.possibleAllocs @@ -212,6 +214,7 @@ import qualified Text.LLVM.AST as L import What4.Interface import What4.Expr( GroundValue ) +import qualified What4.Expr.ArrayUpdateMap as AUM import What4.InterpretedFloatingPoint import What4.ProgramLoc @@ -1253,6 +1256,40 @@ loadRaw sym mem ptr valType alignment = do let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr G.readMem sym PtrWidth gsym ptr valType alignment (memImplHeap mem) +-- | Load an array with concrete size from memory. +loadArrayConcreteSizeRaw :: + forall sym wptr . + (IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym, ?memOpts :: MemOptions) => + sym -> + MemImpl sym -> + LLVMPtr sym wptr -> + Natural -> + Alignment -> + IO (Either (Pred sym) (Pred sym, SymArray sym (SingleCtx (BaseBVType wptr)) (BaseBVType 8))) +loadArrayConcreteSizeRaw sym mem ptr sz alignment + | sz == 0 = do + zero_bv <- bvLit sym knownNat $ BV.zero knownNat + zero_arr <- constantArray sym (Ctx.singleton $ BaseBVRepr PtrWidth) zero_bv + return $ Right (truePred sym, zero_arr) + | otherwise = do + let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) ptr + res <- G.readMem sym PtrWidth gsym ptr (arrayType sz $ bitvectorType 1) alignment (memImplHeap mem) + case res of + Partial.NoErr ok llvm_val_arr -> do + case llvm_val_arr of + LLVMValArray _ llvm_vals -> do + let aum = AUM.fromAscList knownRepr $ V.toList $ V.imap + (\i -> \case + LLVMValInt _ byte | Just Refl <- testEquality (knownNat @8) (bvWidth byte) -> + (Ctx.singleton $ BVIndexLit PtrWidth $ BV.mkBV PtrWidth $ fromIntegral i, byte) + _ -> panic "MemModel.loadArrayRaw" ["expected LLVMValInt"]) + llvm_vals + zero_bv <- bvLit sym knownNat $ BV.zero knownNat + arr <- arrayFromMap sym (Ctx.singleton $ BaseBVRepr PtrWidth) aum zero_bv + return $ Right (ok, arr) + _ -> panic "MemModel.loadArrayRaw" ["expected LLVMValArray"] + Partial.Err err -> return $ Left err + -- | Store an LLVM value in memory. Asserts that the pointer is valid and points -- to a mutable memory region. storeRaw :: diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs index 3ff5651b2..979568c72 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs @@ -58,6 +58,7 @@ module Lang.Crucible.LLVM.MemModel.Generic , branchAbortMem , mergeMem , asMemAllocationArrayStore + , asMemMatchingArrayStore , isAligned , SomeAlloc(..) @@ -78,6 +79,7 @@ import Prelude hiding (pred) import Control.Lens import Control.Monad import Control.Monad.State.Strict +import Control.Monad.Trans.Maybe import Data.IORef import Data.Maybe import qualified Data.List as List @@ -90,6 +92,7 @@ import Numeric.Natural import Prettyprinter import Lang.Crucible.Panic (panic) +import Data.BitVector.Sized (BV) import qualified Data.BitVector.Sized as BV import Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx @@ -790,7 +793,9 @@ readMem' sym w end gsym l0 origMem tp0 alignment (MemWrites ws) = else do -- We're playing a trick here. By making a fresh constant a proof obligation, we can be -- sure it always fails. But, because it's a variable, it won't be constant-folded away -- and we can be relatively sure the annotation will survive. - b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr + b <- if noSatisfyingWriteFreshConstant ?memOpts + then freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr + else return $ falsePred sym Partial.Err <$> Partial.annotateME sym mop (NoSatisfyingWrite tp) b @@ -1449,7 +1454,7 @@ writeArrayMemWithAllocationCheck is_allocated sym w ptr alignment arr sz m = _ -> return default_m - return (m', p1, p2) + return (memInsertArrayBlock (llvmPointerBlock ptr) m', p1, p2) -- | Write an array to memory. -- @@ -1629,6 +1634,22 @@ possibleAllocs n mem = Just (AllocInfo atp sz mut alignment loc) -> [SomeAlloc atp n sz mut alignment loc] +-- | 'IO' plus memoization. The 'IORef' stores suspended computations with +-- 'Left' and evaluated results with 'Right'. +newtype MemoIO m a = MemoIO (IORef (Either (m a) a)) + +putMemoIO :: MonadIO m => m a -> m (MemoIO m a) +putMemoIO comp = MemoIO <$> liftIO (newIORef $ Left comp) + +getMemoIO :: MonadIO m => MemoIO m a -> m a +getMemoIO (MemoIO ref) = liftIO (readIORef ref) >>= \case + Left comp -> do + res <- comp + liftIO $ writeIORef ref $ Right res + return res + Right res -> return res + + -- | Check if @LLVMPtr sym w@ points inside an allocation that is backed -- by an SMT array store. If true, return a predicate that indicates -- when the given array backs the given pointer, the SMT array, @@ -1649,75 +1670,134 @@ asMemAllocationArrayStore :: IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8), (SymBV sym w))) asMemAllocationArrayStore sym w ptr mem | Just blk_no <- asNat (llvmPointerBlock ptr) + , memMemberArrayBlock (llvmPointerBlock ptr) mem , [SomeAlloc _ _ (Just sz) _ _ _] <- List.nub (possibleAllocs blk_no mem) , Just Refl <- testEquality w (bvWidth sz) = - do result <- findArrayStore blk_no sz $ memWritesAtConstant blk_no $ memWrites mem + do memo_nothing <- putMemoIO $ return Nothing + --putStrLn $ "asMemAllocationArrayStore: base=" ++ show blk_no ++ " sz=" ++ show (printSymExpr sz) + result <- findArrayStore sym w blk_no (BV.zero w) sz memo_nothing $ + memWritesAtConstant blk_no $ memWrites mem return $ case result of Just (ok, arr) -> Just (ok, arr, sz) Nothing -> Nothing | otherwise = return Nothing - where - findArrayStore :: - Natural -> - SymBV sym w -> - [MemWrite sym] -> - IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) - - findArrayStore _ _ [] = return Nothing - - findArrayStore blk_no sz (head_mem_write : tail_mem_writes) = - case head_mem_write of - MemWrite write_ptr write_source - | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) - , blk_no == write_blk_no - , Just (BV.BV 0) <- asBV (llvmPointerOffset write_ptr) - , MemArrayStore arr (Just arr_store_sz) <- write_source - , Just Refl <- testEquality w (ptrWidth write_ptr) -> do - ok <- bvEq sym sz arr_store_sz - return (Just (ok, arr)) - - | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) - , blk_no /= write_blk_no -> - findArrayStore blk_no sz tail_mem_writes - - | otherwise -> return Nothing - - WriteMerge cond lhs_mem_writes rhs_mem_writes -> do - lhs_result <- findArrayStore blk_no sz (memWritesAtConstant blk_no lhs_mem_writes) - rhs_result <- findArrayStore blk_no sz (memWritesAtConstant blk_no rhs_mem_writes) - - -- Only traverse the tail if necessary, and be careful - -- only to traverse it once - case (lhs_result, rhs_result) of - (Just _, Just _) -> combineResults cond lhs_result rhs_result - - (Just _, Nothing) -> - do rhs' <- findArrayStore blk_no sz tail_mem_writes - combineResults cond lhs_result rhs' - - (Nothing, Just _) -> - do lhs' <- findArrayStore blk_no sz tail_mem_writes - combineResults cond lhs' rhs_result - - (Nothing, Nothing) -> findArrayStore blk_no sz tail_mem_writes - - combineResults cond (Just (lhs_ok, lhs_arr)) (Just (rhs_ok, rhs_arr)) = - do ok <- itePred sym cond lhs_ok rhs_ok - arr <- arrayIte sym cond lhs_arr rhs_arr - pure (Just (ok,arr)) - - combineResults cond (Just (lhs_ok, lhs_arr)) Nothing = - do ok <- andPred sym cond lhs_ok - pure (Just (ok, lhs_arr)) - - combineResults cond Nothing (Just (rhs_ok, rhs_arr)) = - do cond' <- notPred sym cond - ok <- andPred sym cond' rhs_ok - pure (Just (ok, rhs_arr)) - - combineResults _cond Nothing Nothing = pure Nothing +asMemMatchingArrayStore :: + (IsSymInterface sym, 1 <= w) => + sym -> + NatRepr w -> + LLVMPtr sym w -> + SymBV sym w -> + Mem sym -> + IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) +asMemMatchingArrayStore sym w ptr sz mem + | Just blk_no <- asNat (llvmPointerBlock ptr) + , memMemberArrayBlock (llvmPointerBlock ptr) mem + , Just off <- asBV (llvmPointerOffset ptr) = do + --putStrLn $ "asMemMatchingArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz) + memo_nothing <- putMemoIO $ return Nothing + findArrayStore sym w blk_no off sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem + | otherwise = return Nothing + +findArrayStore :: + (IsSymInterface sym, 1 <= w) => + sym -> + NatRepr w -> + Natural -> + BV w -> + SymBV sym w -> + MemoIO IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) -> + [MemWrite sym] -> + IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8))) +findArrayStore sym w blk_no off sz memo_cont = \case + [] -> getMemoIO memo_cont + head_mem_write : tail_mem_writes -> do + --putStrLn $ " findArrayStore: ptr=" ++ show (blk_no, off) ++ " sz=" ++ show (printSymExpr sz) + --putStrLn $ " findArrayStore: write=" ++ (case head_mem_write of MemWrite{} -> "write"; WriteMerge{} -> "merge") + + case head_mem_write of + MemWrite write_ptr write_source + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no == write_blk_no + , Just Refl <- testEquality w (ptrWidth write_ptr) + , Just write_off <- asBV (llvmPointerOffset write_ptr) + , off == write_off + , MemArrayStore arr (Just arr_store_sz) <- write_source -> do + ok <- bvEq sym sz arr_store_sz + return (Just (ok, arr)) + + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no == write_blk_no + , Just Refl <- testEquality w (ptrWidth write_ptr) + , Just write_off <- asBV (llvmPointerOffset write_ptr) + , Just sz_bv <- asBV sz + , MemCopy src_ptr mem_copy_sz <- write_source + , Just mem_copy_sz_bv <- asBV mem_copy_sz + , BV.ule write_off off + , BV.ule (BV.add w off sz_bv) (BV.add w write_off mem_copy_sz_bv) + , Just src_blk_no <- asNat (llvmPointerBlock src_ptr) + , Just src_off <- asBV (llvmPointerOffset src_ptr) -> + findArrayStore sym w src_blk_no (BV.add w src_off $ BV.sub w off write_off) sz memo_cont tail_mem_writes + + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no == write_blk_no + , Just Refl <- testEquality w (ptrWidth write_ptr) + , Just write_off <- asBV (llvmPointerOffset write_ptr) + , Just sz_bv <- asBV sz + , MemSet val mem_set_sz <- write_source + , Just mem_set_sz_bv <- asBV mem_set_sz + , BV.ule write_off off + , BV.ule (BV.add w off sz_bv) (BV.add w write_off mem_set_sz_bv) -> do + arr <- constantArray sym (Ctx.singleton $ BaseBVRepr w) val + return $ Just (truePred sym, arr) + + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no == write_blk_no + , Just Refl <- testEquality w (ptrWidth write_ptr) + , Just write_off <- asBV (llvmPointerOffset write_ptr) -> do + maybe_write_sz <- runMaybeT $ writeSourceSize sym w write_source + case maybe_write_sz of + Just write_sz + | Just sz_bv <- asBV sz + , Just write_sz_bv <- asBV write_sz + , end <- BV.add w off sz_bv + , write_end <- BV.add w write_off write_sz_bv + , BV.ule end write_off || BV.ule write_end off -> + findArrayStore sym w blk_no off sz memo_cont tail_mem_writes + _ -> return Nothing + + | Just write_blk_no <- asNat (llvmPointerBlock write_ptr) + , blk_no /= write_blk_no -> + findArrayStore sym w blk_no off sz memo_cont tail_mem_writes + + | otherwise -> return Nothing + + WriteMerge cond lhs_mem_writes rhs_mem_writes -> do + -- Only traverse the tail if necessary, and be careful + -- only to traverse it once + memo_tail <- putMemoIO $ findArrayStore sym w blk_no off sz memo_cont tail_mem_writes + + lhs_result <- findArrayStore sym w blk_no off sz memo_tail (memWritesAtConstant blk_no lhs_mem_writes) + rhs_result <- findArrayStore sym w blk_no off sz memo_tail (memWritesAtConstant blk_no rhs_mem_writes) + + case (lhs_result, rhs_result) of + (Just (lhs_ok, lhs_arr), Just (rhs_ok, rhs_arr)) -> + do ok <- itePred sym cond lhs_ok rhs_ok + arr <- arrayIte sym cond lhs_arr rhs_arr + pure (Just (ok,arr)) + + (Just (lhs_ok, lhs_arr), Nothing) -> + do ok <- andPred sym cond lhs_ok + pure (Just (ok, lhs_arr)) + + (Nothing, Just (rhs_ok, rhs_arr)) -> + do cond' <- notPred sym cond + ok <- andPred sym cond' rhs_ok + pure (Just (ok, rhs_arr)) + + (Nothing, Nothing) -> pure Nothing + {- Note [Memory Model Design] diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs index 735575e85..5317528b5 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -56,6 +56,8 @@ module Lang.Crucible.LLVM.MemModel.MemLog , emptyChanges , emptyMem , memEndian + , memInsertArrayBlock + , memMemberArrayBlock -- * Pretty printing , ppType @@ -87,6 +89,8 @@ import qualified Data.List.Extra as List import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe (mapMaybe) +import Data.Set (Set) +import qualified Data.Set as Set import Data.Text (Text) import Numeric.Natural import Prettyprinter @@ -326,7 +330,7 @@ data MemWrite sym -- implementation is able to efficiently merge memories, but requires -- that one only merge memories that were identical prior to the last -- branch. -data Mem sym = Mem { memEndianForm :: EndianForm, _memState :: MemState sym } +data Mem sym = Mem { memEndianForm :: EndianForm, _memState :: MemState sym, memArrayBlocks :: Set Natural } memState :: Lens' (Mem sym) (MemState sym) memState = lens _memState (\s v -> s { _memState = v }) @@ -417,11 +421,21 @@ emptyChanges :: MemChanges sym emptyChanges = (mempty, mempty) emptyMem :: EndianForm -> Mem sym -emptyMem e = Mem { memEndianForm = e, _memState = EmptyMem 0 0 emptyChanges } +emptyMem e = Mem { memEndianForm = e, _memState = EmptyMem 0 0 emptyChanges, memArrayBlocks = Set.empty } memEndian :: Mem sym -> EndianForm memEndian = memEndianForm +memInsertArrayBlock :: IsExprBuilder sym => SymNat sym -> Mem sym -> Mem sym +memInsertArrayBlock blk mem = case asNat blk of + Just blk_no -> mem { memArrayBlocks = Set.insert blk_no (memArrayBlocks mem) } + Nothing -> mem { memArrayBlocks = Set.empty } + +memMemberArrayBlock :: IsExprBuilder sym => SymNat sym -> Mem sym -> Bool +memMemberArrayBlock blk mem = case asNat blk of + Just blk_no -> Set.member blk_no (memArrayBlocks mem) + Nothing -> False + -------------------------------------------------------------------------------- -- Pretty printing @@ -527,16 +541,19 @@ ppMem m = ppMemState ppMemChanges (m^.memState) multiUnion :: (Ord k, Semigroup a) => Map k a -> Map k a -> Map k a multiUnion = Map.unionWith (<>) +-- | This will return 'Just' if the size of the write is bounded and 'Nothing' +-- is the size of the write is unbounded. writeSourceSize :: - (IsExprBuilder sym, HasPtrWidth w) => + (IsExprBuilder sym, 1 <= w) => sym -> + NatRepr w -> WriteSource sym w -> MaybeT IO (SymBV sym w) -writeSourceSize sym = \case +writeSourceSize sym w = \case MemCopy _src sz -> pure sz MemSet _val sz -> pure sz MemStore _val st _align -> - liftIO $ bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth $ toInteger $ typeEnd 0 st + liftIO $ bvLit sym w $ BV.mkBV w $ toInteger $ typeEnd 0 st MemArrayStore _arr Nothing -> MaybeT $ pure Nothing MemArrayStore _arr (Just sz) -> pure sz MemInvalidate _nm sz -> pure sz @@ -551,7 +568,7 @@ writeRangesMemWrite sym = \case | Just Refl <- testEquality ?ptrWidth (ptrWidth ptr) -> case asNat (llvmPointerBlock ptr) of Just blk -> do - sz <- writeSourceSize sym wsrc + sz <- writeSourceSize sym ?ptrWidth wsrc pure $ Map.singleton blk [(llvmPointerOffset ptr, sz)] Nothing -> MaybeT $ pure Nothing | otherwise -> fail "foo" @@ -743,5 +760,6 @@ concMem :: sym -> (forall tp. SymExpr sym tp -> IO (GroundValue tp)) -> Mem sym -> IO (Mem sym) -concMem sym conc (Mem endian st) = - Mem endian <$> concMemState sym conc st +concMem sym conc mem = do + conc_st <- concMemState sym conc $ mem ^. memState + return $ mem & memState .~ conc_st diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs index c6fd1bf0f..7e1181a7e 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Options.hs @@ -67,6 +67,13 @@ data MemOptions -- semantics. -- -- If 'laxLoadsAndStores' is disabled, this option has no effect. + + , noSatisfyingWriteFreshConstant :: !Bool + -- ^ If 'True', for the 'NoSatisfyingWrite' annotation, make a fresh + -- constant as a proof obligation, which ensures it always fails. But, + -- because it's a variable, it won't be constant-folded away and it's + -- relatively sure the annotation will survive. If 'False', annotate + -- 'false'. } @@ -115,6 +122,7 @@ defaultMemOptions = -- The choice of StableSymbolic here doesn't matter too much, since it -- won't have any effect when laxLoadsAndStores is disabled. , indeterminateLoadBehavior = StableSymbolic + , noSatisfyingWriteFreshConstant = True } diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs new file mode 100644 index 000000000..7765c57ab --- /dev/null +++ b/crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopFixpointCHC.hs @@ -0,0 +1,1421 @@ +------------------------------------------------------------------------ +-- | +-- Module : Lang.Crucible.LLVM.SimpleLoopFixpointCHC +-- Description : Execution feature to compute loop fixpoint in +-- conjunction with CHC +-- Copyright : (c) Galois, Inc 2021 +-- License : BSD3 +-- Stability : provisional +-- +-- This offers a similar API to what is offered in +-- "Lang.Crucible.LLVM.SimpleLoopFixpoint", but this generates proof obligations +-- involving a predicate function (named @inv@). The intent is that a user will +-- leverage Z3's constrained horn-clause (CHC) functionality to synthesize an +-- implementation of @inv@ and then substitute it back into the proof +-- obligations. +------------------------------------------------------------------------ + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TupleSections #-} + + +module Lang.Crucible.LLVM.SimpleLoopFixpointCHC + ( FixpointEntry(..) + , FixpointState(..) + , CallFrameContext(..) + , SomeCallFrameContext(..) + , ExecutionFeatureContext(..) + , simpleLoopFixpoint + ) where + +import Control.Lens +import Control.Monad +import Control.Monad.IO.Class +import Control.Monad.Reader +import Control.Monad.State +import Control.Monad.Trans.Maybe +import Data.Foldable +import qualified Data.IntMap as IntMap +import Data.IORef +import Data.Kind +import qualified Data.List as List +import Data.Maybe +import qualified Data.Map as Map +import Data.Map (Map) +import qualified Data.Sequence as Seq +import qualified Data.Set as Set +import Data.Set (Set) +import GHC.TypeLits (KnownNat) +import Numeric.Natural (Natural) +import qualified System.IO + +import qualified Data.BitVector.Sized as BV +import Data.Parameterized.Classes +import qualified Data.Parameterized.Context as Ctx +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.Map (MapF) +import Data.Parameterized.NatRepr +import Data.Parameterized.Some +import Data.Parameterized.TraversableF +import Data.Parameterized.TraversableFC + +import qualified What4.Config as W4 +import qualified What4.Expr.Builder as W4 +import qualified What4.Interface as W4 +import qualified What4.Solver as W4 + +import qualified Lang.Crucible.Analysis.Fixpoint.Components as C +import qualified Lang.Crucible.Backend as C +import qualified Lang.Crucible.CFG.Core as C +import qualified Lang.Crucible.FunctionHandle as C +import qualified Lang.Crucible.Panic as C +import qualified Lang.Crucible.Simulator.CallFrame as C +import qualified Lang.Crucible.Simulator.EvalStmt as C +import qualified Lang.Crucible.Simulator.ExecutionTree as C +import qualified Lang.Crucible.Simulator.GlobalState as C +import qualified Lang.Crucible.Simulator.Operations as C +import qualified Lang.Crucible.Simulator.RegMap as C +import qualified Lang.Crucible.Simulator as C + +import qualified Lang.Crucible.LLVM.Bytes as C +import qualified Lang.Crucible.LLVM.DataLayout as C +import qualified Lang.Crucible.LLVM.MemModel as C +import qualified Lang.Crucible.LLVM.MemModel.MemLog as C hiding (Mem) +import qualified Lang.Crucible.LLVM.MemModel.Pointer as C +import qualified Lang.Crucible.LLVM.MemModel.Type as C +-- import qualified Lang.Crucible.LLVM.MemModel.Generic as C (writeArrayMem) + + +-- | When live loop-carried dependencies are discovered as we traverse +-- a loop body, new "widening" variables are introduced to stand in +-- for those locations. When we introduce such a variable, we +-- capture what value the variable had when we entered the loop (the +-- \"header\" value); this is essentially the initial value of the +-- variable. We also compute what value the variable should take on +-- its next iteration assuming the loop doesn't exit and executes +-- along its backedge. This \"body\" value will be computed in +-- terms of the the set of all discovered live variables so far. +-- We know we have reached fixpoint when we don't need to introduce +-- and more fresh widening variables, and the body values for each +-- variable are stable across iterations. +data FixpointEntry sym tp = FixpointEntry + { headerValue :: W4.SymExpr sym tp + , bodyValue :: W4.SymExpr sym tp + } + +instance OrdF (W4.SymExpr sym) => OrdF (FixpointEntry sym) where + compareF x y = joinOrderingF + (compareF (headerValue x) (headerValue y)) + (compareF (bodyValue x) (bodyValue y)) +instance OrdF (FixpointEntry sym) => W4.TestEquality (FixpointEntry sym) where + testEquality x y = orderingF_refl $ compareF x y + +data MemLocation sym w = MemLocation + { memLocationBlock :: Natural + , memLocationOffset :: W4.SymBV sym w + , memLocationSize :: W4.SymBV sym w + } + +instance OrdF (W4.SymExpr sym) => Ord (MemLocation sym w) where + compare x y = + compare (memLocationBlock x) (memLocationBlock y) + <> toOrdering (compareF (memLocationOffset x) (memLocationOffset y)) + <> toOrdering (compareF (memLocationSize x) (memLocationSize y)) +instance OrdF (W4.SymExpr sym) => Eq (MemLocation sym w) where + x == y = EQ == compare x y + +data MemFixpointEntry sym wptr where + MemStoreFixpointEntry :: + (1 <= w) => + W4.SymBV sym w {- ^ bitvector join variable -} -> + C.StorageType -> + MemFixpointEntry sym wptr + MemArrayFixpointEntry :: + W4.SymArray sym (C.SingleCtx (W4.BaseBVType wptr)) (W4.BaseBVType 8) {- ^ array join variable -} -> + W4.SymBV sym wptr {- ^ length of the allocation -} -> + MemFixpointEntry sym wptr + + +-- | This datatype captures the state machine that progresses as we +-- attempt to compute a loop invariant for a simple structured loop. +data FixpointState sym wptr blocks args + -- | We have not yet encoundered the loop head + = BeforeFixpoint + + -- | We have encountered the loop head at least once, and are in the process + -- of converging to an inductive representation of the live variables + -- in the loop. + | ComputeFixpoint (FixpointRecord sym wptr blocks args) + + -- | We have found an inductively-strong representation of the live variables + -- of the loop, and have discovered the loop index structure controling the + -- execution of the loop. We are now executing the loop once more to compute + -- verification conditions for executions that reamain in the loop. + | CheckFixpoint + (FixpointRecord sym wptr blocks args) + (W4.SomeSymFn sym) -- ^ function that represents the loop invariant + (Some (Ctx.Assignment (W4.SymExpr sym))) -- ^ arguments to the loop invariant + (W4.Pred sym) -- ^ predicate that represents the loop condition + + -- | Finally, we stitch everything we have found together into the rest of the program. + -- Starting from the loop header one final time, we now force execution to exit the loop + -- and continue into the rest of the program. + | AfterFixpoint + (FixpointRecord sym wptr blocks args) + +-- | Data about the loop that we incrementally compute as we approach fixpoint. +data FixpointRecord sym wptr blocks args = FixpointRecord + { + -- | Block identifier of the head of the loop + fixpointBlockId :: C.BlockID blocks args + + -- | identifier for the currently-active assumption frame related to this fixpoint computation + , fixpointAssumptionFrameIdentifier :: C.FrameIdentifier + + -- | Map from introduced widening variables to prestate value before the loop starts, + -- and to the value computed in a single loop iteration, assuming we return to the + -- loop header. These variables may appear only in either registers or memory. + , fixpointSubstitution :: MapF (W4.SymExpr sym) (FixpointEntry sym) + + -- | Prestate values of the Crucible registers when the loop header is first encountered. + , fixpointRegMap :: C.RegMap sym args + + -- | Triples are (blockId, offset, size) to bitvector-typed entries ( bitvector only/not pointers ) + , fixpointMemSubstitution :: Map (MemLocation sym wptr) (MemFixpointEntry sym wptr) + + , fixpointEqualitySubstitution :: MapF (W4.SymExpr sym) (W4.SymExpr sym) + + -- | The loop index variable + , fixpointIndex :: W4.SymBV sym wptr + } + + +data CallFrameContext sym wptr ext init ret blocks = CallFrameContext + { callFrameContextFixpointStates :: MapF (C.BlockID blocks) (FixpointState sym wptr blocks) + , callFrameContextLoopHeaders :: [C.Some (C.BlockID blocks)] + , callFrameContextCFG :: C.CFG ext blocks init ret + , callFrameContextParentLoop :: Map (C.Some (C.BlockID blocks)) (C.Some (C.BlockID blocks)) + , callFrameContextLoopHeaderBlockIds :: Set (C.Some (C.BlockID blocks)) + } + +data CallFrameHandle init ret blocks = CallFrameHandle (C.FnHandle init ret) (Ctx.Assignment (Ctx.Assignment C.TypeRepr) blocks) + deriving (Eq, Ord, Show) + +data SomeCallFrameContext sym wptr ext init ret = + forall blocks . SomeCallFrameContext (CallFrameContext sym wptr ext init ret blocks) + +unwrapSomeCallFrameContext :: + Ctx.Assignment (Ctx.Assignment C.TypeRepr) blocks -> + SomeCallFrameContext sym wptr ext init ret -> + CallFrameContext sym wptr ext init ret blocks +unwrapSomeCallFrameContext blocks_repr (SomeCallFrameContext ctx) = + case W4.testEquality blocks_repr (fmapFC C.blockInputs $ C.cfgBlockMap $ callFrameContextCFG ctx) of + Just Refl -> ctx + Nothing -> C.panic "SimpleLoopFixpoint.unwrapSomeCallFrameContext" ["type mismatch"] + +data ExecutionFeatureContext sym wptr ext = ExecutionFeatureContext + { executionFeatureContextFixpointStates :: C.FnHandleMap (SomeCallFrameContext sym wptr ext) + , executionFeatureContextInvPreds :: [W4.SomeSymFn sym] + , executionFeatureContextLoopFunEquivConds :: [W4.Pred sym] + } + +callFrameContextLookup :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + CallFrameContext sym wptr ext init ret blocks +callFrameContextLookup (CallFrameHandle hdl blocks_repr) ctx = + unwrapSomeCallFrameContext blocks_repr $ + fromMaybe (C.panic "SimpleLoopFixpoint.callFrameContextLookup" ["missing call frame context", show hdl]) $ + C.lookupHandleMap hdl (executionFeatureContextFixpointStates ctx) + +callFrameContextUpdate :: + CallFrameHandle init ret blocks -> + (CallFrameContext sym wptr ext init ret blocks -> CallFrameContext sym wptr ext init ret blocks) -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +callFrameContextUpdate (CallFrameHandle hdl blocks_repr) f ctx = + ctx + { executionFeatureContextFixpointStates = C.updateHandleMap + (SomeCallFrameContext . f . unwrapSomeCallFrameContext blocks_repr) + hdl + (executionFeatureContextFixpointStates ctx) + } + +callFrameContextLookup' :: + CallFrameHandle init ret blocks -> + C.BlockID blocks args -> + ExecutionFeatureContext sym wptr ext -> + Maybe (FixpointState sym wptr blocks args) +callFrameContextLookup' hdl bid ctx = + MapF.lookup bid $ callFrameContextFixpointStates $ callFrameContextLookup hdl ctx + +callFrameContextInsert :: + CallFrameHandle init ret blocks -> + C.BlockID blocks args -> + FixpointState sym wptr blocks args -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +callFrameContextInsert hdl bid fs = + callFrameContextUpdate hdl $ + \ctx -> ctx { callFrameContextFixpointStates = MapF.insert bid fs (callFrameContextFixpointStates ctx) } + +callFrameContextPush :: + CallFrameHandle init ret blocks -> + C.Some (C.BlockID blocks) -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +callFrameContextPush hdl bid = + callFrameContextUpdate hdl $ + \ctx -> ctx { callFrameContextLoopHeaders = bid : callFrameContextLoopHeaders ctx } + +-- | Precondition: the context's 'callFrameContextLoopHeaders' should be +-- non-empty. +callFrameContextPop :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +callFrameContextPop hdl = + callFrameContextUpdate hdl $ + \ctx -> ctx { callFrameContextLoopHeaders = + case callFrameContextLoopHeaders ctx of + _:hdrs -> hdrs + [] -> C.panic "callFrameContextPop" + ["Empty callFrameContextLoopHeaders"] } + +callFrameContextPeek :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + Maybe (C.Some (C.BlockID blocks)) +callFrameContextPeek hdl ctx = + listToMaybe $ callFrameContextLoopHeaders $ callFrameContextLookup hdl ctx + +callFrameContextLoopHeaderBlockIds' :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + Set (C.Some (C.BlockID blocks)) +callFrameContextLoopHeaderBlockIds' hdl = + callFrameContextLoopHeaderBlockIds . callFrameContextLookup hdl + +callFrameContextParentLoop' :: + CallFrameHandle init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + Map (C.Some (C.BlockID blocks)) (C.Some (C.BlockID blocks)) +callFrameContextParentLoop' hdl = + callFrameContextParentLoop . callFrameContextLookup hdl + +executionFeatureContextAddCallFrameContext :: + CallFrameHandle init ret blocks -> + CallFrameContext sym wptr ext init ret blocks -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +executionFeatureContextAddCallFrameContext (CallFrameHandle hdl _blocks_repr) ctx context = + context + { executionFeatureContextFixpointStates = + C.insertHandleMap hdl (SomeCallFrameContext ctx) (executionFeatureContextFixpointStates context) + } + +executionFeatureContextAddInvPred :: + W4.SomeSymFn sym -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +executionFeatureContextAddInvPred inv_pred context = + context { executionFeatureContextInvPreds = inv_pred : executionFeatureContextInvPreds context } + +executionFeatureContextAddLoopFunEquivCond :: + W4.Pred sym -> + ExecutionFeatureContext sym wptr ext -> + ExecutionFeatureContext sym wptr ext +executionFeatureContextAddLoopFunEquivCond cond context = + context { executionFeatureContextLoopFunEquivConds = cond : executionFeatureContextLoopFunEquivConds context } + + +newtype FixpointMonad sym a = + FixpointMonad (StateT (MapF (W4.SymExpr sym) (FixpointEntry sym)) IO a) + deriving (Functor, Applicative, Monad, MonadIO, MonadFail) + +deriving instance s ~ MapF (W4.SymExpr sym) (FixpointEntry sym) => MonadState s (FixpointMonad sym) + +runFixpointMonad :: + FixpointMonad sym a -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + IO (a, MapF (W4.SymExpr sym) (FixpointEntry sym)) +runFixpointMonad (FixpointMonad m) = runStateT m + + +joinRegEntries :: + (?logMessage :: String -> IO (), C.IsSymInterface sym) => + sym -> + Ctx.Assignment (C.RegEntry sym) ctx -> + Ctx.Assignment (C.RegEntry sym) ctx -> + FixpointMonad sym (Ctx.Assignment (C.RegEntry sym) ctx) +joinRegEntries sym = Ctx.zipWithM (joinRegEntry sym) + +joinRegEntry :: + (?logMessage :: String -> IO (), C.IsSymInterface sym) => + sym -> + C.RegEntry sym tp -> + C.RegEntry sym tp -> + FixpointMonad sym (C.RegEntry sym tp) +joinRegEntry sym left right = case C.regType left of + C.LLVMPointerRepr w + + -- special handling for "don't care" registers coming from Macaw + | List.isPrefixOf "cmacaw_reg" (show $ W4.printSymNat $ C.llvmPointerBlock (C.regValue left)) + , List.isPrefixOf "cmacaw_reg" (show $ W4.printSymExpr $ C.llvmPointerOffset (C.regValue left)) -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: cmacaw_reg" + return left + + | C.llvmPointerBlock (C.regValue left) == C.llvmPointerBlock (C.regValue right) -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr" + subst <- get + if isJust (W4.testEquality (C.llvmPointerOffset (C.regValue left)) (C.llvmPointerOffset (C.regValue right))) + then do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: left == right" + return left + else case MapF.lookup (C.llvmPointerOffset (C.regValue left)) subst of + Just join_entry -> do + liftIO $ ?logMessage $ + "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Just: " + ++ show (W4.printSymExpr $ bodyValue join_entry) + ++ " -> " + ++ show (W4.printSymExpr $ C.llvmPointerOffset (C.regValue right)) + put $ MapF.insert + (C.llvmPointerOffset (C.regValue left)) + (join_entry { bodyValue = C.llvmPointerOffset (C.regValue right) }) + subst + return left + Nothing -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: Nothing" + join_variable <- liftIO $ W4.freshConstant sym (W4.safeSymbol "reg_join_var") (W4.BaseBVRepr w) + let join_entry = FixpointEntry + { headerValue = C.llvmPointerOffset (C.regValue left) + , bodyValue = C.llvmPointerOffset (C.regValue right) + } + put $ MapF.insert join_variable join_entry subst + return $ C.RegEntry (C.LLVMPointerRepr w) $ C.LLVMPointer (C.llvmPointerBlock (C.regValue left)) join_variable + | Just{} <- W4.asConcrete (C.llvmPointerOffset (C.regValue left)) -> do + return $ C.RegEntry (C.LLVMPointerRepr w) $ C.LLVMPointer (C.llvmPointerBlock (C.regValue left)) (C.llvmPointerOffset (C.regValue left)) + | otherwise -> + fail $ + "SimpleLoopFixpoint.joinRegEntry: LLVMPointerRepr: unsupported pointer base join: " + ++ show (C.ppPtr $ C.regValue left) + ++ " \\/ " + ++ show (C.ppPtr $ C.regValue right) + + C.BoolRepr + | List.isPrefixOf "cmacaw" (show $ W4.printSymExpr $ C.regValue left) -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: cmacaw_reg" + return left + | otherwise -> do + liftIO $ ?logMessage $ + "SimpleLoopFixpoint.joinRegEntry: BoolRepr:" + ++ show (W4.printSymExpr $ C.regValue left) + ++ " \\/ " + ++ show (W4.printSymExpr $ C.regValue right) + join_varaible <- liftIO $ W4.freshConstant sym (W4.safeSymbol "macaw_reg") W4.BaseBoolRepr + return $ C.RegEntry C.BoolRepr join_varaible + + C.StructRepr field_types -> do + liftIO $ ?logMessage "SimpleLoopFixpoint.joinRegEntry: StructRepr" + C.RegEntry (C.regType left) <$> fmapFC (C.RV . C.regValue) <$> joinRegEntries sym + (Ctx.generate (Ctx.size field_types) $ \i -> + C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue left) Ctx.! i) + (Ctx.generate (Ctx.size field_types) $ \i -> + C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue right) Ctx.! i) + _ -> fail $ "SimpleLoopFixpoint.joinRegEntry: unsupported type: " ++ show (C.regType left) + + +applySubstitutionRegEntries :: + C.IsSymInterface sym => + sym -> + MapF (W4.SymExpr sym) (W4.SymExpr sym) -> + Ctx.Assignment (C.RegEntry sym) ctx -> + Ctx.Assignment (C.RegEntry sym) ctx +applySubstitutionRegEntries sym substitution = fmapFC (applySubstitutionRegEntry sym substitution) + +applySubstitutionRegEntry :: + C.IsSymInterface sym => + sym -> + MapF (W4.SymExpr sym) (W4.SymExpr sym) -> + C.RegEntry sym tp -> + C.RegEntry sym tp +applySubstitutionRegEntry sym substitution entry = case C.regType entry of + C.LLVMPointerRepr{} -> + entry + { C.regValue = C.LLVMPointer + (C.llvmPointerBlock (C.regValue entry)) + (MapF.findWithDefault + (C.llvmPointerOffset (C.regValue entry)) + (C.llvmPointerOffset (C.regValue entry)) + substitution) + } + C.BoolRepr -> + entry + C.StructRepr field_types -> + entry + { C.regValue = fmapFC (C.RV . C.regValue) $ + applySubstitutionRegEntries sym substitution $ + Ctx.generate (Ctx.size field_types) $ + \i -> C.RegEntry (field_types Ctx.! i) $ C.unRV $ (C.regValue entry) Ctx.! i + } + _ -> C.panic "SimpleLoopFixpoint.applySubstitutionRegEntry" ["unsupported type: " ++ show (C.regType entry)] + + +joinMem :: + forall sym wptr . + (C.IsSymInterface sym, C.HasPtrWidth wptr) => + sym -> + C.MemImpl sym -> + C.MemWrites sym -> + IO (Map (MemLocation sym wptr) (MemFixpointEntry sym wptr)) +joinMem sym mem_impl mem_writes = do + ranges <- maybe (fail "SimpleLoopFixpoint: unsupported symbolic pointers") return =<< + runMaybeT (C.writeRangesMem @_ @wptr sym $ C.memImplHeap mem_impl) + + mem_subst <- case mem_writes of + C.MemWrites [C.MemWritesChunkIndexed indexed_writes] -> Map.fromList . catMaybes <$> mapM + (\case + C.MemWrite ptr mem_source + | Just Refl <- W4.testEquality ?ptrWidth (C.ptrWidth ptr) + , Just blk <- W4.asNat (C.llvmPointerBlock ptr) -> do + sz <- maybe (fail "SimpleLoopFixpoint: unsupported MemSource") return =<< + runMaybeT (C.writeSourceSize sym (C.ptrWidth ptr) mem_source) + let mem_loc = MemLocation + { memLocationBlock = blk + , memLocationOffset = C.llvmPointerOffset ptr + , memLocationSize = sz + } + + is_loop_local <- and <$> mapM + (\(prev_off, prev_sz) -> do + disjoint_pred <- C.buildDisjointRegionsAssertionWithSub + sym + ptr + sz + (C.LLVMPointer (C.llvmPointerBlock ptr) prev_off) + prev_sz + return $ W4.asConstantPred disjoint_pred == Just True) + (Map.findWithDefault [] blk ranges) + + if not is_loop_local then do + mem_entry <- case mem_source of + C.MemStore _ storage_type _ -> + case W4.mkNatRepr $ C.bytesToBits (C.typeEnd 0 storage_type) of + C.Some bv_width + | Just C.LeqProof <- W4.testLeq (W4.knownNat @1) bv_width -> do + join_variable <- W4.freshConstant sym (W4.safeSymbol "mem_join_var") (W4.BaseBVRepr bv_width) + return $ MemStoreFixpointEntry join_variable storage_type + | otherwise -> + C.panic + "SimpleLoopFixpoint.simpleLoopFixpoint" + ["unexpected storage type " ++ show storage_type] + + C.MemArrayStore arr _ -> do + join_variable <- W4.freshConstant sym (W4.safeSymbol "mem_join_var") (W4.exprType arr) + return $ MemArrayFixpointEntry join_variable sz + + _ -> fail "SimpleLoopFixpoint.joinMem: unsupported MemSource" + + return $ Just (mem_loc, mem_entry) + + else + return Nothing + + _ -> fail $ "SimpleLoopFixpoint: not MemWrite: " ++ show (C.ppMemWrites mem_writes)) + (List.concat $ IntMap.elems indexed_writes) + + C.MemWrites [] -> return Map.empty + + _ -> fail $ "SimpleLoopFixpoint: not MemWritesChunkIndexed: " ++ show (C.ppMemWrites mem_writes) + + checkDisjointRegions sym $ Map.keys mem_subst + + return mem_subst + +checkDisjointRegions :: + (C.IsSymInterface sym, C.HasPtrWidth wptr) => + sym -> + [MemLocation sym wptr] -> + IO () +checkDisjointRegions sym = \case + hd_mem_loc : tail_mem_locs -> do + mapM_ (checkDisjointRegions' sym hd_mem_loc) tail_mem_locs + checkDisjointRegions sym tail_mem_locs + [] -> return () + +checkDisjointRegions' :: + (C.IsSymInterface sym, C.HasPtrWidth wptr) => + sym -> + MemLocation sym wptr -> + MemLocation sym wptr -> + IO () +checkDisjointRegions' sym mem_loc1 mem_loc2 = do + ptr1 <- memLocationPtr sym mem_loc1 + ptr2 <- memLocationPtr sym mem_loc2 + disjoint_pred <- C.buildDisjointRegionsAssertionWithSub + sym + ptr1 + (memLocationSize mem_loc1) + ptr2 + (memLocationSize mem_loc2) + when (W4.asConstantPred disjoint_pred /= Just True) $ + fail $ + "SimpleLoopFixpoint: non-disjoint ranges: off1=" + ++ show (W4.printSymExpr $ C.llvmPointerOffset ptr1) + ++ ", sz1=" + ++ show (W4.printSymExpr $ memLocationSize mem_loc1) + ++ ", off2=" + ++ show (W4.printSymExpr $ C.llvmPointerOffset ptr2) + ++ ", sz2=" + ++ show (W4.printSymExpr $ memLocationSize mem_loc2) + + +loadMemJoinVariables :: + (C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => + bak -> + C.MemImpl sym -> + Map (MemLocation sym wptr) (MemFixpointEntry sym wptr) -> + IO (MapF (W4.SymExpr sym) (W4.SymExpr sym)) +loadMemJoinVariables bak mem subst = + let sym = C.backendGetSym bak in + MapF.fromList . catMaybes <$> mapM + (\(mem_loc, mem_entry) -> do + ptr <- memLocationPtr sym mem_loc + case mem_entry of + MemStoreFixpointEntry join_variable storage_type -> do + val <- C.doLoad bak mem ptr storage_type (C.LLVMPointerRepr $ W4.bvWidth join_variable) C.noAlignment + case W4.asNat (C.llvmPointerBlock val) of + Just 0 -> return $ Just $ MapF.Pair join_variable $ C.llvmPointerOffset val + _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val) + -- foo <- C.loadRaw sym mem ptr storage_type C.noAlignment + -- case foo of + -- C.NoErr _p val' -> do + -- val <- C.unpackMemValue sym (C.LLVMPointerRepr $ W4.bvWidth join_variable) val' + -- case W4.asNat (C.llvmPointerBlock val) of + -- Just 0 -> return $ Just $ MapF.Pair join_variable $ C.llvmPointerOffset val + -- _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables: unexpected val:" ++ show (C.ppPtr val) + -- C.Err{} -> -- return Nothing + -- fail $ "SimpleLoopFixpoint.loadMemJoinVariables: loadRaw failed" + MemArrayFixpointEntry join_variable _size -> do + -- TODO: handle arrays + maybe_allocation_array <- C.asMemAllocationArrayStore sym ?ptrWidth ptr (C.memImplHeap mem) + case maybe_allocation_array of + Just (ok, arr, _arr_sz) | Just True <- W4.asConstantPred ok -> do + return $ Just $ MapF.Pair join_variable arr + _ -> fail $ "SimpleLoopFixpoint.loadMemJoinVariables") + (Map.toAscList subst) + +storeMemJoinVariables :: + (C.IsSymBackend sym bak, C.HasPtrWidth wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => + bak -> + C.MemImpl sym -> + Map (MemLocation sym wptr) (MemFixpointEntry sym wptr) -> + MapF (W4.SymExpr sym) (W4.SymExpr sym) -> + IO (C.MemImpl sym) +storeMemJoinVariables bak mem mem_subst eq_subst = do + let sym = C.backendGetSym bak + foldlM + (\mem_acc (mem_loc, mem_entry) -> do + ptr <- memLocationPtr sym mem_loc + case mem_entry of + MemStoreFixpointEntry join_variable storage_type -> do + C.doStore bak mem_acc ptr (C.LLVMPointerRepr $ W4.bvWidth join_variable) storage_type C.noAlignment =<< + C.llvmPointer_bv sym (findWithDefaultKey eq_subst join_variable) + MemArrayFixpointEntry join_variable size -> do + C.doArrayStore bak mem_acc ptr C.noAlignment (findWithDefaultKey eq_subst join_variable) size) + -- (heap, p1, p2) <- C.writeArrayMem + -- sym + -- ?ptrWidth + -- ptr + -- C.noAlignment + -- (findWithDefaultKey eq_subst join_variable) + -- (Just size) + -- (C.memImplHeap mem_acc) + -- return $ mem_acc { C.memImplHeap = heap }) + mem + (Map.toAscList mem_subst) + +memLocationPtr :: + C.IsSymInterface sym => + sym -> + MemLocation sym wptr -> + IO (C.LLVMPtr sym wptr) +memLocationPtr sym (MemLocation { memLocationBlock = blk, memLocationOffset = off }) = + C.LLVMPointer <$> W4.natLit sym blk <*> return off + + +dropMemStackFrame :: C.IsSymInterface sym => C.MemImpl sym -> (C.MemImpl sym, C.MemAllocs sym, C.MemWrites sym) +dropMemStackFrame mem = case (C.memImplHeap mem) ^. C.memState of + (C.StackFrame _ _ _ (a, w) s) -> ((mem { C.memImplHeap = (C.memImplHeap mem) & C.memState .~ s }), a, w) + _ -> C.panic "SimpleLoopFixpoint.dropMemStackFrame" ["not a stack frame:", show (C.ppMem $ C.memImplHeap mem)] + + +filterSubstitution :: + C.IsSymInterface sym => + sym -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + MapF (W4.SymExpr sym) (FixpointEntry sym) +filterSubstitution sym substitution = + -- TODO: fixpoint + let uninterp_constants = foldMapF + (Set.map (C.mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . bodyValue) + substitution + in + MapF.filterWithKey (\variable _entry -> Set.member (C.Some variable) uninterp_constants) substitution + +loopIndexLinearSubstitution :: + (C.IsSymInterface sym, C.HasPtrWidth wptr, MonadIO m) => + sym -> + W4.SymBV sym wptr -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + m (MapF (W4.SymExpr sym) (W4.SymExpr sym)) +loopIndexLinearSubstitution sym index_variable = + MapF.traverseMaybeWithKey + (\variable entry -> case W4.testEquality (W4.exprType variable) (W4.exprType index_variable) of + Just Refl -> do + diff <- liftIO $ W4.bvSub sym (bodyValue entry) variable + case W4.asBV diff of + Just{} -> liftIO $ Just <$> (W4.bvAdd sym (headerValue entry) =<< W4.bvMul sym index_variable diff) + Nothing -> return Nothing + Nothing -> return Nothing) + +-- find widening variables that are actually the same (up to syntactic equality) +-- and can be substituted for each other +uninterpretedConstantEqualitySubstitution :: + (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, MonadIO m, MonadFail m, ?logMessage :: String -> IO ()) => + sym -> + MapF (W4.SymExpr sym) (FixpointEntry sym) -> + m (MapF (W4.SymExpr sym) (FixpointEntry sym), MapF (W4.SymExpr sym) (W4.SymExpr sym)) +uninterpretedConstantEqualitySubstitution sym substitution = do + let reverse_substitution = MapF.foldlWithKey' + (\accumulator variable entry -> MapF.insert entry variable accumulator) + MapF.empty + substitution + let uninterpreted_constant_substitution = + MapF.filterWithKey (\variable entry -> isNothing $ W4.testEquality variable entry) $ + fmapF (\entry -> fromJust $ MapF.lookup entry reverse_substitution) + substitution + let normal_substitution = MapF.filterWithKey + (\variable _entry -> isNothing $ MapF.lookup variable uninterpreted_constant_substitution) + substitution + + liftIO $ ?logMessage "vars:" + mapM_ + (\(MapF.Pair variable entry) -> do + let body_vars = Set.map (C.mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry + liftIO $ ?logMessage $ show (W4.printSymExpr variable) ++ " :: "++ show (W4.exprType variable) ++ " -> " ++ (show $ Set.map (C.viewSome $ show . W4.printSymExpr) $ body_vars)) + (MapF.toList normal_substitution) + + foo <- MapF.fromList <$> filterM + (\(MapF.Pair variable entry) -> do + let body_vars = Set.map (C.mapSome $ W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry + if Set.notMember (C.Some variable) body_vars then do + let lalala = runIdentity $ MapF.fromKeysM (return . W4.varExpr sym) $ W4.exprUninterpConstants sym $ bodyValue entry + let foobar = fmapF headerValue $ MapF.mapMaybe (\v -> MapF.lookup v normal_substitution) lalala + bar <- liftIO $ W4.isEq sym (headerValue entry) =<< W4.substituteBoundVars sym foobar (bodyValue entry) + liftIO $ ?logMessage $ "la: " ++ (show $ W4.printSymExpr variable) + liftIO $ ?logMessage $ "headerValue entry: " ++ (show $ W4.printSymExpr $ headerValue entry) + liftIO $ ?logMessage $ "bodyValue entry:" ++ (show $ W4.printSymExpr $ bodyValue entry) + liftIO $ ?logMessage $ "bar: " ++ (show $ W4.printSymExpr $ bar) + if Just True == W4.asConstantPred bar then do + liftIO $ ?logMessage "lala" + return True + else do + notbar <- liftIO $ W4.notPred sym bar + lala <- liftIO $ W4.runZ3InOverride sym (W4.defaultLogData { W4.logVerbosity = 2 }) [notbar] $ return . W4.isUnsat + when lala $ do + liftIO $ ?logMessage "lalala" + return lala + else + return False) + (MapF.toList normal_substitution) + + unless (Set.disjoint (Set.fromList $ MapF.keys foo) (foldMapF (Set.map (C.mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym) $ fmapF bodyValue foo)) $ + fail "SimpleLoopFixpoint: uninterpretedConstantEqualitySubstitution: not disjoint" + + return + ( MapF.mergeWithKey (\_ _ _ -> Nothing) id (const MapF.empty) normal_substitution foo -- difference + , MapF.mergeWithKey (\_ _ -> Just) id id uninterpreted_constant_substitution $ fmapF bodyValue foo -- union + ) + + +-- -- | Given the WTO analysis results, find the nth loop. +-- -- Return the identifier of the loop header, and a list of all the blocks +-- -- that are part of the loop body. It is at this point that we check +-- -- that the loop has the necessary properties; there must be a single +-- -- entry point to the loop, and it must have a single back-edge. Otherwise, +-- -- the analysis will not work correctly. +-- computeLoopBlocks :: forall ext blocks init ret k . +-- (k ~ C.Some (C.BlockID blocks)) => +-- C.CFG ext blocks init ret -> +-- Integer -> +-- IO (k, [k]) +-- computeLoopBlocks cfg loopNum = +-- case List.genericDrop loopNum (Map.toList loop_map) of +-- [] -> fail ("Did not find " ++ show loopNum ++ " loop headers") +-- (p:_) -> do checkSingleEntry p +-- checkSingleBackedge p +-- return p + +-- where +-- -- There should be exactly one block which is not part of the loop body that +-- -- can jump to @hd@. +-- checkSingleEntry :: (k,[k]) -> IO () +-- checkSingleEntry (hd, body) = +-- case filter (\x -> not (elem x body) && elem hd (C.cfgSuccessors cfg x)) allReachable of +-- [_] -> return () +-- _ -> fail "SimpleLoopInvariant feature requires a single-entry loop!" + +-- -- There should be exactly on block in the loop body which can jump to @hd@. +-- checkSingleBackedge :: (k,[k]) -> IO () +-- checkSingleBackedge (hd, body) = +-- case filter (\x -> elem hd (C.cfgSuccessors cfg x)) body of +-- [_] -> return () +-- _ -> fail "SimpleLoopInvariant feature requires a loop with a single backedge!" + +-- flattenWTOComponent = \case +-- C.SCC C.SCCData{..} -> wtoHead : concatMap flattenWTOComponent wtoComps +-- C.Vertex v -> [v] + +-- loop_map = Map.fromList $ mapMaybe +-- (\case +-- C.SCC C.SCCData{..} -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps) +-- C.Vertex{} -> Nothing) +-- wto + +-- allReachable = concatMap flattenWTOComponent wto + +-- wto = C.cfgWeakTopologicalOrdering cfg + + +-- | This execution feature is designed to allow a limited form of +-- verification for programs with unbounded looping structures. +-- +-- It is currently highly experimental and has many limitations. +-- Most notably, it only really works properly for functions +-- consisting of a single, non-nested loop with a single exit point. +-- Moreover, the loop must have an indexing variable that counts up +-- from a starting point by a fixed stride amount. +-- +-- Currently, these assumptions about the loop structure are not +-- checked. +-- +-- The basic use case here is for verifying functions that loop +-- through an array of data of symbolic length. This is done by +-- providing a \""fixpoint function\" which describes how the live +-- values in the loop at an arbitrary iteration are used to compute +-- the final values of those variables before execution leaves the +-- loop. The number and order of these variables depends on +-- internal details of the representation, so is relatively fragile. +simpleLoopFixpoint :: + (C.IsSymInterface sym, sym ~ W4.ExprBuilder t st fs, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions) => + sym -> + C.CFG ext blocks init ret {- ^ The function we want to verify -} -> + C.GlobalVar C.Mem {- ^ global variable representing memory -} -> + Maybe (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), Maybe (W4.Pred sym))) -> + IO (C.ExecutionFeature p sym ext rtp, IORef (ExecutionFeatureContext sym wptr ext)) +simpleLoopFixpoint sym _cfg mem_var maybe_fixpoint_func = do + verbSetting <- W4.getOptionSetting W4.verbosity $ W4.getConfiguration sym + _verb <- fromInteger @Natural <$> W4.getOpt verbSetting + + -- let loop_map = Map.fromList $ mapMaybe + -- (\case + -- scc@(C.SCC _) -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps) + -- C.Vertex{} -> Nothing) + -- (C.cfgWeakTopologicalOrdering cfg) + + -- Doesn't really work if there are nested loops: looop datastructures will + -- overwrite each other. Currently no error message. + + -- Really only works for single-exit loops; need a message for that too. + + -- let flattenWTOComponent = \case + -- C.SCC C.SCCData{..} -> wtoHead : concatMap flattenWTOComponent wtoComps + -- C.Vertex v -> [v] + -- let loop_map = Map.fromList $ mapMaybe + -- (\case + -- C.SCC C.SCCData{..} -> Just (wtoHead, wtoHead : concatMap flattenWTOComponent wtoComps) + -- C.Vertex{} -> Nothing) + -- (C.cfgWeakTopologicalOrdering cfg) + + + -- let parent_wto_component = C.parentWTOComponent $ C.cfgWeakTopologicalOrdering cfg + -- fixpoint_state_ref <- newIORef $ + -- FrameContext + -- { frameContextFixpointStates = MapF.empty + -- , frameContextLoopHeaders = [] + -- , frameContextCFG = cfg + -- , frameContextParentLoop = parent_wto_component + -- , frameContextLoopHeaderBlockIds = Set.fromList $ Map.elems parent_wto_component + -- } + + fixpoint_state_ref <- newIORef $ + ExecutionFeatureContext + { executionFeatureContextFixpointStates = C.emptyHandleMap + , executionFeatureContextInvPreds = [] + , executionFeatureContextLoopFunEquivConds = [] + } + + -- initializeCallFrameContext cfg fixpoint_state_ref + + return $ (, fixpoint_state_ref) $ C.ExecutionFeature $ \exec_state -> do + -- let ?logMessage = \msg -> when (_verb >= 3) $ do + let ?logMessage = \msg -> do + let h = C.printHandle $ C.execStateContext exec_state + System.IO.hPutStrLn h msg + System.IO.hFlush h + + -- cfg_handle <- C.cfgHandle . callFrameContextCFG <$> readIORef fixpoint_state_ref + -- cfg_block_map <- C.cfgBlockMap . callFrameContextCFG <$> readIORef fixpoint_state_ref + -- parent_loop_map <- callFrameContextParentLoop <$> readIORef fixpoint_state_ref + -- loop_header_block_ids <- callFrameContextLoopHeaderBlockIds <$> readIORef fixpoint_state_ref + -- maybe_some_loop_block_id <- callFrameContextPeek <$> readIORef fixpoint_state_ref + C.withBackend (C.execStateContext exec_state) $ \bak -> case exec_state of + C.RunningState (C.RunBlockStart block_id) sim_state + | SomeCallFrameHandle call_frame_handle <- callFrameHandle (sim_state ^. C.stateCrucibleFrame) -> do + loop_header_block_ids <- callFrameContextLoopHeaderBlockIds' call_frame_handle <$> readIORef fixpoint_state_ref + if Set.member (C.Some block_id) loop_header_block_ids then do + ?logMessage $ "!!!SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id + advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id sim_state fixpoint_state_ref + else do + ?logMessage $ "SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id + return C.ExecutionFeatureNoChange + + -- | C.SomeHandle cfg_handle == C.frameHandle (sim_state ^. C.stateCrucibleFrame) + -- -- make sure the types match + -- , Just Refl <- W4.testEquality + -- (fmapFC C.blockInputs cfg_block_map) + -- (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame) + -- -- loop map is what we computed above, is this state at a loop header + -- , Set.member (C.Some block_id) loop_header_block_ids -> + -- advanceFixpointState bak mem_var maybe_fixpoint_func cfg_handle block_id sim_state fixpoint_state_ref + + -- | otherwise -> do + -- ?logMessage $ "SimpleLoopFixpoint: RunningState: RunBlockStart: " ++ show block_id + -- return C.ExecutionFeatureNoChange + + -- TODO: maybe need to rework this, so that we are sure to capture even concrete exits from the loop. + C.SymbolicBranchState branch_condition true_frame false_frame _target sim_state + | JustPausedFrameTgtId true_frame_some_block_id <- pausedFrameTgtId true_frame + , JustPausedFrameTgtId false_frame_some_block_id <- pausedFrameTgtId false_frame + , SomeCallFrameHandle call_frame_handle <- callFrameHandle (sim_state ^. C.stateCrucibleFrame) -> do + maybe_some_loop_block_id <- callFrameContextPeek call_frame_handle <$> readIORef fixpoint_state_ref + parent_loop_map <- callFrameContextParentLoop' call_frame_handle <$> readIORef fixpoint_state_ref + -- , C.SomeHandle cfg_handle == C.frameHandle (sim_state ^. C.stateCrucibleFrame) + -- , Just Refl <- W4.testEquality + -- (fmapFC C.blockInputs cfg_block_map) + -- (fmapFC C.blockInputs $ C.frameBlockMap $ sim_state ^. C.stateCrucibleFrame) + -- , Just (Some loop_block_id) <- maybe_some_loop_block_id + -- , true_frame_parent_loop_id <- Map.lookup true_frame_some_block_id parent_loop_map + -- , false_frame_parent_loop_id <- Map.lookup false_frame_some_block_id parent_loop_map + -- , true_frame_parent_loop_id /= maybe_some_loop_block_id || false_frame_parent_loop_id /= maybe_some_loop_block_id -> do + if| Just (Some loop_block_id) <- maybe_some_loop_block_id + , true_frame_parent_loop_id <- if true_frame_some_block_id /= C.Some loop_block_id then Map.lookup true_frame_some_block_id parent_loop_map else maybe_some_loop_block_id + , false_frame_parent_loop_id <- if false_frame_some_block_id /= C.Some loop_block_id then Map.lookup false_frame_some_block_id parent_loop_map else maybe_some_loop_block_id + , true_frame_parent_loop_id /= maybe_some_loop_block_id || false_frame_parent_loop_id /= maybe_some_loop_block_id -> do + ?logMessage $ "!!!SimpleLoopFixpoint: SymbolicBranchState: " ++ show (true_frame_some_block_id, false_frame_some_block_id) + handleSymbolicBranch + bak + call_frame_handle + loop_block_id + branch_condition + true_frame + false_frame + true_frame_parent_loop_id + false_frame_parent_loop_id + sim_state + fixpoint_state_ref + | otherwise -> do + ?logMessage $ "SimpleLoopFixpoint: SymbolicBranchState: " ++ show (W4.printSymExpr branch_condition, true_frame_some_block_id, false_frame_some_block_id) + return C.ExecutionFeatureNoChange + + C.CallState _return_handler (C.CrucibleCall _block_id call_frame) _sim_state + | C.CallFrame { C._frameCFG = callee_cfg } <- call_frame -> do + initializeCallFrameContext callee_cfg fixpoint_state_ref + return C.ExecutionFeatureNoChange + C.TailCallState _value_from_value (C.CrucibleCall _block_id call_frame) _sim_state + | C.CallFrame { C._frameCFG = callee_cfg } <- call_frame -> do + initializeCallFrameContext callee_cfg fixpoint_state_ref + return C.ExecutionFeatureNoChange + + _ -> return C.ExecutionFeatureNoChange + + +initializeCallFrameContext :: + (?logMessage :: String -> IO ()) => + C.CFG ext blocks init ret -> + IORef (ExecutionFeatureContext sym wptr ext) -> + IO () +initializeCallFrameContext cfg context_ref = do + ?logMessage $ "SimpleLoopFixpoint: cfgHandle: " ++ show (C.cfgHandle cfg) + ?logMessage $ "SimpleLoopFixpoint: cfg: " ++ show (toListFC (\b -> (C.Some (C.blockID b), C.nextBlocks b)) $ C.cfgBlockMap cfg) + ?logMessage $ "SimpleLoopFixpoint: cfgWeakTopologicalOrdering: " ++ show (C.cfgWeakTopologicalOrdering cfg) + let parent_wto_component = C.parentWTOComponent $ C.cfgWeakTopologicalOrdering cfg + let call_frame_handle = CallFrameHandle (C.cfgHandle cfg) $ fmapFC C.blockInputs $ C.cfgBlockMap cfg + modifyIORef' context_ref $ executionFeatureContextAddCallFrameContext call_frame_handle $ + CallFrameContext + { callFrameContextFixpointStates = MapF.empty + , callFrameContextLoopHeaders = [] + , callFrameContextCFG = cfg + , callFrameContextParentLoop = parent_wto_component + , callFrameContextLoopHeaderBlockIds = Set.fromList $ Map.elems parent_wto_component + } + + +initializeFixpointState :: + (C.IsSymBackend sym bak, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) => + bak -> + C.GlobalVar C.Mem -> + CallFrameHandle init ret blocks -> + C.BlockID blocks args -> + C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) -> + IORef (ExecutionFeatureContext sym wptr ext) -> + IO (C.ExecutionFeatureResult p sym ext rtp) +initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref = do + let sym = C.backendGetSym bak + assumption_frame_identifier <- C.pushAssumptionFrame bak + ?logMessage $ "!!!SimpleLoopFixpoint: initializeFixpointState: block_id=" ++ show block_id ++ ", assumption_frame_identifier=" ++ show assumption_frame_identifier + index_var <- W4.freshConstant sym (W4.safeSymbol "index_var") W4.knownRepr + let mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) + let res_mem_impl = mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" $ C.memImplHeap mem_impl } + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ ComputeFixpoint $ + FixpointRecord + { fixpointBlockId = block_id + , fixpointAssumptionFrameIdentifier = assumption_frame_identifier + , fixpointSubstitution = MapF.empty + , fixpointRegMap = sim_state ^. (C.stateCrucibleFrame . C.frameRegs) + , fixpointMemSubstitution = Map.empty + , fixpointEqualitySubstitution = MapF.empty + , fixpointIndex = index_var + } + modifyIORef' fixpoint_state_ref $ callFrameContextPush call_frame_handle $ Some block_id + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + +advanceFixpointState :: + (C.IsSymBackend sym bak, sym ~ W4.ExprBuilder t st fs, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) => + bak -> + C.GlobalVar C.Mem -> + Maybe (MapF (W4.SymExpr sym) (FixpointEntry sym) -> W4.Pred sym -> IO (MapF (W4.SymExpr sym) (W4.SymExpr sym), Maybe (W4.Pred sym))) -> + CallFrameHandle init ret blocks -> + C.BlockID blocks args -> + C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) -> + IORef (ExecutionFeatureContext sym wptr ext) -> + IO (C.ExecutionFeatureResult p sym ext rtp) + +advanceFixpointState bak mem_var maybe_fixpoint_func call_frame_handle block_id sim_state fixpoint_state_ref = do + let sym = C.backendGetSym bak + fixpoint_state <- fromMaybe BeforeFixpoint <$> callFrameContextLookup' call_frame_handle block_id <$> readIORef fixpoint_state_ref + case fixpoint_state of + BeforeFixpoint -> do + ?logMessage $ "SimpleLoopFixpoint: RunningState: BeforeFixpoint -> ComputeFixpoint" + mapM_ (\g -> print =<< C.ppProofObligation sym g) =<< (maybe [] C.goalsToList <$> C.getProofObligations bak) + initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref + + ComputeFixpoint fixpoint_record -> do + ?logMessage $ "SimpleLoopFixpoint: RunningState: ComputeFixpoint: " ++ show block_id + proof_goals_and_assumptions_vars <- Set.map (mapSome $ W4.varExpr sym) <$> + (Set.union <$> C.proofObligationsUninterpConstants bak <*> C.pathConditionUninterpConstants bak) + (frame_assumptions, _) <- C.popAssumptionFrameAndObligations bak $ fixpointAssumptionFrameIdentifier fixpoint_record + loop_condition <- C.assumptionsPred sym frame_assumptions + + -- widen the inductive condition + (join_reg_map, join_substitution) <- runFixpointMonad + (joinRegEntries sym + (C.regMap $ fixpointRegMap fixpoint_record) + (C.regMap $ sim_state ^. (C.stateCrucibleFrame . C.frameRegs))) $ + fixpointSubstitution fixpoint_record + + let body_mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) + let (header_mem_impl, mem_allocs, mem_writes) = dropMemStackFrame body_mem_impl + when (C.sizeMemAllocs mem_allocs /= 0) $ + fail "SimpleLoopFixpoint: unsupported memory allocation in loop body." + + -- widen the memory + mem_substitution_candidate <- joinMem sym header_mem_impl mem_writes + + -- check that the mem substitution always computes the same footprint on every iteration (!?!) + mem_substitution <- if Map.null (fixpointMemSubstitution fixpoint_record) + then return mem_substitution_candidate + else if Map.keys mem_substitution_candidate == Map.keys (fixpointMemSubstitution fixpoint_record) + then return $ fixpointMemSubstitution fixpoint_record + else fail "SimpleLoopFixpoint: unsupported memory writes change" + + assumption_frame_identifier <- C.pushAssumptionFrame bak + + -- check if we are done; if we did not introduce any new variables, we don't have to widen any more + if MapF.keys join_substitution == MapF.keys (fixpointSubstitution fixpoint_record) && Map.keys mem_substitution == Map.keys (fixpointMemSubstitution fixpoint_record) + + -- we found the fixpoint, get ready to wrap up + then do + ?logMessage $ + "SimpleLoopFixpoint: RunningState: ComputeFixpoint -> CheckFixpoint" + + -- we have delayed populating the main substitution map with + -- memory variables, so we have to do that now + + header_mem_substitution <- loadMemJoinVariables bak header_mem_impl $ + fixpointMemSubstitution fixpoint_record + body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $ + fixpointMemSubstitution fixpoint_record + + -- drop variables that don't appear along some back edge + let union_substitution' = filterSubstitution sym $ + MapF.union join_substitution $ + -- this implements zip, because the two maps have the same keys + MapF.intersectWithKeyMaybe + (\_k x y -> Just $ FixpointEntry{ headerValue = x, bodyValue = y }) + header_mem_substitution + body_mem_substitution + loop_index_linear_substitution <- loopIndexLinearSubstitution sym (fixpointIndex fixpoint_record) union_substitution' + + let union_substitution = MapF.filterWithKey + (\variable _entry -> MapF.notMember variable loop_index_linear_substitution) + union_substitution' + -- try to unify widening variables that have the same values + (normal_substitution', equality_substitution') <- uninterpretedConstantEqualitySubstitution sym union_substitution + + zero_bv <- W4.bvLit sym knownNat $ BV.zero knownNat + one_bv <- W4.bvLit sym knownNat $ BV.one knownNat + add_index_one <- W4.bvAdd sym (fixpointIndex fixpoint_record) one_bv + let normal_substitution = MapF.insert + (fixpointIndex fixpoint_record) + FixpointEntry + { headerValue = zero_bv + , bodyValue = add_index_one + } + normal_substitution' + let equality_substitution = MapF.union equality_substitution' loop_index_linear_substitution + + ?logMessage $ "loop_index_linear_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList loop_index_linear_substitution) + ?logMessage $ "normal_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList normal_substitution) + ?logMessage $ "equality_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList equality_substitution) + + -- unify widening variables in the register subst + let res_reg_map = applySubstitutionRegEntries sym equality_substitution join_reg_map + + -- unify widening varialbes in the memory subst + res_mem_impl <- storeMemJoinVariables + bak + (header_mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" (C.memImplHeap header_mem_impl) }) + mem_substitution + equality_substitution + + let body_values_vars = foldMap (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . bodyValue) $ + MapF.elems normal_substitution + let header_values_vars = foldMap (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym . headerValue) $ + MapF.elems normal_substitution + -- let all_vars = Set.union proof_goals_and_assumptions_vars $ Set.union body_values_vars header_values_vars + let all_vars' = Set.insert (Some $ fixpointIndex fixpoint_record) proof_goals_and_assumptions_vars + let all_vars = Set.filter + (\(Some variable) -> MapF.notMember variable equality_substitution) + all_vars' + -- let some_uninterpreted_constants = Ctx.fromList $ Set.toList all_vars + let filtered_vars = Set.filter + (\(Some variable) -> + not (List.isPrefixOf "cundefined_" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable) + && not (List.isPrefixOf "cnoSatisfyingWrite" $ show $ W4.printSymExpr variable)) + all_vars + let some_uninterpreted_constants = Ctx.fromList $ Set.toList filtered_vars + -- let implicit_vars = Set.filter + -- (\(Some variable) -> + -- not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable) + -- && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable) + -- && not (List.isPrefixOf "cundefined_" $ show $ W4.printSymExpr variable) + -- && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable) + -- && not (List.isPrefixOf "cnoSatisfyingWrite" $ show $ W4.printSymExpr variable)) + -- all_vars + some_inv_pred <- case some_uninterpreted_constants of + Some uninterpreted_constants -> do + inv_pred <- W4.freshTotalUninterpFn + sym + (W4.safeSymbol "inv") + (fmapFC W4.exprType uninterpreted_constants) + W4.BaseBoolRepr + + loc <- W4.getCurrentProgramLoc sym + + header_inv <- W4.applySymFn sym inv_pred $ + applySubstitutionFC (fmapF headerValue normal_substitution) uninterpreted_constants + C.addProofObligation bak $ C.LabeledPred header_inv $ C.SimError loc "" + + inv <- W4.applySymFn sym inv_pred uninterpreted_constants + C.addAssumption bak $ C.GenericAssumption loc "inv" inv + + return $ W4.SomeSymFn inv_pred + + modifyIORef' fixpoint_state_ref $ executionFeatureContextAddInvPred some_inv_pred + + ?logMessage $ + "proof_goals_and_assumptions_vars: " + ++ show (map (viewSome W4.printSymExpr) $ Set.toList proof_goals_and_assumptions_vars) + ?logMessage $ + "body_values_vars: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList body_values_vars) + ?logMessage $ + "header_values_vars: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList header_values_vars) + ?logMessage $ + "uninterpreted_constants: " ++ show (map (viewSome W4.printSymExpr) $ Set.toList filtered_vars) + + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ + CheckFixpoint + FixpointRecord + { fixpointBlockId = block_id + , fixpointAssumptionFrameIdentifier = assumption_frame_identifier + , fixpointSubstitution = normal_substitution + , fixpointRegMap = fixpointRegMap fixpoint_record + , fixpointMemSubstitution = mem_substitution + , fixpointEqualitySubstitution = equality_substitution + , fixpointIndex = fixpointIndex fixpoint_record + } + some_inv_pred + -- implicit_vars + some_uninterpreted_constants + loop_condition + + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ C.RegMap res_reg_map + & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + + else do + ?logMessage $ + "SimpleLoopFixpoint: RunningState: ComputeFixpoint: -> ComputeFixpoint" + + -- write any new widening variables into memory state + res_mem_impl <- storeMemJoinVariables bak + (header_mem_impl { C.memImplHeap = C.pushStackFrameMem "fix" (C.memImplHeap header_mem_impl) }) + mem_substitution + MapF.empty + + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ ComputeFixpoint + FixpointRecord + { fixpointBlockId = block_id + , fixpointAssumptionFrameIdentifier = assumption_frame_identifier + , fixpointSubstitution = join_substitution + , fixpointRegMap = C.RegMap join_reg_map + , fixpointMemSubstitution = mem_substitution + , fixpointEqualitySubstitution = MapF.empty + , fixpointIndex = fixpointIndex fixpoint_record + } + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ C.RegMap join_reg_map + & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + + CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants loop_condition -> do + ?logMessage $ + "SimpleLoopFixpoint: RunningState: " + ++ "CheckFixpoint" + ++ " -> " + ++ "AfterFixpoint" + ++ ": " + ++ show block_id + + loc <- W4.getCurrentProgramLoc sym + + -- assert that the hypothesis we made about the loop termination condition is true + (_ :: ()) <- case (some_inv_pred, some_uninterpreted_constants) of + (W4.SomeSymFn inv_pred, Some uninterpreted_constants) + | Just Refl <- testEquality (W4.fnArgTypes inv_pred) (fmapFC W4.exprType uninterpreted_constants) + , Just Refl <- testEquality (W4.fnReturnType inv_pred) W4.BaseBoolRepr -> do + inv <- W4.applySymFn sym inv_pred $ applySubstitutionFC + (fmapF bodyValue $ fixpointSubstitution fixpoint_record) + uninterpreted_constants + C.addProofObligation bak $ C.LabeledPred inv $ C.SimError loc "" + | otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: CheckFixpoint"] + + frame_assumptions <- C.popAssumptionFrame bak $ fixpointAssumptionFrameIdentifier fixpoint_record + + -- body_mem_substitution <- loadMemJoinVariables bak body_mem_impl $ fixpointMemSubstitution fixpoint_record + -- let res_substitution = MapF.mapWithKey + -- (\variable fixpoint_entry -> + -- fixpoint_entry + -- { bodyValue = MapF.findWithDefault (bodyValue fixpoint_entry) variable body_mem_substitution + -- }) + -- (fixpointSubstitution fixpoint_record) + -- ?logMessage $ "res_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr $ bodyValue y)) $ MapF.toList res_substitution) + + -- match things up with the input function that describes the loop body behavior + fixpoint_substitution <- case maybe_fixpoint_func of + Just fixpoint_func -> do + -- (fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func res_substitution loop_condition + + correct_substitution <- traverseF + (\fixpoint_entry -> do + correct_body_value <- W4.substituteBoundVars sym (asBoundVarSubstitution sym $ fixpointEqualitySubstitution fixpoint_record) $ bodyValue fixpoint_entry + return $ fixpoint_entry + { bodyValue = correct_body_value + }) + (fixpointSubstitution fixpoint_record) + (fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func correct_substitution loop_condition + -- (fixpoint_func_substitution, maybe_fixpoint_func_condition) <- fixpoint_func (fixpointSubstitution fixpoint_record) loop_condition + + _ <- case maybe_fixpoint_func_condition of + Just fixpoint_func_condition -> do + bak_assumptions <- liftIO $ C.assumptionsPred sym =<< C.collectAssumptions bak + inv_assumption <- C.assumptionPred <$> headAssumption sym frame_assumptions + all_assumptions <- liftIO $ W4.andPred sym bak_assumptions inv_assumption + implication <- liftIO $ W4.impliesPred sym all_assumptions fixpoint_func_condition + modifyIORef' fixpoint_state_ref $ executionFeatureContextAddLoopFunEquivCond implication + -- tmp_frame_id <- C.pushAssumptionFrame bak + -- C.addProofObligation bak $ C.LabeledPred fixpoint_func_condition $ C.SimError loc "" + -- (_, obligations) <- C.popAssumptionFrameAndObligations bak tmp_frame_id + -- ?logMessage "before convertProofObligationsAsImplications" + -- implications <- C.convertProofObligationsAsImplications sym obligations + -- ?logMessage "after convertProofObligationsAsImplications" + -- forM_ implications $ \implication -> + -- modifyIORef' fixpoint_state_ref $ executionFeatureContextAddLoopFunEquivCond implication + Nothing -> return () + + ?logMessage $ "fixpoint_func_substitution: " ++ show (map (\(MapF.Pair x y) -> (W4.printSymExpr x, W4.printSymExpr y)) $ MapF.toList fixpoint_func_substitution) + + return fixpoint_func_substitution + + Nothing -> return MapF.empty + + let body_mem_impl = fromJust $ C.lookupGlobal mem_var (sim_state ^. C.stateGlobals) + let (header_mem_impl, _mem_allocs, _mem_writes) = dropMemStackFrame body_mem_impl + + fixpoint_equality_substitution <- traverseF + (W4.substituteBoundVars sym $ asBoundVarSubstitution sym fixpoint_substitution) $ + fixpointEqualitySubstitution fixpoint_record + let fixpoint_equality_substitution' = MapF.union fixpoint_substitution fixpoint_equality_substitution + let res_reg_map = C.RegMap $ applySubstitutionRegEntries sym fixpoint_equality_substitution' (C.regMap $ fixpointRegMap fixpoint_record) + res_mem_impl <- storeMemJoinVariables bak header_mem_impl (fixpointMemSubstitution fixpoint_record) fixpoint_equality_substitution' + + (_ :: ()) <- case (some_inv_pred, some_uninterpreted_constants) of + (W4.SomeSymFn inv_pred, Some uninterpreted_constants) + | Just Refl <- testEquality (W4.fnArgTypes inv_pred) (fmapFC W4.exprType uninterpreted_constants) + , Just Refl <- testEquality (W4.fnReturnType inv_pred) W4.BaseBoolRepr -> do + inv <- W4.applySymFn sym inv_pred $ applySubstitutionFC fixpoint_substitution uninterpreted_constants + C.addAssumption bak $ C.GenericAssumption loc "" inv + | otherwise -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint" ["type mismatch: CheckFixpoint"] + + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle block_id $ + AfterFixpoint + -- fixpoint_record{ fixpointSubstitution = res_substitution } + fixpoint_record + + return $ C.ExecutionFeatureModifiedState $ C.RunningState (C.RunBlockStart block_id) $ + sim_state & (C.stateCrucibleFrame . C.frameRegs) .~ res_reg_map + & C.stateGlobals %~ C.insertGlobal mem_var res_mem_impl + + AfterFixpoint{} -> do + ?logMessage $ "SimpleLoopFixpoint: RunningState: AfterFixpoint -> ComputeFixpoint" + initializeFixpointState bak mem_var call_frame_handle block_id sim_state fixpoint_state_ref + + +handleSymbolicBranch :: + (C.IsSymBackend sym bak, C.HasPtrWidth wptr, KnownNat wptr, C.HasLLVMAnn sym, ?memOpts :: C.MemOptions, ?logMessage :: String -> IO ()) => + bak -> + CallFrameHandle init ret blocks -> + C.BlockID blocks tp -> + W4.Pred sym -> + C.PausedFrame p sym ext rtp (C.CrucibleLang blocks r) -> + C.PausedFrame p sym ext rtp (C.CrucibleLang blocks r) -> + Maybe (C.Some (C.BlockID blocks)) -> + Maybe (C.Some (C.BlockID blocks)) -> + C.SimState p sym ext rtp (C.CrucibleLang blocks r) ('Just args) -> + IORef (ExecutionFeatureContext sym wptr ext) -> + IO (C.ExecutionFeatureResult p sym ext rtp) +handleSymbolicBranch bak call_frame_handle loop_block_id branch_condition true_frame false_frame true_frame_parent_loop_id false_frame_parent_loop_id sim_state fixpoint_state_ref = do + let sym = C.backendGetSym bak + + (loop_condition, inside_loop_frame, outside_loop_frame) <- + if true_frame_parent_loop_id == Just (C.Some loop_block_id) + then + return (branch_condition, true_frame, false_frame) + else if false_frame_parent_loop_id == Just (C.Some loop_block_id) + then do + not_branch_condition <- W4.notPred sym branch_condition + return (not_branch_condition, false_frame, true_frame) + else + fail $ "unsupported loop: loop header block id " ++ show loop_block_id ++ " true frame parent loop id " ++ show true_frame_parent_loop_id ++ " false frame parent loop id " ++ show false_frame_parent_loop_id + + Just fixpoint_state <- callFrameContextLookup' call_frame_handle loop_block_id <$> readIORef fixpoint_state_ref + (condition, frame) <- case fixpoint_state of + BeforeFixpoint -> C.panic "SimpleLoopFixpoint.simpleLoopFixpoint:" ["BeforeFixpoint"] + + ComputeFixpoint{} -> do + -- continue in the loop + ?logMessage "SimpleLoopFixpoint: SymbolicBranchState: ComputeFixpoint" + return (loop_condition, inside_loop_frame) + + CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants _ -> do + -- continue in the loop + ?logMessage "SimpleLoopFixpoint: SymbolicBranchState: CheckFixpoint" + modifyIORef' fixpoint_state_ref $ callFrameContextInsert call_frame_handle loop_block_id $ + CheckFixpoint fixpoint_record some_inv_pred some_uninterpreted_constants loop_condition + return (loop_condition, inside_loop_frame) + + AfterFixpoint{} -> do + -- break out of the loop + ?logMessage "SimpleLoopFixpoint: SymbolicBranchState: AfterFixpoint" + modifyIORef' fixpoint_state_ref $ callFrameContextPop call_frame_handle + not_loop_condition <- W4.notPred sym loop_condition + return (not_loop_condition, outside_loop_frame) + + loc <- W4.getCurrentProgramLoc sym + C.addAssumption bak $ C.BranchCondition loc (C.pausedLoc frame) condition + C.ExecutionFeatureNewState <$> + runReaderT + (C.resumeFrame (C.forgetPostdomFrame frame) $ sim_state ^. (C.stateTree . C.actContext)) + sim_state + + +data SomeCallFrameHandle ret blocks = forall init . SomeCallFrameHandle (CallFrameHandle init ret blocks) + +callFrameHandle :: C.CallFrame sym ext blocks ret ctx -> SomeCallFrameHandle ret blocks +callFrameHandle C.CallFrame { _frameCFG = g } = + SomeCallFrameHandle $ CallFrameHandle (C.cfgHandle g) $ fmapFC C.blockInputs $ C.cfgBlockMap g + +data MaybePausedFrameTgtId f where + JustPausedFrameTgtId :: C.Some (C.BlockID b) -> MaybePausedFrameTgtId (C.CrucibleLang b r) + NothingPausedFrameTgtId :: MaybePausedFrameTgtId f + +pausedFrameTgtId :: C.PausedFrame p sym ext rtp f -> MaybePausedFrameTgtId f +pausedFrameTgtId C.PausedFrame{ resume = resume } = case resume of + C.ContinueResumption (C.ResolvedJump tgt_id _) -> JustPausedFrameTgtId $ C.Some tgt_id + C.CheckMergeResumption (C.ResolvedJump tgt_id _) -> JustPausedFrameTgtId $ C.Some tgt_id + _ -> NothingPausedFrameTgtId + + +applySubstitutionFC :: (OrdF k, FunctorFC f) => MapF k k -> f k l -> f k l +applySubstitutionFC substitution = fmapFC $ findWithDefaultKey substitution + +findWithDefaultKey :: forall a (k :: a -> Type) tp . OrdF k => MapF k k -> k tp -> k tp +findWithDefaultKey substitution key = MapF.findWithDefault key key substitution + +asBoundVarSubstitution :: W4.IsSymExprBuilder sym => sym -> MapF (W4.SymExpr sym) a -> MapF (W4.BoundVar sym) a +asBoundVarSubstitution sym = + MapF.fromList . mapMaybe (\(MapF.Pair k_expr v) -> fmap (\k_var -> MapF.Pair k_var v) $ asBoundVar sym k_expr) . MapF.toList + +asBoundVar :: W4.IsSymExprBuilder sym => sym -> W4.SymExpr sym tp -> Maybe (W4.BoundVar sym tp) +asBoundVar sym expr = case Set.toList (W4.exprUninterpConstants sym expr) of + [Some var] + | Just Refl <- testEquality expr (W4.varExpr sym var) -> + Just var + _ -> Nothing + +headAssumption :: sym -> C.Assumptions sym -> IO (C.CrucibleAssumption (W4.SymExpr sym)) +headAssumption sym = \case + C.SingleAssumption a -> return a + C.ManyAssumptions (x Seq.:<| _) -> headAssumption sym x + _ -> fail "SimpleLoopFixpoint.headAssumption: empty assumptions" diff --git a/crucible/src/Lang/Crucible/Backend.hs b/crucible/src/Lang/Crucible/Backend.hs index f8adec788..130173396 100644 --- a/crucible/src/Lang/Crucible/Backend.hs +++ b/crucible/src/Lang/Crucible/Backend.hs @@ -36,6 +36,7 @@ obligations with a solver backend. {-# LANGUAGE RankNTypes #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} module Lang.Crucible.Backend ( IsSymBackend(..) @@ -118,7 +119,6 @@ import Data.Sequence (Seq) import Data.Set (Set) import qualified Prettyprinter as PP import GHC.Stack -import System.IO import Data.Parameterized.Map (MapF) @@ -132,7 +132,6 @@ import What4.Partial import What4.ProgramLoc import What4.Expr (GroundValue, GroundValueWrapper(..)) import What4.Solver -import qualified What4.Solver.CVC5 as CVC5 import qualified What4.Solver.Z3 as Z3 import qualified Lang.Crucible.Backend.AssumptionStack as AS @@ -644,12 +643,12 @@ runCHC bak uninterp_inv_fns = liftIO $ do -- log to stdout let logData = defaultLogData { logCallbackVerbose = \_ -> putStrLn - , logReason = "SAW inv" + , logReason = "Crucible inv" } Z3.runZ3Horn sym True logData uninterp_inv_fns implications >>= \case Sat sub -> return sub - Unsat{} -> fail "Prover returned Infeasible" - Unknown -> fail "Prover returned Fail" + Unsat{} -> fail "Prover returned Unsat" + Unknown -> fail "Prover returned Unknown" -- | Get proof obligations as What4 implications. diff --git a/crux-llvm/src/Crux/LLVM/Config.hs b/crux-llvm/src/Crux/LLVM/Config.hs index c3c015ab4..10424ce05 100644 --- a/crux-llvm/src/Crux/LLVM/Config.hs +++ b/crux-llvm/src/Crux/LLVM/Config.hs @@ -208,6 +208,9 @@ llvmCruxConfig = do , "'unstable-symbolic', which causes each read from uninitialized" , "memory to return a fresh symbolic value." ]) + noSatisfyingWriteFreshConstant <- + Crux.section "no-satisfying-write-fresh-constant" Crux.yesOrNoSpec True + "Make a fresh constant for the NoSatisfyingWrite annotation." return MemOptions{..} transOpts <- do laxArith <- diff --git a/crux-llvm/src/Crux/LLVM/Simulate.hs b/crux-llvm/src/Crux/LLVM/Simulate.hs index e15b0971d..027d70e1e 100644 --- a/crux-llvm/src/Crux/LLVM/Simulate.hs +++ b/crux-llvm/src/Crux/LLVM/Simulate.hs @@ -139,13 +139,13 @@ registerFunctions llvmOpts llvm_module mtrans fs0 = ?memOpts = memOpts llvmOpts -- register the callable override functions - register_llvm_overrides llvm_module [] - (concat [ cruxLLVMOverrides proxy# - , svCompOverrides - , cbmcOverrides proxy# - , maybe [] symio_overrides fs0 - ]) - llvm_ctx + _ <- register_llvm_overrides llvm_module [] + (concat [ cruxLLVMOverrides proxy# + , svCompOverrides + , cbmcOverrides proxy# + , maybe [] symio_overrides fs0 + ]) + llvm_ctx -- register all the functions defined in the LLVM module registerLazyModule sayTranslationWarning mtrans diff --git a/crux-llvm/test-data/golden/golden/float-cast2.z3.good b/crux-llvm/test-data/golden/golden/float-cast2.z3.good index 63af98236..4334bf91d 100644 --- a/crux-llvm/test-data/golden/golden/float-cast2.z3.good +++ b/crux-llvm/test-data/golden/golden/float-cast2.z3.good @@ -1,2 +1,2 @@ -ite (floatIsNaN cX@3:f) 0x0:[32] 0x1:[32] +bvZext 32 (ite (floatIsNaN cX@3:f) 0x0:[1] 0x1:[1]) [Crux] Overall status: Valid. diff --git a/crux/src/Crux.hs b/crux/src/Crux.hs index 709bd66c2..b5bb8fab8 100644 --- a/crux/src/Crux.hs +++ b/crux/src/Crux.hs @@ -74,7 +74,6 @@ import What4.Config (setOpt, getOptionSetting, verbosity, extendConfig import qualified What4.Expr as WE import What4.FunctionName (FunctionName) import What4.Interface (IsExprBuilder, getConfiguration) -import What4.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder) import What4.Protocol.Online (OnlineSolver) import qualified What4.Solver as WS import What4.Solver.CVC4 (cvc4Timeout) diff --git a/dependencies/what4 b/dependencies/what4 index 30309b5d8..8c9401b5d 160000 --- a/dependencies/what4 +++ b/dependencies/what4 @@ -1 +1 @@ -Subproject commit 30309b5d86179c2d4182f68ccf36e8dd5f68360c +Subproject commit 8c9401b5d21d20451d224d4834bd611fc83b850b