diff --git a/deps/crucible b/deps/crucible index 727b375dcf..11c879ea32 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 727b375dcf35be61d384fa6a21d29ecc18f7df1a +Subproject commit 11c879ea32bff1afcc93be2afe02beb9318f46c6 diff --git a/doc/manual/manual.md b/doc/manual/manual.md index ff3c881128..b1547b06f1 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -2586,13 +2586,6 @@ The NULL pointer is called `crucible_null`: crucible_null : SetupValue ~~~~ -Pointers to global variables or functions can be accessed with -`crucible_global`: - -~~~~ -crucible_global : String -> SetupValue -~~~~ - ## Specifying Heap Values Pointers returned by `crucible_alloc` don't, initially, point to @@ -2651,6 +2644,89 @@ crucible_array : [SetupValue] -> SetupValue crucible_struct : [SetupValue] -> SetupValue ~~~~ +## Global variables + +Pointers to global variables or functions can be accessed with +`crucible_global`: + +~~~~ +crucible_global : String -> SetupValue +~~~~ + +Like the pointers returned by `crucible_alloc`, however, these +aren't initialized at the beginning of symbolic simulation. This is intentional +-- setting global variables may be unsound in the presence of +[compositional verification](#compositional-verification). + +To understand the issues surrounding global variables, consider the following C +code: + + +~~~ +int x = 0; + +int f(int y) { + x = x + 1; + return x + y; +} + +int g(int z) { + x = x + 2; + return x + z; +} +~~~ + +One might initially write the following specifications for `f` and `g`: + + +~~~ +m <- llvm_load_module "./test.bc"; + +f_spec <- crucible_llvm_verify m "f" [] true (do { + y <- crucible_fresh_var "y" (llvm_int 32); + crucible_execute_func [crucible_term y]; + crucible_return (crucible_term {{ 1 + y : [32] }}); +}) abc; + +g_spec <- crucible_llvm_verify m "g" [] true (do { + z <- crucible_fresh_var "z" (llvm_int 32); + crucible_execute_func [crucible_term z]; + crucible_return (crucible_term {{ 2 + z : [32] }}); +}) abc; +~~~ + +If globals were always initialized at the beginning of verification, both +of these specs would be provable. However, the results wouldn't truly +be compositional. For instance, it's not the case that +`f(g(z)) == z + 3` for all `z`, because both `f` and `g` modify the global +variable `x` in a way that crosses function boundaries. + +Instead, the specifications for `f` and `g` must make this reliance on the +value of `x` explicit, e.g. one could write + + +~~~ +m <- llvm_load_module "./test.bc"; + + +let init_global name = do { + crucible_points_to (crucible_global name) + (crucible_global_initializer name); +}; + +f_spec <- crucible_llvm_verify m "f" [] true (do { + y <- crucible_fresh_var "y" (llvm_int 32); + init_global "x"; + crucible_execute_func [crucible_term y]; + crucible_return (crucible_term {{ 1 + y : [32] }}); +}) abc; +~~~ + +which initializes `x` to whatever it is initialized to in the C code +at the beginning of verification. This specification is now safe for +compositional verification: SAW won't rewrite a term with `f_spec` +unless it can determine that `x` still has its initial value. + ## Preconditions and Postconditions Sometimes a function is only well-defined under certain conditions, or diff --git a/intTests/runtests.sh b/intTests/runtests.sh index 1051858c37..4e2c3913f4 100755 --- a/intTests/runtests.sh +++ b/intTests/runtests.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ################################################################ # Setup environment. diff --git a/intTests/test0036_global/README b/intTests/test0036_global/README new file mode 100644 index 0000000000..9cd99d3fc5 --- /dev/null +++ b/intTests/test0036_global/README @@ -0,0 +1 @@ +These tests exercise SAW's handling of LLVM globals. \ No newline at end of file diff --git a/intTests/test0036_global/test-fail.saw b/intTests/test0036_global/test-fail.saw new file mode 100644 index 0000000000..ac8d669453 --- /dev/null +++ b/intTests/test0036_global/test-fail.saw @@ -0,0 +1,15 @@ +m <- llvm_load_module "./test.bc"; + +crucible_llvm_verify m "f" [] true (do { + y <- crucible_fresh_var "y" (llvm_int 32); + // We don't initialize x + crucible_execute_func [crucible_term y]; + crucible_return (crucible_term {{ 1 + y : [32] }}); +}) abc; + +crucible_llvm_verify m "g" [] true (do { + z <- crucible_fresh_var "z" (llvm_int 32); + // We don't initialize x + crucible_execute_func [crucible_term z]; + crucible_return (crucible_term {{ 2 + z : [32] }}); +}) abc; \ No newline at end of file diff --git a/intTests/test0036_global/test.bc b/intTests/test0036_global/test.bc new file mode 100644 index 0000000000..fd3749082d Binary files /dev/null and b/intTests/test0036_global/test.bc differ diff --git a/intTests/test0036_global/test.c b/intTests/test0036_global/test.c new file mode 100644 index 0000000000..5980bc5220 --- /dev/null +++ b/intTests/test0036_global/test.c @@ -0,0 +1,15 @@ +int x = 0; + +int f(int y) { + x = x + 1; + return x + y; +} + +int g(int z) { + x = x + 2; + return x + z; +} + +int h(int w) { + return g(f(w)); +} diff --git a/intTests/test0036_global/test.saw b/intTests/test0036_global/test.saw new file mode 100644 index 0000000000..c54dc63246 --- /dev/null +++ b/intTests/test0036_global/test.saw @@ -0,0 +1,29 @@ +m <- llvm_load_module "./test.bc"; + +let init_global name = do { + crucible_points_to (crucible_global name) + (crucible_global_initializer name); +}; + +f_spec <- crucible_llvm_verify m "f" [] true (do { + y <- crucible_fresh_var "y" (llvm_int 32); + init_global "x"; + crucible_execute_func [crucible_term y]; + crucible_return (crucible_term {{ 1 + y : [32] }}); +}) abc; + +g_spec <- crucible_llvm_verify m "g" [] true (do { + z <- crucible_fresh_var "z" (llvm_int 32); + init_global "x"; + crucible_execute_func [crucible_term z]; + crucible_return (crucible_term {{ 2 + z : [32] }}); +}) abc; + +// Note that the f and g overrides are not actually used for +// rewriting, because their preconditions aren't met. +crucible_llvm_verify m "h" [f_spec, g_spec] true (do { + w <- crucible_fresh_var "w" (llvm_int 32); + init_global "x"; + crucible_execute_func [crucible_term w]; + crucible_return (crucible_term {{ 4 + w : [32] }}); +}) abc; \ No newline at end of file diff --git a/intTests/test0036_global/test.sh b/intTests/test0036_global/test.sh new file mode 100755 index 0000000000..df8c1c61a7 --- /dev/null +++ b/intTests/test0036_global/test.sh @@ -0,0 +1,6 @@ +set -e + +$SAW test.saw + +# These tests should fail +! $SAW test-fail.saw diff --git a/saw-script.cabal b/saw-script.cabal index 33772f8707..9a109d776b 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -33,7 +33,7 @@ library , cryptol-verifier , crucible >= 0.4 && < 0.5 , crucible-jvm - , crucible-llvm + , crucible-llvm >= 0.2 , crucible-saw , deepseq , either diff --git a/src/SAWScript/CrucibleBuiltins.hs b/src/SAWScript/CrucibleBuiltins.hs index 897fffb3f0..cb4e174774 100644 --- a/src/SAWScript/CrucibleBuiltins.hs +++ b/src/SAWScript/CrucibleBuiltins.hs @@ -99,7 +99,7 @@ import What4.Utils.MonadST import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.Backend.SAWCore as Crucible import qualified Lang.Crucible.CFG.Core as Crucible - (AnyCFG(..), SomeCFG(..), CFG, TypeRepr(..), cfgHandle, + (AnyCFG(..), CFG, TypeRepr(..), cfgHandle, asBaseType, AsBaseType(..), freshGlobalVar) import qualified Lang.Crucible.CFG.Extension as Crucible (IsSyntaxExtension) @@ -345,7 +345,7 @@ checkRegisterCompatibility mt mt' = return (st == st') resolveArguments :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => CrucibleContext arch -> CrucibleMethodSpecIR -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> @@ -383,7 +383,7 @@ resolveArguments cc mspec env = mapM resolveArg [0..(nArgs-1)] -- function spec, write the given value to the address of the given -- pointer. setupPrePointsTos :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => CrucibleMethodSpecIR -> CrucibleContext arch -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> @@ -415,7 +415,7 @@ setupPrePointsTos mspec cc env pts mem0 = foldM go mem0 pts -- | Sets up globals (ghost variable), and collects boolean terms -- that shuld be assumed to be true. setupPrestateConditions :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => CrucibleMethodSpecIR -> CrucibleContext arch -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> @@ -459,7 +459,7 @@ assertEqualVals cc v1 v2 = -- | Allocate space on the LLVM heap to store a value of the given -- type. Returns the pointer to the allocated memory. doAlloc :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => CrucibleContext arch -> (W4.ProgramLoc, Crucible.MemType) -> StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch)) @@ -472,7 +472,7 @@ doAlloc cc (_loc,tp) = StateT $ \mem -> -- | Allocate read-only space on the LLVM heap to store a value of the -- given type. Returns the pointer to the allocated memory. doAllocConst :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => CrucibleContext arch -> (W4.ProgramLoc, Crucible.MemType) -> StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch)) @@ -498,7 +498,7 @@ ppGlobalPair cc gp = -------------------------------------------------------------------------------- registerOverride :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch) => Options -> CrucibleContext arch -> Crucible.SimContext (Crucible.SAWCruciblePersonality Sym) Sym (Crucible.LLVM arch) -> @@ -528,7 +528,7 @@ registerOverride opts cc _ctx cs = do -------------------------------------------------------------------------------- verifySimulate :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch) => Options -> CrucibleContext arch -> CrucibleMethodSpecIR -> @@ -608,7 +608,7 @@ scAndList sc (x : xs) = foldM (scAnd sc) x xs -------------------------------------------------------------------------------- verifyPoststate :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth wptr, wptr ~ Crucible.ArchWidth arch) => Options {- ^ saw script debug and print options -} -> SharedContext {- ^ saw core context -} -> CrucibleContext arch {- ^ crucible context -} -> @@ -662,7 +662,7 @@ verifyPoststate opts sc cc mspec env0 globals ret = setupCrucibleContext :: BuiltinContext -> Options -> LLVMModule -> - (forall arch. (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => CrucibleContext arch -> TopLevel a) -> + (forall arch. (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => CrucibleContext arch -> TopLevel a) -> TopLevel a setupCrucibleContext bic opts (LLVMModule _ llvm_mod (Some mtrans)) action = do halloc <- getHandleAlloc @@ -690,11 +690,6 @@ setupCrucibleContext bic opts (LLVMModule _ llvm_mod (Some mtrans)) action = do -- register the callable override functions _llvmctx' <- execStateT Crucible.register_llvm_overrides ctx - -- initialize LLVM global variables - _ <- case Crucible.initMemoryCFG mtrans of - Crucible.SomeCFG initCFG -> - Crucible.callCFG initCFG Crucible.emptyRegMap - -- register all the functions defined in the LLVM module mapM_ Crucible.registerModuleFn $ Map.toList $ Crucible.cfgMap mtrans @@ -991,14 +986,17 @@ crucible_fresh_expanded_val bic _opts lty = CrucibleSetupM $ memTypeForLLVMType :: BuiltinContext -> L.Type -> CrucibleSetup arch Crucible.MemType memTypeForLLVMType _bic lty = do case Crucible.liftMemType lty of - Just m -> return m - Nothing -> fail ("unsupported type: " ++ show (L.ppType lty)) + Right m -> return m + Left err -> fail $ unlines [ "unsupported type: " ++ show (L.ppType lty) + , "Details:" + , err + ] -- | See 'crucible_fresh_expanded_val' -- -- This is the recursively-called worker function. constructExpandedSetupValue :: - (?lc::Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc::Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => SharedContext {- ^ shared context -} -> W4.ProgramLoc -> Crucible.MemType {- ^ LLVM mem type -} -> @@ -1015,8 +1013,11 @@ constructExpandedSetupValue sc loc t = Crucible.PtrType symTy -> case Crucible.asMemType symTy of - Just memTy -> constructFreshPointer (symTypeAlias symTy) loc memTy - Nothing -> fail ("lhs not a valid pointer type: " ++ show symTy) + Right memTy -> constructFreshPointer (symTypeAlias symTy) loc memTy + Left err -> fail $ unlines [ "lhs not a valid pointer type: " ++ show symTy + , "Details:" + , err + ] Crucible.ArrayType n memTy -> SetupArray <$> replicateM n (constructExpandedSetupValue sc loc memTy) @@ -1043,8 +1044,11 @@ crucible_alloc _bic _opt lty = CrucibleSetupM $ do let ?dl = Crucible.llvmDataLayout ?lc loc <- toW4Loc "crucible_alloc" <$> lift getPosition memTy <- case Crucible.liftMemType lty of - Just s -> return s - Nothing -> fail ("unsupported type in crucible_alloc: " ++ show (L.ppType lty)) + Right s -> return s + Left err -> fail $ unlines [ "unsupported type in crucible_alloc: " ++ show (L.ppType lty) + , "Details:" + , err + ] n <- csVarCounter <<%= nextAllocIndex currentState.csAllocs.at n ?= (loc,memTy) -- TODO: refactor @@ -1062,8 +1066,11 @@ crucible_alloc_readonly _bic _opt lty = CrucibleSetupM $ do let ?dl = Crucible.llvmDataLayout ?lc loc <- toW4Loc "crucible_alloc_readonly" <$> lift getPosition memTy <- case Crucible.liftMemType lty of - Just s -> return s - Nothing -> fail ("unsupported type in crucible_alloc: " ++ show (L.ppType lty)) + Right s -> return s + Left err -> fail $ unlines [ "unsupported type in crucible_alloc: " ++ show (L.ppType lty) + , "Details:" + , err + ] n <- csVarCounter <<%= nextAllocIndex currentState.csConstAllocs.at n ?= (loc,memTy) case llvmTypeAlias lty of @@ -1114,8 +1121,12 @@ crucible_points_to typed _bic _opt ptr val = CrucibleSetupM $ lhsTy <- case ptrTy of Crucible.PtrType symTy -> case Crucible.asMemType symTy of - Just lhsTy -> return lhsTy - Nothing -> fail $ "lhs not a valid pointer type: " ++ show ptrTy + Right lhsTy -> return lhsTy + Left err -> fail $ unlines [ "lhs not a valid pointer type: " ++ show ptrTy + , "Details:" + , err + ] + _ -> fail $ "lhs not a pointer type: " ++ show ptrTy valTy <- typeOfSetupValue cc env nameEnv val when typed (checkMemTypeCompatibility lhsTy valTy) diff --git a/src/SAWScript/CrucibleLLVM.hs b/src/SAWScript/CrucibleLLVM.hs index f348d75433..743f4ac0f1 100644 --- a/src/SAWScript/CrucibleLLVM.hs +++ b/src/SAWScript/CrucibleLLVM.hs @@ -52,13 +52,18 @@ module SAWScript.CrucibleLLVM , mkStructInfo , Ident -- re-exported from llvm-pretty package -- * Re-exports from "Lang.Crucible.LLVM.LLVMContext" - , LLVMTyCtx + , TyCtx.TypeContext , llvmMetadataMap , llvmDataLayout , asMemType , liftType , liftMemType , liftRetType + -- * Re-exports from "Lang.Crucible.LLVM.Globals" + , GlobalInitializerMap + , initializeMemory + , makeGlobalMap + , populateConstGlobals -- * Re-exports from "Lang.Crucible.LLVM.Translation" , ModuleTranslation , llvmMemVar @@ -68,8 +73,6 @@ module SAWScript.CrucibleLLVM , cfgMap , transContext , llvmPtrWidth - , initializeMemory - , initMemoryCFG , LLVMContext , translateModule -- * Re-exports from "Lang.Crucible.LLVM.MemModel" @@ -144,14 +147,17 @@ import Lang.Crucible.LLVM.MemType siFields, siFieldInfo, siFieldOffset, siFieldTypes, siIsPacked, mkStructInfo) -import Lang.Crucible.LLVM.LLVMContext +import Lang.Crucible.LLVM.TypeContext (llvmMetadataMap, llvmDataLayout, asMemType, liftType, liftMemType, liftRetType) -import qualified Lang.Crucible.LLVM.LLVMContext as TyCtx +import qualified Lang.Crucible.LLVM.TypeContext as TyCtx + +import Lang.Crucible.LLVM.Globals + (GlobalInitializerMap, initializeMemory, makeGlobalMap, populateConstGlobals) import Lang.Crucible.LLVM.Translation - (llvmMemVar, toStorableType, symbolMap, LLVMHandleInfo(LLVMHandleInfo), - cfgMap, transContext, llvmPtrWidth, initializeMemory, initMemoryCFG, + (llvmMemVar, symbolMap, LLVMHandleInfo(LLVMHandleInfo), + cfgMap, transContext, llvmPtrWidth, ModuleTranslation, LLVMContext, translateModule) import Lang.Crucible.LLVM.MemModel @@ -164,10 +170,7 @@ import Lang.Crucible.LLVM.MemModel pattern PtrWidth, llvmPointer_bv, withPtrWidth, pattern LLVMPointer, pattern PtrRepr, llvmPointerView, projectLLVM_bv, typeF, Type, TypeF(Struct, Float, Double, Array, Bitvector), - typeSize, fieldVal, bitvectorType, fieldPad, arrayType, mkStructType, - AllocType(HeapAlloc, GlobalAlloc), Mutability(..)) + typeSize, toStorableType, fieldVal, bitvectorType, fieldPad, arrayType, + mkStructType, AllocType(HeapAlloc, GlobalAlloc), Mutability(..)) import Lang.Crucible.Syntax (mkStruct) - --- | Renamed copy of 'TyCtx.LLVMContext' from module "Lang.Crucible.LLVM.LLVMContext". -type LLVMTyCtx = TyCtx.LLVMContext diff --git a/src/SAWScript/CrucibleMethodSpecIR.hs b/src/SAWScript/CrucibleMethodSpecIR.hs index fbe559124e..ecf701cbcd 100644 --- a/src/SAWScript/CrucibleMethodSpecIR.hs +++ b/src/SAWScript/CrucibleMethodSpecIR.hs @@ -70,15 +70,21 @@ newtype AllocIndex = AllocIndex Int nextAllocIndex :: AllocIndex -> AllocIndex nextAllocIndex (AllocIndex n) = AllocIndex (n + 1) +-- | From the manual: "The SetupValue type corresponds to values that can occur +-- during symbolic execution, which includes both Term values, pointers, and +-- composite types consisting of either of these (both structures and arrays)." data SetupValue where - SetupVar :: AllocIndex -> SetupValue - SetupTerm :: TypedTerm -> SetupValue - SetupStruct :: [SetupValue] -> SetupValue - SetupArray :: [SetupValue] -> SetupValue - SetupElem :: SetupValue -> Int -> SetupValue - SetupField :: SetupValue -> String -> SetupValue - SetupNull :: SetupValue - SetupGlobal :: String -> SetupValue + SetupVar :: AllocIndex -> SetupValue + SetupTerm :: TypedTerm -> SetupValue + SetupStruct :: [SetupValue] -> SetupValue + SetupArray :: [SetupValue] -> SetupValue + SetupElem :: SetupValue -> Int -> SetupValue + SetupField :: SetupValue -> String -> SetupValue + SetupNull :: SetupValue + -- | A pointer to a global variable + SetupGlobal :: String -> SetupValue + -- | This represents the value of a global's initializer. + SetupGlobalInitializer :: String -> SetupValue deriving (Show) setupToTypedTerm :: Options -> SharedContext -> SetupValue -> MaybeT IO TypedTerm @@ -262,7 +268,7 @@ makeLenses ''ResolvedState ccLLVMContext :: Simple Lens (CrucibleContext wptr) (CL.LLVMContext wptr) ccLLVMContext = ccLLVMModuleTrans . CL.transContext -ccTypeCtx :: Simple Lens (CrucibleContext wptr) CL.LLVMTyCtx +ccTypeCtx :: Simple Lens (CrucibleContext wptr) CL.TypeContext ccTypeCtx = ccLLVMContext . CL.llvmTypeCtx -------------------------------------------------------------------------------- @@ -331,22 +337,24 @@ ppSetupError (InvalidArgTypes ts) = text "to Crucible types." resolveArgs :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => [L.Type] -> Either SetupError [CL.MemType] resolveArgs args = do -- TODO: make sure we resolve aliases let mtys = traverse CL.liftMemType args - maybe (Left (InvalidArgTypes args)) Right mtys + -- TODO: should the error message be propagated? + either (\_ -> Left (InvalidArgTypes args)) Right mtys resolveRetTy :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => L.Type -> Either SetupError (Maybe CL.MemType) resolveRetTy ty = do -- TODO: make sure we resolve aliases let ret = CL.liftRetType ty - maybe (Left (InvalidReturnType ty)) Right ret + -- TODO: should the error message be propagated? + either (\_ -> Left (InvalidReturnType ty)) Right ret initialStateSpec :: StateSpec initialStateSpec = StateSpec @@ -360,7 +368,7 @@ initialStateSpec = StateSpec } initialDefCrucibleMethodSpecIR :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => L.Define -> ProgramLoc -> Either SetupError CrucibleMethodSpecIR @@ -381,7 +389,7 @@ initialDefCrucibleMethodSpecIR def loc = do } initialDeclCrucibleMethodSpecIR :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => L.Declare -> ProgramLoc -> Either SetupError CrucibleMethodSpecIR @@ -402,7 +410,7 @@ initialDeclCrucibleMethodSpecIR dec loc = do } initialCrucibleSetupState :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => CrucibleContext wptr -> L.Define -> ProgramLoc -> @@ -418,7 +426,7 @@ initialCrucibleSetupState cc def loc = do } initialCrucibleSetupStateDecl :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => CrucibleContext wptr -> L.Declare -> ProgramLoc -> diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index fa842fb00f..36b92ce458 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -237,7 +237,7 @@ failure loc e = OM (lift (throwE (OF loc e))) -- all the merging is computed. methodSpecHandler :: forall arch rtp args ret. - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> CrucibleContext arch {- ^ context for interacting with Crucible -} -> @@ -279,7 +279,7 @@ methodSpecHandler opts sc cc css retTy = do Left _err -> do Crucible.overrideReturn' (Crucible.RegEntry (Crucible.MaybeRepr retTy) W4.Unassigned) Right (retVal, st) -> - do let loc = st^.osLocation + do let loc = st^.osLocation liftIO $ writeIORef preCondRef (Just (st^.osAsserts)) forM_ (st^.osAssumes) $ \asum -> let rsn = Crucible.AssumptionReason loc "override postcondition" in @@ -336,7 +336,7 @@ methodSpecHandler opts sc cc css retTy = do -- Now project the mabye value we defined above. This has the effect of asserting that -- _some_ override was chosen. let fsym = (head css)^.csName - Crucible.readPartExpr sym (Crucible.regValue ret) + Crucible.readPartExpr sym (Crucible.regValue ret) (Crucible.AssertFailureSimError ("No applicable override for " ++ fsym)) @@ -360,7 +360,7 @@ disjunction sym = foldM (W4.orPred sym) (W4.falsePred sym) -- and execute the post condition. methodSpecHandler1 :: forall arch ret ctx. - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> CrucibleContext arch {- ^ context for interacting with Crucible -} -> @@ -391,7 +391,7 @@ methodSpecHandler1 opts sc cc args retTy cs = computeReturnValue opts cc sc cs retTy (cs^.csRetValue) -- learn pre/post condition -learnCond :: (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) +learnCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> CrucibleContext arch @@ -434,7 +434,7 @@ termId t = -- execute a pre/post condition -executeCond :: (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) +executeCond :: (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> CrucibleContext arch @@ -476,7 +476,7 @@ refreshTerms sc ss = -- an override's precondition are disjoint. Read-only allocations are -- allowed to alias other read-only allocations, however. enforceDisjointness :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => CrucibleContext arch -> W4.ProgramLoc -> StateSpec -> OverrideMatcher arch () enforceDisjointness cc loc ss = do sym <- getSymInterface @@ -515,7 +515,7 @@ enforceDisjointness cc loc ss = -- statement cannot be executed until bindings for any/all lhs -- variables exist. matchPointsTos :: forall arch. - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ saw script print out opts -} -> SharedContext {- ^ term construction context -} -> CrucibleContext arch {- ^ simulator context -} -> @@ -562,20 +562,21 @@ matchPointsTos opts sc cc spec prepost = go False [] setupVars :: SetupValue -> Set AllocIndex setupVars v = case v of - SetupVar i -> Set.singleton i - SetupStruct xs -> foldMap setupVars xs - SetupArray xs -> foldMap setupVars xs - SetupElem x _ -> setupVars x - SetupField x _ -> setupVars x - SetupTerm _ -> Set.empty - SetupNull -> Set.empty - SetupGlobal _ -> Set.empty + SetupVar i -> Set.singleton i + SetupStruct xs -> foldMap setupVars xs + SetupArray xs -> foldMap setupVars xs + SetupElem x _ -> setupVars x + SetupField x _ -> setupVars x + SetupTerm _ -> Set.empty + SetupNull -> Set.empty + SetupGlobal _ -> Set.empty + SetupGlobalInitializer _ -> Set.empty ------------------------------------------------------------------------ computeReturnValue :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options {- ^ saw script debug and print options -} -> CrucibleContext arch {- ^ context of the crucible simulation -} -> SharedContext {- ^ context for generating saw terms -} -> @@ -813,7 +814,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.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> CrucibleContext arch -> @@ -846,7 +847,7 @@ learnGhost sc cc loc prepost var expected = -- the CrucibleSetup block. First, load the value from the address -- indicated by 'ptr', and then match it against the pattern 'val'. learnPointsTo :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> CrucibleContext arch -> @@ -921,7 +922,7 @@ learnPred sc cc loc prepost t = -- | Perform an allocation as indicated by a 'crucible_alloc' -- statement from the postcondition section. executeAllocation :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> CrucibleContext arch -> (AllocIndex, (W4.ProgramLoc, Crucible.MemType)) -> @@ -948,7 +949,7 @@ executeAllocation opts cc (var, (loc, memTy)) = -- | Update the simulator state based on the postconditions from the -- procedure specification. executeSetupCondition :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> CrucibleContext arch -> @@ -977,7 +978,7 @@ executeGhost sc var val = -- the CrucibleSetup block. First we compute the value indicated by -- 'val', and then write it to the address indicated by 'ptr'. executePointsTo :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => Options -> SharedContext -> CrucibleContext arch -> @@ -1059,14 +1060,15 @@ instantiateSetupValue :: IO SetupValue instantiateSetupValue sc s v = case v of - SetupVar _ -> return v - SetupTerm tt -> SetupTerm <$> doTerm tt - SetupStruct vs -> SetupStruct <$> mapM (instantiateSetupValue sc s) vs - SetupArray vs -> SetupArray <$> mapM (instantiateSetupValue sc s) vs - SetupElem _ _ -> return v - SetupField _ _ -> return v - SetupNull -> return v - SetupGlobal _ -> return v + SetupVar _ -> return v + SetupTerm tt -> SetupTerm <$> doTerm tt + SetupStruct vs -> SetupStruct <$> mapM (instantiateSetupValue sc s) vs + SetupArray vs -> SetupArray <$> mapM (instantiateSetupValue sc s) vs + SetupElem _ _ -> return v + SetupField _ _ -> return v + SetupNull -> return v + SetupGlobal _ -> return v + SetupGlobalInitializer _ -> return v where doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t @@ -1107,7 +1109,7 @@ resolveSetupValue opts cc sc spec sval = ------------------------------------------------------------------------ asPointer :: - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => W4.ProgramLoc -> (Crucible.MemType, Crucible.AnyValue Sym) -> OverrideMatcher arch (Crucible.MemType, LLVMPtr (Crucible.ArchWidth arch)) @@ -1116,7 +1118,7 @@ asPointer _ (Crucible.PtrType pty, Crucible.AnyValue Crucible.PtrRepr val) - | Just pty' <- Crucible.asMemType pty + | Right pty' <- Crucible.asMemType pty = return (pty', val) asPointer loc _ = failure loc BadPointerCast diff --git a/src/SAWScript/CrucibleResolveSetupValue.hs b/src/SAWScript/CrucibleResolveSetupValue.hs index cee742a877..cd697d4348 100644 --- a/src/SAWScript/CrucibleResolveSetupValue.hs +++ b/src/SAWScript/CrucibleResolveSetupValue.hs @@ -1,5 +1,7 @@ -{-# LANGUAGE ImplicitParams #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} module SAWScript.CrucibleResolveSetupValue ( LLVMVal, LLVMPtr @@ -32,13 +34,15 @@ import Data.Parameterized.Some (Some(..)) import Data.Parameterized.NatRepr (NatRepr(..), someNat, natValue, LeqProof(..), isPosNat) -import qualified What4.BaseTypes as W4 -import qualified What4.Interface as W4 +import qualified What4.BaseTypes as W4 +import qualified What4.Interface as W4 import qualified What4.Expr.Builder as W4 -import qualified What4.ProgramLoc as W4 +import qualified What4.ProgramLoc as W4 -import qualified Lang.Crucible.Backend.SAWCore as Crucible -import qualified SAWScript.CrucibleLLVM as Crucible +import qualified Lang.Crucible.LLVM.MemModel as Crucible +import qualified Lang.Crucible.LLVM.Translation as Crucible +import qualified Lang.Crucible.Backend.SAWCore as Crucible +import qualified SAWScript.CrucibleLLVM as Crucible import Verifier.SAW.Rewriter import Verifier.SAW.SharedTerm @@ -95,7 +99,9 @@ resolveSetupFieldIndex cc env nameEnv v n = [] -> Nothing o:_ -> do Crucible.PtrType symTy <- typeOfSetupValue cc env nameEnv v - Crucible.StructType si <- let ?lc = lc in Crucible.asMemType symTy + Crucible.StructType si <- + let ?lc = lc + in either (\_ -> Nothing) Just $ Crucible.asMemType symTy V.findIndex (\fi -> Crucible.bytesToBits (Crucible.fiOffset fi) == toInteger o) (Crucible.siFields si) _ -> Nothing @@ -113,7 +119,7 @@ typeOfSetupValue cc env nameEnv val = do let ?lc = cc^.ccTypeCtx typeOfSetupValue' cc env nameEnv val -typeOfSetupValue' :: +typeOfSetupValue' :: forall m wptr. Monad m => CrucibleContext wptr -> Map AllocIndex (W4.ProgramLoc, Crucible.MemType) -> @@ -156,7 +162,7 @@ typeOfSetupValue' cc env nameEnv val = case memTy of Crucible.PtrType symTy -> case let ?lc = lc in Crucible.asMemType symTy of - Just memTy' -> + Right memTy' -> case memTy' of Crucible.ArrayType n memTy'' | i < n -> return (Crucible.PtrType (Crucible.MemType memTy'')) @@ -166,7 +172,7 @@ typeOfSetupValue' cc env nameEnv val = Just fi -> return (Crucible.PtrType (Crucible.MemType (Crucible.fiType fi))) Nothing -> fail $ "typeOfSetupValue: struct type index out of bounds: " ++ show i _ -> fail msg - Nothing -> fail msg + Left err -> fail (unlines [msg, "Details:", err]) _ -> fail msg SetupNull -> -- We arbitrarily set the type of NULL to void*, because a) it @@ -174,24 +180,38 @@ typeOfSetupValue' cc env nameEnv val = -- and b) it prevents us from doing a type-safe dereference -- operation. return (Crucible.PtrType Crucible.VoidType) - SetupGlobal name -> - do let m = cc^.ccLLVMModule - tys = [ (L.globalSym g, L.globalType g) | g <- L.modGlobals m ] ++ - [ (L.decName d, L.decFunType d) | d <- L.modDeclares m ] ++ - [ (L.defName d, L.defFunType d) | d <- L.modDefines m ] - case lookup (L.Symbol name) tys of - Nothing -> fail $ "typeOfSetupValue: unknown global " ++ show name - Just ty -> - case let ?lc = lc in Crucible.liftType ty of - Nothing -> fail $ "typeOfSetupValue: invalid type " ++ show ty - Just symTy -> return (Crucible.PtrType symTy) + -- A global and its initializer have the same type. + SetupGlobal name -> do + let m = cc^.ccLLVMModule + tys = [ (L.globalSym g, L.globalType g) | g <- L.modGlobals m ] ++ + [ (L.decName d, L.decFunType d) | d <- L.modDeclares m ] ++ + [ (L.defName d, L.defFunType d) | d <- L.modDefines m ] + case lookup (L.Symbol name) tys of + Nothing -> fail $ "typeOfSetupValue: unknown global " ++ show name + Just ty -> + case let ?lc = lc in Crucible.liftType ty of + Left err -> fail $ unlines [ "typeOfSetupValue: invalid type " ++ show ty + , "Details:" + , err + ] + Right symTy -> return (Crucible.PtrType symTy) + SetupGlobalInitializer name -> do + case Map.lookup (L.Symbol name) (Crucible.globalInitMap $ cc^.ccLLVMModuleTrans) of + Just (g, _) -> + case let ?lc = lc in Crucible.liftMemType (L.globalType g) of + Left err -> fail $ unlines [ "typeOfSetupValue: invalid type " ++ show (L.globalType g) + , "Details:" + , err + ] + Right memTy -> return memTy + Nothing -> fail $ "resolveSetupVal: global not found: " ++ name where lc = cc^.ccTypeCtx dl = Crucible.llvmDataLayout lc -- | Translate a SetupValue into a Crucible LLVM value, resolving -- references -resolveSetupVal :: +resolveSetupVal :: forall arch. Crucible.HasPtrWidth (Crucible.ArchWidth arch) => CrucibleContext arch -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> @@ -227,7 +247,7 @@ resolveSetupVal cc env tyenv nameEnv val = delta <- case memTy of Crucible.PtrType symTy -> case let ?lc = lc in Crucible.asMemType symTy of - Just memTy' -> + Right memTy' -> case memTy' of Crucible.ArrayType n memTy'' | i < n -> return (fromIntegral i * Crucible.memTypeSize dl memTy'') @@ -236,7 +256,7 @@ resolveSetupVal cc env tyenv nameEnv val = Just d -> return d Nothing -> fail $ "resolveSetupVal: struct type index out of bounds: " ++ show (i, memTy') _ -> fail msg - Nothing -> fail msg + Left err -> fail $ unlines [msg, "Details:", err] _ -> fail msg ptr <- resolveSetupVal cc env tyenv nameEnv v case ptr of @@ -250,6 +270,15 @@ resolveSetupVal cc env tyenv nameEnv val = SetupGlobal name -> do let mem = cc^.ccLLVMEmptyMem Crucible.ptrToPtrVal <$> Crucible.doResolveGlobal sym mem (L.Symbol name) + SetupGlobalInitializer name -> + case Map.lookup (L.Symbol name) + (Crucible.globalInitMap $ cc^.ccLLVMModuleTrans) of + -- There was an error in global -> constant translation + Just (_, (Left e)) -> fail e + Just (_, (Right v)) -> + let ?lc = lc + in Crucible.constToLLVMVal @(Crucible.ArchWidth arch) sym (cc^.ccLLVMEmptyMem) (snd v) + Nothing -> fail $ "resolveSetupVal: global not found: " ++ name where sym = cc^.ccBackend lc = cc^.ccTypeCtx @@ -395,9 +424,10 @@ typeOfLLVMVal _dl val = case val of Crucible.LLVMValInt _bkl bv -> Crucible.bitvectorType (Crucible.intWidthSize (fromIntegral (natValue (W4.bvWidth bv)))) - Crucible.LLVMValFloat _ _ -> error "FIXME: typeOfLLVMVal LLVMValFloat" + Crucible.LLVMValFloat _ _ -> error "FIXME: typeOfLLVMVal LLVMValFloat" Crucible.LLVMValStruct flds -> Crucible.mkStructType (fmap fieldType flds) Crucible.LLVMValArray tp vs -> Crucible.arrayType (fromIntegral (V.length vs)) tp + Crucible.LLVMValZero tp -> tp where fieldType (f, _) = (f ^. Crucible.fieldVal, Crucible.fieldPad f) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 87814507d4..befc75b3c3 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1756,6 +1756,15 @@ primitives = Map.fromList [ "Return a SetupValue representing a pointer to the named global." , "The String may be either the name of a global value or a function name." ] + , prim "crucible_global_initializer" + "String -> SetupValue" + (pureVal CIR.SetupGlobalInitializer) + [ "Return a SetupValue representing the value of the initializer of a named" + , "global. The String should be the name of a global value." + , "Note that initializing global variables may be unsound in the presence" + , "of compositional verification (see GaloisInc/saw-script#203)." + ] -- TODO: There should be a section in the manual about global-unsoundness. + , prim "crucible_term" "Term -> SetupValue" (pureVal CIR.SetupTerm) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index bdc31da052..8fe2f094a0 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -481,7 +481,7 @@ data LLVMSetupState type LLVMSetup a = StateT LLVMSetupState TopLevel a type CrucibleSetup arch a = - (?lc :: Crucible.LLVMTyCtx, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => StateT (CIR.CrucibleSetupState arch) TopLevel a + (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => StateT (CIR.CrucibleSetupState arch) TopLevel a data CrucibleSetupM a = CrucibleSetupM { runCrucibleSetupM :: forall arch. CrucibleSetup arch a }