Scalable Polonius support on nightly

[nikomatsakis]

Metadata
Point of contact	@lqd
Team(s)	types
Goal document	2025h1/Polonius

Summary

Keep working on implementing a native rustc version of the Polonius next generation borrow checking algorithm, that would scale better than the previous datalog implementation, continuing from the 2024h2 goal.

Tasks and status

• Design review (@nikomatsakis)
• Factoring out higher-ranked concerns from the main path (@amandasystems)
  • rewrite invalid universe constraints with outlives 'static constraints — PR #123720
  • completely remove placeholders — in progress, PR #130227
• Replace parts of the borrow checker with location-insensitive Polonius
• Location-sensitive prototype on nightly (@lqd)
  • create structures for location-dependent outlives constraints
  • build new constraint graph from typeck constraints and liveness constraints
  • update NLLs for required changes to local & region liveness, loan liveness & loan scopes, (possibly unreachable) kills, bidirectional traversal & active loans
  • land on nightly — PRs #134268, #134315, #134378, #134670, #134914, #134920, #134980 and #135290.
• Debugging / dump tool for analysis of location-sensitive analysis (@lqd), PRs #136031, #136104 and #136278
• Tests and validation of location-sensitive Polonius (@lqd) — in progress
  • limit regressions about diagnostics when using the new constraints on diagnostics tailored to the old constraints — PR #136299
  • make the full test suite pass — in progress
  • do a crater run for assertions and backwards-compatibility
  • expand test suite with tests about the new capabilities
• Location-sensitive pass on nightly, tested on CI (@lqd)
• Standard reviews (types ): thanks to @jackh726 and @matthewjasper for the many reviews.

[lqd]

I can't modify the issue text, but the following is needed to fix the link:

[pc3]: https://blog.rust-lang.org/inside-rust/2023/10/06/polonius-update.html#background-on-polonius

[nikomatsakis]

This issue is intended for status updates only.

For general questions or comments, please contact the owner(s) directly.

[lqd]

Status update:

• we've completed the first task of removing universe errors out of the main path and moving higher-ranked concerns out of the borrowck, in @amandasystems' PR #123720. During SCC construction, we now detect these constraints and rewrite them to regular constraints outliving 'static. We have possible improvements in mind that we can do in the future here, but we've also just started trying to remove placeholders, by replacing them with constraints again.

• we've also made more progress on the location-sensitive analysis, though not as much as we'd like. By now we have a "localized" constraint graph to implement propagation in a flow-sensitive manner, with constraints from typeck and liveness, and have it hooked it up to the existing borrow checking in non-lexical scope and active loans computation. It's still buggy though: there are a couple hundred of UI test failures at the moment, including important cases that don't work yet. Some of these failures are due to the diagnostics subsystem not yet handling flow-sensitive concerns. The next immediate steps are to analyze and fix the test failures, and to help with this we're also expanding the existing NLL logging, MIR dumps, and visualizations.

• and we've also started work on the item to use more of the polonius model in the borrow-checker, though we're still in the preparation phase to have an overview of what we want, need, and can change here. Currently, the gated location-insensitive analysis is mainly implemented in the borrowck dataflow analyses, but we want to expand this to replace code and data existing in both models, avoid duplicate work, and simplify the implementation. For example, we can either change components internals to do so, or have them generic enough to work with both models: this applies at least to region liveness, region values, SCC values, etc. We also want to do this unification while taking the location-sensitive requirements into account, as well as constraints that existing downstream code can't be impacted or changed too much for now (e.g. diagnostics).

[lqd]

Key developments:

• We were able to fix a bunch of test failures due to some off-by-one errors (in both typeck and livenesss constraints) from the old "mid-points" that don't exist anymore.
• We're still debugging the large number of test failures, and continued the design work on the unified debugging visualization to help with that. We're currently manually doing the tracing work, and after a few run-throughs within the team, should be able to automate it.
• We've also focused on some examples that we want to accept but do not yet, in particular all the variations of issue #47680. Some adjustments to the active loans computation may be needed, and/or the locations where effects happen (which also relate to the mid-points item above), which was unexpected. It shouldn't be hard to fix though.
• Amanda has continued cleaning up placeholders in the work-in-progress PR #130227.
• There was no particular progress on using more of the polonius model within the borrowck,. We also had a bit less time than usual with me going to RustConf, and Amanda going to EuroRust and doing a presentation on polonius 🎉. We'll add a link to the recording once they're made available.

