Module polonius

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:

• https://smallcultfollowing.com/babysteps/blog/2023/09/22/polonius-part-1/
• https://smallcultfollowing.com/babysteps/blog/2023/09/29/polonius-part-2/

Data flows like this:

1. during MIR typeck, record liveness data needed later: live region variances, as well as the usual NLL liveness data (just computed on more locals). That’s the PoloniusLivenessContext.
2. once that is done, variance data is transferred, and the NLL region liveness is converted to the polonius shape. That’s the main PoloniusContext.
3. during region inference, that data and the NLL outlives constraints are used to create the localized outlives constraints, as described above. That’s the PoloniusDiagnosticsContext.
4. transfer this back to the main borrowck procedure: it handles computing errors and diagnostics, debugging and MIR dumping concerns.

Modules

constraints 🔒

dump 🔒

legacy 🔒

Functions dedicated to fact generation for the -Zpolonius=legacy datalog implementation.

liveness_constraints 🔒

loan_liveness 🔒

typeck_constraints 🔒

Structs

PoloniusContext 🔒

This struct holds the data needed to create the Polonius localized constraints. Its data is transferred and converted from the PoloniusLivenessContext at the end of MIR typeck.

PoloniusDiagnosticsContext 🔒

This struct holds the data needed by the borrowck error computation and diagnostics. Its data is computed from the PoloniusContext when computing NLL regions.

PoloniusLivenessContext 🔒

This struct holds the liveness data created during MIR typeck, and which will be used later in the process, to compute the polonius localized constraints.

Enums

ConstraintDirection 🔒

The direction a constraint can flow into. Used to create liveness constraints according to variance.

Type Aliases

LiveLoans 🔒