Support memory invalidation in LLVM memory model

crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs

@@ -28,6 +28,7 @@
 
 module Lang.Crucible.LLVM.Globals
   ( initializeMemory
+  , initializeMemoryConstGlobals
   , populateGlobal
   , populateGlobals
   , populateAllGlobals
@@ -148,7 +149,24 @@ initializeMemory
    -> LLVMContext arch
    -> L.Module
    -> IO (MemImpl sym)
-initializeMemory sym llvm_ctx m = do
+initializeMemory = initializeMemory' (const True)
+
+initializeMemoryConstGlobals
+   :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
+   => sym
+   -> LLVMContext arch
+   -> L.Module
+   -> IO (MemImpl sym)
+initializeMemoryConstGlobals = initializeMemory' (L.gaConstant . L.globalAttrs)
+
+initializeMemory'
+   :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
+   => (L.Global -> Bool)
+   -> sym
+   -> LLVMContext arch
+   -> L.Module
+   -> IO (MemImpl sym)
+initializeMemory' predicate sym llvm_ctx m = do
    -- Create initial memory of appropriate endianness
    let ?lc = llvm_ctx^.llvmTypeCtx
    let dl = llvmDataLayout ?lc
@@ -191,7 +209,7 @@ initializeMemory sym llvm_ctx m = do
                             _ -> return tyAlign
                         return (g, aliases, sz, alignment))
                     globals
-   allocGlobals sym gs_alloc mem
+   allocGlobals sym (filter (\(g, _, _, _) -> predicate g) gs_alloc) mem
 
 allocLLVMHandleInfo :: (IsSymInterface sym, HasPtrWidth wptr)
                     => sym

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -68,6 +68,7 @@ module Lang.Crucible.LLVM.MemModel
   , doLookupHandle
   , doMemcpy
   , doMemset
+  , doInvalidate
   , doCalloc
   , doFree
   , doLoad
@@ -180,6 +181,7 @@ import           Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import           Data.Set (Set)
 import qualified Data.Set as Set
+import           Data.Text (Text)
 import           Data.Word
 import           GHC.TypeNats
 import           System.IO (Handle, hPutStrLn)
