[WIP] term annotations #437
Closed
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
types. This propigates this new parameter to a variety of other types and touches quite a few type signatures. I beleive this patch is a purely type-level change.
This makes the argument order considerably more uniform and less confusing.
…tation type parameter.
push minimial corrections into downstream packages. This mostly involves selecting "dummy" annotations when creating symbolic backends.
…llvm. Instead, a language-extension expression former `LLVM_SideConditions` has been added that directly references the `LLVM_SafetyCondition` type.
`PartialExpr` and `AssertionClassifier` class constraints. The LLVM memory model is now the only place where assertion trees are used. Next, they will instead be replaced by internal predicate annotations.
verifying that the representation details don't leak very far. MemModel.Generic is the only other module impacted.
is a constructor of the `Expr` datatype rather than the `App` datatype. This has a few advantages, among them that the `App` datatype requires fewer type parameters this way. In addition, we lift the restriction that the annotation type be hashable and have an equality test. Instead, we allocate a fresh nonce when `annotateTerm` is called and use that as a proxy for the annotation. As a result, hash-consing will not coallesce idential terms with the same annotations. I expect this will be an uncommon occurence. However, it means that the equality test for identical terms will be quick, regardless of the structure of the annotations, and avoids propigating annoying class restrictions throughout the code.
partial llvm values.
predicate annotations instead.
|
I'm thinking this isn't the correct approach anymore. |
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.
Fairly major refactoring to replace the
AssertionTreeand related data structures with inline term annotations. This hopefully will fix performance problems, and also allow more sophisticated proof condition explanations.This will have relatively significant client package impacts, so I'm spinning up this PR before its fully done to have CI assist with figuring out where updates need to be made.