simplify polonius=next

Remove incomplete handling of kills during traversal for loan liveness
to get to a simpler and actionable prototype.

This handles the cases, on sufficiently simple examples, that were
deferred from NLLs (NLL problem case 3, lending iterators), and is still
a good step to put in people's hands without needing to wait for another
full implementation. This is a practical cut in scope, but it also
shows where are the areas of improvement, that we will explore in the
future.

Author: lqd

compiler/rustc_borrowck/src/polonius/constraints.rs

@@ -7,9 +7,7 @@ use rustc_mir_dataflow::points::PointIndex;
 ///
 /// This models two sources of constraints:
 /// - constraints that traverse the subsets between regions at a given point, `a@p: b@p`. These
-///   depend on typeck constraints generated via assignments, calls, etc. (In practice there are
-///   subtleties where a statement's effect only starts being visible at the successor point, via
-///   the "result" of that statement).
+///   depend on typeck constraints generated via assignments, calls, etc.
 /// - constraints that traverse the CFG via the same region, `a@p: a@q`, where `p` is a predecessor
 ///   of `q`. These depend on the liveness of the regions at these points, as well as their
 ///   variance.

compiler/rustc_borrowck/src/polonius/liveness_constraints.rs

@@ -105,22 +105,14 @@ fn propagate_loans_between_points(
         });
     }
 
