Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Provisional changes to fix CI #606

Closed
wants to merge 2 commits into from
Closed

Provisional changes to fix CI #606

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
1c7873c
Revert "Merge pull request #593 from GaloisInc/invalidate-memory-opti…
chameco Dec 7, 2019
d079239
Bump crucible version
chameco Dec 7, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion deps/crucible
Open in desktop
Submodule crucible updated 9 files
+1 −0 crucible-llvm/crucible-llvm.cabal
+4 −1 crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs
+0 −1 crucible/src/Lang/Crucible/Simulator/EvalStmt.hs
+11 −0 crux/src/Crux/Config/Common.hs
+23 −10 crux/src/Crux/Goal.hs
+5 −3 what4/src/What4/Expr/Builder.hs
+0 −1 what4/src/What4/Interface.hs
+1 −1 what4/src/What4/Protocol/SMTLib2/Syntax.hs
+1 −1 what4/src/What4/Solver/Yices.hs
28 changes: 4 additions & 24 deletions src/SAWScript/Crucible/LLVM/Override.hs
View file
Open in desktop
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 opts sc cc cs
invalidateMutableAllocs cc cs

traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs))
traverse_ (executePointsTo opts sc cc cs) (ss ^. MS.csPointsTos)
Expand Down Expand Up @@ -1223,16 +1223,13 @@ 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". As an optimization, a memory allocation that
-- is overwritten by a postcondition memory write is not invalidated.
-- "crucible_alloc_global".
invalidateMutableAllocs ::
(?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
Options ->
SharedContext ->
LLVMCrucibleContext arch ->
MS.CrucibleMethodSpecIR (LLVM arch) ->
OverrideMatcher (LLVM arch) RW ()
invalidateMutableAllocs opts sc cc cs = do
invalidateMutableAllocs cc cs = do
sym <- use syminterface
mem <- readGlobal . Crucible.llvmMemVar $ cc ^. ccLLVMContext
sub <- use setupValueSub
Expand Down Expand Up @@ -1270,27 +1267,10 @@ invalidateMutableAllocs opts sc 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 danglingPtrs
) mem $ allocPtrs ++ globalPtrs

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

Expand Down