Whats the differences between polonius in datalog and -Zpolonius and -Zpolonius=legacy and -Zpolonius=next ？Do they actually implement the flow-sensitive subst relation and region(contain Loans instead of Points) ? Is the location sensitive means flow-sensitive subst relation ? I'm confused about the above questions, thanks for you help
Hello,
I'm seeking clarification on several aspects of Polonius and its implementations:
Differences Between Polonius Implementations:
What are the distinctions between the original Datalog-based Polonius and the -Zpolonius, -Zpolonius=legacy, and -Zpolonius=next implementations in Rust?
Flow-Sensitive Substitution Relation:
Do these implementations support a flow-sensitive substitution relation, and how is it represented?
Region vs. Loan Tracking:
In Polonius, is the term region synonymous with loan? If not, how do they differ in the analysis?
Location Sensitivity and Flow Sensitivity:
Does location sensitivity imply flow sensitivity in the context of Polonius?
I appreciate any insights or resources that can help clarify these points.
These are the same and are the Datalog-based Polonius.
-ZPolonius
-ZPolonius=legacy
This is the one implemented in rustc.
-ZPolonius=next
What exactly distinguishes what they can handle is both a moving target, and not formally documented as far as I know. This is a good thread to follow since you're interested in the topic. This recent PR outlines a possible "Polonius Alpha". You could also check out the tests that highlight some differences between the different borrow checkers.
The level of detail you desire to know may require looking at the source code and/or talking to the devs working on Polonius.
AFAIK both are more flow-sensitive than NLL, but the datalog version covers more. I'm not sure what exactly distinguishes "flow sensitively" from "location sensitive subtyping", if anything. (As an interested outsider I use them pretty interchangeably).
The Polonius Alpha PR says
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.
[...]
I've added tests with improvements, like the NLL problem case 3 and others, as well as some that behave the same as NLLs today and are thus worse than the datalog implementation
As for the implementation, you're probably best off looking at source code or talking to compiler devs. As a starting point, perhaps checkout the PRs linked here. And of course the changes in the Polonius Alpha PR.
Both NLL and Polonius distinguish between lifetimes/regions and loans/borrows. For example, see here. The "kills" are still a part of the Polonius algorithm. The Polonius Alpha removes some amount of kill analysis, whatever that means. (I'm not really in a position to attempt a more precise definition of regions, loans, kills, etc. as used in the different borrow checker implementations / by the primary devs, though.)
