diff --git a/CHANGES.md b/CHANGES.md index c15604d362..5c7cacdc3b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,19 @@ +# Nightly + +* New commands `enable_what4_eval` and `disable_what4_eval` to enable or + disable What4 translation for SAWCore expressions during Crucible symbolic + execution. + +* New command `llvm_alloc_sym_init` like `llvm_alloc`, but assume that the + allocation is initialized with symbolic bytes. New commands + `disable_alloc_sym_init_check` and `enable_alloc_sym_init_check` to + disable or enable the allocation initialization check associated with + `llvm_alloc_sym_init` during override application. + +* New command `set_crucible_timeout` to set the timeout for the SMT solver + during the LLVM and X86 Crucible symbolic execution. This is used for + path-sat checks, and sat checks when applying overrides. + # Version 0.9 ## New Features diff --git a/intTests/test0070_llvm_alloc_sym_init/test.bc b/intTests/test0070_llvm_alloc_sym_init/test.bc new file mode 100644 index 0000000000..c87c519be0 Binary files /dev/null and b/intTests/test0070_llvm_alloc_sym_init/test.bc differ diff --git a/intTests/test0070_llvm_alloc_sym_init/test.c b/intTests/test0070_llvm_alloc_sym_init/test.c new file mode 100644 index 0000000000..294a4de06c --- /dev/null +++ b/intTests/test0070_llvm_alloc_sym_init/test.c @@ -0,0 +1,19 @@ +#include + +int f(int *x) +{ + return *x; +} + +int test_f_calloc() +{ + int *x = (int *) calloc(1, sizeof(int)); + return f(x); +} + +int test_f_malloc() +{ + int *x = (int *) malloc(sizeof(int)); + return f(x); +} + diff --git a/intTests/test0070_llvm_alloc_sym_init/test.saw b/intTests/test0070_llvm_alloc_sym_init/test.saw new file mode 100644 index 0000000000..2a78eaf57c --- /dev/null +++ b/intTests/test0070_llvm_alloc_sym_init/test.saw @@ -0,0 +1,25 @@ +enable_experimental; + +m <- llvm_load_module "test.bc"; + +let f_spec = do { + x_ptr <- llvm_alloc_sym_init (llvm_int 32); + llvm_execute_func [x_ptr]; + x <- llvm_fresh_var "x" (llvm_int 32); + llvm_return (llvm_term x); +}; + +let test_spec = do { + llvm_execute_func []; + x <- llvm_fresh_var "x" (llvm_int 32); + llvm_return (llvm_term x); +}; + +f_ov <- llvm_verify m "f" [] false f_spec trivial; +llvm_verify m "test_f_calloc" [f_ov] false test_spec trivial; +fails (llvm_verify m "test_f_malloc" [f_ov] false test_spec trivial); +disable_alloc_sym_init_check; +llvm_verify m "test_f_malloc" [f_ov] false test_spec trivial; +enable_alloc_sym_init_check; +fails (llvm_verify m "test_f_malloc" [f_ov] false test_spec trivial); + diff --git a/intTests/test0070_llvm_alloc_sym_init/test.sh b/intTests/test0070_llvm_alloc_sym_init/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test0070_llvm_alloc_sym_init/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index cd58c24f62..8e106a03ae 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -1320,13 +1320,13 @@ parseUninterpretedSAW sym st sc ref trm app ty = parseUninterpretedSAW sym st sc ref trm' app' t2 VBoolType - -> VBool <$> mkUninterpretedSAW sym st ref trm app BaseBoolRepr + -> VBool <$> mkUninterpretedSAW sym st sc ref trm app BaseBoolRepr VIntType - -> VInt <$> mkUninterpretedSAW sym st ref trm app BaseIntegerRepr + -> VInt <$> mkUninterpretedSAW sym st sc ref trm app BaseIntegerRepr VIntModType n - -> VIntMod n <$> mkUninterpretedSAW sym st ref (ArgTermFromIntMod n trm) app BaseIntegerRepr + -> VIntMod n <$> mkUninterpretedSAW sym st sc ref (ArgTermFromIntMod n trm) app BaseIntegerRepr -- 0 width bitvector is a constant VVecType 0 VBoolType @@ -1334,7 +1334,7 @@ parseUninterpretedSAW sym st sc ref trm app ty = VVecType n VBoolType | Just (Some (PosNat w)) <- somePosNat n - -> (VWord . DBV) <$> mkUninterpretedSAW sym st ref trm app (BaseBVRepr w) + -> (VWord . DBV) <$> mkUninterpretedSAW sym st sc ref trm app (BaseBVRepr w) VVecType n ety | n >= 0 -> do ety' <- termOfTValue sc ety @@ -1349,7 +1349,7 @@ parseUninterpretedSAW sym st sc ref trm app ty = | Just (Some idx_repr) <- valueAsBaseType ity , Just (Some elm_repr) <- valueAsBaseType ety -> (VArray . SArray) <$> - mkUninterpretedSAW sym st ref trm app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr) + mkUninterpretedSAW sym st sc ref trm app (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) elm_repr) VUnitType -> return VUnit @@ -1367,12 +1367,16 @@ mkUninterpretedSAW :: forall n st fs t. B.ExprBuilder n st fs -> SAWCoreState n -> + SharedContext -> IORef (SymFnCache (B.ExprBuilder n st fs)) -> ArgTerm -> UnintApp (SymExpr (B.ExprBuilder n st fs)) -> BaseTypeRepr t -> IO (SymExpr (B.ExprBuilder n st fs) t) -mkUninterpretedSAW sym st ref trm (UnintApp nm args tys) ret = +mkUninterpretedSAW sym st sc ref trm (UnintApp nm args tys) ret + | Just Refl <- testEquality Ctx.empty tys = + bindSAWTerm sym st ret =<< reconstructArgTerm trm sc [] + | otherwise = do fn <- mkSymFn sym ref nm tys ret sawRegisterSymFunInterp st fn (reconstructArgTerm trm) W.applySymFn sym fn args diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 66c93c1e2d..758c7337d9 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -47,6 +47,7 @@ import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule) import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType) import SAWScript.Crucible.LLVM.X86 (defaultStackBaseAlign) +import qualified SAWScript.Crucible.Common as CC (defaultSAWCoreBackendTimeout) import qualified SAWScript.Crucible.Common.MethodSpec as CMS (ProvedSpec, GhostGlobal) import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule) import SAWScript.Options (Options(..), processEnv, defaultOptions) @@ -220,9 +221,12 @@ initialState readFileFn = , rwDebugIntrinsics = True , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False + , rwWhat4Eval = False , rwStackBaseAlign = defaultStackBaseAlign , rwProofs = [] , rwPreservedRegs = [] + , rwAllocSymInitCheck = True + , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout } return (SAWState emptyEnv bic [] ro rw M.empty) diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs index 45f9681972..c54c92dbf4 100644 --- a/src/SAWScript/Crucible/Common.hs +++ b/src/SAWScript/Crucible/Common.hs @@ -14,6 +14,8 @@ module SAWScript.Crucible.Common , setupProfiling , SAWCruciblePersonality(..) , newSAWCoreBackend + , newSAWCoreBackendWithTimeout + , defaultSAWCoreBackendTimeout , sawCoreState ) where @@ -24,7 +26,8 @@ import Lang.Crucible.Simulator.Profiling import Lang.Crucible.Backend (AbortExecReason(..), ppAbortExecReason, IsSymInterface) import Lang.Crucible.Backend.Online import qualified Data.Parameterized.Nonce as Nonce -import qualified What4.Solver.Yices as Yices +import qualified What4.Solver.Z3 as Z3 +import qualified What4.Protocol.SMTLib2 as SMT2 import qualified What4.Config as W4 import qualified What4.Expr as W4 import qualified What4.Interface as W4 @@ -40,16 +43,24 @@ import Verifier.SAW.SharedTerm as SC import Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState, newSAWCoreState) -- | The symbolic backend we use for SAW verification -type Sym = OnlineBackendUserSt Nonce.GlobalNonceGenerator Yices.Connection SAWCoreState (W4.Flags W4.FloatReal) +type Sym = OnlineBackendUserSt Nonce.GlobalNonceGenerator (SMT2.Writer Z3.Z3) SAWCoreState (W4.Flags W4.FloatReal) data SAWCruciblePersonality sym = SAWCruciblePersonality newSAWCoreBackend :: SC.SharedContext -> IO Sym -newSAWCoreBackend sc = +newSAWCoreBackend sc = newSAWCoreBackendWithTimeout sc 0 + +defaultSAWCoreBackendTimeout :: Integer +defaultSAWCoreBackendTimeout = 10000 + +newSAWCoreBackendWithTimeout :: SC.SharedContext -> Integer -> IO Sym +newSAWCoreBackendWithTimeout sc timeout = do st <- newSAWCoreState sc - sym <- newOnlineBackend W4.FloatRealRepr Nonce.globalNonceGenerator Yices.yicesDefaultFeatures st - W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym) + sym <- newOnlineBackend W4.FloatRealRepr Nonce.globalNonceGenerator (SMT2.defaultFeatures Z3.Z3) st + W4.extendConfig Z3.z3Options (W4.getConfiguration sym) + z3TimeoutSetting <- W4.getOptionSetting Z3.z3Timeout (W4.getConfiguration sym) + _ <- W4.setOpt z3TimeoutSetting timeout return sym sawCoreState :: Sym -> IO (SAWCoreState Nonce.GlobalNonceGenerator) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 70252b74d5..32a3431019 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -57,6 +57,7 @@ module SAWScript.Crucible.LLVM.Builtins , llvm_alloc_readonly , llvm_alloc_readonly_aligned , llvm_alloc_with_size + , llvm_alloc_sym_init , llvm_symbolic_alloc , llvm_alloc_global , llvm_fresh_expanded_val @@ -487,7 +488,7 @@ withMethodSpec :: LLVMModule arch -> String {- ^ Name of the function -} -> LLVMCrucibleSetupM () {- ^ Boundary specification -} -> - ((?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ((?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, ?w4EvalTactic :: W4EvalTactic, ?checkAllocSymInit :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> TopLevel a) -> TopLevel a withMethodSpec pathSat lm nm setup action = @@ -533,6 +534,8 @@ withMethodSpec pathSat lm nm setup action = verifyMethodSpec :: ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , ?checkAllocSymInit :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -739,7 +742,7 @@ checkSpecReturnType cc mspec = -- Returns a tuple of (arguments, preconditions, pointer values, -- memory). verifyPrestate :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> @@ -853,7 +856,7 @@ checkRegisterCompatibility mt mt' = return (st == st') resolveArguments :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> Crucible.MemImpl Sym -> MS.CrucibleMethodSpecIR (LLVM arch) -> @@ -925,7 +928,7 @@ setupGlobalAllocs cc mspec mem0 = foldM go mem0 $ mspec ^. MS.csGlobalAllocs -- function spec, write the given value to the address of the given -- pointer. setupPrePointsTos :: forall arch. - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => MS.CrucibleMethodSpecIR (LLVM arch) -> Options -> LLVMCrucibleContext arch -> @@ -954,7 +957,7 @@ setupPrePointsTos mspec opts cc env pts mem0 = foldM go mem0 pts -- | Sets up globals (ghost variable), and collects boolean terms -- that should be assumed to be true. setupPrestateConditions :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => MS.CrucibleMethodSpecIR (LLVM arch) -> LLVMCrucibleContext arch -> Crucible.MemImpl Sym -> @@ -1007,20 +1010,19 @@ assertEqualVals cc v1 v2 = -- TODO(langston): combine with/move to executeAllocation doAlloc :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> AllocIndex -> LLVMAllocSpec -> StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch)) -doAlloc cc i (LLVMAllocSpec mut _memTy alignment sz loc fresh) +doAlloc cc i (LLVMAllocSpec mut _memTy alignment sz loc fresh initialization) | fresh = liftIO $ executeFreshPointer cc i | otherwise = StateT $ \mem -> do let sym = cc^.ccBackend sz' <- liftIO $ resolveSAWSymBV cc Crucible.PtrWidth sz let l = show (W4.plSourceLoc loc) - liftIO $ - Crucible.doMalloc sym Crucible.HeapAlloc mut l mem sz' alignment + liftIO $ doAllocSymInit sym mem mut alignment sz' l initialization -------------------------------------------------------------------------------- @@ -1045,6 +1047,8 @@ ppGlobalPair cc gp = registerOverride :: ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , ?checkAllocSymInit :: Bool , Crucible.HasPtrWidth wptr , wptr ~ Crucible.ArchWidth arch , Crucible.HasLLVMAnn Sym @@ -1087,6 +1091,8 @@ registerOverride opts cc sim_ctx top_loc cs = registerInvariantOverride :: ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , ?checkAllocSymInit :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -1168,6 +1174,8 @@ withBreakpointCfgAndBlockId context name parent k = verifySimulate :: ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , ?checkAllocSymInit :: Bool , Crucible.HasPtrWidth wptr , wptr ~ Crucible.ArchWidth arch , Crucible.HasLLVMAnn Sym @@ -1287,6 +1295,8 @@ scAndList sc = conj . filter nontrivial verifyPoststate :: ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , ?checkAllocSymInit :: Bool , Crucible.HasPtrWidth wptr , wptr ~ Crucible.ArchWidth arch , Crucible.HasLLVMAnn Sym @@ -1355,7 +1365,7 @@ verifyPoststate cc mspec env0 globals ret = setupLLVMCrucibleContext :: Bool {- ^ enable path sat checking -} -> LLVMModule arch -> - ((?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ((?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, ?w4EvalTactic :: W4EvalTactic, ?checkAllocSymInit :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> TopLevel a) -> TopLevel a setupLLVMCrucibleContext pathSat lm action = @@ -1370,6 +1380,9 @@ setupLLVMCrucibleContext pathSat lm action = crucible_assert_then_assume_enabled <- gets rwCrucibleAssertThenAssume what4HashConsing <- gets rwWhat4HashConsing laxPointerOrdering <- gets rwLaxPointerOrdering + what4Eval <- gets rwWhat4Eval + allocSymInitCheck <- gets rwAllocSymInitCheck + crucibleTimeout <- gets rwCrucibleTimeout Crucible.llvmPtrWidth ctx $ \wptr -> Crucible.withPtrWidth wptr $ do let ?lc = ctx^.Crucible.llvmTypeCtx @@ -1378,10 +1391,12 @@ setupLLVMCrucibleContext pathSat lm action = } let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions let ?recordLLVMAnnotation = \_ _ -> return () + let ?w4EvalTactic = W4EvalTactic { doW4Eval = what4Eval } + let ?checkAllocSymInit = allocSymInitCheck cc <- io $ do let verbosity = simVerbose opts - sym <- Common.newSAWCoreBackend sc + sym <- Common.newSAWCoreBackendWithTimeout sc crucibleTimeout let cfg = W4.getConfiguration sym verbSetting <- W4.getOptionSetting W4.verbosity cfg @@ -1866,9 +1881,10 @@ llvm_alloc_with_mutability_and_size :: Crucible.Mutability -> Maybe (Crucible.Bytes) -> Maybe Crucible.Alignment -> + LLVMAllocSpecInit -> L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) -llvm_alloc_with_mutability_and_size mut sz alignment lty = +llvm_alloc_with_mutability_and_size mut sz alignment initialization lty = LLVMCrucibleSetupM $ do cctx <- getLLVMCrucibleContext loc <- getW4Position "llvm_alloc" @@ -1913,13 +1929,14 @@ llvm_alloc_with_mutability_and_size mut sz alignment lty = , _allocSpecBytes = sz'' , _allocSpecLoc = loc , _allocSpecFresh = False + , _allocSpecInit = initialization } llvm_alloc :: L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) llvm_alloc = - llvm_alloc_with_mutability_and_size Crucible.Mutable Nothing Nothing + llvm_alloc_with_mutability_and_size Crucible.Mutable Nothing Nothing LLVMAllocSpecNoInitialization llvm_alloc_aligned :: Int -> @@ -1932,7 +1949,7 @@ llvm_alloc_readonly :: L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) llvm_alloc_readonly = - llvm_alloc_with_mutability_and_size Crucible.Immutable Nothing Nothing + llvm_alloc_with_mutability_and_size Crucible.Immutable Nothing Nothing LLVMAllocSpecNoInitialization llvm_alloc_readonly_aligned :: Int -> @@ -1952,6 +1969,7 @@ llvm_alloc_aligned_with_mutability mut n lty = mut Nothing (Just alignment) + LLVMAllocSpecNoInitialization lty coerceAlignment :: Int -> CrucibleSetup (LLVM arch) Crucible.Alignment @@ -1975,8 +1993,13 @@ llvm_alloc_with_size sz lty = Crucible.Mutable (Just (Crucible.toBytes sz)) Nothing + LLVMAllocSpecNoInitialization lty +llvm_alloc_sym_init :: L.Type -> LLVMCrucibleSetupM (AllLLVM SetupValue) +llvm_alloc_sym_init = + llvm_alloc_with_mutability_and_size Crucible.Mutable Nothing Nothing LLVMAllocSpecSymbolicInitialization + llvm_symbolic_alloc :: Bool -> Int -> @@ -2008,6 +2031,7 @@ llvm_symbolic_alloc ro align_bytes sz = , _allocSpecBytes = sz , _allocSpecLoc = loc , _allocSpecFresh = False + , _allocSpecInit = LLVMAllocSpecNoInitialization } n <- Setup.csVarCounter <<%= nextAllocIndex Setup.currentState . MS.csAllocs . at n ?= spec @@ -2057,6 +2081,7 @@ constructFreshPointer mid loc memTy = , _allocSpecBytes = sz , _allocSpecLoc = loc , _allocSpecFresh = True + , _allocSpecInit = LLVMAllocSpecNoInitialization } -- TODO: refactor case mid of diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 9934bb32b2..fedada1446 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -39,12 +39,14 @@ module SAWScript.Crucible.LLVM.MethodSpecIR , csParentName -- * LLVMAllocSpec , LLVMAllocSpec(..) + , LLVMAllocSpecInit(..) , allocSpecType , allocSpecAlign , allocSpecMut , allocSpecLoc , allocSpecBytes , allocSpecFresh + , allocSpecInit , mutIso , isMut -- * LLVMModule @@ -188,6 +190,14 @@ type instance MS.MethodId (LLVM _) = LLVMMethodId -------------------------------------------------------------------------------- -- *** LLVMAllocSpec +-- | Allocation initialization policy +data LLVMAllocSpecInit + = LLVMAllocSpecSymbolicInitialization + -- ^ allocation is initialized with a fresh symbolic array of bytes + | LLVMAllocSpecNoInitialization + -- ^ allocation not initialized + deriving (Eq, Ord, Show) + data LLVMAllocSpec = LLVMAllocSpec { _allocSpecMut :: CL.Mutability @@ -196,6 +206,7 @@ data LLVMAllocSpec = , _allocSpecBytes :: Term , _allocSpecLoc :: ProgramLoc , _allocSpecFresh :: Bool -- ^ Whether declared with @crucible_fresh_pointer@ + , _allocSpecInit :: LLVMAllocSpecInit } deriving (Eq, Show) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 398a0a15a8..431e14edb7 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -41,12 +41,15 @@ module SAWScript.Crucible.LLVM.Override , learnSetupCondition , executeSetupCondition , matchArg + , matchPointsToValue , assertTermEqualities , methodSpecHandler , valueToSC , storePointsToValue + , doAllocSymInit , diffMemTypes + , ppPointsToAsLLVMVal , enableSMTArrayMemoryModel ) where @@ -158,7 +161,7 @@ ppLLVMVal cc val = do -- | Resolve a 'SetupValue' into a 'LLVMVal' and pretty-print it ppSetupValueAsLLVMVal :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ output/verbosity options -} -> LLVMCrucibleContext arch -> SharedContext {- ^ context for constructing SAW terms -} -> @@ -194,7 +197,7 @@ mkStructuralMismatch _opts cc _sc spec llvmval setupval memTy = -- | Instead of using 'ppPointsTo', which prints 'SetupValue', translate -- expressions to 'LLVMVal'. ppPointsToAsLLVMVal :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ output/verbosity options -} -> LLVMCrucibleContext arch -> SharedContext {- ^ context for constructing SAW terms -} -> @@ -213,7 +216,7 @@ ppPointsToAsLLVMVal opts cc sc spec (LLVMPointsTo loc cond ptr val) = do -- | Create an error stating that the 'LLVMVal' was not equal to the 'SetupValue' notEqual :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => PrePost -> Options {- ^ output/verbosity options -} -> W4.ProgramLoc {- ^ where is the assertion from? -} -> @@ -370,6 +373,8 @@ methodSpecHandler :: forall arch rtp args ret. ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , ?checkAllocSymInit :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -592,6 +597,8 @@ methodSpecHandler_prestate :: forall arch ctx. ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , ?checkAllocSymInit :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -626,7 +633,7 @@ methodSpecHandler_prestate opts sc cc args cs = -- and computing postcondition predicates. methodSpecHandler_poststate :: forall arch ret. - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> @@ -641,6 +648,8 @@ methodSpecHandler_poststate opts sc cc retTy cs = learnCond :: ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , ?checkAllocSymInit :: Bool , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -664,6 +673,7 @@ learnCond opts sc cc cs prepost globals extras ss = assertTermEqualities :: + (?w4EvalTactic :: W4EvalTactic) => SharedContext -> LLVMCrucibleContext arch -> OverrideMatcher (LLVM arch) md () @@ -696,7 +706,7 @@ enforceCompleteSubstitution loc ss = -- execute a pre/post condition -executeCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) +executeCond :: (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> SharedContext -> LLVMCrucibleContext arch @@ -734,7 +744,7 @@ refreshTerms sc ss = -- override's precondition are allocated, and meet the appropriate -- requirements for alignment and mutability. enforcePointerValidity :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?memOpts::Crucible.MemOptions, ?w4EvalTactic :: W4EvalTactic, ?checkAllocSymInit :: Bool, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => SharedContext -> LLVMCrucibleContext arch -> W4.ProgramLoc -> @@ -763,17 +773,55 @@ enforcePointerValidity sc cc loc ss = addAssert c $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" - | (LLVMAllocSpec mut _pty alignment psz _ploc fresh, ptr) <- mems + case initialization of + LLVMAllocSpecSymbolicInitialization + | ?checkAllocSymInit -> + do maybeOk <- liftIO $ checkMemLoad sym mem ptr psz' alignment + let msg' = PP.vcat $ map (PP.pretty . unwords) + [ [ "Memory region not initialized:" ] + , [ " pointer =", show (Crucible.ppPtr ptr) ] + , [ " size =", showTerm psz ] + ] + case maybeOk of + Just ok -> + addAssert ok $ Crucible.SimError loc $ + Crucible.AssertFailureSimError (show msg') "" + Nothing -> failure loc (BadPointerLoad (Right msg') "") + _ -> return () + + | (LLVMAllocSpec mut _pty alignment psz _ploc fresh initialization, ptr) <- mems , not fresh -- Fresh symbolic pointers are not assumed to be valid; don't check them ] +checkMemLoad :: + (?memOpts::Crucible.MemOptions, Crucible.IsSymInterface sym, Crucible.HasPtrWidth wptr, Crucible.HasLLVMAnn sym) => + sym -> + Crucible.MemImpl sym -> + Crucible.LLVMPtr sym wptr -> + W4.SymBV sym wptr -> + Crucible.Alignment -> + IO (Maybe (W4.Pred sym)) +checkMemLoad sym mem ptr sz align = + case BV.asNatural <$> W4.asBV sz of + Just n -> do + res <- Crucible.loadRaw sym mem ptr (Crucible.arrayType n $ Crucible.bitvectorType 1) align + case res of + Crucible.NoErr pred_ _val -> do + return $ Just pred_ + _ -> return Nothing + Nothing -> do + maybe_allocation_array <- Crucible.asMemAllocationArrayStore sym Crucible.PtrWidth ptr (Crucible.memImplHeap mem) + case maybe_allocation_array of + Just (ok, _arr, _sz) -> return $ Just ok + Nothing -> return Nothing + ------------------------------------------------------------------------ -- | Generate assertions that all of the memory allocations matched by -- an override's precondition are disjoint. Read-only allocations are -- allowed to alias other read-only allocations, however. enforceDisjointness :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => SharedContext -> LLVMCrucibleContext arch -> W4.ProgramLoc -> @@ -815,7 +863,7 @@ enforceDisjointness sc cc loc globals extras ss = -- not be disjoint. Similarly, fresh pointers need not be checked for -- disjointness. enforceDisjointAllocSpec :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => SharedContext -> LLVMCrucibleContext arch -> Sym -> W4.ProgramLoc -> @@ -823,8 +871,8 @@ enforceDisjointAllocSpec :: (LLVMAllocSpec, LLVMPtr (Crucible.ArchWidth arch)) -> OverrideMatcher (LLVM arch) md () enforceDisjointAllocSpec sc cc sym loc - (LLVMAllocSpec pmut _pty _palign psz ploc pfresh, p) - (LLVMAllocSpec qmut _qty _qalign qsz qloc qfresh, q) + (LLVMAllocSpec pmut _pty _palign psz ploc pfresh _p_sym_init, p) + (LLVMAllocSpec qmut _qty _qalign qsz qloc qfresh _q_sym_init, q) | (pmut, qmut) == (Crucible.Immutable, Crucible.Immutable) = pure () -- Read-only allocations may alias each other | pfresh || qfresh = @@ -856,7 +904,7 @@ enforceDisjointAllocGlobal :: (LLVMAllocGlobal arch, LLVMPtr (Crucible.ArchWidth arch)) -> OverrideMatcher (LLVM arch) md () enforceDisjointAllocGlobal sym loc - (LLVMAllocSpec _pmut _pty _palign psz ploc _pfresh, p) + (LLVMAllocSpec _pmut _pty _palign psz ploc _pfresh _p_sym_init, p) (LLVMAllocGlobal qloc (L.Symbol qname), q) = do let Crucible.LLVMPointer pblk _ = p let Crucible.LLVMPointer qblk _ = q @@ -885,6 +933,7 @@ ppProgramLoc loc = matchPointsTos :: forall arch md. ( ?lc :: Crucible.TypeContext , ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -952,7 +1001,7 @@ matchPointsTos opts sc cc spec prepost = go False [] ------------------------------------------------------------------------ computeReturnValue :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ saw script debug and print options -} -> LLVMCrucibleContext arch {- ^ context of the crucible simulation -} -> SharedContext {- ^ context for generating saw terms -} -> @@ -1071,6 +1120,7 @@ diffMemTypesList i ((x, y) : ts) = -- | Match the value of a function argument with a symbolic 'SetupValue'. matchArg :: + (?w4EvalTactic :: W4EvalTactic) => Options {- ^ saw script print out opts -} -> Crucible.HasPtrWidth (Crucible.ArchWidth arch) => SharedContext {- ^ context for constructing SAW terms -} -> @@ -1084,10 +1134,7 @@ matchArg :: OverrideMatcher (LLVM arch) md () matchArg opts sc cc cs prepost actual expectedTy expected = do - let mvar = Crucible.llvmMemVar (ccLLVMContext cc) - mem <- case Crucible.lookupGlobal mvar $ cc ^. ccLLVMGlobals of - Nothing -> fail "internal error: LLVM Memory global not found" - Just mem -> pure mem + mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc case (actual, expectedTy, expected) of (_, _, SetupTerm expectedTT) | TypedTermSchema (Cryptol.Forall [] [] tyexpr) <- ttType expectedTT @@ -1301,7 +1348,7 @@ matchTerm sc cc loc prepost real expect = -- | Use the current state to learn about variable assignments based on -- preconditions for a procedure specification. learnSetupCondition :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1353,6 +1400,7 @@ learnPointsTo :: forall arch md ann. ( ?lc :: Crucible.TypeContext , ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -1364,6 +1412,28 @@ learnPointsTo :: PointsTo (LLVM arch) -> OverrideMatcher (LLVM arch) md (Maybe (PP.Doc ann)) learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) = + do (_memTy, ptr1) <- resolveSetupValue opts cc sc spec Crucible.PtrRepr ptr + matchPointsToValue opts sc cc spec prepost loc maybe_cond ptr1 val + +matchPointsToValue :: + forall arch md ann. + ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => + Options -> + SharedContext -> + LLVMCrucibleContext arch -> + MS.CrucibleMethodSpecIR (LLVM arch) -> + PrePost -> + W4.ProgramLoc -> + Maybe TypedTerm -> + LLVMPtr (Crucible.ArchWidth arch) -> + LLVMPointsToValue arch -> + OverrideMatcher (LLVM arch) md (Maybe (PP.Doc ann)) +matchPointsToValue opts sc cc spec prepost loc maybe_cond ptr val = do let tyenv = MS.csAllocations spec nameEnv = MS.csTypeNames spec sym <- Ov.getSymInterface @@ -1371,8 +1441,6 @@ learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) = mem <- readGlobal $ Crucible.llvmMemVar $ ccLLVMContext cc - (_memTy, ptr1) <- resolveSetupValue opts cc sc spec Crucible.PtrRepr ptr - let alignment = Crucible.noAlignment -- default to byte alignment (FIXME) case val of @@ -1381,12 +1449,12 @@ learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) = -- In case the types are different (from llvm_points_to_untyped) -- then the load type should be determined by the rhs. storTy <- Crucible.toStorableType memTy - res <- liftIO $ Crucible.loadRaw sym mem ptr1 storTy alignment + res <- liftIO $ Crucible.loadRaw sym mem ptr storTy alignment let summarizeBadLoad = let dataLayout = Crucible.llvmDataLayout (ccTypeCtx cc) sz = Crucible.memTypeSize dataLayout memTy in map (PP.pretty . unwords) - [ [ "When reading through pointer:", show (Crucible.ppPtr ptr1) ] + [ [ "When reading through pointer:", show (Crucible.ppPtr ptr) ] , [ "in the ", stateCond prepost, "of an override" ] , [ "Tried to read something of size:" , show (Crucible.bytesToInteger sz) @@ -1406,7 +1474,7 @@ learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) = _ -> do -- When we have a concrete failure, we do a little more computation to -- try and find out why. - let (blk, _offset) = Crucible.llvmPointerView ptr1 + let (blk, _offset) = Crucible.llvmPointerView ptr pure $ Just $ PP.vcat . (summarizeBadLoad ++) $ case W4.asNat blk of Nothing -> [""] @@ -1430,22 +1498,49 @@ learnPointsTo opts sc cc spec prepost (LLVMPointsTo loc maybe_cond ptr val) = SymbolicSizeValue expected_arr_tm expected_sz_tm -> do maybe_allocation_array <- liftIO $ - Crucible.asMemAllocationArrayStore sym Crucible.PtrWidth ptr1 (Crucible.memImplHeap mem) + Crucible.asMemAllocationArrayStore sym Crucible.PtrWidth ptr (Crucible.memImplHeap mem) let errMsg = PP.vcat $ map (PP.pretty . unwords) - [ [ "When reading through pointer:", show (Crucible.ppPtr ptr1) ] + [ [ "When reading through pointer:", show (Crucible.ppPtr ptr) ] , [ "in the ", stateCond prepost, "of an override" ] , [ "Tried to read an array prefix of size:", show (MS.ppTypedTerm expected_sz_tm) ] ] case maybe_allocation_array of Just (ok, arr, sz) - | Crucible.LLVMPointer _ off <- ptr1 - , Just 0 <- BV.asUnsigned <$> W4.asBV off -> + | Crucible.LLVMPointer _ off <- ptr -> do addAssert ok $ Crucible.SimError loc $ Crucible.GenericSimError $ show errMsg + sub <- OM (use termSub) st <- liftIO (sawCoreState sym) - arr_tm <- liftIO $ toSC sym st arr - instantiateExtMatchTerm sc cc (spec ^. MS.csLoc) prepost arr_tm (ttTerm expected_arr_tm) + + ptr_width_tm <- liftIO $ scNat sc $ natValue ?ptrWidth + off_type_tm <- liftIO $ scBitvector sc $ natValue ?ptrWidth + off_tm <- liftIO $ toSC sym st off + alloc_arr_tm <- liftIO $ toSC sym st arr + + arr_tm <- liftIO $ case BV.asUnsigned <$> W4.asBV off of + Just 0 -> return alloc_arr_tm + _ -> + do byte_width_tm <- scNat sc 8 + byte_type_tm <- scBitvector sc 8 + + zero_off_tm <- scBvNat sc ptr_width_tm =<< scNat sc 0 + zero_byte_tm <- scBvNat sc byte_width_tm =<< scNat sc 0 + zero_arr_const_tm <- scArrayConstant sc off_type_tm byte_type_tm zero_byte_tm + + instantiated_expected_sz_tm <- scInstantiateExt sc sub $ ttTerm expected_sz_tm + scArrayCopy sc ptr_width_tm byte_type_tm + zero_arr_const_tm -- dest array + zero_off_tm -- dest offset + alloc_arr_tm -- src array + off_tm -- src offset + instantiated_expected_sz_tm -- length + + instantiateExtMatchTerm sc cc loc prepost arr_tm $ ttTerm expected_arr_tm + sz_tm <- liftIO $ toSC sym st sz - instantiateExtMatchTerm sc cc (spec ^. MS.csLoc) prepost sz_tm (ttTerm expected_sz_tm) + expected_end_off_tm <- liftIO $ scBvAdd sc ptr_width_tm off_tm $ ttTerm expected_sz_tm + inbounds_check_tm <- liftIO $ scBvULe sc ptr_width_tm expected_end_off_tm sz_tm + learnPred sc cc loc prepost inbounds_check_tm + return Nothing _ -> return $ Just errMsg @@ -1459,7 +1554,7 @@ stateCond PostState = "postcondition" -- | Process an @llvm_equal@ statement from the precondition -- section of the CrucibleSetup block. learnEqual :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1479,6 +1574,7 @@ learnEqual opts sc cc spec loc prepost v1 v2 = do -- | Process an @llvm_precond@ statement from the precondition -- section of the CrucibleSetup block. learnPred :: + (?w4EvalTactic :: W4EvalTactic) => SharedContext -> LLVMCrucibleContext arch -> W4.ProgramLoc -> @@ -1490,6 +1586,7 @@ learnPred sc cc loc prepost t = addAssert p (Crucible.SimError loc (Crucible.AssertFailureSimError (stateCond prepost) "")) instantiateExtResolveSAWPred :: + (?w4EvalTactic :: W4EvalTactic) => SharedContext -> LLVMCrucibleContext arch -> Term -> @@ -1499,7 +1596,7 @@ instantiateExtResolveSAWPred sc cc cond = do liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond instantiateExtResolveSAWSymBV :: - (1 <= w) => + (?w4EvalTactic :: W4EvalTactic, 1 <= w) => SharedContext -> LLVMCrucibleContext arch -> NatRepr w -> @@ -1518,6 +1615,7 @@ instantiateExtResolveSAWSymBV sc cc w tm = do -- Return a map containing the overwritten memory allocations. invalidateMutableAllocs :: ( ?lc :: Crucible.TypeContext + , ?w4EvalTactic :: W4EvalTactic , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym ) => @@ -1609,13 +1707,13 @@ invalidateMutableAllocs opts sc cc cs = do -- | Perform an allocation as indicated by an @llvm_alloc@ or -- @llvm_fresh_pointer@ statement from the postcondition section. executeAllocation :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> SharedContext -> LLVMCrucibleContext arch -> (AllocIndex, LLVMAllocSpec) -> OverrideMatcher (LLVM arch) RW () -executeAllocation opts sc cc (var, LLVMAllocSpec mut memTy alignment sz loc fresh) +executeAllocation opts sc cc (var, LLVMAllocSpec mut memTy alignment sz loc fresh initialization) | fresh = do ptr <- liftIO $ executeFreshPointer cc var OM (setupValueSub %= Map.insert var ptr) @@ -1631,17 +1729,38 @@ executeAllocation opts sc cc (var, LLVMAllocSpec mut memTy alignment sz loc fres mem <- readGlobal memVar sz' <- instantiateExtResolveSAWSymBV sc cc Crucible.PtrWidth sz let l = show (W4.plSourceLoc loc) ++ " (Poststate)" - (ptr, mem') <- liftIO $ - Crucible.doMalloc sym Crucible.HeapAlloc mut l mem sz' alignment + (ptr, mem') <- liftIO $ doAllocSymInit sym mem mut alignment sz' l initialization writeGlobal memVar mem' assignVar cc loc var ptr +doAllocSymInit :: + (Crucible.IsSymInterface sym, Crucible.HasPtrWidth wptr, Crucible.HasLLVMAnn sym) => + sym -> + Crucible.MemImpl sym -> + Crucible.Mutability -> + Crucible.Alignment -> + W4.SymBV sym wptr {- ^ allocation size -} -> + String {- ^ source location for use in error messages -} -> + LLVMAllocSpecInit {- ^ allocation initialization policy -} -> + IO (Crucible.LLVMPtr sym wptr, Crucible.MemImpl sym) +doAllocSymInit sym mem mut alignment sz loc initialization = do + (ptr, mem') <- Crucible.doMalloc sym Crucible.HeapAlloc mut loc mem sz alignment + mem'' <- case initialization of + LLVMAllocSpecSymbolicInitialization -> do + arr <- W4.freshConstant + sym + (W4.systemSymbol "arr!") + (W4.BaseArrayRepr (Ctx.singleton $ W4.BaseBVRepr ?ptrWidth) (W4.BaseBVRepr (W4.knownNat @8))) + Crucible.doArrayConstStore sym mem' ptr alignment arr sz + LLVMAllocSpecNoInitialization -> return mem' + return (ptr, mem'') + ------------------------------------------------------------------------ -- | Update the simulator state based on the postconditions from the -- procedure specification. executeSetupCondition :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1680,7 +1799,7 @@ executeGhost _sc _var (TypedTerm tp _) = -- the CrucibleSetup block. First we compute the value indicated by -- 'val', and then write it to the address indicated by 'ptr'. executePointsTo :: - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1711,7 +1830,7 @@ executePointsTo opts sc cc spec overwritten_allocs (LLVMPointsTo _loc cond ptr v writeGlobal memVar mem' storePointsToValue :: - (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => Options -> LLVMCrucibleContext arch -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> @@ -1797,7 +1916,7 @@ storePointsToValue opts cc env tyenv nameEnv base_mem maybe_cond ptr val maybe_i -- | Process an @llvm_equal@ statement from the postcondition -- section of the CrucibleSetup block. executeEqual :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1814,6 +1933,7 @@ executeEqual opts sc cc spec v1 v2 = do -- | Process an @llvm_postcond@ statement from the postcondition -- section of the CrucibleSetup block. executePred :: + (?w4EvalTactic :: W4EvalTactic) => SharedContext -> LLVMCrucibleContext arch -> TypedTerm {- ^ the term to assert as a postcondition -} -> @@ -1863,7 +1983,7 @@ instantiateSetupValue sc s v = ------------------------------------------------------------------------ resolveSetupValueLLVM :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> LLVMCrucibleContext arch -> SharedContext -> @@ -1882,7 +2002,7 @@ resolveSetupValueLLVM opts cc sc spec sval = return (memTy, lval) resolveSetupValue :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> LLVMCrucibleContext arch -> SharedContext -> diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 333347729c..7aa00ad0e8 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -28,6 +28,7 @@ module SAWScript.Crucible.LLVM.ResolveSetupValue , equalValsPred , memArrayToSawCoreTerm , scPtrWidthBvNat + , W4EvalTactic(..) ) where import Control.Lens ((^.)) @@ -39,6 +40,7 @@ import Data.Maybe (fromMaybe, listToMaybe, fromJust) import Data.Map (Map) import qualified Data.Map as Map +import qualified Data.Set as Set import qualified Data.Vector as V import Numeric.Natural @@ -46,6 +48,7 @@ import qualified Text.LLVM.AST as L import qualified Cryptol.Eval.Type as Cryptol (TValue(..), tValTy, evalValType) import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..)) +import qualified Verifier.SAW.Cryptol.Simpset as Cryptol import Data.Parameterized.Some (Some(..)) import Data.Parameterized.NatRepr @@ -64,7 +67,9 @@ import qualified Verifier.SAW.Prim as Prim import qualified Verifier.SAW.Simulator.Concrete as Concrete import Verifier.SAW.Cryptol (importType, emptyEnv) +import Verifier.SAW.Name import Verifier.SAW.TypedTerm +import Verifier.SAW.Simulator.What4 import Verifier.SAW.Simulator.What4.ReturnTrip import Text.LLVM.DebugUtils as L @@ -72,6 +77,7 @@ import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..), ppTypedTermType) import SAWScript.Crucible.LLVM.MethodSpecIR +import qualified SAWScript.Proof as SP --import qualified SAWScript.LLVMBuiltins as LB @@ -289,10 +295,18 @@ resolveSetupElemIndexOrFail cc env nameEnv v i = do lc = ccTypeCtx cc dl = Crucible.llvmDataLayout lc + +-- | The tactic for What4 translation for SAWCore expressions during +-- Crucible symbolic execution. The boolean option specifies whether +-- non-user-defined symbols are translated. Note that ground constants are +-- always translated. +newtype W4EvalTactic = W4EvalTactic { doW4Eval :: Bool } + deriving (Eq, Ord, Show) + -- | Translate a SetupValue into a Crucible LLVM value, resolving -- references resolveSetupVal :: forall arch. - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> Crucible.MemImpl Sym -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> @@ -353,7 +367,7 @@ resolveSetupVal cc mem env tyenv nameEnv val = do dl = Crucible.llvmDataLayout lc resolveTypedTerm :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> TypedTerm -> IO LLVMVal @@ -368,6 +382,7 @@ resolveTypedTerm cc tm = ] resolveSAWPred :: + (?w4EvalTactic :: W4EvalTactic) => LLVMCrucibleContext arch -> Term -> IO (W4.Pred Sym) @@ -385,10 +400,20 @@ resolveSAWPred cc tm = do _ -> return Nothing case mx of Just x -> return $ W4.backendPred sym x - Nothing -> bindSAWTerm sym st W4.BaseBoolRepr tm' + Nothing + | doW4Eval ?w4EvalTactic -> + do cryptol_ss <- Cryptol.mkCryptolSimpset @SP.TheoremNonce sc + (_,tm'') <- rewriteSharedTerm sc cryptol_ss tm' + (_,tm''') <- rewriteSharedTerm sc ss tm'' + if not (any (\(name, _, _) -> not (isPreludeName name)) (Map.elems $ getConstantSet tm''')) then + do (_names, (_mlabels, p)) <- w4Eval sym st sc mempty Set.empty tm''' + return p + else bindSAWTerm sym st W4.BaseBoolRepr tm' + | otherwise -> + bindSAWTerm sym st W4.BaseBoolRepr tm' resolveSAWSymBV :: - (1 <= w) => + (?w4EvalTactic :: W4EvalTactic, 1 <= w) => LLVMCrucibleContext arch -> NatRepr w -> Term -> @@ -405,10 +430,31 @@ resolveSAWSymBV cc w tm = _ -> return Nothing case mx of Just x -> W4.bvLit sym w (BV.mkBV w x) - Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm + Nothing + | doW4Eval ?w4EvalTactic -> + do let ss = cc^.ccBasicSS + (_,tm') <- rewriteSharedTerm sc ss tm + cryptol_ss <- Cryptol.mkCryptolSimpset @SP.TheoremNonce sc + (_,tm'') <- rewriteSharedTerm sc cryptol_ss tm' + (_,tm''') <- rewriteSharedTerm sc ss tm'' + if not (any (\(name, _, _) -> not (isPreludeName name)) (Map.elems $ getConstantSet tm''')) then + do (_names, _, _, x) <- w4EvalAny sym st sc mempty Set.empty tm''' + case valueToSymExpr x of + Just (Some y) + | Just Refl <- testEquality (W4.BaseBVRepr w) (W4.exprType y) -> + return y + _ -> fail $ "resolveSAWSymBV: unexpected w4Eval result " ++ show x + else bindSAWTerm sym st (W4.BaseBVRepr w) tm + | otherwise -> + bindSAWTerm sym st (W4.BaseBVRepr w) tm + +isPreludeName :: NameInfo -> Bool +isPreludeName = \case + ModuleIdentifier ident -> identModule ident == preludeName + _ -> False resolveSAWTerm :: - Crucible.HasPtrWidth (Crucible.ArchWidth arch) => + (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> Cryptol.TValue -> Term -> diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index e5431f2431..03aa1efb8d 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -84,6 +84,7 @@ import SAWScript.Crucible.LLVM.ResolveSetupValue import qualified SAWScript.Crucible.LLVM.Override as LO import qualified SAWScript.Crucible.LLVM.MethodSpecIR as LMS (LLVM) +import qualified What4.Concrete as W4 import qualified What4.Config as W4 import qualified What4.Expr as W4 import qualified What4.FunctionName as W4 @@ -141,6 +142,7 @@ type X86Constraints = , C.LLVM.HasLLVMAnn Sym , ?memOpts :: C.LLVM.MemOptions , ?lc :: C.LLVM.TypeContext + , ?w4EvalTactic :: W4EvalTactic ) newtype X86Sim a = X86Sim { unX86Sim :: StateT X86State IO a } @@ -301,10 +303,18 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se sc <- getSharedContext opts <- getOptions basic_ss <- getBasicSS - sym <- liftIO $ newSAWCoreBackend sc rw <- getTopLevelRW + sym <- liftIO $ newSAWCoreBackendWithTimeout sc $ rwCrucibleTimeout rw cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms $ W4.getConfiguration sym _ <- liftIO $ W4.setOpt cacheTermsSetting $ rwWhat4HashConsingX86 rw + liftIO $ W4.extendConfig + [ W4.opt + LO.enableSMTArrayMemoryModel + (W4.ConcreteBool $ rwSMTArrayMemoryModel rw) + ("Enable SMT array memory model" :: Text) + ] + (W4.getConfiguration sym) + let ?w4EvalTactic = W4EvalTactic { doW4Eval = rwWhat4Eval rw } sawst <- liftIO $ sawCoreState sym halloc <- getHandleAlloc let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule @@ -728,13 +738,12 @@ assumeAllocation :: Map MS.AllocIndex Ptr -> (MS.AllocIndex, LLVMAllocSpec) {- ^ llvm_alloc statement -} -> X86Sim (Map MS.AllocIndex Ptr) -assumeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc False) = do +assumeAllocation env (i, LLVMAllocSpec mut _memTy align sz loc False initialization) = do cc <- use x86CrucibleContext sym <- use x86Sym mem <- use x86Mem sz' <- liftIO $ resolveSAWSymBV cc knownNat sz - (ptr, mem') <- liftIO $ C.LLVM.doMalloc sym C.LLVM.HeapAlloc mut - (show $ W4.plSourceLoc loc) mem sz' align + (ptr, mem') <- liftIO $ LO.doAllocSymInit sym mem mut align sz' (show $ W4.plSourceLoc loc) initialization x86Mem .= mem' pure $ Map.insert i ptr env assumeAllocation env _ = pure env @@ -750,15 +759,12 @@ assumePointsTo :: LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} -> X86Sim () assumePointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptval) = do - when (isJust cond) $ throwX86 "unsupported x86_64 command: llvm_conditional_points_to" - tval <- checkConcreteSizePointsToValue tptval - sym <- use x86Sym + opts <- use x86Options cc <- use x86CrucibleContext mem <- use x86Mem ptr <- resolvePtrSetupValue env tyenv tptr - val <- liftIO $ resolveSetupVal cc mem env tyenv Map.empty tval - storTy <- liftIO $ C.LLVM.toStorableType =<< typeOfSetupValue cc tyenv nameEnv tval - mem' <- liftIO $ C.LLVM.storeConstRaw sym mem ptr storTy C.LLVM.noAlignment val + cond' <- liftIO $ mapM (resolveSAWPred cc . ttTerm) cond + mem' <- liftIO $ LO.storePointsToValue opts cc env tyenv nameEnv mem cond' ptr tptval Nothing x86Mem .= mem' resolvePtrSetupValue :: @@ -785,11 +791,6 @@ resolvePtrSetupValue env tyenv tptr = do _ -> liftIO $ C.LLVM.unpackMemValue sym (C.LLVM.LLVMPointerRepr $ knownNat @64) =<< resolveSetupVal cc mem env tyenv Map.empty tptr -checkConcreteSizePointsToValue :: LLVMPointsToValue LLVMArch -> X86Sim (MS.SetupValue LLVM) -checkConcreteSizePointsToValue = \case - ConcreteSizeValue val -> return val - SymbolicSizeValue{} -> throwX86 "unsupported x86_64 command: llvm_points_to_array_prefix" - -- | Write each SetupValue passed to llvm_execute_func to the appropriate -- x86_64 register from the calling convention. setArgs :: @@ -851,7 +852,6 @@ assertPost globals env premem preregs = do postregs <- use x86Regs let tyenv = ms ^. MS.csPreState . MS.csAllocs - nameEnv = MS.csTypeNames ms prersp <- getReg Macaw.RSP preregs expectedIP <- liftIO $ C.LLVM.doLoad sym premem prersp (C.LLVM.bitvectorType 8) @@ -888,8 +888,9 @@ assertPost globals env premem preregs = do _ -> throwX86 $ "Invalid return type: " <> show (C.LLVM.ppMemType retTy) _ -> pure [] + pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos) - $ assertPointsTo env tyenv nameEnv + $ assertPointsTo env tyenv let setupConditionMatchesPre = fmap -- assume preconditions (LO.executeSetupCondition opts sc cc ms) @@ -930,24 +931,22 @@ assertPointsTo :: X86Constraints => Map MS.AllocIndex Ptr {- ^ Associates each AllocIndex with the corresponding allocation -} -> Map MS.AllocIndex LLVMAllocSpec {- ^ Associates each AllocIndex with its specification -} -> - Map MS.AllocIndex C.LLVM.Ident {- ^ Associates each AllocIndex with its name -} -> LLVMPointsTo LLVMArch {- ^ llvm_points_to statement from the precondition -} -> X86Sim (LLVMOverrideMatcher md ()) -assertPointsTo env tyenv nameEnv (LLVMPointsTo _ cond tptr tptexpected) = do - when (isJust cond) $ throwX86 "unsupported x86_64 command: llvm_conditional_points_to" - texpected <- checkConcreteSizePointsToValue tptexpected - sym <- use x86Sym +assertPointsTo env tyenv pointsTo@(LLVMPointsTo loc cond tptr tptval) = do opts <- use x86Options sc <- use x86SharedContext cc <- use x86CrucibleContext ms <- use x86MethodSpec - mem <- use x86Mem - ptr <- resolvePtrSetupValue env tyenv tptr - memTy <- liftIO $ typeOfSetupValue cc tyenv nameEnv texpected - storTy <- liftIO $ C.LLVM.toStorableType memTy - actual <- liftIO $ C.LLVM.assertSafe sym =<< C.LLVM.loadRaw sym mem ptr storTy C.LLVM.noAlignment - pure $ LO.matchArg opts sc cc ms MS.PostState actual memTy texpected + ptr <- resolvePtrSetupValue env tyenv tptr + pure $ do + err <- LO.matchPointsToValue opts sc cc ms MS.PostState loc cond ptr tptval + case err of + Just msg -> do + doc <- LO.ppPointsToAsLLVMVal opts cc sc ms pointsTo + O.failure loc (O.BadPointerLoad (Right doc) msg) + Nothing -> pure () -- | Gather and run the solver on goals from the simulator. checkGoals :: diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 0d2d48c0a9..1a798e4686 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -82,6 +82,7 @@ import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW -- Crucible import qualified Lang.Crucible.JVM as CJ +import qualified SAWScript.Crucible.Common as CC import qualified SAWScript.Crucible.Common.MethodSpec as CMS import qualified SAWScript.Crucible.JVM.BuiltinsJVM as CJ import SAWScript.Crucible.LLVM.Builtins @@ -483,8 +484,11 @@ buildTopLevelEnv proxy opts = , rwDebugIntrinsics = True , rwWhat4HashConsing = False , rwWhat4HashConsingX86 = False + , rwWhat4Eval = False , rwPreservedRegs = [] , rwStackBaseAlign = defaultStackBaseAlign + , rwAllocSymInitCheck = True + , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout } return (bic, ro0, rw0) @@ -595,6 +599,16 @@ disable_x86_what4_hash_consing = do rw <- getTopLevelRW putTopLevelRW rw { rwWhat4HashConsingX86 = False } +enable_what4_eval :: TopLevel () +enable_what4_eval = do + rw <- getTopLevelRW + putTopLevelRW rw { rwWhat4Eval = True } + +disable_what4_eval :: TopLevel () +disable_what4_eval = do + rw <- getTopLevelRW + putTopLevelRW rw { rwWhat4Eval = False } + add_x86_preserved_reg :: String -> TopLevel () add_x86_preserved_reg r = do rw <- getTopLevelRW @@ -615,6 +629,21 @@ default_x86_stack_base_align = do rw <- getTopLevelRW putTopLevelRW rw { rwStackBaseAlign = defaultStackBaseAlign } +enable_alloc_sym_init_check :: TopLevel () +enable_alloc_sym_init_check = do + rw <- getTopLevelRW + putTopLevelRW rw { rwAllocSymInitCheck = True } + +disable_alloc_sym_init_check :: TopLevel () +disable_alloc_sym_init_check = do + rw <- getTopLevelRW + putTopLevelRW rw { rwAllocSymInitCheck = False } + +set_crucible_timeout :: Integer -> TopLevel () +set_crucible_timeout t = do + rw <- getTopLevelRW + putTopLevelRW rw { rwCrucibleTimeout = t } + include_value :: FilePath -> TopLevel () include_value file = do oldpath <- io $ getCurrentDirectory @@ -2326,6 +2355,13 @@ primitives = Map.fromList Experimental [ "Legacy alternative name for `llvm_alloc_with_size`." ] + , prim "llvm_alloc_sym_init" "LLVMType -> LLVMSetup SetupValue" + (pureVal llvm_alloc_sym_init) + Experimental + [ "Like `llvm_alloc`, but assume that the allocation is initialized with" + , "symbolic bytes." + ] + , prim "llvm_symbolic_alloc" "Bool -> Int -> Term -> LLVMSetup SetupValue" (pureVal llvm_symbolic_alloc) Current @@ -2616,6 +2652,16 @@ primitives = Map.fromList Current [ "Use the default set of callee-saved registers during x86 verification." ] + , prim "enable_what4_eval" "TopLevel ()" + (pureVal enable_what4_eval) + Experimental + [ "Enable What4 translation for SAWCore expressions during Crucible symbolic execution." ] + + , prim "disable_what4_eval" "TopLevel ()" + (pureVal disable_what4_eval) + Current + [ "Disable What4 translation for SAWCore expressions during Crucible symbolic execution." ] + , prim "set_x86_stack_base_align" "Int -> TopLevel ()" (pureVal set_x86_stack_base_align) Experimental @@ -2626,6 +2672,28 @@ primitives = Map.fromList Experimental [ "Use the default stack allocation base alignment during x86 verification." ] + , prim "enable_alloc_sym_init_check" "TopLevel ()" + (pureVal enable_alloc_sym_init_check) + Experimental + [ "Enable the allocation initialization check associated with alloc_sym_init during override application." ] + + , prim "disable_alloc_sym_init_check" "TopLevel ()" + (pureVal disable_alloc_sym_init_check) + Current + [ "Disable the allocation initialization check associated with alloc_sym_init during override application." + , "Disabling this check allows an override to apply when the memory region specified by the alloc_sym_init command" + , "in the override specification is not written to in the calling context." + , "This makes the implicit assumption that there is some unspecified byte at any valid memory address." + ] + + , prim "set_crucible_timeout" "Int -> TopLevel ()" + (pureVal set_crucible_timeout) + Experimental + [ "Set the timeout for the SMT solver during the LLVM and X86 Crucible symbolic execution," + ,"in milliseconds (0 is no timeout). The default is 10000ms (10s)." + ,"This is used for path-sat checks, and sat checks when applying overrides." + ] + , prim "llvm_array_value" "[SetupValue] -> SetupValue" (pureVal CIR.anySetupArray) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index f53f096456..c3007ad64f 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -446,8 +446,14 @@ data TopLevelRW = , rwWhat4HashConsing :: Bool , rwWhat4HashConsingX86 :: Bool + , rwWhat4Eval :: Bool + , rwPreservedRegs :: [String] , rwStackBaseAlign :: Integer + + , rwAllocSymInitCheck :: Bool + + , rwCrucibleTimeout :: Integer } newtype TopLevel a =