Skip to content
This repository was archived by the owner on May 28, 2025. It is now read-only.

Commit 0b8e535

Browse files
committed
Auto merge of rust-lang#134268 - lqd:polonius-next, r=<try>
Foundations of location-sensitive polonius I'd to land the prototype I'm describing in the [polonius project goal](rust-lang/rust-project-goals#118). It still is incomplete and naive and terrible but it's working "well enough" to consider landing. I'd also like to make review easier by not opening a huge PR, but have a couple small-ish ones (the +/- line change summary of this PR looks big, but >80% is moving datalog to a single place). This PR starts laying the foundation for that work: - it refactors and collects 99% of the old datalog fact gen, which was spread around everywhere, into a single dedicated module. It's still present at 3 small places (one of which we should revert anyways) that are kinda deep within localized components that are not as easily extractable into the rest of fact gen, so it's fine for now. - starts introducing the localized constraints, the building blocks of the naive way of implementing the location-sensitive analysis in-tree, which is roughly sketched out in https://smallcultfollowing.com/babysteps/blog/2023/09/22/polonius-part-1/ and https://smallcultfollowing.com/babysteps/blog/2023/09/29/polonius-part-2/ but with a different vibe than per-point environments, just `r1@p: r2@q` constraints. - sets up the skeleton of generating these localized constraints: converting NLL typeck constraints, and creating liveness constraints - introduces the polonius dual to NLL MIR to help development and debugging. It doesn't do much original currently but is a way to see these localized constraints: its an NLL MIR dump + a dumb listing of the constraints. It's not intended to be a long-term thing, it's for testing purposes, and I will replace its contents in the future with a different approach (an HTML where we can more easily explore these constraints, have mermaid graphs of the usual graphviz dumps, etc) I've started documenting the approach in this PR, I'll add more in the future. It's quite simple, and should be very clear when more constraints are introduced anyways. r? `@matthewjasper` Best reviewed per commit so that the datalog move is less bothersome to read, but if you'd prefer we separate that into a different PR, I can do that.
2 parents 4847d6a + 1331ccb commit 0b8e535

File tree

16 files changed

+772
-427
lines changed

16 files changed

+772
-427
lines changed

compiler/rustc_borrowck/src/lib.rs

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -206,6 +206,7 @@ fn do_mir_borrowck<'tcx>(
206206
polonius_output,
207207
opt_closure_req,
208208
nll_errors,
209+
localized_outlives_constraints,
209210
} = nll::compute_regions(
210211
&infcx,
211212
free_regions,
@@ -318,6 +319,16 @@ fn do_mir_borrowck<'tcx>(
318319

319320
mbcx.report_move_errors();
320321

322+
// If requested, dump polonius MIR.
323+
polonius::dump_polonius_mir(
324+
&infcx,
325+
body,
326+
&regioncx,
327+
&borrow_set,
328+
&localized_outlives_constraints,
329+
&opt_closure_req,
330+
);
331+
321332
// For each non-user used mutable variable, check if it's been assigned from
322333
// a user-declared local. If so, then put that local into the used_mut set.
323334
// Note that this set is expected to be small - only upvars from closures

compiler/rustc_borrowck/src/nll.rs

Lines changed: 65 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ use crate::consumers::ConsumerOptions;
2929
use crate::diagnostics::RegionErrors;
3030
use crate::facts::{AllFacts, AllFactsExt, RustcFacts};
3131
use crate::location::LocationTable;
32+
use crate::polonius::LocalizedOutlivesConstraintSet;
3233
use crate::region_infer::RegionInferenceContext;
3334
use crate::type_check::{self, MirTypeckResults};
3435
use crate::universal_regions::UniversalRegions;
@@ -45,6 +46,9 @@ pub(crate) struct NllOutput<'tcx> {
4546
pub polonius_output: Option<Box<PoloniusOutput>>,
4647
pub opt_closure_req: Option<ClosureRegionRequirements<'tcx>>,
4748
pub nll_errors: RegionErrors<'tcx>,
49+
50+
/// When using `-Zpolonius=next`: the localized typeck and liveness constraints.
51+
pub localized_outlives_constraints: LocalizedOutlivesConstraintSet,
4852
}
4953

