diff options
| author | Rémy Rakic <remy.rakic+github@gmail.com> | 2024-12-13 10:35:28 +0000 |
|---|---|---|
| committer | Rémy Rakic <remy.rakic+github@gmail.com> | 2024-12-18 07:33:26 +0000 |
| commit | a5f05919e0b6d7036a4cd161a02b93150af41758 (patch) | |
| tree | 1fe1f861289ca620b228a010790dea328bc916f1 | |
| parent | b70a9159a629e15bdb1aa104cc195c9d4614da89 (diff) | |
| download | rust-a5f05919e0b6d7036a4cd161a02b93150af41758.tar.gz rust-a5f05919e0b6d7036a4cd161a02b93150af41758.zip | |
add general documentation on the polonius module
this describes the rough algorithm using the localized constraint graph
| -rw-r--r-- | compiler/rustc_borrowck/src/polonius/mod.rs | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/compiler/rustc_borrowck/src/polonius/mod.rs b/compiler/rustc_borrowck/src/polonius/mod.rs index 391ef2069f9..70f8fdaa637 100644 --- a/compiler/rustc_borrowck/src/polonius/mod.rs +++ b/compiler/rustc_borrowck/src/polonius/mod.rs @@ -1,3 +1,38 @@ +//! 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/> +//! + mod constraints; pub(crate) use constraints::*; |
