bjoernager/rust
bjoernager/rust
1
Fork 0
Code Activity

deal with naive reachability weakness

Browse source 
it's a bit mind-bending
This commit is contained in:
Rémy Rakic 2024-12-31 17:37:58 +00:00
parent 550cf1f4a4
commit 0f3dd33e1d
1 changed files with 82 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

79
compiler/rustc_borrowck/src/polonius/loan_liveness.rs
View file

@ -53,16 +53,70 @@ 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 {
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,7 +219,8 @@ 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| {
let definitely_conflicting_borrows = other_borrows_of_local
.filter(|&i| {
places_conflict(
self.tcx,
self.body,
@ -160,7 +228,8 @@ impl<'tcx> KillsCollector<'_, 'tcx> {
place,
PlaceConflictBias::NoOverlap,
)
});
})
.filter(|&loan| filter_unreachable_kills(loan));
self.kills.entry(location).or_default().extend(definitely_conflicting_borrows);
}