diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Classify.hs b/uc-crux-llvm/src/UCCrux/LLVM/Classify.hs index 1ca73c352..66b793512 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Classify.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Classify.hs @@ -79,6 +79,7 @@ import UCCrux.LLVM.FullType (FullType(FTPtr), MapToCrucibleType, FullT import UCCrux.LLVM.FullType.MemType (toMemType) import UCCrux.LLVM.Logging (Verbosity(Hi)) import UCCrux.LLVM.Module (makeFuncSymbol, makeGlobalSymbol, globalSymbol) +import UCCrux.LLVM.Newtypes.PreSimulationMem (PreSimulationMem, getPreSimulationMem) import UCCrux.LLVM.Overrides.Skip (SkipOverrideName) import UCCrux.LLVM.Setup (SymValue) import UCCrux.LLVM.Setup.Monad (TypedSelector(..), mallocLocation) @@ -208,7 +209,7 @@ classifyBadBehavior :: FunctionContext m arch argTypes -> sym -> -- | Initial LLVM memory (containing globals and functions) - LLVMMem.MemImpl sym -> + PreSimulationMem sym -> -- | Functions skipped during execution Set SkipOverrideName -> -- | Simulation error (including source position) @@ -250,7 +251,7 @@ doClassifyBadBehavior :: FunctionContext m arch argTypes -> sym -> -- | Program memory - LLVMMem.MemImpl sym -> + PreSimulationMem sym -> -- | Functions skipped during execution Set SkipOverrideName -> -- | Simulation error (including source position) @@ -529,7 +530,7 @@ doClassifyBadBehavior appCtx modCtx funCtx sym memImpl skipped simError (Crucibl then unclass appCtx badBehavior errorLoc else truePositive (ReadUninitializedHeap loc) Just (G.AllocInfo G.GlobalAlloc _sz _mut _align _loc) -> - case flip Map.lookup (LLVMMem.memImplSymbolMap memImpl) =<< blk of + case flip Map.lookup (LLVMMem.memImplSymbolMap (getPreSimulationMem memImpl)) =<< blk of Nothing -> requirePossiblePointer ReadNonPointer ptr Just glob -> case ( makeFuncSymbol glob (modCtx ^. funcTypes), diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Newtypes/PreSimulationMem.hs b/uc-crux-llvm/src/UCCrux/LLVM/Newtypes/PreSimulationMem.hs new file mode 100644 index 000000000..0abc4234c --- /dev/null +++ b/uc-crux-llvm/src/UCCrux/LLVM/Newtypes/PreSimulationMem.hs @@ -0,0 +1,23 @@ +{- +Module : UCCrux.LLVM.Newtypes.PreSimulationMem +Copyright : (c) Galois, Inc 2020 +License : BSD3 +Maintainer : Langston Barrett +Stability : provisional +-} + +module UCCrux.LLVM.Newtypes.PreSimulationMem + ( PreSimulationMem + , makePreSimulationMem + , getPreSimulationMem + ) where + +import Lang.Crucible.LLVM.MemModel (MemImpl) + +-- | LLVM memory just before symbolic execution. Populated with globals, defined +-- functions, and arguments to the entry point. +newtype PreSimulationMem sym = + PreSimulationMem { getPreSimulationMem :: MemImpl sym } + +makePreSimulationMem :: MemImpl sym -> PreSimulationMem sym +makePreSimulationMem = PreSimulationMem diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs index 792db78ff..5c44c824d 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs @@ -55,7 +55,7 @@ import qualified Lang.Crucible.Simulator.RegMap as Crucible import Lang.Crucible.FunctionHandle (HandleAllocator) -- crucible-llvm -import Lang.Crucible.LLVM.MemModel (MemImpl, HasLLVMAnn) +import Lang.Crucible.LLVM.MemModel (HasLLVMAnn) import Lang.Crucible.LLVM.Extension (LLVM) -- crux @@ -78,6 +78,7 @@ import UCCrux.LLVM.Errors.Panic (panic) import UCCrux.LLVM.FullType (FullType, FullTypeRepr, MapToCrucibleType) import qualified UCCrux.LLVM.FullType.CrucibleType as FT import UCCrux.LLVM.Module (DefnSymbol, FuncSymbol(FuncDefnSymbol), defnSymbolToString) +import UCCrux.LLVM.Newtypes.PreSimulationMem (PreSimulationMem, getPreSimulationMem) import qualified UCCrux.LLVM.Overrides.Check as Check import qualified UCCrux.LLVM.Overrides.Stack as Stack import UCCrux.LLVM.PP (ppRegMap) @@ -120,7 +121,7 @@ newtype CheckResult m arch (argTypes :: Ctx (FullType m)) = IsSymInterface sym => sym -> -- | Pre-simulation memory - MemImpl sym -> + PreSimulationMem sym -> -- | Arguments passed to the entry point Assignment (Shape m (SymValue sym arch)) argTypes -> Crux.CruxSimulationResult -> @@ -351,7 +352,7 @@ ppSomeCheckResult _appCtx entry proxy@(SomeCheckResult _ftReprs (CheckResult k)) forall sym. IsSymInterface sym => sym -> - MemImpl sym -> + PreSimulationMem sym -> SomeCheckedCalls m sym arch -> IO (Maybe (PP.Doc ann)) ppOne sym mem (SomeCheckedCalls k') = @@ -370,7 +371,7 @@ ppSomeCheckResult _appCtx entry proxy@(SomeCheckResult _ftReprs (CheckResult k)) IsSymInterface sym => FunctionContext m arch argTypes -> sym -> - MemImpl sym -> + PreSimulationMem sym -> Check.CheckedCall m sym arch argTypes -> IO (PP.Doc ann) ppCheckedCall funCtx sym mem call = @@ -383,7 +384,7 @@ ppSomeCheckResult _appCtx entry proxy@(SomeCheckResult _ftReprs (CheckResult k)) Crucible.RegEntry (argFTys ^. ixF' i . to (FT.toCrucibleType proxy)) (Check.checkedCallArgs call ^. ixF' i' . to Crucible.unRV)) - prettyArgs <- ppRegMap proxy funCtx sym mem (Crucible.RegMap args) + prettyArgs <- ppRegMap proxy funCtx sym (getPreSimulationMem mem) (Crucible.RegMap args) prettyChecked <- mapM (ppCheckedConstraint sym) (Check.checkedCallConstraints call) return $ diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs index 6a42b91a1..3ba5cc58d 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs @@ -83,7 +83,7 @@ import Lang.Crucible.LLVM (llvmGlobalsToCtx, registerModuleFn) import qualified Lang.Crucible.LLVM.Errors as LLVMErrors import qualified Lang.Crucible.LLVM.Intrinsics as LLVMIntrinsics import Lang.Crucible.LLVM.MemModel.CallStack (ppCallStack) -import Lang.Crucible.LLVM.MemModel (HasLLVMAnn, LLVMAnnMap, MemImpl, MemOptions) +import Lang.Crucible.LLVM.MemModel (HasLLVMAnn, LLVMAnnMap, MemOptions) import Lang.Crucible.LLVM.Translation (transContext, llvmMemVar, llvmTypeCtx, cfgMap, allModuleDeclares) import Lang.Crucible.LLVM.TypeContext (TypeContext) @@ -112,6 +112,7 @@ import UCCrux.LLVM.Context.Module (ModuleContext, llvmModule, moduleTr import UCCrux.LLVM.Errors.Panic (panic) import UCCrux.LLVM.Logging (Verbosity(Hi)) import UCCrux.LLVM.Module (getModule) +import UCCrux.LLVM.Newtypes.PreSimulationMem (PreSimulationMem, makePreSimulationMem) import UCCrux.LLVM.Overrides.Skip (SkipOverrideName, unsoundSkipOverrides, ppClobberSpecError) import UCCrux.LLVM.Overrides.Polymorphic (PolymorphicLLVMOverride, getPolymorphicLLVMOverride, getForAllSymArch) import UCCrux.LLVM.Overrides.Unsound (UnsoundOverrideName, unsoundOverrides) @@ -165,7 +166,7 @@ data SimulatorHooks sym m arch (argTypes :: Ctx (FullType m)) r = , resultHook :: sym -> -- | Pre-simulation memory - MemImpl sym -> + PreSimulationMem sym -> -- | Arguments passed to the entry point Assignment (Shape m (SymValue sym arch)) argTypes -> Crux.CruxSimulationResult -> @@ -341,7 +342,7 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts = -- | Overrides that were passed in as arguments [SymCreateOverrideFn sym arch] -> IORef (Set SkipOverrideName) -> - IORef (Maybe (MemImpl sym)) -> + IORef (Maybe (PreSimulationMem sym)) -> IORef (Maybe (Crucible.RegMap sym (MapToCrucibleType arch argTypes))) -> IORef (Maybe (Map (Some (What4.SymAnnotation sym)) (Some (TypedSelector m arch argTypes)))) -> IORef (Maybe (Assignment (Shape m (SymValue sym arch)) argTypes)) -> @@ -371,7 +372,7 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts = pure (mem, anns, assumptions, argShapes, args) -- Save initial state so that it can be used during classification - IORef.writeIORef memRef (Just mem) + IORef.writeIORef memRef (Just (makePreSimulationMem mem)) IORef.writeIORef argRef (Just args) IORef.writeIORef argAnnRef (Just argAnnotations) IORef.writeIORef argShapeRef (Just argShapes) @@ -466,7 +467,7 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts = (sym ~ What4.ExprBuilder t st fs) => sym -> IORef (Set SkipOverrideName) -> - IORef (Maybe (MemImpl sym)) -> + IORef (Maybe (PreSimulationMem sym)) -> IORef (Maybe (Crucible.RegMap sym (MapToCrucibleType arch argTypes))) -> IORef (Maybe (Map (Some (What4.SymAnnotation sym)) (Some (TypedSelector m arch argTypes)))) -> IORef (Maybe (Assignment (Shape m (SymValue sym arch)) argTypes)) -> @@ -546,11 +547,11 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts = IORef (Set SkipOverrideName) -> IORef (Set UnsoundOverrideName) -> IORef [Located (Explanation m arch argTypes)] -> - IORef (Maybe (MemImpl sym)) -> + IORef (Maybe (PreSimulationMem sym)) -> IORef (Maybe (Assignment (Shape m (SymValue sym arch)) argTypes)) -> Crux.CruxSimulationResult -> (sym -> - MemImpl sym -> + PreSimulationMem sym -> Assignment (Shape m (SymValue sym arch)) argTypes -> Crux.CruxSimulationResult -> UCCruxSimulationResult m arch argTypes -> diff --git a/uc-crux-llvm/uc-crux-llvm.cabal b/uc-crux-llvm/uc-crux-llvm.cabal index 46ecb21d2..365fab2cb 100644 --- a/uc-crux-llvm/uc-crux-llvm.cabal +++ b/uc-crux-llvm/uc-crux-llvm.cabal @@ -61,6 +61,7 @@ library UCCrux.LLVM.Mem UCCrux.LLVM.Module UCCrux.LLVM.Newtypes.FunctionName + UCCrux.LLVM.Newtypes.PreSimulationMem UCCrux.LLVM.Newtypes.Seconds UCCrux.LLVM.Overrides.Check UCCrux.LLVM.Overrides.Polymorphic