@@ -697,6 +699,29 @@ doMemset sym w mem dest val len = do
 
   return mem{ memImplHeap = heap' }
 
+doInvalidate ::
+  (1 <= w, IsSymInterface sym, HasPtrWidth wptr) =>
+  sym ->
+  NatRepr w ->
+  MemImpl sym ->
+  LLVMPtr sym wptr {- ^ destination -} ->
+  Text             {- ^ message     -} ->
+  SymBV sym w      {- ^ length      -} ->
+  IO (MemImpl sym)
+doInvalidate sym w mem dest msg len = do
+  len' <- sextendBVTo sym w PtrWidth len
+
+  (heap', p) <- G.invalidateMem sym PtrWidth dest msg len' (memImplHeap mem)
+
+  assert sym p . AssertFailureSimError $ mconcat
+    [ "Invalidation of unallocated or immutable region: "
+    , show $ printSymExpr len
+    , " bytes at "
+    , show $ G.ppPtr dest
+    ]
+
+  return mem{ memImplHeap = heap' }
+
 -- | Store an array in memory.
 --
 -- Precondition: the pointer is valid and points to a mutable memory region.
@@ -1504,15 +1529,20 @@ doResolveGlobal ::
   MemImpl sym ->
   L.Symbol {- ^ name of global -} ->
   IO (LLVMPtr sym wptr)
-doResolveGlobal _sym mem symbol =
+doResolveGlobal sym mem symbol@(L.Symbol name) =
   let lookedUp = Map.lookup symbol (memImplGlobalMap mem)
   in case lookedUp of
        Just (SomePointer ptr) | PtrWidth <- ptrWidth ptr -> return ptr
-       _ -> panic "MemModel.doResolveGlobal" $
-               (if isJust lookedUp
-               then "Symbol was not a pointer of the correct width."
-               else "Unable to resolve global symbol.") :
-               [ "*** Name: " ++ show symbol ]
+       _ -> addFailedAssertion sym . AssertFailureSimError $
+         if isJust lookedUp
+         then mconcat [ "Allocation associated with global symbol \""
+                      , name
+                      , "\" is not a pointer of the correct width"
+                      ]
+         else mconcat [ "Global symbol \""
+                      , name
+                      , "\" has no associated allocation"
+                      ]
 
 -- | Add an entry to the global map of the given 'MemImpl'.
 --

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs

@@ -46,6 +46,7 @@ module Lang.Crucible.LLVM.MemModel.Generic
   , writeConstMem
   , copyMem
   , setMem
+  , invalidateMem
   , writeArrayMem
   , writeArrayConstMem
   , pushStackFrameMem
@@ -83,6 +84,7 @@ import qualified Data.Map as Map
 import           Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import           Data.Monoid
+import           Data.Text (Text, unpack)
 import qualified Data.Vector as V
 import           GHC.Generics (Generic, Generic1)
 import           Numeric.Natural
@@ -144,6 +146,8 @@ data WriteSource sym w
     -- @len@ at the destination; @MemArrayStore block Nothing@ writes byte-array
     -- @block@ of unbounded size
   | MemArrayStore (SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)) (Maybe (SymBV sym w))
+    -- | @MemInvalidate len@ flags @len@ bytes as uninitialized.
+  | MemInvalidate Text (SymBV sym w)
 
 data MemWrite sym
     -- | @MemWrite dst src@ represents a write to @dst@ from the given source.
@@ -636,6 +640,55 @@ readMemArrayStore sym w end (LLVMPointer blk read_off) tp write_off arr size rea
             | Nothing <- size = symbolicUnboundedRangeLoad pref tp
       evalMuxValueCtor sym w end varFn subFn rngLd
 
+readMemInvalidate ::
+  forall arch sym w .
+  (1 <= w, IsSymInterface sym) =>
+  sym -> NatRepr w ->
+  EndianForm ->
+  LLVMPtr sym w {- ^ The loaded offset                   -} ->
+  StorageType   {- ^ The type we are reading             -} ->
+  SymBV sym w   {- ^ The destination of the invalidation -} ->
+  Text          {- ^ The error message                   -} ->
+  SymBV sym w   {- ^ The length of the set region        -} ->
+  (StorageType -> LLVMPtr sym w -> ReadMem arch sym (PartLLVMVal arch sym)) ->
+  ReadMem arch sym (PartLLVMVal arch sym)
+readMemInvalidate sym w end (LLVMPointer blk off) tp d msg sz readPrev =
+  do let ld = asUnsignedBV off
+     let dd = asUnsignedBV d
+     let varFn = ExprEnv off d (Just sz)
+     case (ld, dd) of
+       -- Offset if known
+       (Just lo, Just so) ->
+         do let subFn :: RangeLoad Addr Addr -> ReadMem arch sym (PartLLVMVal arch sym)
+                subFn (OutOfRange o tp') = do
+                  o' <- liftIO $ bvLit sym w (bytesToInteger o)
+                  readPrev tp' (LLVMPointer blk o')
+                subFn (InRange _o _tp') =
+                  pure . W4P.Err $ Partial.Invalidated msg
+            case asUnsignedBV sz of
+              Just csz -> do
+                let s = R (fromInteger so) (fromInteger (so + csz))
+                let vcr = rangeLoad (fromInteger lo) tp s
+                liftIO . genValueCtor sym end =<< traverse subFn vcr
+              _ -> evalMuxValueCtor sym w end varFn subFn $
+                     fixedOffsetRangeLoad (fromInteger lo) tp (fromInteger so)
+       -- Symbolic offsets
+       _ ->
+         do let subFn :: RangeLoad OffsetExpr IntExpr -> ReadMem arch sym (PartLLVMVal arch sym)
+                subFn (OutOfRange o tp') = do
+                  o' <- liftIO $ genOffsetExpr sym w varFn o
+                  readPrev tp' (LLVMPointer blk o')
+                subFn (InRange _o _tp') =
+                  pure . W4P.Err $ Partial.Invalidated msg
+            let pref | Just{} <- dd = FixedStore
+                     | Just{} <- ld = FixedLoad
+                     | otherwise = NeitherFixed
+            let mux0 | Just csz <- asUnsignedBV sz =
+                         fixedSizeRangeLoad pref tp (fromInteger csz)
+                     | otherwise =
+                         symbolicRangeLoad pref tp
+            evalMuxValueCtor sym w end varFn subFn mux0
+
 -- | Read a value from memory.
 readMem :: forall arch sym w.
   (1 <= w, IsSymInterface sym) => sym ->
@@ -755,6 +808,7 @@ readMem' sym w end l0 tp0 alignment (MemWrites ws) =
                             MemSet v sz    -> readMemSet sym w end l tp d v sz readPrev
                             MemStore v stp storeAlign -> readMemStore sym w end l tp d v stp alignment storeAlign readPrev
                             MemArrayStore arr sz -> readMemArrayStore sym w end l tp d arr sz readPrev
+                            MemInvalidate msg sz -> readMemInvalidate sym w end l tp d msg sz readPrev
                     sameBlock <- liftIO $ natEq sym blk1 blk2
                     case asConstantPred sameBlock of
                       Just True  -> do
@@ -906,6 +960,7 @@ memWritesSingleton ptr src
       MemStore{} -> True
       MemArrayStore{} -> True
       MemSet{} -> True
+      MemInvalidate{} -> True
       MemCopy{} -> False
 
 memWritesSize :: MemWrites sym -> Int
@@ -1416,6 +1471,18 @@ writeArrayConstMem sym w ptr alignment arr sz m =
      p2 <- isAligned sym w ptr alignment
      return (memAddWrite ptr (MemArrayStore arr sz) m, p1, p2)
 
+-- | Explicitly invalidate a region of memory.
+invalidateMem ::
+  (1 <= w, IsSymInterface sym) =>
+  sym -> NatRepr w ->
+  LLVMPtr sym w {- ^ Pointer -} ->
+  Text          {- ^ Message -} ->
+  SymBV sym w   {- ^ Number of bytes to set -} ->
+  Mem sym -> IO (Mem sym, Pred sym)
+invalidateMem sym w ptr msg sz m =
+  do p <- isAllocatedMutable sym w noAlignment ptr (Just sz) m
+     return (memAddWrite ptr (MemInvalidate msg sz) m, p)
+
 -- | Allocate a new empty memory region.
 allocMem :: AllocType -- ^ Type of allocation
          -> Natural -- ^ Block id for allocation
@@ -1714,6 +1781,8 @@ ppWrite (MemWrite d (MemStore v _ _)) = do
   char '*' <> ppPtr d <+> text ":=" <+> ppTermExpr v
 ppWrite (MemWrite d (MemArrayStore arr _)) = do
   char '*' <> ppPtr d <+> text ":=" <+> printSymExpr arr
+ppWrite (MemWrite d (MemInvalidate msg l)) = do
+  text "invalidate" <+> parens (text $ unpack msg) <+> ppPtr d <+> printSymExpr l
 ppWrite (WriteMerge c (MemWrites x) (MemWrites y)) = do
   text "merge" <$$> ppMerge ppMemWritesChunk c x y
 

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs

@@ -100,6 +100,7 @@ data MemoryLoadError sym =
   | PreviousErrors Text [MemoryLoadError sym]
   | ApplyViewFail ValueView
   | Invalid StorageType
+  | Invalidated Text
   | Other (Maybe String)
     -- ^ TODO: eliminate this constructor, replace with more specific messages
   deriving (Generic)
@@ -132,6 +133,8 @@ ppMemoryLoadError =
       "Failure when applying value view" <+> text (show vw)
     Invalid ty ->
       "Load from invalid memory at type " <+> text (show ty)
+    Invalidated msg ->
+      "Load from explicitly invalidated memory:" <+> text (unpack msg)
     Other msg -> vcat $ [ text "Generic memory load error." ] ++
                    case msg of
                      Just msg' -> [text "Details:", text msg']