-    let Some(current_live_regions) = live_regions.row(current_point) else {
-        // There are no constraints to add: there are no live regions at the current point.
-        return;
-    };
     let Some(next_live_regions) = live_regions.row(next_point) else {
         // There are no constraints to add: there are no live regions at the next point.
         return;
     };
 
     for region in next_live_regions.iter() {
-        if !current_live_regions.contains(region) {
-            continue;
-        }
-
-        // `region` is indeed live at both points, add a constraint between them, according to
-        // variance.
+        // `region` could be live at the current point, and is live at the next point: add a
+        // constraint between them, according to variance.
         if let Some(&direction) = live_region_variances.get(&region) {
             add_liveness_constraint(
                 region,

compiler/rustc_borrowck/src/polonius/loan_liveness.rs

@@ -1,39 +1,25 @@
-use std::collections::{BTreeMap, BTreeSet};
-
 use rustc_data_structures::fx::{FxHashMap, FxHashSet, FxIndexSet};
-use rustc_middle::mir::visit::Visitor;
-use rustc_middle::mir::{
-    Body, Local, Location, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
-};
-use rustc_middle::ty::{RegionVid, TyCtxt};
+use rustc_middle::ty::RegionVid;
 use rustc_mir_dataflow::points::PointIndex;
 
 use super::{LiveLoans, LocalizedOutlivesConstraintSet};
+use crate::BorrowSet;
 use crate::constraints::OutlivesConstraint;
-use crate::dataflow::BorrowIndex;
 use crate::region_infer::values::LivenessValues;
 use crate::type_check::Locations;
-use crate::{BorrowSet, PlaceConflictBias, places_conflict};
 
-/// Compute loan reachability, stop at kills, and trace loan liveness throughout the CFG, by
+/// Compute loan reachability to approximately trace loan liveness throughout the CFG, by
 /// traversing the full graph of constraints that combines:
 /// - the localized constraints (the physical edges),
 /// - with the constraints that hold at all points (the logical edges).
 pub(super) fn compute_loan_liveness<'tcx>(
-    tcx: TyCtxt<'tcx>,
-    body: &Body<'tcx>,
     liveness: &LivenessValues,
     outlives_constraints: impl Iterator<Item = OutlivesConstraint<'tcx>>,
     borrow_set: &BorrowSet<'tcx>,
     localized_outlives_constraints: &LocalizedOutlivesConstraintSet,
 ) -> LiveLoans {
     let mut live_loans = LiveLoans::new(borrow_set.len());
 
-    // FIXME: it may be preferable for kills to be encoded in the edges themselves, to simplify and
-    // likely make traversal (and constraint generation) more efficient. We also display kills on
-    // edges when visualizing the constraint graph anyways.
-    let kills = collect_kills(body, tcx, borrow_set);
-
     // Create the full graph with the physical edges we've localized earlier, and the logical edges
     // of constraints that hold at all points.
     let logical_constraints =
@@ -59,15 +45,15 @@ pub(super) fn compute_loan_liveness<'tcx>(
                 continue;
             }
 
-            // Record the loan as being live on entry to this point.
-            live_loans.insert(node.point, loan_idx);
-
-            // Here, we have a conundrum. There's currently a weakness in our theory, in that
-            // we're using a single notion of reachability to represent what used to be _two_
-            // different transitive closures. It didn't seem impactful when coming up with the
-            // single-graph and reachability through space (regions) + time (CFG) concepts, but in
-            // practice the combination of time-traveling with kills is more impactful than
-            // initially anticipated.
+            // Record the loan as being live on entry to this point if it reaches a live region
+            // there.
+            //
+            // This is an approximation of liveness (which is the thing we want), in that we're
+            // using a single notion of reachability to represent what used to be _two_ different
+            // transitive closures. It didn't seem impactful when coming up with the single-graph
+            // and reachability through space (regions) + time (CFG) concepts, but in practice the
+            // combination of time-traveling with kills is more impactful than initially
+            // anticipated.
             //
             // Kills should prevent a loan from reaching its successor points in the CFG, but not
             // while time-traveling: we're not actually at that CFG point, but looking for
@@ -92,40 +78,20 @@ pub(super) fn compute_loan_liveness<'tcx>(
             //   two-step traversal described above: only kills encountered on exit via a backward
             //   edge are ignored.
             //
-            // In our test suite, there are a couple of cases where kills are encountered while
-            // time-traveling, however as far as we can tell, always in cases where they would be
-            // unreachable. We have reason to believe that this is a property of the single-graph
-            // approach (but haven't proved it yet):
-            // - reachable kills while time-traveling would also be encountered via regular
-            //   traversal
-            // - it makes _some_ sense to ignore unreachable kills, but subtleties around dead code
-            //   in general need to be better thought through (like they were for NLLs).
-            // - ignoring kills is a conservative approximation: the loan is still live and could
-            //   cause false positive errors at another place access. Soundness issues in this
-            //   domain should look more like the absence of reachability instead.
-            //
-            // This is enough in practice to pass tests, and therefore is what we have implemented
-            // for now.
+            // This version of the analysis, however, is enough in practice to pass the tests that
+            // we care about and NLLs reject, without regressions on crater, and is an actionable
+            // subset of the full analysis. It also naturally points to areas of improvement that we
+            // wish to explore later, namely handling kills appropriately during traversal, instead
+            // of continuing traversal to all the reachable nodes.
             //
-            // FIXME: all of the above. Analyze potential unsoundness, possibly in concert with a
-            // borrowck implementation in a-mir-formality, fuzzing, or manually crafting
-            // counter-examples.
+            // FIXME: analyze potential unsoundness, possibly in concert with a borrowck
+            // implementation in a-mir-formality, fuzzing, or manually crafting counter-examples.
 
-            // Continuing traversal will depend on whether the loan is killed at this point, and
-            // whether we're time-traveling.
-            let current_location = liveness.location_from_point(node.point);
-            let is_loan_killed =
-                kills.get(&current_location).is_some_and(|kills| kills.contains(&loan_idx));
+            if liveness.is_live_at(node.region, liveness.location_from_point(node.point)) {
+                live_loans.insert(node.point, loan_idx);
+            }
 
             for succ in graph.outgoing_edges(node) {
-                // If the loan is killed at this point, it is killed _on exit_. But only during
-                // forward traversal.
-                if is_loan_killed {
-                    let destination = liveness.location_from_point(succ.point);
-                    if current_location.is_predecessor_of(destination, body) {
-                        continue;
-                    }
-                }
                 stack.push(succ);
             }
         }
@@ -192,116 +158,3 @@ impl LocalizedConstraintGraph {
         physical_edges.chain(materialized_edges)
     }
 }
