Draft: Invalidate memory properly with laxLoadsAndStores

Prior to this change, invalidated memory would always result in an error when
read from. This isn't quite the semantics that we would want when
`laxLoadsAndStores` is enabled, however, since reading should always result in
a symbolic value of some sort. This patch changes the mechanics of
`doInvalidate` and `readMemInvalidate` such that when `laxLoadsAndStores` is
enabled, the memory is given the appropriate semantics depending on whether
`indeterminateLoadBehavior` is `StableSymbolic` or `UnstableSymbolic`.

This adds a `?memOpts :: MemOptions` constraint to `doInvalidate`, which is a
breaking API change. That being said, the only call site that I am aware of for
the `doInvalidate` function is SAW, so the breakage should be relatively minor.
Furthermore, there were no test cases for `doInvalidate` before this, so this
patch adds some.

crucible-llvm/CHANGELOG.md

@@ -12,5 +12,5 @@
     `initializeAllMemory`, `initializeMemoryConstGlobals`, `populateGlobals`,
     `populateAllGlobals`, and `populateConstGlobals`
   * `Lang.Crucible.LLVM.MemModel`:
-    `doAlloca`, `doCalloc`, `doMalloc`, `doMallocUnbounded`, `mallocRaw`,
-    `mallocConstRaw`, `allocGlobals`, and `allocGlobal`
+    `doAlloca`, `doCalloc`, `doInvalidate`, `doMalloc`, `doMallocUnbounded`,
+    `mallocRaw`, `mallocConstRaw`, `allocGlobals`, and `allocGlobal`

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

@@ -566,10 +566,7 @@ doAlloca sym mem sz alignment loc = do
   let mem'  = mem{ memImplHeap = heap' }
   mem'' <- if laxLoadsAndStores ?memOpts
                 && indeterminateLoadBehavior ?memOpts == StableSymbolic
-           then do bytes <- freshConstant sym emptySymbol
-                              (BaseArrayRepr (Ctx.singleton $ BaseBVRepr ?ptrWidth)
-                                             (BaseBVRepr (knownNat @8)))
-                   doArrayStore sym mem' ptr alignment bytes sz
+           then doStoreStableSymbolic sym mem ptr (Just sz) alignment
            else pure mem'
   pure (ptr, mem'')
 
@@ -710,12 +707,7 @@ doMallocSize sz sym allocType mut loc mem alignment = do
                 && mut == G.Mutable
                 && allocType == G.HeapAlloc
                 && indeterminateLoadBehavior ?memOpts == StableSymbolic
-           then do bytes <- freshConstant sym emptySymbol
-                              (BaseArrayRepr (Ctx.singleton $ BaseBVRepr ?ptrWidth)
-                                             (BaseBVRepr (knownNat @8)))
-                   case sz of
-                     Just sz' -> doArrayStore sym mem' ptr alignment bytes sz'
-                     Nothing  -> doArrayStoreUnbounded sym mem' ptr alignment bytes
+           then doStoreStableSymbolic sym mem' ptr sz alignment
            else pure mem'
   return (ptr, mem'')
 
@@ -854,7 +846,8 @@ doMemset sym w mem dest val len = do
   return mem{ memImplHeap = heap' }
 
 doInvalidate ::
-  (1 <= w, IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym) =>
+  ( 1 <= w, IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym
+  , ?memOpts :: MemOptions ) =>
   sym ->
   NatRepr w ->
   MemImpl sym ->
@@ -865,7 +858,12 @@ doInvalidate ::
 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)
