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.
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add dataflow analysis of enum variants #96991
Add dataflow analysis of enum variants #96991
Changes from all commits
468742b
cd37d5c
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the documentation update. What is the partial order under which this is a lattice? If this is a well-known result from theory (I'm not terribly familar) feel free to just provide a link to a reference
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
there's no theory, it's just that each fact gets inserted at a specific location ( body + stmt idx ), so I attempt to keep later facts more than more recent ones, like an LRU cache.
What I mean is that we could represent the entire set of facts using a
HashMap<Idx, Value>
, but this will grow linearly with the size of the program (or at least whatever is being analyzed). Instead, to use constant space, we keep a set of facts that evicts older ones, which we assume are no longer relevant, and replaces them with the most recent updates. This a strict subset of theHashMap<Idx, Value>
, so should also be a lattice.This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok, yeah, sorry, what I said before was silly. Yes, the subset partial order is an option, but it's not clear to me that that results in a lattice. Under the subset partial order the least upper bound of two states each storingN
facts is a state that would have to store2*N
facts, which you can't representI should start thinking before I say things. Yeah, ok, this does seem like a lattice - let me go and re-read some stuff then
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, ok I thought about this a bunch more and I think it's ok. We can imagine this fact cache as implicitly storing
for each
I
. Locals which do not have an entry in the fact cache are implicitlyTop
. The partial order within eachLocalResult
is thenBot < Fact(F, min) < ... < Fact(F, max) < Top
for eachF
, and the partial order for the fact cache as a whole is then the product partial order. This does indeed form a lattice. This should be documented though.