5054
/// Rewrites the regions in the MIR to use NLL variables, also scraping out the set of universal
@@ -116,14 +120,15 @@ pub(crate) fn compute_regions<'a, 'tcx>(
116120
let var_origins = infcx.get_region_var_origins();
117121

118122
// If requested, emit legacy polonius facts.
119-
polonius::emit_facts(
123+
polonius::legacy::emit_facts(
120124
&mut all_facts,
121125
infcx.tcx,
122126
location_table,
123127
body,
124128
borrow_set,
125129
move_data,
126130
&universal_region_relations,
131+
&constraints,
127132
);
128133

129134
let mut regioncx = RegionInferenceContext::new(
@@ -134,6 +139,18 @@ pub(crate) fn compute_regions<'a, 'tcx>(
134139
elements,
135140
);
136141

142+
// If requested for `-Zpolonius=next`, convert NLL constraints to localized outlives
143+
// constraints.
144+
let mut localized_outlives_constraints = LocalizedOutlivesConstraintSet::default();
145+
if infcx.tcx.sess.opts.unstable_opts.polonius.is_next_enabled() {
146+
polonius::create_localized_constraints(
147+
&mut regioncx,
148+
infcx.infcx.tcx,
149+
body,
150+
&mut localized_outlives_constraints,
151+
);
152+
}
153+
137154
// If requested: dump NLL facts, and run legacy polonius analysis.
138155
let polonius_output = all_facts.as_ref().and_then(|all_facts| {
139156
if infcx.tcx.sess.opts.unstable_opts.nll_facts {
@@ -174,6 +191,7 @@ pub(crate) fn compute_regions<'a, 'tcx>(
174191
polonius_output,
175192
opt_closure_req: closure_region_requirements,
176193
nll_errors,
194+
localized_outlives_constraints,
177195
}
178196
}
179197

@@ -214,40 +232,7 @@ pub(super) fn dump_nll_mir<'tcx>(
214232
&0,
215233
body,
216234
|pass_where, out| {
217-
match pass_where {
218-
// Before the CFG, dump out the values for each region variable.
219-
PassWhere::BeforeCFG => {
220-
regioncx.dump_mir(tcx, out)?;
221-
writeln!(out, "|")?;
222-
223-
if let Some(closure_region_requirements) = closure_region_requirements {
224-
writeln!(out, "| Free Region Constraints")?;
225-
for_each_region_constraint(tcx, closure_region_requirements, &mut |msg| {
226-
writeln!(out, "| {msg}")
227-
})?;
228-
writeln!(out, "|")?;
229-
}
230-
231-
if borrow_set.len() > 0 {
232-
writeln!(out, "| Borrows")?;
233-
for (borrow_idx, borrow_data) in borrow_set.iter_enumerated() {
234-
writeln!(
235-
out,
236-
"| {:?}: issued at {:?} in {:?}",
237-
borrow_idx, borrow_data.reserve_location, borrow_data.region
238-
)?;
239-
}
240-
writeln!(out, "|")?;
241-
}
242-
}
243-
244-
PassWhere::BeforeLocation(_) => {}
245-
246-
PassWhere::AfterTerminator(_) => {}
247-
248-
PassWhere::BeforeBlock(_) | PassWhere::AfterLocation(_) | PassWhere::AfterCFG => {}
249-
}
250-
Ok(())
235+
emit_nll_mir(tcx, regioncx, closure_region_requirements, borrow_set, pass_where, out)
251236
},
252237
options,
253238
);
@@ -265,6 +250,51 @@ pub(super) fn dump_nll_mir<'tcx>(
265250
};
266251
}
267252

253+
/// Produces the actual NLL MIR sections to emit during the dumping process.
254+
pub(crate) fn emit_nll_mir<'tcx>(
255+
tcx: TyCtxt<'tcx>,
256+
regioncx: &RegionInferenceContext<'tcx>,
257+
closure_region_requirements: &Option<ClosureRegionRequirements<'tcx>>,
258+
borrow_set: &BorrowSet<'tcx>,
259+
pass_where: PassWhere,
260+
out: &mut dyn io::Write,
261+
) -> io::Result<()> {
262+
match pass_where {
263+
// Before the CFG, dump out the values for each region variable.
264+
PassWhere::BeforeCFG => {
265+
regioncx.dump_mir(tcx, out)?;
266+
writeln!(out, "|")?;
267+
268+
if let Some(closure_region_requirements) = closure_region_requirements {
269+
writeln!(out, "| Free Region Constraints")?;
270+
for_each_region_constraint(tcx, closure_region_requirements, &mut |msg| {
271+
writeln!(out, "| {msg}")
272+
})?;
273+
writeln!(out, "|")?;
274+
}
275+
276+
if borrow_set.len() > 0 {
277+
writeln!(out, "| Borrows")?;
278+
for (borrow_idx, borrow_data) in borrow_set.iter_enumerated() {
279+
writeln!(
280+
out,
281+
"| {:?}: issued at {:?} in {:?}",
282+
borrow_idx, borrow_data.reserve_location, borrow_data.region
283+
)?;
284+
}
285+
writeln!(out, "|")?;
286+
}
287+
}
288+
289+
PassWhere::BeforeLocation(_) => {}
290+
291+
PassWhere::AfterTerminator(_) => {}
292+
293+
PassWhere::BeforeBlock(_) | PassWhere::AfterLocation(_) | PassWhere::AfterCFG => {}
294+
}
295+
Ok(())
296+
}
297+
268298
#[allow(rustc::diagnostic_outside_of_impl)]
269299
#[allow(rustc::untranslatable_diagnostic)]
270300
pub(super) fn dump_annotation<'tcx, 'infcx>(
Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
use rustc_middle::ty::RegionVid;
2+
use rustc_mir_dataflow::points::PointIndex;
3+
4+
/// A localized outlives constraint reifies the CFG location where the outlives constraint holds,
5+
/// within the origins themselves as if they were different from point to point: from `a: b`
6+
/// outlives constraints to `a@p: b@p`, where `p` is the point in the CFG.
7+
///
8+
/// This models two sources of constraints:
9+
/// - 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).
13+
/// - constraints that traverse the CFG via the same region, `a@p: a@q`, where `p` is a predecessor
14+
/// of `q`. These depend on the liveness of the regions at these points, as well as their
15+
/// variance.
16+
///
17+
/// The `source` origin at `from` flows into the `target` origin at `to`.
18+
///
19+
/// This dual of NLL's [crate::constraints::OutlivesConstraint] therefore encodes the
20+
/// position-dependent outlives constraints used by Polonius, to model the flow-sensitive loan
21+
/// propagation via reachability within a graph of localized constraints.
22+
#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash)]
23+
pub(crate) struct LocalizedOutlivesConstraint {
24+
pub source: RegionVid,
25+
pub from: PointIndex,
26+
pub target: RegionVid,
27+
pub to: PointIndex,
28+
}
29+
30+
/// A container of [LocalizedOutlivesConstraint]s that can be turned into a traversable
31+
/// `rustc_data_structures` graph.
32+
#[derive(Clone, Default, Debug)]
33+
pub(crate) struct LocalizedOutlivesConstraintSet {
34+
pub outlives: Vec<LocalizedOutlivesConstraint>,
35+
}
36+
37+
impl LocalizedOutlivesConstraintSet {
38+
pub(crate) fn push(&mut self, constraint: LocalizedOutlivesConstraint) {
39+
if constraint.source == constraint.target && constraint.from == constraint.to {
40+
// 'a@p: 'a@p is pretty uninteresting
41+
return;
42+
}
43+
self.outlives.push(constraint);
44+
}
45+
}
Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
use std::io;
2+
3+
use rustc_middle::mir::pretty::{PrettyPrintMirOptions, dump_mir_with_options};
4+
use rustc_middle::mir::{Body, ClosureRegionRequirements, PassWhere};
5+
use rustc_middle::ty::TyCtxt;
6+
use rustc_session::config::MirIncludeSpans;
7+
8+
use crate::borrow_set::BorrowSet;
9+
use crate::polonius::{LocalizedOutlivesConstraint, LocalizedOutlivesConstraintSet};
10+
use crate::{BorrowckInferCtxt, RegionInferenceContext};
11+
12+
/// `-Zdump-mir=polonius` dumps MIR annotated with NLL and polonius specific information.
13+
// Note: this currently duplicates most of NLL MIR, with some additions for the localized outlives
14+
// constraints. This is ok for now as this dump will change in the near future to an HTML file to
15+
// become more useful.
16+
pub(crate) fn dump_polonius_mir<'tcx>(
17+
infcx: &BorrowckInferCtxt<'tcx>,
18+
body: &Body<'tcx>,
19+
regioncx: &RegionInferenceContext<'tcx>,
20+
borrow_set: &BorrowSet<'tcx>,
21+
localized_outlives_constraints: &LocalizedOutlivesConstraintSet,
22+
closure_region_requirements: &Option<ClosureRegionRequirements<'tcx>>,
23+
) {
24+
let tcx = infcx.tcx;
25+
if !tcx.sess.opts.unstable_opts.polonius.is_next_enabled() {
26+
return;
27+
}
28+
29+
// We want the NLL extra comments printed by default in NLL MIR dumps (they were removed in
30+
// #112346). Specifying `-Z mir-include-spans` on the CLI still has priority: for example,
31+
// they're always disabled in mir-opt tests to make working with blessed dumps easier.
32+
let options = PrettyPrintMirOptions {
33+
include_extra_comments: matches!(
34+
tcx.sess.opts.unstable_opts.mir_include_spans,
35+
MirIncludeSpans::On | MirIncludeSpans::Nll
36+
),
37+
};
38+
39+
dump_mir_with_options(
40+
tcx,
41+
false,
42+
"polonius",
43+
&0,
44+
body,
45+
|pass_where, out| {
46+
emit_polonius_mir(
47+
tcx,
48+
regioncx,
49+
closure_region_requirements,
50+
borrow_set,
51+
localized_outlives_constraints,
52+
pass_where,
53+
out,
54+
)
55+
},
56+
options,
57+
);
58+
}
59+
60+
/// Produces the actual NLL + Polonius MIR sections to emit during the dumping process.
61+
fn emit_polonius_mir<'tcx>(
62+
tcx: TyCtxt<'tcx>,
63+
regioncx: &RegionInferenceContext<'tcx>,
64+
closure_region_requirements: &Option<ClosureRegionRequirements<'tcx>>,
65+
borrow_set: &BorrowSet<'tcx>,
66+
localized_outlives_constraints: &LocalizedOutlivesConstraintSet,
67+
pass_where: PassWhere,
68+
out: &mut dyn io::Write,
69+
) -> io::Result<()> {
70+
// Emit the regular NLL front-matter
71+
crate::nll::emit_nll_mir(
72+
tcx,
73+
regioncx,
74+
closure_region_requirements,
75+
borrow_set,
76+
pass_where.clone(),
77+
out,
78+
)?;
79+
80+
let liveness = regioncx.liveness_constraints();
81+
82+
// Add localized outlives constraints
83+
match pass_where {
84+
PassWhere::BeforeCFG => {
85+
if localized_outlives_constraints.outlives.len() > 0 {
86+
writeln!(out, "| Localized constraints")?;
87+
88+
for constraint in &localized_outlives_constraints.outlives {
89+
let LocalizedOutlivesConstraint { source, from, target, to } = constraint;
90+
let from = liveness.location_from_point(*from);
91+
let to = liveness.location_from_point(*to);
92+
writeln!(out, "| {source:?} at {from:?} -> {target:?} at {to:?}")?;
93+
}
94+
writeln!(out, "|")?;
95+
}
96+
}
97+
_ => {}
98+
}
99+
100+
Ok(())
101+
}

0 commit comments

Comments
 (0)