Expand description
Polonius analysis and support code:
- dedicated constraints
- conversion from NLL constraints
- debugging utilities
- etc.
The current implementation models the flow-sensitive borrow-checking concerns as a graph containing both information about regions and information about the control flow.
Loan propagation is seen as a reachability problem (with some subtleties) between where the loan is introduced and a given point.
Constraints arising from type-checking allow loans to flow from region to region at the same CFG point. Constraints arising from liveness allow loans to flow within from point to point, between live regions at these points.
Edges can be bidirectional to encode invariant relationships, and loans can flow “back in time” to traverse these constraints arising earlier in the CFG.
When incorporating kills in the traversal, the loans reaching a given point are considered live.
After this, the usual NLL process happens. These live loans are fed into a dataflow analysis combining them with the points where loans go out of NLL scope (the frontier where they stop propagating to a live region), to yield the “loans in scope” or “active loans”, at a given point.
Illegal accesses are still computed by checking whether one of these resulting loans is invalidated.
More information on this simple approach can be found in the following links, and in the future in the rustc dev guide:
Modules§
- dump 🔒
- legacy 🔒Functions dedicated to fact generation for the
-Zpolonius=legacydatalog implementation.
Structs§
- This struct holds the data needed to create the Polonius localized constraints.
Enums§
- The direction a constraint can flow into. Used to create liveness constraints according to variance.
Functions§
- Propagate loans throughout the subset graph at a given point (with some subtleties around the location where effects start to be visible).