-
-/// Traverses the MIR and collects kills.
-fn collect_kills<'tcx>(
-    body: &Body<'tcx>,
-    tcx: TyCtxt<'tcx>,
-    borrow_set: &BorrowSet<'tcx>,
-) -> BTreeMap<Location, BTreeSet<BorrowIndex>> {
-    let mut collector = KillsCollector { borrow_set, tcx, body, kills: BTreeMap::default() };
-    for (block, data) in body.basic_blocks.iter_enumerated() {
-        collector.visit_basic_block_data(block, data);
-    }
-    collector.kills
-}
-
-struct KillsCollector<'a, 'tcx> {
-    body: &'a Body<'tcx>,
-    tcx: TyCtxt<'tcx>,
-    borrow_set: &'a BorrowSet<'tcx>,
-
-    /// The set of loans killed at each location.
-    kills: BTreeMap<Location, BTreeSet<BorrowIndex>>,
-}
-
-// This visitor has a similar structure to the `Borrows` dataflow computation with respect to kills,
-// and the datalog polonius fact generation for the `loan_killed_at` relation.
-impl<'tcx> KillsCollector<'_, 'tcx> {
-    /// Records the borrows on the specified place as `killed`. For example, when assigning to a
-    /// local, or on a call's return destination.
-    fn record_killed_borrows_for_place(&mut self, place: Place<'tcx>, location: Location) {
-        // For the reasons described in graph traversal, we also filter out kills
-        // unreachable from the loan's introduction point, as they would stop traversal when
-        // e.g. checking for reachability in the subset graph through invariance constraints
-        // higher up.
-        let filter_unreachable_kills = |loan| {
-            let introduction = self.borrow_set[loan].reserve_location;
-            let reachable = introduction.is_predecessor_of(location, self.body);
-            reachable
-        };
-
-        let other_borrows_of_local = self
-            .borrow_set
-            .local_map
-            .get(&place.local)
-            .into_iter()
-            .flat_map(|bs| bs.iter())
-            .copied();
-
-        // If the borrowed place is a local with no projections, all other borrows of this
-        // local must conflict. This is purely an optimization so we don't have to call
-        // `places_conflict` for every borrow.
-        if place.projection.is_empty() {
-            if !self.body.local_decls[place.local].is_ref_to_static() {
-                self.kills
-                    .entry(location)
-                    .or_default()
-                    .extend(other_borrows_of_local.filter(|&loan| filter_unreachable_kills(loan)));
-            }
-            return;
-        }
-
-        // By passing `PlaceConflictBias::NoOverlap`, we conservatively assume that any given
-        // pair of array indices are not equal, so that when `places_conflict` returns true, we
-        // will be assured that two places being compared definitely denotes the same sets of
-        // locations.
-        let definitely_conflicting_borrows = other_borrows_of_local
-            .filter(|&i| {
-                places_conflict(
-                    self.tcx,
-                    self.body,
-                    self.borrow_set[i].borrowed_place,
-                    place,
-                    PlaceConflictBias::NoOverlap,
-                )
-            })
-            .filter(|&loan| filter_unreachable_kills(loan));
-
-        self.kills.entry(location).or_default().extend(definitely_conflicting_borrows);
-    }
-
-    /// Records the borrows on the specified local as `killed`.
-    fn record_killed_borrows_for_local(&mut self, local: Local, location: Location) {
-        if let Some(borrow_indices) = self.borrow_set.local_map.get(&local) {
-            self.kills.entry(location).or_default().extend(borrow_indices.iter());
-        }
-    }
-}
-
-impl<'tcx> Visitor<'tcx> for KillsCollector<'_, 'tcx> {
-    fn visit_statement(&mut self, statement: &Statement<'tcx>, location: Location) {
-        // Make sure there are no remaining borrows for locals that have gone out of scope.
-        if let StatementKind::StorageDead(local) = statement.kind {
-            self.record_killed_borrows_for_local(local, location);
-        }
-
-        self.super_statement(statement, location);
-    }
-
-    fn visit_assign(&mut self, place: &Place<'tcx>, rvalue: &Rvalue<'tcx>, location: Location) {
-        // When we see `X = ...`, then kill borrows of `(*X).foo` and so forth.
-        self.record_killed_borrows_for_place(*place, location);
-        self.super_assign(place, rvalue, location);
-    }
-
-    fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, location: Location) {
-        // A `Call` terminator's return value can be a local which has borrows, so we need to record
-        // those as killed as well.
-        if let TerminatorKind::Call { destination, .. } = terminator.kind {
-            self.record_killed_borrows_for_place(destination, location);
-        }
-
-        self.super_terminator(terminator, location);
-    }
-}

