about summary refs log tree commit diff
diff options
context:
space:
mode:
authorRémy Rakic <remy.rakic+github@gmail.com>2024-12-13 10:35:28 +0000
committerRémy Rakic <remy.rakic+github@gmail.com>2024-12-18 07:33:26 +0000
commita5f05919e0b6d7036a4cd161a02b93150af41758 (patch)
tree1fe1f861289ca620b228a010790dea328bc916f1
parentb70a9159a629e15bdb1aa104cc195c9d4614da89 (diff)
downloadrust-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.rs35
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::*;