Refactor the memory model in preparation for tracking block IDs #174
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The main goals of the refactor are to: 1. Separate the core memory model data structure from the implementation of primitive crucible support operations (only the former need to be augmented for the memory model improvements) 2. Remove unnecessary duplication (e.g., the symbolic sequence has a shared implementation in crucible) 3. Clarify semantics 4. Document interfaces Note that this is a work in progress
They are all exported, so make it clear that they can be used in many places
There are no more undefined cases, I think, but this draft does not account for the pointer validity checks. The next commit will restore those, but factored out so that they are configurable.
There is now less implied code sharing, but this approach will reduce complexity. Now, the `ValidityPolicy` validates and returns the validated term (whatever that means for the backend). All of the logic for term creation is now thus in the `ValidityPolicy`. There are two policies right now: 1. The unsafe policy that just assumes that every operation works out 2. The "conservative" policy that injects undefined pointer terms (as undefined functions) as the original memory model did This paves the way for the future optimistic memory model that generates assertions that must be proved to safely use the simple terms, but would also enable a fallback to the conservative terms when necessary. The major improvements of this are: 1. Removing any direct dependency on the undefined pointers in the crucible extension for macaw 2. Providing a new (and simpler) mechanism for identifying the undefined operations that a term depends on (see notes in the code for the rationale and function)
|
out of date / subsumed |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The main goals of the refactor are to:
primitive crucible support operations (only the former need to be augmented for
the memory model improvements)
implementation in crucible)
Note that this is a work in progress