compiler/rustc_borrowck/src/polonius/mod.rs

@@ -146,8 +146,8 @@ impl PoloniusContext {
     /// - converting NLL typeck constraints to be localized
     /// - encoding liveness constraints
     ///
-    /// Then, this graph is traversed, and combined with kills, reachability is recorded as loan
-    /// liveness, to be used by the loan scope and active loans computations.
+    /// Then, this graph is traversed, reachability is recorded as loan liveness, to be used by the
+    /// loan scope and active loans computations.
     ///
     /// The constraint data will be used to compute errors and diagnostics.
     pub(crate) fn compute_loan_liveness<'tcx>(
@@ -182,8 +182,6 @@ impl PoloniusContext {
         // Now that we have a complete graph, we can compute reachability to trace the liveness of
         // loans for the next step in the chain, the NLL loan scope and active loans computations.
         let live_loans = compute_loan_liveness(
-            tcx,
-            body,
             regioncx.liveness_constraints(),
             regioncx.outlives_constraints(),
             borrow_set,

compiler/rustc_borrowck/src/polonius/typeck_constraints.rs

@@ -47,9 +47,7 @@ pub(super) fn convert_typeck_constraints<'tcx>(
                         tcx,
                         body,
                         stmt,
-                        liveness,
                         &outlives_constraint,
-                        location,
                         point,
                         universal_regions,
                     )
@@ -78,9 +76,7 @@ fn localize_statement_constraint<'tcx>(
     tcx: TyCtxt<'tcx>,
     body: &Body<'tcx>,
     stmt: &Statement<'tcx>,
-    liveness: &LivenessValues,
     outlives_constraint: &OutlivesConstraint<'tcx>,
-    current_location: Location,
     current_point: PointIndex,
     universal_regions: &UniversalRegions<'tcx>,
 ) -> LocalizedOutlivesConstraint {
@@ -119,16 +115,8 @@ fn localize_statement_constraint<'tcx>(
                 "there should be no common regions between the LHS and RHS of an assignment"
             );
 
-            // As mentioned earlier, we should be tracking these better upstream but: we want to
-            // relate the types on entry to the type of the place on exit. That is, outlives
-            // constraints on the RHS are on entry, and outlives constraints to/from the LHS are on
-            // exit (i.e. on entry to the successor location).
             let lhs_ty = body.local_decls[lhs.local].ty;
-            let successor_location = Location {
-                block: current_location.block,
-                statement_index: current_location.statement_index + 1,
-            };
-            let successor_point = liveness.point_from_location(successor_location);
+            let successor_point = current_point;
             compute_constraint_direction(
                 tcx,
                 outlives_constraint,

tests/ui/nll/issue-46589.polonius_next.stderr

@@ -0,0 +1,15 @@
+error[E0499]: cannot borrow `**other` as mutable more than once at a time
+  --> $DIR/issue-46589.rs:24:21
+   |
+LL |         *other = match (*other).get_self() {
+   |                        -------- first mutable borrow occurs here
+LL |             Some(s) => s,
+LL |             None => (*other).new_self()
+   |                     ^^^^^^^^
+   |                     |
+   |                     second mutable borrow occurs here
+   |                     first borrow later used here
+
+error: aborting due to 1 previous error
+
+For more information about this error, try `rustc --explain E0499`.

tests/ui/nll/issue-46589.rs

@@ -1,6 +1,6 @@
 //@ ignore-compare-mode-polonius (explicit revisions)
 //@ revisions: nll polonius_next polonius
-//@ [polonius_next] check-pass
+//@ [polonius_next] check-fail
 //@ [polonius_next] compile-flags: -Zpolonius=next
 //@ [polonius] check-pass
 //@ [polonius] compile-flags: -Zpolonius
@@ -23,6 +23,7 @@ impl Foo {
             Some(s) => s,
             None => (*other).new_self()
             //[nll]~^ ERROR cannot borrow `**other` as mutable more than once at a time [E0499]
+            //[polonius_next]~^^ ERROR cannot borrow `**other` as mutable more than once at a time [E0499]
         };
 
         let c = other;