diff --git a/deps/crucible b/deps/crucible index a4c77ca293..ab43acda61 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit a4c77ca2932b012e130378c1f0f72be0af0bb888 +Subproject commit ab43acda610b01c1a9dcecc4edcb3297c7dca0c0 diff --git a/examples/llvm/global.saw b/examples/llvm/global.saw index a7466706c8..b3af382c4c 100644 --- a/examples/llvm/global.saw +++ b/examples/llvm/global.saw @@ -11,11 +11,13 @@ let ptr_to_fresh n ty = do { }; let clear_setup = do { + crucible_alloc_global "g"; crucible_execute_func []; crucible_points_to (crucible_global "g") (crucible_term {{ 0 : [32] }}); }; let set_setup = do { + crucible_alloc_global "g"; x <- crucible_fresh_var "x" (llvm_int 32); crucible_execute_func [crucible_term x]; crucible_points_to (crucible_global "g") (crucible_term x); @@ -26,4 +28,4 @@ let main : TopLevel () = do { crucible_llvm_verify m "clear" [] false clear_setup abc; crucible_llvm_verify m "set" [] false set_setup abc; print "Done."; -}; +}; \ No newline at end of file diff --git a/examples/multi-override/multi-override.saw b/examples/multi-override/multi-override.saw index 7279121fb9..e1fef1dca4 100644 --- a/examples/multi-override/multi-override.saw +++ b/examples/multi-override/multi-override.saw @@ -27,6 +27,7 @@ let sum_spec n : CrucibleSetup() = do { crucible_execute_func[arrp, crucible_term {{ `n:[32]}}]; crucible_return (crucible_term {{ mysum arr }}); + crucible_points_to arrp (crucible_term arr); }; let example_sums : CrucibleSetup() = do { @@ -35,6 +36,7 @@ let example_sums : CrucibleSetup() = do { }; let set_myglobal n : CrucibleSetup() = do { + crucible_alloc_global "myglobal"; old <- crucible_fresh_var "old" (llvm_int 32); crucible_precond {{ old < 1000 }}; crucible_points_to (crucible_global "myglobal") (crucible_term old); @@ -44,8 +46,11 @@ let set_myglobal n : CrucibleSetup() = do { }; let myglobal_example : CrucibleSetup() = do { + crucible_alloc_global "myglobal"; crucible_execute_func[]; crucible_return (crucible_term {{ 120 : [32] }}); + crucible_points_to (crucible_global "myglobal") + (crucible_term {{ 120 : [32] }}); }; let main : TopLevel () = do { diff --git a/examples/salsa20/salsa.saw b/examples/salsa20/salsa.saw index 91272a4f81..a7ab983d42 100644 --- a/examples/salsa20/salsa.saw +++ b/examples/salsa20/salsa.saw @@ -60,8 +60,14 @@ let salsa20_djb_setup = do { }; let salsa20_expansion_32 = do { - (k, pk) <- ptr_to_fresh "k" (llvm_array 32 (llvm_int 8)); - (n, pn) <- ptr_to_fresh "n" (llvm_array 16 (llvm_int 8)); + // (k, pk) <- ptr_to_fresh "k" (llvm_array 32 (llvm_int 8)); + // (n, pn) <- ptr_to_fresh "n" (llvm_array 16 (llvm_int 8)); + k <- crucible_fresh_var "k" (llvm_array 32 (llvm_int 8)); + pk <- crucible_alloc_readonly (llvm_array 32 (llvm_int 8)); + crucible_points_to pk (crucible_term k); + n <- crucible_fresh_var "n" (llvm_array 16 (llvm_int 8)); + pn <- crucible_alloc_readonly (llvm_array 16 (llvm_int 8)); + crucible_points_to pn (crucible_term n); pks <- crucible_alloc (llvm_array 64 (llvm_int 8)); crucible_execute_func [pk, pn, pks]; let rks = {{ Salsa20_expansion`{a=2}(k, n)}}; diff --git a/intTests/test0036_global/test.saw b/intTests/test0036_global/test.saw index c54dc63246..efa07dd73c 100644 --- a/intTests/test0036_global/test.saw +++ b/intTests/test0036_global/test.saw @@ -1,6 +1,7 @@ m <- llvm_load_module "./test.bc"; let init_global name = do { + crucible_alloc_global name; crucible_points_to (crucible_global name) (crucible_global_initializer name); }; diff --git a/intTests/test_boilerplate/test.bc b/intTests/test_boilerplate/test.bc index e042319914..851a7da286 100644 Binary files a/intTests/test_boilerplate/test.bc and b/intTests/test_boilerplate/test.bc differ diff --git a/intTests/test_boilerplate/test.c b/intTests/test_boilerplate/test.c index d65304cf30..cf3b45c649 100644 --- a/intTests/test_boilerplate/test.c +++ b/intTests/test_boilerplate/test.c @@ -4,14 +4,14 @@ #include #include -uint64_t GLOBAL = 0; +const uint64_t GLOBAL = 1; uint64_t test0(uint64_t x, uint64_t y) { return x + y; } -void test1() { - GLOBAL += test0(GLOBAL, GLOBAL); +uint64_t test1() { + return test0(GLOBAL, GLOBAL); } uint64_t test2(uint64_t *buf) { diff --git a/intTests/test_llvm_unsound_alloc/test.sh b/intTests/test_llvm_unsound_alloc/test.sh new file mode 100755 index 0000000000..4fbf80c9cb --- /dev/null +++ b/intTests/test_llvm_unsound_alloc/test.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +if ! $SAW unsound_alloc.saw ; then + exit 0 +else + exit 1 +fi diff --git a/intTests/test_llvm_unsound_alloc/unsound_alloc.bc b/intTests/test_llvm_unsound_alloc/unsound_alloc.bc new file mode 100644 index 0000000000..91ccaf0af5 Binary files /dev/null and b/intTests/test_llvm_unsound_alloc/unsound_alloc.bc differ diff --git a/intTests/test_llvm_unsound_alloc/unsound_alloc.c b/intTests/test_llvm_unsound_alloc/unsound_alloc.c new file mode 100644 index 0000000000..2e62f5aa9b --- /dev/null +++ b/intTests/test_llvm_unsound_alloc/unsound_alloc.c @@ -0,0 +1,12 @@ +#include + +uint32_t foo(uint32_t *x) { + uint32_t tmp = *x + 1; + *x += 42; + return tmp; +}; + +uint32_t bar() { + uint32_t val = 1; + return foo(&val) + val; +}; diff --git a/intTests/test_llvm_unsound_alloc/unsound_alloc.saw b/intTests/test_llvm_unsound_alloc/unsound_alloc.saw new file mode 100644 index 0000000000..80aa9885cc --- /dev/null +++ b/intTests/test_llvm_unsound_alloc/unsound_alloc.saw @@ -0,0 +1,23 @@ +MODULE <- llvm_load_module "unsound_alloc.bc"; + +let foo_setup = do { + x <- crucible_alloc (llvm_int 32); + x_star <- crucible_fresh_var "x" (llvm_int 32); + crucible_points_to x (crucible_term x_star); + crucible_execute_func [x]; + crucible_return (crucible_term {{ x_star + 1 : [32] }}); +}; +foo_spec <- crucible_llvm_verify MODULE "foo" [] false foo_setup z3; + +let bar_setup = do { + crucible_execute_func []; + crucible_return (crucible_term {{ 3 : [32] }}); +}; + +// the below line (without override) correctly fails +// crucible_llvm_verify MODULE "bar" [] false bar_setup z3; + +// works, but shouldn't +crucible_llvm_verify MODULE "bar" [foo_spec] false bar_setup z3; + +print "Should not have succeeded - unsound!"; \ No newline at end of file diff --git a/intTests/test_llvm_unsound_global/test.sh b/intTests/test_llvm_unsound_global/test.sh new file mode 100755 index 0000000000..61a12c89dd --- /dev/null +++ b/intTests/test_llvm_unsound_global/test.sh @@ -0,0 +1,7 @@ +#!/bin/sh + +if ! $SAW unsound_global.saw ; then + exit 0 +else + exit 1 +fi diff --git a/intTests/test_llvm_unsound_global/unsound_global.bc b/intTests/test_llvm_unsound_global/unsound_global.bc new file mode 100644 index 0000000000..9a53b8f662 Binary files /dev/null and b/intTests/test_llvm_unsound_global/unsound_global.bc differ diff --git a/intTests/test_llvm_unsound_global/unsound_global.c b/intTests/test_llvm_unsound_global/unsound_global.c new file mode 100644 index 0000000000..dd4e27fe44 --- /dev/null +++ b/intTests/test_llvm_unsound_global/unsound_global.c @@ -0,0 +1,22 @@ +// unsound_global.c + +#include +#include + +uint32_t TEST; + +uint32_t GLOBAL[2]; + +uint32_t foo(uint32_t x) { + GLOBAL[1] = x; + return x + 1; +}; + +uint32_t bar() { + TEST = 42; + GLOBAL[1] = 0; + uint32_t val = foo(1); + printf("%u\n", TEST); + // GLOBAL[1] = 0; + return val + GLOBAL[1]; +}; diff --git a/intTests/test_llvm_unsound_global/unsound_global.saw b/intTests/test_llvm_unsound_global/unsound_global.saw new file mode 100644 index 0000000000..989a7948ea --- /dev/null +++ b/intTests/test_llvm_unsound_global/unsound_global.saw @@ -0,0 +1,25 @@ +MODULE <- llvm_load_module "unsound_global.bc"; + +let foo_setup = do { + crucible_alloc_global "GLOBAL"; + x <- crucible_fresh_var "x" (llvm_int 32); + crucible_execute_func [crucible_term x]; + crucible_return (crucible_term {{ x + 1 : [32] }}); + // crucible_points_to (crucible_elem (crucible_global "GLOBAL") 1) (crucible_term x); +}; +foo_spec <- crucible_llvm_verify MODULE "foo" [] false foo_setup z3; + +let bar_setup = do { + crucible_alloc_global "GLOBAL"; + crucible_alloc_global "TEST"; + crucible_execute_func []; + crucible_return (crucible_term {{ 2 : [32] }}); +}; + +// the below line (without override) correctly fails +// crucible_llvm_verify MODULE "bar" [] false bar_setup z3; + +// works, but shouldn't +crucible_llvm_verify MODULE "bar" [foo_spec] false bar_setup z3; + +print "Should not have succeeded - unsound!"; \ No newline at end of file diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index daf3555c7e..c17bc91371 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -298,6 +298,9 @@ type family ExtType ext :: Type -- | The type of points-to assertions type family PointsTo ext :: Type +-- | The type of global allocations +type family AllocGlobal ext :: Type + -------------------------------------------------------------------------------- -- *** StateSpec @@ -362,6 +365,7 @@ data CrucibleMethodSpecIR ext = , _csPostState :: StateSpec ext -- ^ state after the function runs , _csArgBindings :: Map Integer (ExtType ext, SetupValue ext) -- ^ function arguments , _csRetValue :: Maybe (SetupValue ext) -- ^ function return value + , _csGlobalAllocs :: [AllocGlobal ext] -- ^ globals allocated , _csSolverStats :: SolverStats -- ^ statistics about the proof that produced this , _csCodebase :: Codebase ext -- ^ the codebase this spec was verified against , _csLoc :: ProgramLoc -- ^ where in the SAWscript was this spec? @@ -410,6 +414,7 @@ makeCrucibleMethodSpecIR meth args ret loc code = do ,_csPostState = initialStateSpec ,_csArgBindings = Map.empty ,_csRetValue = Nothing + ,_csGlobalAllocs = [] ,_csSolverStats = mempty ,_csLoc = loc ,_csCodebase = code diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index aa9296bbae..d940d84523 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -124,7 +124,7 @@ makeLenses ''OverrideState initialState :: Sym {- ^ simulator -} -> Crucible.SymGlobalState Sym {- ^ initial global variables -} -> - Map AllocIndex (Pointer ext) {- ^ initial allocation substituion -} -> + Map AllocIndex (Pointer ext) {- ^ initial allocation substituion -} -> Map VarIndex Term {- ^ initial term substituion -} -> Set VarIndex {- ^ initial free terms -} -> W4.ProgramLoc {- ^ location information for the override -} -> diff --git a/src/SAWScript/Crucible/Common/Setup/Type.hs b/src/SAWScript/Crucible/Common/Setup/Type.hs index de98c23a3a..4cb263915e 100644 --- a/src/SAWScript/Crucible/Common/Setup/Type.hs +++ b/src/SAWScript/Crucible/Common/Setup/Type.hs @@ -26,6 +26,7 @@ module SAWScript.Crucible.Common.Setup.Type , CrucibleSetupT , currentState , addPointsTo + , addAllocGlobal , addCondition , freshVariable ) where @@ -86,6 +87,9 @@ currentState f x = case x^. csPrePost of addPointsTo :: Monad m => MS.PointsTo ext -> CrucibleSetupT ext m () addPointsTo pt = currentState . MS.csPointsTos %= (pt : ) +addAllocGlobal :: Monad m => MS.AllocGlobal ext -> CrucibleSetupT ext m () +addAllocGlobal ag = csMethodSpec . MS.csGlobalAllocs %= (ag : ) + addCondition :: Monad m => MS.SetupCondition ext -> CrucibleSetupT ext m () addCondition cond = currentState . MS.csConditions %= (cond : ) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index d49b771795..004b8115ac 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -46,6 +46,7 @@ module SAWScript.Crucible.LLVM.Builtins , crucible_alloc , crucible_alloc_readonly , crucible_alloc_with_size + , crucible_alloc_global , crucible_fresh_expanded_val -- @@ -488,10 +489,13 @@ verifyPrestate opts cc mspec globals = do (mspec ^. MS.csPreState . MS.csFreshPointers) let env = Map.unions [env1, env2] - mem'' <- setupPrePointsTos mspec opts cc env (mspec ^. MS.csPreState . MS.csPointsTos) mem' - let globals1 = Crucible.insertGlobal lvar mem'' globals - (globals2,cs) <- setupPrestateConditions mspec cc env globals1 (mspec ^. MS.csPreState . MS.csConditions) - args <- resolveArguments cc mspec env + mem'' <- setupGlobalAllocs cc (mspec ^. MS.csGlobalAllocs) mem' + + mem''' <- setupPrePointsTos mspec opts cc env (mspec ^. MS.csPreState . MS.csPointsTos) mem'' + + let globals1 = Crucible.insertGlobal lvar mem''' globals + (globals2,cs) <- setupPrestateConditions mspec cc mem''' env globals1 (mspec ^. MS.csPreState . MS.csConditions) + args <- resolveArguments cc mem''' mspec env return (args, cs, env, globals2) @@ -511,10 +515,11 @@ checkRegisterCompatibility mt mt' = resolveArguments :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => LLVMCrucibleContext arch -> + Crucible.MemImpl Sym -> MS.CrucibleMethodSpecIR (LLVM arch) -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> IO [(Crucible.MemType, LLVMVal)] -resolveArguments cc mspec env = mapM resolveArg [0..(nArgs-1)] +resolveArguments cc mem mspec env = mapM resolveArg [0..(nArgs-1)] where nArgs = toInteger (length (mspec ^. MS.csArgs)) tyenv = MS.csAllocations mspec @@ -537,12 +542,57 @@ resolveArguments cc mspec env = mapM resolveArg [0..(nArgs-1)] Just (mt, sv) -> do mt' <- typeOfSetupValue cc tyenv nameEnv sv checkArgTy i mt mt' - v <- resolveSetupVal cc env tyenv nameEnv sv + v <- resolveSetupVal cc mem env tyenv nameEnv sv return (mt, v) Nothing -> fail $ unwords ["Argument", show i, "unspecified when verifying", show nm] -------------------------------------------------------------------------------- +-- | For each "crucible_global_alloc" in the method specification, allocate and +-- register the appropriate memory. +setupGlobalAllocs :: forall arch. + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + LLVMCrucibleContext arch -> + [MS.AllocGlobal (LLVM arch)] -> + MemImpl -> + IO MemImpl +setupGlobalAllocs cc allocs mem0 = foldM go mem0 allocs + where + sym = cc ^. ccBackend + + go :: MemImpl -> MS.AllocGlobal (LLVM arch) -> IO MemImpl + go mem (LLVMAllocGlobal _ symbol@(L.Symbol name)) = do + let LLVMModule _ _ mtrans = cc ^. ccLLVMModule + gimap = Crucible.globalInitMap mtrans + case Map.lookup symbol gimap of + Just (g, Right (mt, _)) -> do + when (L.gaConstant $ L.globalAttrs g) . fail $ mconcat + [ "Global variable \"" + , name + , "\" is not mutable" + ] + let sz = Crucible.memTypeSize (Crucible.llvmDataLayout ?lc) mt + sz' <- W4.bvLit sym ?ptrWidth $ Crucible.bytesToInteger sz + alignment <- + case L.globalAlign g of + Just a | a > 0 -> + case Crucible.toAlignment $ Crucible.toBytes a of + Nothing -> fail $ mconcat + [ "Global variable \"" + , name + , "\" has invalid alignment: " + , show a + ] + Just al -> return al + _ -> pure $ Crucible.memTypeAlign (Crucible.llvmDataLayout ?lc) mt + (ptr, mem') <- Crucible.doMalloc sym Crucible.GlobalAlloc Crucible.Mutable name mem sz' alignment + pure $ Crucible.registerGlobal mem' [symbol] ptr + _ -> fail $ mconcat + [ "Global variable \"" + , name + , "\" does not exist" + ] + -- | For each points-to constraint in the pre-state section of the -- function spec, write the given value to the address of the given -- pointer. @@ -562,7 +612,7 @@ setupPrePointsTos mspec opts cc env pts mem0 = foldM go mem0 pts go :: MemImpl -> MS.PointsTo (LLVM arch) -> IO MemImpl go mem (LLVMPointsTo _loc ptr val) = - do ptr' <- resolveSetupVal cc env tyenv nameEnv ptr + do ptr' <- resolveSetupVal cc mem env tyenv nameEnv ptr ptr'' <- case ptr' of Crucible.LLVMValInt blk off | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth @@ -577,11 +627,12 @@ setupPrestateConditions :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => MS.CrucibleMethodSpecIR (LLVM arch) -> LLVMCrucibleContext arch -> + Crucible.MemImpl Sym -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> Crucible.SymGlobalState Sym -> [MS.SetupCondition (LLVM arch)] -> IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term Crucible.AssumptionReason]) -setupPrestateConditions mspec cc env = aux [] +setupPrestateConditions mspec cc mem env = aux [] where tyenv = MS.csAllocations mspec nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames @@ -589,8 +640,8 @@ setupPrestateConditions mspec cc env = aux [] aux acc globals [] = return (globals, acc) aux acc globals (MS.SetupCond_Equal loc val1 val2 : xs) = - do val1' <- resolveSetupVal cc env tyenv nameEnv val1 - val2' <- resolveSetupVal cc env tyenv nameEnv val2 + do val1' <- resolveSetupVal cc mem env tyenv nameEnv val1 + val2' <- resolveSetupVal cc mem env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition") aux (lp:acc) globals xs @@ -958,7 +1009,7 @@ setupLLVMCrucibleContext bic opts lm@(LLVMModule _ llvm_mod mtrans) action = do let simctx = Crucible.initSimContext sym intrinsics halloc stdout bindings (Crucible.llvmExtensionImpl Crucible.defaultMemOptions) CrucibleSAW.SAWCruciblePersonality mem <- Crucible.populateConstGlobals sym (Crucible.globalInitMap mtrans) - =<< Crucible.initializeMemory sym ctx llvm_mod + =<< Crucible.initializeMemoryConstGlobals sym ctx llvm_mod let globals = Crucible.llvmGlobals ctx mem @@ -983,7 +1034,6 @@ setupLLVMCrucibleContext bic opts lm@(LLVMModule _ llvm_mod mtrans) action = do return LLVMCrucibleContext{ _ccLLVMModule = lm , _ccBackend = sym - , _ccLLVMEmptyMem = mem , _ccLLVMSimContext = lsimctx , _ccLLVMGlobals = lglobals } @@ -1459,6 +1509,16 @@ crucible_alloc_with_size bic opts sz lty = opts lty +crucible_alloc_global :: + BuiltinContext -> + Options -> + String -> + LLVMCrucibleSetupM () +crucible_alloc_global _bic _opts name = LLVMCrucibleSetupM $ + do cc <- getLLVMCrucibleContext + loc <- getW4Position "crucible_alloc_global" + Setup.addAllocGlobal . LLVMAllocGlobal loc $ L.Symbol name + crucible_fresh_pointer :: BuiltinContext -> Options -> diff --git a/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs b/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs index fec63d0f27..9e3ce048ca 100644 --- a/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs +++ b/src/SAWScript/Crucible/LLVM/CrucibleLLVM.hs @@ -43,6 +43,7 @@ module SAWScript.Crucible.LLVM.CrucibleLLVM , SymType(MemType, Alias, VoidType) , MemType(..) , memTypeSize + , memTypeAlign , fiOffset , fiType , siFields @@ -63,7 +64,7 @@ module SAWScript.Crucible.LLVM.CrucibleLLVM , liftRetType -- * Re-exports from "Lang.Crucible.LLVM.Globals" , GlobalInitializerMap - , initializeMemory + , initializeMemoryConstGlobals , makeGlobalMap , populateConstGlobals -- * Re-exports from "Lang.Crucible.LLVM.Translation" @@ -148,7 +149,7 @@ import Lang.Crucible.LLVM.Intrinsics import Lang.Crucible.LLVM.MemType (SymType(MemType, Alias, VoidType), MemType(..), - Ident, memTypeSize, fiOffset, fiType, + Ident, memTypeSize, memTypeAlign, fiOffset, fiType, siFields, siFieldInfo, siFieldOffset, siFieldTypes, siIsPacked, mkStructInfo, ppMemType) @@ -158,7 +159,7 @@ import Lang.Crucible.LLVM.TypeContext import qualified Lang.Crucible.LLVM.TypeContext as TyCtx import Lang.Crucible.LLVM.Globals - (GlobalInitializerMap, initializeMemory, makeGlobalMap, populateConstGlobals) + (GlobalInitializerMap, initializeMemoryConstGlobals, makeGlobalMap, populateConstGlobals) import Lang.Crucible.LLVM.Translation (llvmMemVar, symbolMap, LLVMHandleInfo(LLVMHandleInfo), diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index da8e9079f9..3d94067db6 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -209,7 +209,6 @@ data LLVMCrucibleContext arch = LLVMCrucibleContext { _ccLLVMModule :: LLVMModule arch , _ccBackend :: Sym - , _ccLLVMEmptyMem :: CL.MemImpl Sym -- ^ A heap where LLVM globals are allocated, but not initialized. , _ccLLVMSimContext :: Crucible.SimContext (Crucible.SAWCruciblePersonality Sym) Sym (CL.LLVM arch) , _ccLLVMGlobals :: Crucible.SymGlobalState Sym } @@ -245,6 +244,21 @@ ppPointsTo (LLVMPointsTo _loc ptr val) = instance PPL.Pretty (LLVMPointsTo arch) where pretty = ppPointsTo +-------------------------------------------------------------------------------- +-- ** AllocGlobal + +type instance MS.AllocGlobal (CL.LLVM arch) = LLVMAllocGlobal arch + +data LLVMAllocGlobal arch = LLVMAllocGlobal ProgramLoc L.Symbol + +ppAllocGlobal :: LLVMAllocGlobal arch -> PPL.Doc +ppAllocGlobal (LLVMAllocGlobal _loc (L.Symbol name)) = + PPL.text "allocate global" + PPL.<+> PPL.text name + +instance PPL.Pretty (LLVMAllocGlobal arch) where + pretty = ppAllocGlobal + -------------------------------------------------------------------------------- -- ** ??? diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index be4723ccfd..6412edf0c0 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -58,6 +58,7 @@ import Data.Maybe (fromMaybe, catMaybes) import Data.Proxy import Data.Set (Set) import qualified Data.Set as Set +import Data.Text (pack) import qualified Data.Vector as V import GHC.Generics (Generic) import qualified Text.PrettyPrint.ANSI.Leijen as PP @@ -76,6 +77,7 @@ import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(UnitRepr)) import qualified Lang.Crucible.CFG.Extension.Safety as Crucible import qualified Lang.Crucible.FunctionHandle as Crucible import qualified Lang.Crucible.LLVM.MemModel as Crucible +import qualified Lang.Crucible.LLVM.Translation as Crucible import qualified Lang.Crucible.Simulator.GlobalState as Crucible import qualified Lang.Crucible.Simulator.OverrideSim as Crucible import qualified Lang.Crucible.Simulator.RegMap as Crucible @@ -663,11 +665,12 @@ executeCond opts sc cc cs ss = do (ss ^. MS.csFreshPointers) OM (setupValueSub %= Map.union ptrs) + invalidateMutableAllocs cc cs + traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) traverse_ (executePointsTo opts sc cc cs) (ss ^. MS.csPointsTos) traverse_ (executeSetupCondition opts sc cc cs) (ss ^. MS.csConditions) - -- | Allocate fresh variables for all of the "fresh" vars -- used in this phase and add them to the term substitution. refreshTerms :: @@ -881,7 +884,11 @@ matchArg :: SetupValue (Crucible.LLVM arch) {- ^ expected specification value -} -> OverrideMatcher (LLVM arch) md () -matchArg opts sc cc cs prepost actual expectedTy expected = +matchArg opts sc cc cs prepost actual expectedTy expected = do + let mvar = Crucible.llvmMemVar $ cc ^. ccLLVMContext + mem <- case Crucible.lookupGlobal mvar $ cc ^. ccLLVMGlobals of + Nothing -> fail "internal error: LLVM Memory global not found" + Just mem -> pure mem case (actual, expectedTy, expected) of (_, _, SetupTerm expectedTT) | Cryptol.Forall [] [] tyexpr <- ttSchema expectedTT @@ -915,8 +922,7 @@ matchArg opts sc cc cs prepost actual expectedTy expected = notEqual prepost opts (cs ^. MS.csLoc) cc sc cs expected actual SetupGlobal () name | Just Refl <- testEquality (W4.bvWidth off) Crucible.PtrWidth -> - do let mem = cc^.ccLLVMEmptyMem - sym <- Ov.getSymInterface + do sym <- Ov.getSymInterface ptr2 <- liftIO $ Crucible.doResolveGlobal sym mem (L.Symbol name) pred_ <- liftIO $ Crucible.ptrEq sym Crucible.PtrWidth (Crucible.LLVMPointer blk off) ptr2 @@ -1217,6 +1223,61 @@ learnPred sc cc loc prepost t = ------------------------------------------------------------------------ +-- | Invalidate all mutable memory that was allocated in the method spec +-- precondition, either through explicit calls to "crucible_alloc" or to +-- "crucible_alloc_global". +invalidateMutableAllocs :: + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + LLVMCrucibleContext arch -> + MS.CrucibleMethodSpecIR (LLVM arch) -> + OverrideMatcher (LLVM arch) RW () +invalidateMutableAllocs cc cs = do + sym <- use syminterface + mem <- readGlobal . Crucible.llvmMemVar $ cc ^. ccLLVMContext + sub <- use setupValueSub + + let mutableAllocs = Map.filter (view isMut) $ cs ^. MS.csPreState . MS.csAllocs + allocPtrs = + (\(ptr, spec) -> + ( ptr + , _allocSpecBytes spec + , mconcat + [ "state of memory allocated in precondition (at " + , pack . show . W4.plSourceLoc $ spec ^. allocSpecLoc + , ") not described in postcondition" + ] + ) + ) <$> Map.elems (Map.intersectionWith (,) sub mutableAllocs) + LLVMModule _ _ mtrans = cc ^. ccLLVMModule + gimap = Crucible.globalInitMap mtrans + mutableGlobals = cs ^. MS.csGlobalAllocs + + globalPtrs <- liftIO . fmap catMaybes . forM mutableGlobals $ \(LLVMAllocGlobal loc s@(L.Symbol st)) -> + case Map.lookup s gimap of + Just (_, Right (mt, _)) -> do + ptr <- Crucible.doResolveGlobal sym mem s + pure $ Just + ( ptr + , Crucible.memTypeSize (Crucible.llvmDataLayout ?lc) mt + , mconcat + [ "state of mutable global variable \"" + , pack st + , "\" (allocated at " + , pack . show $ W4.plSourceLoc loc + , ") not described in postcondition" + ] + ) + _ -> pure Nothing + + mem' <- foldM (\m (ptr, sz, msg) -> + liftIO $ Crucible.doInvalidate sym ?ptrWidth m ptr msg + =<< W4.bvLit sym ?ptrWidth (Crucible.bytesToInteger sz) + ) mem $ allocPtrs ++ globalPtrs + + writeGlobal (Crucible.llvmMemVar $ cc ^. ccLLVMContext) mem' + +------------------------------------------------------------------------ + -- | Perform an allocation as indicated by a 'crucible_alloc' -- statement from the postcondition section. executeAllocation :: @@ -1343,7 +1404,7 @@ storePointsToValue opts cc env tyenv nameEnv mem ptr val = do Crucible.doArrayConstStore sym mem ptr alignment arr sz _ -> do val' <- X.handle (handleException opts) $ - resolveSetupVal cc env tyenv nameEnv val + resolveSetupVal cc mem env tyenv nameEnv val Crucible.storeConstRaw sym mem ptr storTy alignment val' @@ -1432,11 +1493,12 @@ resolveSetupValueLLVM :: resolveSetupValueLLVM opts cc sc spec sval = do m <- OM (use setupValueSub) s <- OM (use termSub) + mem <- readGlobal (Crucible.llvmMemVar (cc^.ccLLVMContext)) let tyenv = MS.csAllocations spec nameEnv = MS.csTypeNames spec memTy <- liftIO $ typeOfSetupValue cc tyenv nameEnv sval sval' <- liftIO $ instantiateSetupValue sc s sval - lval <- liftIO $ resolveSetupVal cc m tyenv nameEnv sval' `X.catch` handleException opts + lval <- liftIO $ resolveSetupVal cc mem m tyenv nameEnv sval' `X.catch` handleException opts return (memTy, lval) resolveSetupValue :: diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 5eccb6c2c1..1f1b15119c 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -259,19 +259,20 @@ typeOfSetupValue' cc env nameEnv val = resolveSetupVal :: forall arch. Crucible.HasPtrWidth (Crucible.ArchWidth arch) => LLVMCrucibleContext arch -> + Crucible.MemImpl Sym -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> Map AllocIndex LLVMAllocSpec -> Map AllocIndex Crucible.Ident -> - SetupValue (Crucible.LLVM arch) -> + SetupValue (Crucible.LLVM arch) -> IO LLVMVal -resolveSetupVal cc env tyenv nameEnv val = +resolveSetupVal cc mem env tyenv nameEnv val = do case val of SetupVar i | Just ptr <- Map.lookup i env -> return (Crucible.ptrToPtrVal ptr) | otherwise -> fail ("resolveSetupVal: Unresolved prestate variable:" ++ show i) SetupTerm tm -> resolveTypedTerm cc tm SetupStruct () packed vs -> do - vals <- mapM (resolveSetupVal cc env tyenv nameEnv) vs + vals <- mapM (resolveSetupVal cc mem env tyenv nameEnv) vs let tps = map (typeOfLLVMVal dl) vals let t = Crucible.mkStructType (V.fromList (mkFields packed dl Crucible.noAlignment 0 tps)) let flds = case Crucible.storageTypeF t of @@ -280,12 +281,12 @@ resolveSetupVal cc env tyenv nameEnv val = return $ Crucible.LLVMValStruct (V.zip flds (V.fromList vals)) SetupArray () [] -> fail "resolveSetupVal: invalid empty array" SetupArray () vs -> do - vals <- V.mapM (resolveSetupVal cc env tyenv nameEnv) (V.fromList vs) + vals <- V.mapM (resolveSetupVal cc mem env tyenv nameEnv) (V.fromList vs) let tp = typeOfLLVMVal dl (V.head vals) return $ Crucible.LLVMValArray tp vals SetupField () v n -> do i <- resolveSetupFieldIndexOrFail cc tyenv nameEnv v n - resolveSetupVal cc env tyenv nameEnv (SetupElem () v i) + resolveSetupVal cc mem env tyenv nameEnv (SetupElem () v i) SetupElem () v i -> do memTy <- typeOfSetupValue cc tyenv nameEnv v let msg = "resolveSetupVal: crucible_elem requires pointer to struct or array, found " ++ show memTy @@ -303,7 +304,7 @@ resolveSetupVal cc env tyenv nameEnv val = _ -> fail msg Left err -> fail $ unlines [msg, "Details:", err] _ -> fail msg - ptr <- resolveSetupVal cc env tyenv nameEnv v + ptr <- resolveSetupVal cc mem env tyenv nameEnv v case ptr of Crucible.LLVMValInt blk off -> do delta' <- W4.bvLit sym (W4.bvWidth off) (Crucible.bytesToInteger delta) @@ -313,8 +314,7 @@ resolveSetupVal cc env tyenv nameEnv val = SetupNull () -> Crucible.ptrToPtrVal <$> Crucible.mkNullPointer sym Crucible.PtrWidth SetupGlobal () name -> - do let mem = cc^.ccLLVMEmptyMem - Crucible.ptrToPtrVal <$> Crucible.doResolveGlobal sym mem (L.Symbol name) + Crucible.ptrToPtrVal <$> Crucible.doResolveGlobal sym mem (L.Symbol name) SetupGlobalInitializer () name -> case Map.lookup (L.Symbol name) (Crucible.globalInitMap $ cc^.ccLLVMModuleTrans) of @@ -322,7 +322,7 @@ resolveSetupVal cc env tyenv nameEnv val = Just (_, Left e) -> fail e Just (_, Right (_, Just v)) -> let ?lc = lc - in Crucible.constToLLVMVal @(Crucible.ArchWidth arch) sym (cc^.ccLLVMEmptyMem) v + in Crucible.constToLLVMVal @(Crucible.ArchWidth arch) sym mem v Just (_, Right (_, Nothing)) -> fail $ "resolveSetupVal: global has no initializer: " ++ name Nothing -> diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 33f132d8ce..6983145754 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1803,6 +1803,11 @@ primitives = Map.fromList , "The specified size must be greater than the size of the LLVM type." ] + , prim "crucible_alloc_global" "String -> CrucibleSetup ()" + (bicVal crucible_alloc_global) + Current + [] + , prim "crucible_fresh_pointer" "LLVMType -> CrucibleSetup SetupValue" (bicVal crucible_fresh_pointer) Current