Fancy assumptions #769
Fancy assumptions #769
Conversation
This abstracts more fully over the types of assumptions and assertions and delays the specialization to @LabeledPred@. It removes some intermedidate type aliaes that seemed mostly to be confusing. This sets the stage for modifying the representation of assumptions and assertions.
Instead of a flat sequence of assumptions, we now have a tree structure based on mux values.
This allows us to track program events alongside the existing assumption tracking. Using this, we can reconstruct a linear sequences of events that occured along the program run when we find counterexamples to proof goals. Initially, the only event we track is the creation of user-requested symbolic variables, but others are planned. By tracking symbolic variables this way, we can accurately reconstruct a linear sequence of values to replay, which allows us to fix #587.
These are no longer necessary.
In crux-llvm, we need to make sure that declarations are emitted for each of the types so the counterexample code will compile. Previously, this was handed by prepopulating the Model map, but this is fragile and mixes crux-llvm concerns into crux proper. Here, we split this concern out, and push the handling of this issue into crux-llvm, where it belongs.
It is better to use the `ProcessedGoals` record instead.
It will be unnecessary when we properly implement event-based program location tracking.
when counterexamples are found.
Use this feature in crux to record a detailed sequence of program points that can later be used to reconstruct a concrete program run.
There was a problem hiding this comment.
Ooh, exciting! Does this fix any bugs on its own, or is this a preparatory refactoring for future efforts? I see quite a bit of refactoring around data types in Crux.Types (e.g., NotProvedGoal now has a list of CrucibleAssumptions)—is there a way to test out this new code by using crux itself?
I've done a quick pass over the code, mostly commenting on typos and minor stylistic nits. If there is a part of the patch that you feel deserves closer scrutiny, let me know.
|
@RyanGlScott This PR fixes #587, which is related to incorrect counterexample generation, and is a crux-specific bug. I intend to add a test case, but we'll need to add something to the test harness to be able to observe the concrete model generated, which is why I haven't done it yet. But more generally, I think this should help a lot with the counterexample witness generation you've been looking into. |
I see. In that case, I'd be fine with just opening another issue to serve as a reminder to augment the test suite later.
Indeed, I'm currently looking into trying to debug-print these |
Refactor various aspects of assumption handling. The main aim here is to allow "events" to be tracked alongside the logical assumptions that are already tracked. This will allow us to concretely reconstruct a linear sequence of events when counterexamples to proof goals are found so that we can replay the creation of symbolic variables and identify sequences of program points the run passed through.