Skip to content

Commit 37d26b4

Browse files
authored
Rollup merge of rust-lang#143093 - lqd:polonius-pre-alpha, r=jackh726
Simplify polonius location-sensitive analysis This PR reworks the location-sensitive analysis into what we think is a worthwhile subset of the datalog analysis. A sort of polonius alpha analysis that handles NLL problem case 3 and more, but is still using the faster "reachability as an approximation of liveness", as well as the same loans-in-scope computation as NLLs -- and thus doesn't handle full flow-sensitivity like the datalog implementation. In the last few months, we've identified this subset as being actionable: - we believe we can make a stabilizable version of this analysis - it is an improvement over the status quo - it can also be modeled in a-mir-formality, or some other formalism, for assurances about soundness, and I believe `@nikomatsakis` is interested in looking into this during H2. - and we've identified the areas of work we wish to explore later to gradually expand the supported cases: the differences between reachability and liveness, support of kills, and considerations of time-traveling, for example. The approach in this PR is to try less to have the graph only represent live paths, by checking whether we reach a live region during traversal and recording the loan as live there, instead of equating traversal with liveness like today because it has subtleties with the typeck edges in statements (that could forward loans to the successor point without ensuring their liveness). We can then also simplify these typeck stmt edges. And we also can simplify traversal by removing looking at kills, because that's enough to handle a bunch of NLL problem 3 cases -- and we can gradually support them more and more in traversal in the future, to reduce the approximation of liveness. There's still some in-progress pieces of work w/r/t opaque types that I'm expecting [lcnr's opaque types rework](rust-lang#139587), and [amanda's SCCs rework](rust-lang#130227) to handle. That didn't seem to show up in tests until I rebased today (and shows lack of test coverage once again) when rust-lang#142255 introduced a couple of test failures with the new captures rules from edition 2024. It's not unexpected since we know more work is needed with member constraints (and we're not even using SCCs in this prototype yet) I'll look into these anyways, both for future work, and checking how these other 2 PRs would change things. --- I'm not sure the following means a lot until we have some formalism in-place, but: - I've changed the polonius compare-mode to use this analysis: the tests pass with it, except 2 cases with minor diagnostics differences, and the 2 edition 2024 opaque types one I mentioned above and need to investigate - things that are expected to work still do work: it bootstraps, can run our rustc-perf benchmarks (and the results are not even that bad), and a crater run didn't find any regressions (forgetting that crater currently fails to test around a quarter of all crates 👼) - I've added tests with improvements, like the NLL problem case 3 and others, as well as some that behave the same as NLLs today and are thus worse than the datalog implementation r? `@jackh726` (no rush I know you're deep in phd work and "implmentating" the new trait solver for r-a :p <3) This also fixes rust-lang#135646, a diagnostics ICE from the previous implementation.
2 parents f95c41f + b99fe2b commit 37d26b4

35 files changed

+624
-247
lines changed

compiler/rustc_borrowck/src/polonius/constraints.rs

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,7 @@ use rustc_mir_dataflow::points::PointIndex;
77
///
88
/// This models two sources of constraints:
99
/// - constraints that traverse the subsets between regions at a given point, `a@p: b@p`. These
10-
/// depend on typeck constraints generated via assignments, calls, etc. (In practice there are
11-
/// subtleties where a statement's effect only starts being visible at the successor point, via
12-
/// the "result" of that statement).
10+
/// depend on typeck constraints generated via assignments, calls, etc.
1311
/// - constraints that traverse the CFG via the same region, `a@p: a@q`, where `p` is a predecessor
1412
/// of `q`. These depend on the liveness of the regions at these points, as well as their
1513
/// variance.

compiler/rustc_borrowck/src/polonius/liveness_constraints.rs

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -105,22 +105,14 @@ fn propagate_loans_between_points(
105105
});
106106
}
107107

108-
let Some(current_live_regions) = live_regions.row(current_point) else {
109-
// There are no constraints to add: there are no live regions at the current point.
110-
return;
111-
};
112108
let Some(next_live_regions) = live_regions.row(next_point) else {
113109
// There are no constraints to add: there are no live regions at the next point.
114110
return;
115111
};
116112

