Compositional crux-mir #1117
Compositional crux-mir #1117
Conversation
There was a problem hiding this comment.
This looks great to me. I left a few comments that might suggest changes, but I'll leave that up to you. There were also some aspects of the MIR-related details that I probably can't properly review due to my lack of familiarity with the underlying MIR implementation for Crucible. I appreciate how many tests you included, though, and if all of those are passing I'm quite happy to merge this.
| Map VarIndex Term {- ^ initial term substitution -} -> | ||
| Set VarIndex {- ^ initial free variables -} -> | ||
| W4.ProgramLoc {- ^ override location information -} -> | ||
| OverrideMatcher ext md a {- ^ matching action -} -> | ||
| IO (Either (OverrideFailure ext) (a, OverrideState ext)) | ||
| OverrideMatcher' sym ext md m a {- ^ matching action -} -> |
There was a problem hiding this comment.
Good to know that this doesn't need to be in IO!
| @@ -0,0 +1,237 @@ | |||
| {-# LANGUAGE LambdaCase #-} | |||
There was a problem hiding this comment.
I wonder whether this test framework is something that could be more shared between tools.
|
|
||
| -- Handle return value and post-state PointsTos | ||
|
|
||
| -- TODO: clobber all writable memory that's accessible in the pre state |
There was a problem hiding this comment.
How easily could this be implemented now? Or should we leave it until later?
There was a problem hiding this comment.
I actually did it already, but forgot to remove the comment. The mechanism is a little bit indirect: for each accessible location, add_arg not only adds a pre-state PointsTo (representing a constraint on the contents of the initial memory), but also adds a post-state PointsTo that causes the value to be overwritten with a fresh symbolic variable.
|
Following on my test comment, I'd love to see those tests integrated into CI, but I know that'll require adding some substantial chunks to the configuration to make sure all the Rust tools are installed. |
Should I try copying over the relevant parts of the GaloisInc/crucible CI config? Or is the setup going to be complex enough that I should just leave it as a separate issue? |
I think it's reasonable to leave that for a separate issue. We might also be able to get help from @LisannaAtGalois at some point. |
spernsteiner
force-pushed
the
sp/crux-mir-comp
branch
2 times, most recently
from
7de3339 to
1fadf37
Compare
spernsteiner
force-pushed
the
sp/crux-mir-comp
branch
from
1fadf37 to
1342765
Compare
spernsteiner
force-pushed
the
sp/crux-mir-comp
branch
from
58e4751 to
5806e0c
Compare
RyanGlScott
added
the
subsystem: crucible-mir
RyanGlScott
added
the
subsystem: crucible-mir-comp
This branch adds
crux-mir-comp, a variant ofcrux-mirthat supports compositional reasoning. This is a proof-of-concept implementation, which includes the essential functionality but is missing some usability features.For details of the design, see
crux-mir-comp/DESIGN.md.The corresponding crucible/crux-mir changes are in GaloisInc/crucible#659.