Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Explicit handling of global variables #311

Merged
merged 4 commits into from
Oct 9, 2018
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
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:")
langston-barrett committed Oct 8, 2018
commit 783f83d4e6e4d4981df97a695d6bd794fd9e32ea
2 changes: 1 addition & 1 deletion deps/crucible
Submodule crucible updated 29 files
+23 −26 crucible-c/src/Main.hs
+48 −44 crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs
+46 −53 crucible-jvm/src/Lang/Crucible/JVM/Translation.hs
+30 −4 crucible-llvm/crucible-llvm.cabal
+0 −2 crucible-llvm/src/Lang/Crucible/LLVM/Bytes.hs
+3 −3 crucible-llvm/src/Lang/Crucible/LLVM/DataLayout.hs
+264 −0 crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs
+6 −6 crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+119 −8 crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+6 −11 crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs
+12 −13 crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+182 −30 crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Value.hs
+4 −4 crucible-llvm/src/Lang/Crucible/LLVM/MemType.hs
+43 −2,228 crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs
+75 −21 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Constant.hs
+519 −0 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs
+1,601 −0 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+198 −0 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Monad.hs
+9 −36 crucible-llvm/src/Lang/Crucible/LLVM/Translation/Types.hs
+47 −33 crucible-llvm/src/Lang/Crucible/LLVM/TypeContext.hs
+120 −0 crucible-llvm/test/Tests.hs
+5 −0 crucible-llvm/test/data/global-extern.c
+5 −0 crucible-llvm/test/data/global-int.c
+13 −0 crucible-llvm/test/data/global-struct.c
+5 −0 crucible-llvm/test/data/global-uninitialized.c
+6 −0 what4/src/What4/Expr/Builder.hs
+1 −1 what4/src/What4/Protocol/SMTLib2/Syntax.hs
+0 −19 what4/src/What4/Protocol/SMTWriter.hs
+3 −0 what4/src/What4/Solver/Yices.hs
56 changes: 36 additions & 20 deletions src/SAWScript/CrucibleBuiltins.hs
Original file line number Diff line number Diff line change
@@ -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)
26 changes: 15 additions & 11 deletions src/SAWScript/CrucibleLLVM.hs
Original file line number Diff line number Diff line change
@@ -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
20 changes: 11 additions & 9 deletions src/SAWScript/CrucibleMethodSpecIR.hs
Original file line number Diff line number Diff line change
@@ -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 ->
Loading