117113
for region in next_live_regions.iter() {
118-
if !current_live_regions.contains(region) {
119-
continue;
120-
}
121-
122-
// `region` is indeed live at both points, add a constraint between them, according to
123-
// variance.
114+
// `region` could be live at the current point, and is live at the next point: add a
115+
// constraint between them, according to variance.
124116
if let Some(&direction) = live_region_variances.get(&region) {
125117
add_liveness_constraint(
126118
region,
Lines changed: 22 additions & 169 deletions
Original file line numberDiff line numberDiff line change
@@ -1,39 +1,25 @@
1-
use std::collections::{BTreeMap, BTreeSet};
2-
31
use rustc_data_structures::fx::{FxHashMap, FxHashSet, FxIndexSet};
4-
use rustc_middle::mir::visit::Visitor;
5-
use rustc_middle::mir::{
6-
Body, Local, Location, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
7-
};
8-
use rustc_middle::ty::{RegionVid, TyCtxt};
2+
use rustc_middle::ty::RegionVid;
93
use rustc_mir_dataflow::points::PointIndex;
104

115
use super::{LiveLoans, LocalizedOutlivesConstraintSet};
6+
use crate::BorrowSet;
127
use crate::constraints::OutlivesConstraint;
13-
use crate::dataflow::BorrowIndex;
148
use crate::region_infer::values::LivenessValues;
159
use crate::type_check::Locations;
16-
use crate::{BorrowSet, PlaceConflictBias, places_conflict};
1710

18-
/// Compute loan reachability, stop at kills, and trace loan liveness throughout the CFG, by
11+
/// Compute loan reachability to approximately trace loan liveness throughout the CFG, by
1912
/// traversing the full graph of constraints that combines:
2013
/// - the localized constraints (the physical edges),
2114
/// - with the constraints that hold at all points (the logical edges).
2215
pub(super) fn compute_loan_liveness<'tcx>(
23-
tcx: TyCtxt<'tcx>,
24-
body: &Body<'tcx>,
2516
liveness: &LivenessValues,
2617
outlives_constraints: impl Iterator<Item = OutlivesConstraint<'tcx>>,
2718
borrow_set: &BorrowSet<'tcx>,
2819
localized_outlives_constraints: &LocalizedOutlivesConstraintSet,
2920
) -> LiveLoans {
3021
let mut live_loans = LiveLoans::new(borrow_set.len());
3122

32-
// FIXME: it may be preferable for kills to be encoded in the edges themselves, to simplify and
33-
// likely make traversal (and constraint generation) more efficient. We also display kills on
34-
// edges when visualizing the constraint graph anyways.
35-
let kills = collect_kills(body, tcx, borrow_set);
36-
3723
// Create the full graph with the physical edges we've localized earlier, and the logical edges
3824
// of constraints that hold at all points.
3925
let logical_constraints =
@@ -59,15 +45,15 @@ pub(super) fn compute_loan_liveness<'tcx>(
5945
continue;
6046
}
6147

62-
// Record the loan as being live on entry to this point.
63-
live_loans.insert(node.point, loan_idx);
64-
65-
// Here, we have a conundrum. There's currently a weakness in our theory, in that
66-
// we're using a single notion of reachability to represent what used to be _two_
67-
// different transitive closures. It didn't seem impactful when coming up with the
68-
// single-graph and reachability through space (regions) + time (CFG) concepts, but in
69-
// practice the combination of time-traveling with kills is more impactful than
70-
// initially anticipated.
48+
// Record the loan as being live on entry to this point if it reaches a live region
49+
// there.
50+
//
51+
// This is an approximation of liveness (which is the thing we want), in that we're
52+
// using a single notion of reachability to represent what used to be _two_ different
53+
// transitive closures. It didn't seem impactful when coming up with the single-graph
54+
// and reachability through space (regions) + time (CFG) concepts, but in practice the
55+
// combination of time-traveling with kills is more impactful than initially
56+
// anticipated.
7157
//
7258
// Kills should prevent a loan from reaching its successor points in the CFG, but not
7359
// 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>(
9278
// two-step traversal described above: only kills encountered on exit via a backward
9379
// edge are ignored.
9480
//
95-
// In our test suite, there are a couple of cases where kills are encountered while
96-
// time-traveling, however as far as we can tell, always in cases where they would be
97-
// unreachable. We have reason to believe that this is a property of the single-graph
98-
// approach (but haven't proved it yet):
99-
// - reachable kills while time-traveling would also be encountered via regular
100-
// traversal
101-
// - it makes _some_ sense to ignore unreachable kills, but subtleties around dead code
102-
// in general need to be better thought through (like they were for NLLs).
103-
// - ignoring kills is a conservative approximation: the loan is still live and could
104-
// cause false positive errors at another place access. Soundness issues in this
105-
// domain should look more like the absence of reachability instead.
106-
//
107-
// This is enough in practice to pass tests, and therefore is what we have implemented
108-
// for now.
81+
// This version of the analysis, however, is enough in practice to pass the tests that
82+
// we care about and NLLs reject, without regressions on crater, and is an actionable
83+
// subset of the full analysis. It also naturally points to areas of improvement that we
84+
// wish to explore later, namely handling kills appropriately during traversal, instead
85+
// of continuing traversal to all the reachable nodes.
10986
//
110-
// FIXME: all of the above. Analyze potential unsoundness, possibly in concert with a
111-
// borrowck implementation in a-mir-formality, fuzzing, or manually crafting
112-
// counter-examples.
87+
// FIXME: analyze potential unsoundness, possibly in concert with a borrowck
88+
// implementation in a-mir-formality, fuzzing, or manually crafting counter-examples.
11389

114-
// Continuing traversal will depend on whether the loan is killed at this point, and
115-
// whether we're time-traveling.
116-
let current_location = liveness.location_from_point(node.point);
117-
let is_loan_killed =
118-
kills.get(&current_location).is_some_and(|kills| kills.contains(&loan_idx));
90+
if liveness.is_live_at(node.region, liveness.location_from_point(node.point)) {
91+
live_loans.insert(node.point, loan_idx);
92+
}
11993

12094
for succ in graph.outgoing_edges(node) {
121-
// If the loan is killed at this point, it is killed _on exit_. But only during
122-
// forward traversal.
123-
if is_loan_killed {
124-
let destination = liveness.location_from_point(succ.point);
125-
if current_location.is_predecessor_of(destination, body) {
126-
continue;
127-
}
128-
}
12995
stack.push(succ);
13096
}
13197
}
@@ -192,116 +158,3 @@ impl LocalizedConstraintGraph {
192158
physical_edges.chain(materialized_edges)
193159
}
194160
}
195-
196-
/// Traverses the MIR and collects kills.
197-
fn collect_kills<'tcx>(
198-
body: &Body<'tcx>,
199-
tcx: TyCtxt<'tcx>,
200-
borrow_set: &BorrowSet<'tcx>,
201-
) -> BTreeMap<Location, BTreeSet<BorrowIndex>> {
202-
let mut collector = KillsCollector { borrow_set, tcx, body, kills: BTreeMap::default() };
203-
for (block, data) in body.basic_blocks.iter_enumerated() {
204-
collector.visit_basic_block_data(block, data);
205-
}
206-
collector.kills
207-
}
208-
209-
struct KillsCollector<'a, 'tcx> {
210-
body: &'a Body<'tcx>,
211-
tcx: TyCtxt<'tcx>,
212-
borrow_set: &'a BorrowSet<'tcx>,
213-
214-
/// The set of loans killed at each location.
215-
kills: BTreeMap<Location, BTreeSet<BorrowIndex>>,
216-
}
217-
218-
// This visitor has a similar structure to the `Borrows` dataflow computation with respect to kills,
219-
// and the datalog polonius fact generation for the `loan_killed_at` relation.
220-
impl<'tcx> KillsCollector<'_, 'tcx> {
221-
/// Records the borrows on the specified place as `killed`. For example, when assigning to a
222-
/// local, or on a call's return destination.
223-
fn record_killed_borrows_for_place(&mut self, place: Place<'tcx>, location: Location) {
224-
// For the reasons described in graph traversal, we also filter out kills
225-
// unreachable from the loan's introduction point, as they would stop traversal when
226-
// e.g. checking for reachability in the subset graph through invariance constraints
227-
// higher up.
228-
let filter_unreachable_kills = |loan| {
229-
let introduction = self.borrow_set[loan].reserve_location;
230-
let reachable = introduction.is_predecessor_of(location, self.body);
231-
reachable
232-
};
233-
234-
let other_borrows_of_local = self
235-
.borrow_set
236-
.local_map
237-
.get(&place.local)
238-
.into_iter()
239-
.flat_map(|bs| bs.iter())
240-
.copied();
241-
242-
// If the borrowed place is a local with no projections, all other borrows of this
243-
// local must conflict. This is purely an optimization so we don't have to call
244-
// `places_conflict` for every borrow.
245-
if place.projection.is_empty() {
246-
if !self.body.local_decls[place.local].is_ref_to_static() {
247-
self.kills
248-
.entry(location)
249-
.or_default()
250-
.extend(other_borrows_of_local.filter(|&loan| filter_unreachable_kills(loan)));
251-
}
252-
return;
253-
}
254-
255-
// By passing `PlaceConflictBias::NoOverlap`, we conservatively assume that any given
256-
// pair of array indices are not equal, so that when `places_conflict` returns true, we
257-
// will be assured that two places being compared definitely denotes the same sets of
258-
// locations.
259-
let definitely_conflicting_borrows = other_borrows_of_local
260-
.filter(|&i| {
261-
places_conflict(
262-
self.tcx,
263-
self.body,
264-
self.borrow_set[i].borrowed_place,
265-
place,
266-
PlaceConflictBias::NoOverlap,
267-
)
268-
})
269-
.filter(|&loan| filter_unreachable_kills(loan));
270-
271-
self.kills.entry(location).or_default().extend(definitely_conflicting_borrows);
272-
}
273-
274-
/// Records the borrows on the specified local as `killed`.
275-
fn record_killed_borrows_for_local(&mut self, local: Local, location: Location) {
276-
if let Some(borrow_indices) = self.borrow_set.local_map.get(&local) {
277-
self.kills.entry(location).or_default().extend(borrow_indices.iter());
278-
}
279-
}
280-
}
281-
282-
impl<'tcx> Visitor<'tcx> for KillsCollector<'_, 'tcx> {
283-
fn visit_statement(&mut self, statement: &Statement<'tcx>, location: Location) {
284-
// Make sure there are no remaining borrows for locals that have gone out of scope.
285-
if let StatementKind::StorageDead(local) = statement.kind {
286-
self.record_killed_borrows_for_local(local, location);
287-
}
288-
289-
self.super_statement(statement, location);
290-
}
291-
292-
fn visit_assign(&mut self, place: &Place<'tcx>, rvalue: &Rvalue<'tcx>, location: Location) {
293-
// When we see `X = ...`, then kill borrows of `(*X).foo` and so forth.
294-
self.record_killed_borrows_for_place(*place, location);
295-
self.super_assign(place, rvalue, location);
296-
}
297-
298-
fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, location: Location) {
299-
// A `Call` terminator's return value can be a local which has borrows, so we need to record
300-
// those as killed as well.
301-
if let TerminatorKind::Call { destination, .. } = terminator.kind {
302-
self.record_killed_borrows_for_place(destination, location);
303-
}
304-
305-
self.super_terminator(terminator, location);
306-
}
307-
}

