Add cache for base pointers with array stores.

GaloisInc · Jun 27, 2023 · 9277c1f · 9277c1f
1 parent 8eaedd7
commit 9277c1f
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 5 deletions.
diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
@@ -1452,7 +1452,7 @@ writeArrayMemWithAllocationCheck is_allocated sym w ptr alignment arr sz m =
 
        _ -> return default_m
 
-     return (m', p1, p2)
+     return (memInsertArrayBlock (llvmPointerBlock ptr) m', p1, p2)
 
 -- | Write an array to memory.
 --
@@ -1667,6 +1667,7 @@ asMemAllocationArrayStore ::
   IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8), (SymBV sym w)))
 asMemAllocationArrayStore sym w ptr mem
   | Just blk_no <- asNat (llvmPointerBlock ptr)
+  , memMemberArrayBlock (llvmPointerBlock ptr) mem
   , [SomeAlloc _ _ (Just sz) _ _ _] <- List.nub (possibleAllocs blk_no mem)
   , Just Refl <- testEquality w (bvWidth sz) =
      do memo_nothing <- putMemoIO $ return Nothing
@@ -1688,6 +1689,7 @@ asMemMatchingArrayStore ::
   IO (Maybe (Pred sym, SymArray sym (SingleCtx (BaseBVType w)) (BaseBVType 8)))
 asMemMatchingArrayStore sym w ptr sz mem
   | Just blk_no <- asNat (llvmPointerBlock ptr)
+  , memMemberArrayBlock (llvmPointerBlock ptr) mem
   , Just off <- asBV (llvmPointerOffset ptr) = do
     memo_nothing <- putMemoIO $ return Nothing
     findArrayStore sym w blk_no off sz memo_nothing $ memWritesAtConstant blk_no $ memWrites mem

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs
@@ -57,6 +57,8 @@ module Lang.Crucible.LLVM.MemModel.MemLog
   , emptyChanges
   , emptyMem
   , memEndian
+  , memInsertArrayBlock
+  , memMemberArrayBlock
 
     -- * Pretty printing
   , ppType
@@ -87,6 +89,8 @@ import qualified Data.List.Extra as List
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Maybe (mapMaybe)
+import           Data.Set (Set)
+import qualified Data.Set as Set
 import           Data.Text (Text)
 import           Numeric.Natural
 import           Prettyprinter
@@ -326,7 +330,7 @@ data MemWrite sym
 -- implementation is able to efficiently merge memories, but requires
 -- that one only merge memories that were identical prior to the last
 -- branch.
-data Mem sym = Mem { memEndianForm :: EndianForm, _memState :: MemState sym }
+data Mem sym = Mem { memEndianForm :: EndianForm, _memState :: MemState sym, memArrayBlocks :: Set Natural }
 
 memState :: Lens' (Mem sym) (MemState sym)
 memState = lens _memState (\s v -> s { _memState = v })
@@ -417,11 +421,21 @@ emptyChanges :: MemChanges sym
 emptyChanges = (mempty, mempty)
 
 emptyMem :: EndianForm -> Mem sym
-emptyMem e = Mem { memEndianForm = e, _memState = EmptyMem 0 0 emptyChanges }
+emptyMem e = Mem { memEndianForm = e, _memState = EmptyMem 0 0 emptyChanges, memArrayBlocks = Set.empty }
 
 memEndian :: Mem sym -> EndianForm
 memEndian = memEndianForm
 
+memInsertArrayBlock :: IsExprBuilder sym => SymNat sym -> Mem sym -> Mem sym
+memInsertArrayBlock blk mem = case asNat blk of
+  Just blk_no -> mem { memArrayBlocks = Set.insert blk_no (memArrayBlocks mem) }
+  Nothing -> mem { memArrayBlocks = Set.empty }
+
+memMemberArrayBlock :: IsExprBuilder sym => SymNat sym -> Mem sym -> Bool
+memMemberArrayBlock blk mem = case asNat blk of
+  Just blk_no -> Set.member blk_no (memArrayBlocks mem)
+  Nothing -> False
+
 
 --------------------------------------------------------------------------------
 -- Pretty printing
@@ -744,5 +758,6 @@ concMem ::
   sym ->
   (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
   Mem sym -> IO (Mem sym)
-concMem sym conc (Mem endian st) =
-  Mem endian <$> concMemState sym conc st
+concMem sym conc mem = do
+  conc_st <- concMemState sym conc $ mem ^. memState
+  return $ mem & memState .~ conc_st