deal with naive reachability weakness

it's a bit mind-bending

Author: lqd

compiler/rustc_borrowck/src/polonius/loan_liveness.rs

@@ -53,15 +53,69 @@ pub(super) fn compute_loan_liveness<'tcx>(
             // Record the loan as being live on entry to this point.
             live_loans.insert(node.point, loan_idx);
 
-            // Continuing traversal will depend on whether the loan is killed at this point.
+            // 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.
+            //
+            // 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
+            // predecessor regions that contain the loan. One of the two TCs we had pushed the
+            // transitive subset edges to each point instead of having backward edges, and the
+            // problem didn't exist before. In the abstract, naive reachability is not enough to
+            // model this, we'd need a slightly different solution. For example, maybe with a
+            // two-step traversal:
+            // - at each point we first traverse the subgraph (and possibly time-travel) looking for
+            //   exit nodes while ignoring kills,
+            // - and then when we're back at the current point, we continue normally.
+            //
+            // Another (less annoying) subtlety is that kills and the loan use-map are
+            // flow-insensitive. Kills can actually appear in places before a loan is introduced, or
+            // at a location that is actually unreachable in the CFG from the introduction point,
+            // and these can also be encountered during time-traveling.
+            //
+            // The simplest change that made sense to "fix" the issues above is taking into
+            // account kills that are:
+            // - reachable from the introduction point
+            // - encountered during forward traversal. Note that this is not transitive like the
+            //   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.
+            //
+            // 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.
+
+            // 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));
 
             for succ in outgoing_edges(&graph, node) {
-                // If the loan is killed at this point, it is killed _on exit_.
+                // If the loan is killed at this point, it is killed _on exit_. But only during
+                // forward traversal.
                 if is_loan_killed {
-                    continue;
+                    let destination = liveness.location_from_point(succ.point);
+                    if current_location.is_predecessor_of(destination, body) {
+                        continue;
+                    }
                 }
                 stack.push(succ);
             }
@@ -130,6 +184,16 @@ 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
@@ -143,7 +207,10 @@ impl<'tcx> KillsCollector<'_, 'tcx> {
         // `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);
+                self.kills
+                    .entry(location)
+                    .or_default()
+                    .extend(other_borrows_of_local.filter(|&loan| filter_unreachable_kills(loan)));
             }
             return;
         }
@@ -152,15 +219,17 @@ impl<'tcx> KillsCollector<'_, 'tcx> {
         // 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,
-            )
-        });
+        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);
     }