[lqd]

Key developments, with good progress:

• I've completed the loan liveness + active loans changes I mentioned last time, with kills stopping traversal in the new localized constraint graph
• issues with missing liveness edges when regions flowed into universal regions were fixed
• issues with liveness optimizations for NLLs, that don't apply anymore in a location-sensitive context, were fixed
• I'm currently double-checking invariant edges on assignments/calls: they should be bidirectional, but some of the edges allowing backwards propagation are missing, causing some test failures
• I identified an issue in diagnostics causing 80 or so differences in tests, adding to the diagnostics differences caused by the NLL optimization described above: some errors and handcrafted diagnostics are tailored to the current liveness NLL behavior and structure.
• a lot of work was done on the NLL+polonius data visualization ("debugger"). There's still quite a lot to do here but it already was crucial in diagnosing and fixing the above issues, even in its early state
• overall around 70 real test failures are left to analyze, and then I'll look at the diagnostics differences to see what can be done. The ICEs there expecting NLL constraints should be fixable. The others may require more creative solutions, e.g. piggybacking on the existing code.
• we're also still working out how to best land all this work
• Amanda has done non-trivial work in Remove placeholders completely rust#130227 which now also handles type tests. The PR should be ready to review, and a crater run is currently in-progress.
• Amanda's EuroRust talk on polonius from last month is also now available on YouTube.

[lqd]

Here are the key developments for the last update of the year:

• Amanda has made even more progress on removing placeholders, in particular on lazy constraints and early error reporting, as well as investigating issues with rewriting type tests. A few tests are still failing, and it seems error reporting and diagnostics will be hard to keep exactly as today. Unfortunately, what was devilishly marketed as hoped to be a straightforward refactor turned out to have a lot of hidden complexity
• I've continued analyzing the test failures and fixing them. We're now at 6 failures of interest that still need investigation, and the rest are diagnostics changes.
• I've also hit some kind of weakness in our initial approach: our unified naive reachability conflates the two different transitive closures we used to have. That should have been fine, and the problem didn't exist in our datalog implementation, but with backwards edges we can encounter kills when time-traveling (and they can be impactful). Who knew that time-traveling and spacetime reachability could be mind bending. We haven't fully thought things through just yet, but we can still model reachability as a two-step process anyways. The implementation has a conservative approximation for these cases, but it still was surprising. We'll need a bit more analysis.
• even with the few test failures, we feel the prototype is working well enough that it's worthwhile to land. So I've spent most of the time cleaning it up and opening PRs: Foundations of location-sensitive polonius rust#134268, A couple of polonius fact generation cleanups rust#134315, An octuple of polonius fact generation cleanups rust#134378, Compute liveness constraints in location-sensitive polonius rust#134670, A couple datalog/borrowck cleanups rust#134914 have landed already. Convert typeck constraints in location-sensitive polonius rust#134920 and Location-sensitive polonius prototype: endgame rust#134980 are currently in review.
• These last 2 actually complete end-to-end testing, and replace the location-insensitive analysis in-tree. With that, basically all of the progress done on the prototype, that we've been reporting here, should be available soon-ish. There's of course still a lot of work left to do, but it's still good a milestone.

(Happy Holidays and Happy New Year everyone!)

[lqd]

Key developments from this month:

• @amandasystems has continued working on the Sisyphean Remove placeholders completely rust#130227 and has made progress on rewriting type tests, diagnostics issues, fixing bugs, kept up with changes on master, and more.
• big thanks to @jackh726 and @matthewjasper on reviews: with their help, all the PRs from the previous update have landed on nightly.
• I've opened a couple of PRs on the analysis itself (Encode constraints that hold at all points as logical edges in location-sensitive polonius rust#135290, Ignore NLL boring locals in polonius diagnostics rust#136299) as well as a few cleanups. With these, there are only around 4 failing tests that still need investigation, and 8-10 diagnostics differences to iron out. This is my current focus, but we'll also need to expand test coverage.
• I've also opened a handful of PRs gradually expanding the polonius MIR dump with visualizations. I'll next add the interactive "tool" I've been using to help debug the test failures.
• on organization and collaboration:
  • we've met with one of Amanda's students for a possible Master's thesis on the more engineer-y side of polonius (perf <3)
  • and have also discussed, with @RalfJung's team, the related topic of modeling the borrowck in a-mir-formality

[nikomatsakis]

This is a continuing project goal, and the updates below this comment will be for the new period 2025h1