user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

simplify polonius=next

Browse source 
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.
This commit is contained in:
Rémy Rakic 2025-08-08 15:14:17 +00:00
parent f4094ea252
commit a5adde8eaa
5 changed files with 28 additions and 199 deletions
Download patch file Download diff file Expand all files Collapse all files

4
compiler/rustc_borrowck/src/polonius/constraints.rs
View file

@ -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.

12
compiler/rustc_borrowck/src/polonius/liveness_constraints.rs
View file

@ -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,

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

@ -1,27 +1,18 @@
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>,
@ -29,11 +20,6 @@ pub(super) fn compute_loan_liveness<'tcx>(
) -> 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 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.
//
// 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.
// 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);
}
}

6
compiler/rustc_borrowck/src/polonius/mod.rs
View file

@ -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,

14
compiler/rustc_borrowck/src/polonius/typeck_constraints.rs
View file

@ -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,