diff options
| -rw-r--r-- | compiler/rustc_borrowck/src/polonius/loan_liveness.rs | 95 |
1 files changed, 82 insertions, 13 deletions
diff --git a/compiler/rustc_borrowck/src/polonius/loan_liveness.rs b/compiler/rustc_borrowck/src/polonius/loan_liveness.rs index aacc342e0f1..c519453652f 100644 --- a/compiler/rustc_borrowck/src/polonius/loan_liveness.rs +++ b/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(¤t_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); } |