[analysis] Add an abstraction lattice #8036
Open
+326
−0
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
tlively
force-pushed
the
lattice-abstraction
branch
from
0ed9242 to
82ce454
Compare
The abstraction lattice is composed of increasingly abstract sub-lattices. Elements of the abstraction lattice are variants that may hold the elements of any of its constituent lattices. When elements from different sub-lattices are compared or joined, the more concrete element is first abstracted into the lattice of the other element. Unrelated elements in the same lattice may be abstracted before they are joined. This choice and the abstraction operation itself are provided by CRTP subclasses of Abstraction. This is an important building block for eventually reconstructing PossibleContents on top of the lattice framework.
tlively
force-pushed
the
lattice-abstraction
branch
from
82ce454 to
7b596ad
Compare
kripken
reviewed
Nov 10, 2025
| // template<size_t I, typename E> | ||
| // bool shouldAbstract(const E&. const E&) const | ||
| // | ||
| // shouldAbstract is only queries for unrelated elements. Related elements of |
Member
There was a problem hiding this comment.
Suggested change
| // shouldAbstract is only queries for unrelated elements. Related elements of | |
| // shouldAbstract is only queried for unrelated elements. Related elements of |
| } | ||
|
|
||
| using OddEvenInt = analysis::Flat<uint32_t>; | ||
| using OddEvenBool = analysis::Flat<bool>; |
Member
There was a problem hiding this comment.
What does "odd even int" mean? Every integer is already even or odd. This seems like just an integer?
"odd even bool" I can see as being interpreted as "a boolean saying whether it is even or odd"- is that right?
Member
Author
There was a problem hiding this comment.
Yes, this is just an integer. I could use a namespace instead of the OddEven name prefix, perhaps. Yes, the bool is true for even, false for odd, and top when it can be either.
kripken
reviewed
Nov 10, 2025
| return LESS; | ||
| case NO_RELATION: | ||
| case GREATER: | ||
| return NO_RELATION; |
Member
There was a problem hiding this comment.
I don't follow this. We abstract a, then compare - but we turn that outcome into either "less" or "no"? Why can't we return "greater"or "equal"?
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 abstraction lattice is composed of increasingly abstract
sub-lattices. Elements of the abstraction lattice are variants that may
hold the elements of any of its constituent lattices. When elements from
different sub-lattices are compared or joined, the more concrete element
is first abstracted into the lattice of the other element. Unrelated
elements in the same lattice may be abstracted before they are joined.
This choice and the abstraction operation itself are provided by CRTP
subclasses of Abstraction.
This is an important building block for eventually reconstructing
PossibleContents on top of the lattice framework.