-
Notifications
You must be signed in to change notification settings - Fork 13.5k
Simplify polonius location-sensitive analysis #143093
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
Open
lqd
wants to merge
9
commits into
rust-lang:master
Choose a base branch
from
lqd:polonius-pre-alpha
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
+1,087
−228
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
The suboptimal error only appears with NLLs due to liveness differences where polonius cannot have as many boring locals.
Remove incomplete handling of kills during traversal for loan liveness to get to a simpler and actionable prototype. This handles the cases, on sufficiently simple examples, that were deferred from NLLs (NLL problem case 3, lending iterators), and is still a good step to put in people's hands without needing to wait for another full implementation. This is a practical cut in scope, but it also shows where are the areas of improvement, that we will explore in the future.
This PR changes a file inside Some changes occurred in src/tools/compiletest cc @jieyouxu |
This comment was marked as resolved.
This comment was marked as resolved.
That includes a filtering lending iterator using GATs from 92985 but it still is not enough to make it practical for real world use due to other GATs limitations.
These are just some sanity checks to ensure NLLs, the polonius alpha analysis, and the datalog implementation behave the same on these common examples.
These tests showcase the same imprecision as NLLs, unlike the datalog implementation, when using reachability as a liveness approximation.
These are example that are similar to the linked-list cursor examples where the alpha shows the same imprecision as NLLs, but can work due to the loans not being live after the loop, or the constraint graph being simple enough that the cfg/subset relationships are the same for reachability and liveness.
Happy to review, but don't expect it for 2 weeks :) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
A-compiletest
Area: The compiletest test runner
A-testsuite
Area: The testsuite used to check the correctness of rustc
S-waiting-on-review
Status: Awaiting review from the assignee but also interested parties.
T-bootstrap
Relevant to the bootstrap subteam: Rust's build system (x.py and src/bootstrap)
T-compiler
Relevant to the compiler team, which will review and decide on the PR/issue.
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 PR reworks the location-sensitive analysis into what we think is a worthwhile subset of the datalog analysis. A sort of polonius alpha analysis that handles NLL problem case 3 and more, but is still using the faster "reachability as an approximation of liveness", as well as the same loans-in-scope computation as NLLs -- and thus doesn't handle full flow-sensitivity like the datalog implementation.
In the last few months, we've identified this subset as being actionable:
The approach in this PR is to try less to have the graph only represent live paths, by checking whether we reach a live region during traversal and recording the loan as live there, instead of equating traversal with liveness like today because it has subtleties with the typeck edges in statements (that could forward loans to the successor point without ensuring their liveness). We can then also simplify these typeck stmt edges. And we also can simplify traversal by removing looking at kills, because that's enough to handle a bunch of NLL problem 3 cases -- and we can gradually support them more and more in traversal in the future, to reduce the approximation of liveness.
There's still some in-progress pieces of work w/r/t opaque types that I'm expecting lcnr's opaque types rework, and amanda's SCCs rework to handle. That didn't seem to show up in tests until I rebased today (and shows lack of test coverage once again) when #142255 introduced a couple of test failures with the new captures rules from edition 2024. It's not unexpected since we know more work is needed with member constraints (and we're not even using SCCs in this prototype yet)
I'll look into these anyways, both for future work, and checking how these other 2 PRs would change things.
I'm not sure the following means a lot until we have some formalism in-place, but:
r? @jackh726
(no rush I know you're deep in phd work and "implmentating" the new trait solver for r-a :p <3)
This also fixes #135646, a diagnostics ICE from the previous implementation.