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.
This is a WIP PR to attempt tackling #20.
This tries to contract the CFG to simplify the
subset
computation while still keeping it equivalent (in our limited tests and benchmarks) with regards to the live borrows they propagate.Marked as WIP because:
borrow_live_at
are still correct, completely separating compression from the variant prevents correctly computing errors in the optimized variant, so while tests and our datasets work: it's unknown what this can break. (Even though I'm more and more thinking we should revert the errors computation in the optimized variant, until we know more of what/when/how Polonius will work and which parts should be done here or in rustc. And then when the system is more connected, remove the possible impedance mismatch between the 2, remove duplicated/unneeded work, etc.)There are comments explaining the approach, but it is close to the one described in #20 except in a key point, the
outlives
constraint specified there is ignored: in the polonius analysis, subsets between two points don't interact with theoutlives
facts, onlyregion_live_at
between the 2 points. (In fact, adding this "empty outlives" constraint wouldn't find any of the CFG edges inclap
as compressible. At one point, I also had a constraint where theoutlives
sets for each point had to be equal, before I realized they were not used in the datalog rules, and it removed 5000 additional edges fromclap
).Some numbers, contracting the CFG looks like this:
clap
: 51 896cfg_edge
tuples reduced to 11 027issue-47680
: 61cfg_edge
tuples reduced to 19Once the CFG is contracted, the other facts are also pruned, so that we don't spend time computing intermediary results for points absent from the CFG (some of these might be needed in cases I wasn't able to test yet, I'm just describing the WIP state).
Pruning looks like this on
clap
:borrow_region
: unchanged, 1 886 tupleskilled
: removed 252 tuples out of 980outlives
: removed 408 802 tuples out of 53 4327region_live_at
: removed 896 790 tuples out of 1 076 158There is a
--compress-cfg
flag to the CLI to be able to test on different inputs, and a new dataset input (extracted from rustc) containing code Polonius should reject — useful to test errors manually, until final integration where it will become part of the unit tests.I have tested manually:
ui
tests incompare-mode=polonius
have the same behaviour compressed and uncompressed (by creating a temporary variant -- absent from this PR -- forcing the facts compression and decompressing the live loans before computing the errors) for the Opt computation (as well as the Naive variant which I had modified to produce errors instead of live loans for the manual tests)