compiler/rustc_borrowck/src/polonius/mod.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -146,8 +146,8 @@ impl PoloniusContext {
146146
/// - converting NLL typeck constraints to be localized
147147
/// - encoding liveness constraints
148148
///
149-
/// Then, this graph is traversed, and combined with kills, reachability is recorded as loan
150-
/// liveness, to be used by the loan scope and active loans computations.
149+
/// Then, this graph is traversed, reachability is recorded as loan liveness, to be used by the
150+
/// loan scope and active loans computations.
151151
///
152152
/// The constraint data will be used to compute errors and diagnostics.
153153
pub(crate) fn compute_loan_liveness<'tcx>(
@@ -182,8 +182,6 @@ impl PoloniusContext {
182182
// Now that we have a complete graph, we can compute reachability to trace the liveness of
183183
// loans for the next step in the chain, the NLL loan scope and active loans computations.
184184
let live_loans = compute_loan_liveness(
185-
tcx,
186-
body,
187185
regioncx.liveness_constraints(),
188186
regioncx.outlives_constraints(),
189187
borrow_set,

compiler/rustc_borrowck/src/polonius/typeck_constraints.rs

Lines changed: 4 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -47,9 +47,7 @@ pub(super) fn convert_typeck_constraints<'tcx>(
4747
tcx,
4848
body,
4949
stmt,
50-
liveness,
5150
&outlives_constraint,
52-
location,
5351
point,
5452
universal_regions,
5553
)
@@ -78,9 +76,7 @@ fn localize_statement_constraint<'tcx>(
7876
tcx: TyCtxt<'tcx>,
7977
body: &Body<'tcx>,
8078
stmt: &Statement<'tcx>,
81-
liveness: &LivenessValues,
8279
outlives_constraint: &OutlivesConstraint<'tcx>,
83-
current_location: Location,
8480
current_point: PointIndex,
8581
universal_regions: &UniversalRegions<'tcx>,
8682
) -> LocalizedOutlivesConstraint {
@@ -98,8 +94,8 @@ fn localize_statement_constraint<'tcx>(
9894
// - and that should be impossible in MIR
9995
//
10096
// When we have a more complete implementation in the future, tested with crater, etc,
101-
// we can relax this to a debug assert instead, or remove it.
102-
assert!(
97+
// we can remove this assertion. It's a debug assert because it can be expensive.
98+
debug_assert!(
10399
{
104100
let mut lhs_regions = FxHashSet::default();
105101
tcx.for_each_free_region(lhs, |region| {
@@ -119,16 +115,8 @@ fn localize_statement_constraint<'tcx>(
119115
"there should be no common regions between the LHS and RHS of an assignment"
120116
);
121117

122-
// As mentioned earlier, we should be tracking these better upstream but: we want to
123-
// relate the types on entry to the type of the place on exit. That is, outlives
124-
// constraints on the RHS are on entry, and outlives constraints to/from the LHS are on
125-
// exit (i.e. on entry to the successor location).
126118
let lhs_ty = body.local_decls[lhs.local].ty;
127-
let successor_location = Location {
128-
block: current_location.block,
129-
statement_index: current_location.statement_index + 1,
130-
};
131-
let successor_point = liveness.point_from_location(successor_location);
119+
let successor_point = current_point;
132120
compute_constraint_direction(
133121
tcx,
134122
outlives_constraint,
@@ -195,6 +183,7 @@ fn localize_terminator_constraint<'tcx>(
195183
}
196184
}
197185
}
186+
198187
/// For a given outlives constraint and CFG edge, returns the localized constraint with the
199188
/// appropriate `from`-`to` direction. This is computed according to whether the constraint flows to
200189
/// or from a free region in the given `value`, some kind of result for an effectful operation, like

src/tools/compiletest/src/runtest.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1766,7 +1766,7 @@ impl<'test> TestCx<'test> {
17661766

17671767
match self.config.compare_mode {
17681768
Some(CompareMode::Polonius) => {
1769-
rustc.args(&["-Zpolonius"]);
1769+
rustc.args(&["-Zpolonius=next"]);
17701770
}
17711771
Some(CompareMode::NextSolver) => {
17721772
rustc.args(&["-Znext-solver"]);

tests/crashes/135646.rs

Lines changed: 0 additions & 7 deletions
This file was deleted.

0 commit comments

Comments
 (0)