Refactor #newUndefined
#20
Merged
Conversation
This file contains hidden or 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
janvrany
force-pushed
the
pr/refactor-newUndefined
branch
2 times, most recently
from
27d0b9f to
b8e245e
Compare
A Jib program may contain enums, structs and unions. These get
ultimately reduced to Z3 datatypes. For this reason, each program must
have its own Z3 context in which datatypes are defined. Also, this
context is the one to use when creating Z3 nodes representing "values".
This commit implements this by holding on a Z3 context from program's
environment and making sure semantic analysis and interpreter set this
context as current when analyzing and interpreting. This prompted
1. creation of specialized `JibProgramEnvironment` that holds on such Z3
context and
2. basic "analysis" that fills in environment for program and
defined `fn`s, `let`s and `register`s
This commit adds `#sort` method to type nodes, returning the Z3 sort that corresponds to given (Jib) type. For now, it is implemented only for "scalar" types (bitvectors, numbers, bool). Support for "user defined" types (enums, structs, unions) will come later.
This commit refactor `#newUndefined`. The implementation was temporary and completely bogus. This commits replaces the old implementation with new one which simply return a fresh Z3 variable of corresponding sort, prefixed with string "undefined" to make it easier to spot. While at it, move the method to `Sail-Jib-Interpreter` package.
janvrany
force-pushed
the
pr/refactor-newUndefined
branch
from
b8e245e to
a54579f
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
No description provided.