+  (heap', p) <- if laxLoadsAndStores ?memOpts &&
+                   indeterminateLoadBehavior ?memOpts == StableSymbolic
+                then do p <- G.isAllocatedMutable sym PtrWidth noAlignment dest (Just len') (memImplHeap mem)
+                        mem' <- doStoreStableSymbolic sym mem dest (Just len') noAlignment
+                        pure (memImplHeap mem', p)
+                else G.invalidateMem sym PtrWidth dest msg len' (memImplHeap mem)
 
   let gsym = unsymbol <$> isGlobalPointer (memImplSymbolMap mem) dest
   let mop = MemInvalidateOp msg gsym dest len (memImplHeap mem)
@@ -1038,6 +1036,25 @@ doPtrAddOffset sym m x@(LLVMPointer blk _) off = do
     in assertUndefined sym callStack v (UB.PtrAddOffsetOutOfBounds (RV x) (RV off))
   return x'
 
+-- | Store a fresh symbolic value of the appropriate size in the supplied
+-- pointer. This is used in various spots whenever 'laxLoadsAndStores' is
+-- enabled and 'indeterminateLoadBehavior' is set to 'StableSymbolic'.
+doStoreStableSymbolic ::
+   (IsSymInterface sym, HasPtrWidth wptr, Partial.HasLLVMAnn sym) =>
+  sym ->
+  MemImpl sym ->
+  LLVMPtr sym wptr       {- ^ destination       -} ->
+  Maybe (SymBV sym wptr) {- ^ allocation size   -} ->
+  Alignment              {- ^ pointer alignment -} ->
+  IO (MemImpl sym)
+doStoreStableSymbolic sym mem ptr mbSz alignment = do
+  bytes <- freshConstant sym emptySymbol
+             (BaseArrayRepr (Ctx.singleton (BaseBVRepr ?ptrWidth))
+                            (BaseBVRepr (knownNat @8)))
+  case mbSz of
+    Just sz -> doArrayStore sym mem ptr alignment bytes sz
+    Nothing -> doArrayStoreUnbounded sym mem ptr alignment bytes
+
 -- | This predicate tests if the pointer is a valid, live pointer
 --   into the heap, OR is the distinguished NULL pointer.
 isValidPointer ::

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

@@ -41,6 +41,7 @@ module Lang.Crucible.LLVM.MemModel.Generic
   , allocAndWriteMem
   , readMem
   , isValidPointer
+  , isAllocatedMutable
   , isAllocatedAlignedPointer
   , notAliasable
   , writeMem
@@ -634,7 +635,8 @@ readMemArrayStore sym w end mop (LLVMPointer blk read_off) tp write_off arr size
 
 readMemInvalidate ::
   forall sym w .
-  (1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>
+  ( 1 <= w, IsSymInterface sym, HasLLVMAnn sym
+  , ?memOpts :: MemOptions ) =>
   sym -> NatRepr w ->
   EndianForm ->
   MemoryOp sym w ->
@@ -645,7 +647,12 @@ readMemInvalidate ::
   SymBV sym w   {- ^ The length of the set region        -} ->
   (StorageType -> LLVMPtr sym w -> ReadMem sym (PartLLVMVal sym)) ->
   ReadMem sym (PartLLVMVal sym)
-readMemInvalidate sym w end mop (LLVMPointer blk off) tp d msg sz readPrev =
+readMemInvalidate sym w end mop (LLVMPointer blk off) tp d msg sz readPrev
+  | laxLoadsAndStores ?memOpts &&
+    indeterminateLoadBehavior ?memOpts == UnstableSymbolic =
+  liftIO (Partial.totalLLVMVal sym <$> freshLLVMVal sym tp)
+
+  | otherwise =
   do let ld = BV.asUnsigned <$> asBV off
      let dd = BV.asUnsigned <$> asBV d
      let varFn = ExprEnv off d (Just sz)

crucible-llvm/test/TestMemory.hs

@@ -1,7 +1,9 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
 module TestMemory
@@ -36,6 +38,7 @@ import           Lang.Crucible.LLVM.DataLayout ( noAlignment )
 import qualified Lang.Crucible.LLVM.DataLayout as LLVMD
 import           Lang.Crucible.LLVM.MemModel ( doLoad, doStore, projectLLVM_bv, ptrAdd )
 import qualified Lang.Crucible.LLVM.MemModel as LLVMMem
+import qualified Lang.Crucible.LLVM.MemModel.Generic as LLVMMemG
 
 
 memoryTests :: T.TestTree
@@ -49,6 +52,7 @@ memoryTests = T.testGroup "Memory"
   , testPointerStore
   , testMemArrayCopy
   , testMemArraySet
+  , testMemInvalidate
   ]
 
 
@@ -429,6 +433,68 @@ testMemAllocs =
      res <- checkSat sym =<< What4.notPred sym assertion
      True @=? W4Sat.isUnsat res
 
+-- | This test case checks that 'doInvalidate' behaves as expected with and
+-- without 'laxLoadsAndStores' enabled.
+testMemInvalidate :: T.TestTree
+testMemInvalidate =
+  testCase "memory invalidation" $ withMem LLVMD.BigEndian $ \(sym :: sym) mem0 ->
+  do sz <- What4.bvLit sym ?ptrWidth $ BV.mkBV ?ptrWidth 64
+     let long_type_repr = Crucible.baseToType $ What4.BaseBVRepr $ knownNat @64
+         long_storage_type = LLVMMem.bitvectorType 8
+     zero_val <- What4.bvLit sym (knownNat @64) (BV.zero knownNat)
+
+     let withInvalidatedReadVal :: LLVMMem.MemOptions
+                                -> (LLVMMem.PartLLVMVal sym -> IO a)
+                                -> IO a
+         withInvalidatedReadVal memOpts k = do
+           let ?memOpts = memOpts
+           -- First, allocate some memory on the stack...
+           (ptr, mem1) <- LLVMMem.doAlloca sym mem0 sz noAlignment "<alloca>"
+           -- ...write some value to it (the exact value is unimportant)...
+           mem2 <- LLVMMem.doStore sym mem1 ptr
+                                   long_type_repr long_storage_type
+                                   noAlignment zero_val
+           -- ...invalidate the memory...
+           mem3 <- LLVMMem.doInvalidate sym ?ptrWidth mem2 ptr "<invalidate>" sz
+           -- ...and finally, read from the invalidated memory.
+           partVal <- LLVMMemG.readMem sym ?ptrWidth Nothing ptr
+                                       long_storage_type noAlignment
+                                       (LLVMMem.memImplHeap mem3)
+           k partVal
+
+         testLaxInvalidatedRead :: String -> LLVMMem.IndeterminateLoadBehavior -> IO ()
+         testLaxInvalidatedRead stability indeterminateLoadBehavior =
+           withInvalidatedReadVal (?memOpts{ LLVMMem.laxLoadsAndStores = True
+                                           , LLVMMem.indeterminateLoadBehavior = indeterminateLoadBehavior
+                                           }) $ \partVal ->
+           case partVal of
+             LLVMMem.NoErr p _val -> do
+               res <- checkSat sym p
+               True @=? W4Sat.isSat res
+             LLVMMem.Err p -> assertFailure $ unlines
+               [ "Reading from invalidated, " ++ stability ++ "-symbolic memory unexpectedly failed"
+               , "Predicate: " ++ show p
+               ]
+
+     -- Test with laxLoadsAndStores disabled, where reading from invalidated
+     -- memory should result in an error.
+     withInvalidatedReadVal (?memOpts{LLVMMem.laxLoadsAndStores = False}) $ \partVal ->
+       case partVal of
+         LLVMMem.Err p -> do
+           res <- checkSat sym p
+           True @=? W4Sat.isUnsat res
+         LLVMMem.NoErr p val -> assertFailure $ unlines
+           [ "Reading from invalidated memory unexpectedly succeeded"
+           , "Predicate: " ++ show p
+           , "LLVM value read: " ++ show val
+           ]
+
+     -- Test with laxLoadsAndStores enabled, using both the
+     -- StableSymbolic and UnstableSymbolic settings for
+     -- indeterminateLoadBehavior. Here, reading from invalidated memory should succeed.
+     testLaxInvalidatedRead "stable" LLVMMem.StableSymbolic
+     testLaxInvalidatedRead "unstable" LLVMMem.UnstableSymbolic
+
 -- | Test storing and retrieving pointer in an SMT-backed array memory model
 testPointerStore :: T.TestTree
 testPointerStore = testCase "pointer store" $ withMem LLVMD.BigEndian $ \sym mem0 -> do