uc-crux-llvm: Introduce a newtype for pre-simulation memory (#921)

This concept was used throughout the codebase, so it's nice to have types act as
documentation.

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),

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 <[email protected]>
+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

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 $

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 ->

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