From 470a8376079b200a34d5fe1704f5a793204a5c97 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 26 Sep 2018 13:55:39 -0700 Subject: [PATCH 1/4] manual: add a section on global variables --- doc/manual/manual.md | 80 ++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 73 insertions(+), 7 deletions(-) diff --git a/doc/manual/manual.md b/doc/manual/manual.md index ff3c881128..b7b0812c27 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,79 @@ 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`: + +~~~ +let f_setup = do { + y <- crucible_fresh_var "y" (llvm_int 32); + crucible_execute_func [crucible_term y]; + crucible_return (crucible_term {{ 1 + y : [32] }}); +}; + +let f_setup = do { + z <- crucible_fresh_var "z" (llvm_int 32); + crucible_execute_func [crucible_term z]; + crucible_return (crucible_term {{ 2 + z : [32] }}); +}; + +m <- llvm_load_module "module.bc"; +f_ms <- crucible_llvm_verify m "f" [] false f_setup abc; +g_ms <- crucible_llvm_verify m "g" [] false g_setup 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 + +~~~ +let f_setup = do { + y <- crucible_fresh_var "y" (llvm_int 32); + crucible_points_to (crucible_global "x") + (crucible_global_init "x"); + crucible_execute_func [crucible_term y]; + crucible_return (crucible_term {{ 1 + y : [32] }}); +}; +~~~ + +which initializes `x` to whatever it is initialized to in the C code +at the beginning of verification. + ## Preconditions and Postconditions Sometimes a function is only well-defined under certain conditions, or From 64efcc240d296bf6526c2d4da313798b5feeb2ed Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 26 Sep 2018 13:56:46 -0700 Subject: [PATCH 2/4] llvm: don't initialize globals by default Instead, add crucible_global_initializer. The current behavior of globals is unsound (ref: #203). Instead, we provide an option for the user to initialize globals as necessary. It would be best to have more informative error messages when the symbolic simulator accesses invalid memory because a global hasn't been initialized. I initially assumed that `SetupGlobalInitializer name` should have the same type as `SetupGlobal name`. However, `SetupGlobal` adds a pointer wrapper (as it should). Instead, we now directly translate the type of the global's initializer from the LLVM AST. --- intTests/runtests.sh | 2 +- saw-script.cabal | 2 +- src/SAWScript/CrucibleBuiltins.hs | 7 +-- src/SAWScript/CrucibleLLVM.hs | 3 +- src/SAWScript/CrucibleMethodSpecIR.hs | 22 ++++++---- src/SAWScript/CrucibleOverride.hs | 34 ++++++++------- src/SAWScript/CrucibleResolveSetupValue.hs | 50 +++++++++++++++------- src/SAWScript/Interpreter.hs | 9 ++++ 8 files changed, 79 insertions(+), 50 deletions(-) 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/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..7b10f168b9 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) @@ -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 diff --git a/src/SAWScript/CrucibleLLVM.hs b/src/SAWScript/CrucibleLLVM.hs index f348d75433..9f6b5dd01b 100644 --- a/src/SAWScript/CrucibleLLVM.hs +++ b/src/SAWScript/CrucibleLLVM.hs @@ -69,7 +69,6 @@ module SAWScript.CrucibleLLVM , transContext , llvmPtrWidth , initializeMemory - , initMemoryCFG , LLVMContext , translateModule -- * Re-exports from "Lang.Crucible.LLVM.MemModel" @@ -151,7 +150,7 @@ import qualified Lang.Crucible.LLVM.LLVMContext as TyCtx import Lang.Crucible.LLVM.Translation (llvmMemVar, toStorableType, symbolMap, LLVMHandleInfo(LLVMHandleInfo), - cfgMap, transContext, llvmPtrWidth, initializeMemory, initMemoryCFG, + cfgMap, transContext, llvmPtrWidth, initializeMemory, ModuleTranslation, LLVMContext, translateModule) import Lang.Crucible.LLVM.MemModel diff --git a/src/SAWScript/CrucibleMethodSpecIR.hs b/src/SAWScript/CrucibleMethodSpecIR.hs index fbe559124e..0e9cc3d423 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 diff --git a/src/SAWScript/CrucibleOverride.hs b/src/SAWScript/CrucibleOverride.hs index fa842fb00f..6d2aa14e00 100644 --- a/src/SAWScript/CrucibleOverride.hs +++ b/src/SAWScript/CrucibleOverride.hs @@ -562,14 +562,15 @@ 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 ------------------------------------------------------------------------ @@ -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 diff --git a/src/SAWScript/CrucibleResolveSetupValue.hs b/src/SAWScript/CrucibleResolveSetupValue.hs index cee742a877..cb7a8564c5 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 @@ -37,8 +39,9 @@ import qualified What4.Interface as W4 import qualified What4.Expr.Builder 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.Translation as CrucibleT +import qualified Lang.Crucible.Backend.SAWCore as Crucible +import qualified SAWScript.CrucibleLLVM as Crucible import Verifier.SAW.Rewriter import Verifier.SAW.SharedTerm @@ -113,7 +116,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) -> @@ -174,24 +177,32 @@ 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 + Nothing -> fail $ "typeOfSetupValue: invalid type " ++ show ty + Just symTy -> return (Crucible.PtrType symTy) + SetupGlobalInitializer name -> do + case Map.lookup (L.Symbol name) (CrucibleT.globalMap $ cc^.ccLLVMModuleTrans) of + Just (g, _) -> + case let ?lc = lc in Crucible.liftMemType (L.globalType g) of + Nothing -> fail $ "typeOfSetupValue: invalid type " ++ show (L.globalType g) + Just 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)) -> @@ -250,6 +261,13 @@ 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) (CrucibleT.globalMap $ cc^.ccLLVMModuleTrans) of + -- There was an error in global -> constant translation + Just (_, (Left e)) -> fail e + Just (_, (Right v)) -> + let ?lc = lc in CrucibleT.constToLLVMVal @arch sym (cc^.ccLLVMEmptyMem) v + Nothing -> fail $ "resolveSetupVal: global not found: " ++ name where sym = cc^.ccBackend lc = cc^.ccTypeCtx 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) From 75ca03a9e65357f4695304adf73c265c3f71ba0f Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 28 Sep 2018 16:42:22 -0700 Subject: [PATCH 3/4] Add integration tests for new global handling manual: define auxilary function init_global --- doc/manual/manual.md | 44 +++++++++++++-------- intTests/test0036_global/README | 1 + intTests/test0036_global/test-fail.saw | 15 +++++++ intTests/test0036_global/test.bc | Bin 0 -> 2204 bytes intTests/test0036_global/test.c | 15 +++++++ intTests/test0036_global/test.saw | 29 ++++++++++++++ intTests/test0036_global/test.sh | 6 +++ src/SAWScript/CrucibleResolveSetupValue.hs | 17 ++++---- 8 files changed, 102 insertions(+), 25 deletions(-) create mode 100644 intTests/test0036_global/README create mode 100644 intTests/test0036_global/test-fail.saw create mode 100644 intTests/test0036_global/test.bc create mode 100644 intTests/test0036_global/test.c create mode 100644 intTests/test0036_global/test.saw create mode 100755 intTests/test0036_global/test.sh diff --git a/doc/manual/manual.md b/doc/manual/manual.md index b7b0812c27..b1547b06f1 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -2661,38 +2661,38 @@ aren't initialized at the beginning of symbolic simulation. This is intentional 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; + x = x + 1; + return x + y; } int g(int z) { - x = x + 2; - return x + z; + x = x + 2; + return x + z; } ~~~ One might initially write the following specifications for `f` and `g`: + ~~~ -let f_setup = do { +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; -let f_setup = do { +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] }}); -}; - -m <- llvm_load_module "module.bc"; -f_ms <- crucible_llvm_verify m "f" [] false f_setup abc; -g_ms <- crucible_llvm_verify m "g" [] false g_setup abc; +}) abc; ~~~ If globals were always initialized at the beginning of verification, both @@ -2704,18 +2704,28 @@ 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 + ~~~ -let f_setup = do { +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); - crucible_points_to (crucible_global "x") - (crucible_global_init "x"); + 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. +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 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 0000000000000000000000000000000000000000..fd3749082d31861fce75d40ce98a871f5732e4dc GIT binary patch literal 2204 zcma)7Urbxq89$e6e4OBa1Xr?~d+)9T?L4If#{}2ZAlbelby^-w!vp)L*bu;8iF2`y zZA>&>W5^*Js+=wlmR3!8YNbwlp=-7Fp{k6{GK*OqV^b6%hGHc{C}IdznUsf0+jnT# zA}yMBq;tOWo%5aV{JwwZ_@vTymkFUpgwU|o-gfc3UySYl`HS}RjDs#As}`ZZG6*#_ zSWyG;Ezohc^_I7)x~Mify5D8yv@bPkEQ0E%!-}@A!S`;H?~2i3a%s$O9(Onv{CSfo zU0C=4SscEHetrIybv57}$S&4%fBT8bazQ;{M(7>TdGdQNKlvv#Mqxb-E>XKMna0z3 z5;NmWkX#S5(`k~CamiI1^^$3UP*syo3{|X65dMgf&L2TKOF- zx0>bGin?7Zw~^&HgIqbw!!C+zaI!#RNRzaY=>l;oc-lrL{RBp*9j8H+h)Yy>r^ul) zzg^VTyh6E1Ro$=i8!P;7k$YIwt!4R*BL5$4sWfr=amr4npATuP&To47M@9brAtZ|J zSupgtOl0|g9S;f{b#AN3Rg1dEfT0cubu~uVT;j`FVV$uPIS5u@MJA~*o5>Sd!D)cx z`fva2WQB5wy9*Y1h3%}c7UFj6JQ%fF6lyEnnpfC_yS(38W0qKDiO6{pw}Gp3lM2b8 z1IDnoq}x;UXjUkDg)fWTF2E>)$Am{-P$ei`c6_~nr-Qk!FiDoMb0`OXjsaVs@Va4A z!abj{%7-{rAhMl6Sf3ZfM-a-QZl})IvchJGyH}@X{@dY@Hy0s)AU#pbEJ8O$gdkm! z<5X26UYS?@%=-Qu3=igtdDDsh8;ebISNe@yTov@#8ayv*3ax0q8N^YG{d$RYKWTI? z<(zYXiQpD+X^}d2L zMx0#2aq;Qy$3`4e@EZnA^9j$5MN>0#&S$<`&_uqP=M6^WV*srN07$ktY?OLKpI@z~3+-%&|rjpvxj*KJ~^ zK+{Lyo2wwxsZqGqIyYuwdKVv z(8`xX!kGQ0`}3T8UF!aX?fE>{Gsn7X2c~2Y&xG--VTd_?RiT+B2XWGdlTR8!ZAu}R zHDuCEVvs3?>?`{R`u+R*f0Xolc6PW*%Z`IYgK;awt$kD9A@$w7)LoUj3y0%p71wRa zwZOV>S32O*uV>wVVcp9W?e8N*9wIS0mk8rD#MVp_OT_Z!CBr^4d==0?%$MkWZzI>@ZP<>%^z%3 z*S2;q9D9-4`zy%RCZJ8n;ayKbAq~j|sTV@IEOoC}W_P$d@MOXpyaJCpzkBFg^d~3? zHJrhIx2F^FUpbe}bi)t12o_FV@ zh!B)2a_Ehx=9o`eo4rS2|41bf8inVf1Lz6%wtR$<%F>VdJaoDifKD5wbZ?n5(2hX| zmm({4>Z5N%KWbEtHhTWqPXAxjh7SLEx=#OlN{`klD#{rXHFA=sdU v4X|OH?x)Ab!-r{@b~!IQ&$UlQ-;Q2OMcXGL(W!L%cyuZ;8c&=Vp`z$t;(MV` literal 0 HcmV?d00001 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/src/SAWScript/CrucibleResolveSetupValue.hs b/src/SAWScript/CrucibleResolveSetupValue.hs index cb7a8564c5..91b313e795 100644 --- a/src/SAWScript/CrucibleResolveSetupValue.hs +++ b/src/SAWScript/CrucibleResolveSetupValue.hs @@ -34,14 +34,14 @@ 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.LLVM.Translation as CrucibleT -import qualified Lang.Crucible.Backend.SAWCore as Crucible -import qualified SAWScript.CrucibleLLVM as Crucible +import qualified Lang.Crucible.LLVM.Translation.Constant as Crucible +import qualified Lang.Crucible.Backend.SAWCore as Crucible +import qualified SAWScript.CrucibleLLVM as Crucible import Verifier.SAW.Rewriter import Verifier.SAW.SharedTerm @@ -190,7 +190,7 @@ typeOfSetupValue' cc env nameEnv val = Nothing -> fail $ "typeOfSetupValue: invalid type " ++ show ty Just symTy -> return (Crucible.PtrType symTy) SetupGlobalInitializer name -> do - case Map.lookup (L.Symbol name) (CrucibleT.globalMap $ cc^.ccLLVMModuleTrans) of + case Map.lookup (L.Symbol name) (CrucibleT.globalInitMap $ cc^.ccLLVMModuleTrans) of Just (g, _) -> case let ?lc = lc in Crucible.liftMemType (L.globalType g) of Nothing -> fail $ "typeOfSetupValue: invalid type " ++ show (L.globalType g) @@ -262,7 +262,8 @@ resolveSetupVal cc env tyenv nameEnv val = do let mem = cc^.ccLLVMEmptyMem Crucible.ptrToPtrVal <$> Crucible.doResolveGlobal sym mem (L.Symbol name) SetupGlobalInitializer name -> - case Map.lookup (L.Symbol name) (CrucibleT.globalMap $ cc^.ccLLVMModuleTrans) of + case Map.lookup (L.Symbol name) + (CrucibleT.globalInitMap $ cc^.ccLLVMModuleTrans) of -- There was an error in global -> constant translation Just (_, (Left e)) -> fail e Just (_, (Right v)) -> From 783f83d4e6e4d4981df97a695d6bd794fd9e32ea Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Mon, 8 Oct 2018 09:37:35 -0700 Subject: [PATCH 4/4] update crucible to 8a53094 This update changes the handling of global variables so that they aren't automatically initialized. Instead, the user/client has more granular control. update CrucibleLLVM API, change LLVMTyCtx -> TypeContext Crucible replaced a few "Maybe"s with "MonadError String"s. Instead of throwing that information away, more of it is now propagated (after the text "Details:") --- deps/crucible | 2 +- src/SAWScript/CrucibleBuiltins.hs | 56 ++++++++++++++-------- src/SAWScript/CrucibleLLVM.hs | 26 +++++----- src/SAWScript/CrucibleMethodSpecIR.hs | 20 ++++---- src/SAWScript/CrucibleOverride.hs | 32 ++++++------- src/SAWScript/CrucibleResolveSetupValue.hs | 43 ++++++++++------- src/SAWScript/Value.hs | 2 +- 7 files changed, 107 insertions(+), 74 deletions(-) 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/src/SAWScript/CrucibleBuiltins.hs b/src/SAWScript/CrucibleBuiltins.hs index 7b10f168b9..cb4e174774 100644 --- a/src/SAWScript/CrucibleBuiltins.hs +++ b/src/SAWScript/CrucibleBuiltins.hs @@ -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 @@ -986,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 -} -> @@ -1010,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) @@ -1038,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 @@ -1057,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 @@ -1109,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 9f6b5dd01b..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,7 +73,6 @@ module SAWScript.CrucibleLLVM , cfgMap , transContext , llvmPtrWidth - , initializeMemory , LLVMContext , translateModule -- * Re-exports from "Lang.Crucible.LLVM.MemModel" @@ -143,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, + (llvmMemVar, symbolMap, LLVMHandleInfo(LLVMHandleInfo), + cfgMap, transContext, llvmPtrWidth, ModuleTranslation, LLVMContext, translateModule) import Lang.Crucible.LLVM.MemModel @@ -163,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 0e9cc3d423..ecf701cbcd 100644 --- a/src/SAWScript/CrucibleMethodSpecIR.hs +++ b/src/SAWScript/CrucibleMethodSpecIR.hs @@ -268,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 -------------------------------------------------------------------------------- @@ -337,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 @@ -366,7 +368,7 @@ initialStateSpec = StateSpec } initialDefCrucibleMethodSpecIR :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => L.Define -> ProgramLoc -> Either SetupError CrucibleMethodSpecIR @@ -387,7 +389,7 @@ initialDefCrucibleMethodSpecIR def loc = do } initialDeclCrucibleMethodSpecIR :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => L.Declare -> ProgramLoc -> Either SetupError CrucibleMethodSpecIR @@ -408,7 +410,7 @@ initialDeclCrucibleMethodSpecIR dec loc = do } initialCrucibleSetupState :: - (?lc :: CL.LLVMTyCtx) => + (?lc :: CL.TypeContext) => CrucibleContext wptr -> L.Define -> ProgramLoc -> @@ -424,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 6d2aa14e00..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 -} -> @@ -576,7 +576,7 @@ matchPointsTos opts sc cc spec prepost = go False [] ------------------------------------------------------------------------ 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 -} -> @@ -814,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 -> @@ -847,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 -> @@ -922,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)) -> @@ -949,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 -> @@ -978,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 -> @@ -1109,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)) @@ -1118,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 91b313e795..cd697d4348 100644 --- a/src/SAWScript/CrucibleResolveSetupValue.hs +++ b/src/SAWScript/CrucibleResolveSetupValue.hs @@ -39,9 +39,10 @@ import qualified What4.Interface as W4 import qualified What4.Expr.Builder as W4 import qualified What4.ProgramLoc as W4 -import qualified Lang.Crucible.LLVM.Translation.Constant as Crucible -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 @@ -98,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 @@ -159,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'')) @@ -169,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 @@ -187,14 +190,20 @@ typeOfSetupValue' cc env nameEnv val = 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) + 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) (CrucibleT.globalInitMap $ cc^.ccLLVMModuleTrans) of + case Map.lookup (L.Symbol name) (Crucible.globalInitMap $ cc^.ccLLVMModuleTrans) of Just (g, _) -> case let ?lc = lc in Crucible.liftMemType (L.globalType g) of - Nothing -> fail $ "typeOfSetupValue: invalid type " ++ show (L.globalType g) - Just memTy -> return memTy + 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 @@ -238,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'') @@ -247,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 @@ -263,11 +272,12 @@ resolveSetupVal cc env tyenv nameEnv val = Crucible.ptrToPtrVal <$> Crucible.doResolveGlobal sym mem (L.Symbol name) SetupGlobalInitializer name -> case Map.lookup (L.Symbol name) - (CrucibleT.globalInitMap $ cc^.ccLLVMModuleTrans) of + (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 CrucibleT.constToLLVMVal @arch sym (cc^.ccLLVMEmptyMem) 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 @@ -414,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/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 }