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

mir_unsafe_assume_spec #1959

Merged
merged 5 commits into from
Nov 22, 2023
Merged

mir_unsafe_assume_spec #1959

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0a6be48
Add maConditionMetadata to MirAllocSpec
RyanGlScott Aug 29, 2023
6234628
Refactor: Move checkCompatibleTys, readMaybeType, firstPointsToReferent
RyanGlScott Aug 29, 2023
69f0dc5
Use ppMIRVal in mkStructuralMismatch
RyanGlScott Aug 29, 2023
256251d
Refactor: Move some definitions to SAWScript.Crucible.Common.Override
RyanGlScott Aug 29, 2023
ac46b5b
`mir_unsafe_assume_spec`
RyanGlScott Aug 27, 2023
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
31 changes: 15 additions & 16 deletions crucible-mir-comp/src/Mir/Compositional/Builder.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,9 @@ addArg tpr argRef msb =
sv <- regToSetup bak Pre (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv

void $ forNewRefs Pre $ \fr -> do
let len = fr ^. frAllocSpec . maLen
let allocSpec = fr ^. frAllocSpec
let len = allocSpec ^. maLen
let md = allocSpec ^. maConditionMetadata
svPairs <- forM [0 .. len - 1] $ \i -> do
-- Record a points-to entry
iSym <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ fromIntegral i
Expand All @@ -267,12 +269,6 @@ addArg tpr argRef msb =
return (sv, sv')

let (svs, svs') = unzip svPairs
let md = MS.ConditionMetadata
{ MS.conditionLoc = loc
, MS.conditionTags = mempty
, MS.conditionType = "add argument value"
, MS.conditionContext = ""
}
msbSpec . MS.csPreState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs :)
msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs' :)

Expand All @@ -293,7 +289,6 @@ setReturn tpr argRef msb =
ovrWithBackend $ \bak ->
execBuilderT msb $ do
let sym = backendGetSym bak
loc <- liftIO $ W4.getCurrentProgramLoc sym
let ty = case msb ^. msbSpec . MS.csRet of
Just x -> x
Nothing -> M.TyTuple []
Expand All @@ -303,7 +298,9 @@ setReturn tpr argRef msb =
sv <- regToSetup bak Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv

void $ forNewRefs Post $ \fr -> do
let len = fr ^. frAllocSpec . maLen
let allocSpec = fr ^. frAllocSpec
let len = allocSpec ^. maLen
let md = allocSpec ^. maConditionMetadata
svs <- forM [0 .. len - 1] $ \i -> do
-- Record a points-to entry
iSym <- liftIO $ W4.bvLit sym knownNat $ BV.mkBV knownNat $ fromIntegral i
Expand All @@ -312,12 +309,6 @@ setReturn tpr argRef msb =
let shp = tyToShapeEq col (fr ^. frMirType) (fr ^. frType)
regToSetup bak Post (\_tpr expr -> SAW.mkTypedTerm sc =<< eval expr) shp rv

let md = MS.ConditionMetadata
{ MS.conditionLoc = loc
, MS.conditionTags = mempty
, MS.conditionType = "set return value"
, MS.conditionContext = ""
}
msbSpec . MS.csPostState . MS.csPointsTos %= (MirPointsTo md (MS.SetupVar (fr ^. frAlloc)) svs :)

msbSpec . MS.csRetValue .= Just sv
Expand Down Expand Up @@ -779,7 +770,15 @@ refToAlloc bak p mutbl ty tpr ref len = do
Nothing -> do
alloc <- use msbNextAlloc
msbNextAlloc %= MS.nextAllocIndex
let fr = FoundRef alloc (MirAllocSpec tpr mutbl ty len) ref
let sym = backendGetSym bak
loc <- liftIO $ W4.getCurrentProgramLoc sym
let md = MS.ConditionMetadata
{ MS.conditionLoc = loc
, MS.conditionTags = mempty
, MS.conditionType = "reference-to-allocation conversion"
, MS.conditionContext = ""
}
let fr = FoundRef alloc (MirAllocSpec md tpr mutbl ty len) ref
msbPrePost p . seRefs %= (Seq.|> Some fr)
msbPrePost p . seNewRefs %= (Seq.|> Some fr)
return alloc
Expand Down
Loading
Loading