Skip to content

Commit

Permalink
Optimize memory invalidation in postcondition use.
Browse files Browse the repository at this point in the history
A memory allocation that is overwritten by a postcondition memory
write not invalidated anymore.
  • Loading branch information
andreistefanescu committed Nov 22, 2019
1 parent 0177adb commit 604a612
Showing 1 changed file with 24 additions and 4 deletions.
28 changes: 24 additions & 4 deletions src/SAWScript/Crucible/LLVM/Override.hs
Original file line number Diff line number Diff line change
Expand Up @@ -665,7 +665,7 @@ executeCond opts sc cc cs ss = do
(ss ^. MS.csFreshPointers)
OM (setupValueSub %= Map.union ptrs)

invalidateMutableAllocs cc cs
invalidateMutableAllocs opts sc cc cs

traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs))
traverse_ (executePointsTo opts sc cc cs) (ss ^. MS.csPointsTos)
Expand Down Expand Up @@ -1225,13 +1225,16 @@ learnPred sc cc loc prepost t =

-- | Invalidate all mutable memory that was allocated in the method spec
-- precondition, either through explicit calls to "crucible_alloc" or to
-- "crucible_alloc_global".
-- "crucible_alloc_global". As an optimization, a memory allocation that
-- is overwritten by a postcondition memory write is not invalidated.
invalidateMutableAllocs ::
(?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
Options ->
SharedContext ->
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
OverrideMatcher (LLVM arch) RW ()
invalidateMutableAllocs cc cs = do
invalidateMutableAllocs opts sc cc cs = do
sym <- use syminterface
mem <- readGlobal . Crucible.llvmMemVar $ cc ^. ccLLVMContext
sub <- use setupValueSub
Expand Down Expand Up @@ -1269,10 +1272,27 @@ invalidateMutableAllocs cc cs = do
)
_ -> pure Nothing

-- set of (concrete base pointer, size) for each postcondition memory write
postPtrs <- Set.fromList <$> mapM
(\(LLVMPointsTo _loc ptr val) -> do
(_, Crucible.LLVMPointer blk _) <- resolveSetupValue opts cc sc cs Crucible.PtrRepr ptr
sz <- (return . Crucible.storageTypeSize)
=<< Crucible.toStorableType
=<< typeOfSetupValue cc (MS.csAllocations cs) (MS.csTypeNames cs) val
return (W4.asNat blk, sz))
(cs ^. MS.csPostState ^. MS.csPointsTos)

-- filter out each allocation overwritten by a postcondition write
let danglingPtrs = filter
(\((Crucible.LLVMPointer blk _), sz, _) ->
Set.notMember (W4.asNat blk, sz) postPtrs)
(allocPtrs ++ globalPtrs)

-- invalidate each allocation that is not overwritten by a postcondition write
mem' <- foldM (\m (ptr, sz, msg) ->
liftIO $ Crucible.doInvalidate sym ?ptrWidth m ptr msg
=<< W4.bvLit sym ?ptrWidth (Crucible.bytesToInteger sz)
) mem $ allocPtrs ++ globalPtrs
) mem danglingPtrs

writeGlobal (Crucible.llvmMemVar $ cc ^. ccLLVMContext) mem'

Expand Down

0 comments on commit 604a612

Please sign in to comment.