forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 6
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Auto merge of rust-lang#134268 - lqd:polonius-next, r=jackh726
Foundations of location-sensitive polonius I'd like 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 and 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 described in these posts, 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 currently but is a way to see these localized constraints: it's an NLL MIR dump + a dumb listing of the constraints, that can be dumped with `-Zdump-mir=polonius -Zpolonius=next`. Its current state is not intended to be a long-term thing, just for testing purposes -- I will replace its contents in the future with a different approach (an HTML+js file where we can more easily explore/filter/trace these constraints and loan reachability, 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 (and michael has offered to review these more mechanical changes if it'd help).
- Loading branch information
Showing
8 changed files
with
409 additions
and
34 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,45 @@ | ||
use rustc_middle::ty::RegionVid; | ||
use rustc_mir_dataflow::points::PointIndex; | ||
|
||
/// A localized outlives constraint reifies the CFG location where the outlives constraint holds, | ||
/// within the origins themselves as if they were different from point to point: from `a: b` | ||
/// outlives constraints to `a@p: b@p`, where `p` is the point in the CFG. | ||
/// | ||
/// 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). | ||
/// - 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. | ||
/// | ||
/// The `source` origin at `from` flows into the `target` origin at `to`. | ||
/// | ||
/// This dual of NLL's [crate::constraints::OutlivesConstraint] therefore encodes the | ||
/// position-dependent outlives constraints used by Polonius, to model the flow-sensitive loan | ||
/// propagation via reachability within a graph of localized constraints. | ||
#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash)] | ||
pub(crate) struct LocalizedOutlivesConstraint { | ||
pub source: RegionVid, | ||
pub from: PointIndex, | ||
pub target: RegionVid, | ||
pub to: PointIndex, | ||
} | ||
|
||
/// A container of [LocalizedOutlivesConstraint]s that can be turned into a traversable | ||
/// `rustc_data_structures` graph. | ||
#[derive(Clone, Default, Debug)] | ||
pub(crate) struct LocalizedOutlivesConstraintSet { | ||
pub outlives: Vec<LocalizedOutlivesConstraint>, | ||
} | ||
|
||
impl LocalizedOutlivesConstraintSet { | ||
pub(crate) fn push(&mut self, constraint: LocalizedOutlivesConstraint) { | ||
if constraint.source == constraint.target && constraint.from == constraint.to { | ||
// 'a@p: 'a@p is pretty uninteresting | ||
return; | ||
} | ||
self.outlives.push(constraint); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,104 @@ | ||
use std::io; | ||
|
||
use rustc_middle::mir::pretty::{PrettyPrintMirOptions, dump_mir_with_options}; | ||
use rustc_middle::mir::{Body, ClosureRegionRequirements, PassWhere}; | ||
use rustc_middle::ty::TyCtxt; | ||
use rustc_session::config::MirIncludeSpans; | ||
|
||
use crate::borrow_set::BorrowSet; | ||
use crate::polonius::{LocalizedOutlivesConstraint, LocalizedOutlivesConstraintSet}; | ||
use crate::{BorrowckInferCtxt, RegionInferenceContext}; | ||
|
||
/// `-Zdump-mir=polonius` dumps MIR annotated with NLL and polonius specific information. | ||
// Note: this currently duplicates most of NLL MIR, with some additions for the localized outlives | ||
// constraints. This is ok for now as this dump will change in the near future to an HTML file to | ||
// become more useful. | ||
pub(crate) fn dump_polonius_mir<'tcx>( | ||
infcx: &BorrowckInferCtxt<'tcx>, | ||
body: &Body<'tcx>, | ||
regioncx: &RegionInferenceContext<'tcx>, | ||
borrow_set: &BorrowSet<'tcx>, | ||
localized_outlives_constraints: Option<LocalizedOutlivesConstraintSet>, | ||
closure_region_requirements: &Option<ClosureRegionRequirements<'tcx>>, | ||
) { | ||
let tcx = infcx.tcx; | ||
if !tcx.sess.opts.unstable_opts.polonius.is_next_enabled() { | ||
return; | ||
} | ||
|
||
let localized_outlives_constraints = localized_outlives_constraints | ||
.expect("missing localized constraints with `-Zpolonius=next`"); | ||
|
||
// We want the NLL extra comments printed by default in NLL MIR dumps (they were removed in | ||
// #112346). Specifying `-Z mir-include-spans` on the CLI still has priority: for example, | ||
// they're always disabled in mir-opt tests to make working with blessed dumps easier. | ||
let options = PrettyPrintMirOptions { | ||
include_extra_comments: matches!( | ||
tcx.sess.opts.unstable_opts.mir_include_spans, | ||
MirIncludeSpans::On | MirIncludeSpans::Nll | ||
), | ||
}; | ||
|
||
dump_mir_with_options( | ||
tcx, | ||
false, | ||
"polonius", | ||
&0, | ||
body, | ||
|pass_where, out| { | ||
emit_polonius_mir( | ||
tcx, | ||
regioncx, | ||
closure_region_requirements, | ||
borrow_set, | ||
&localized_outlives_constraints, | ||
pass_where, | ||
out, | ||
) | ||
}, | ||
options, | ||
); | ||
} | ||
|
||
/// Produces the actual NLL + Polonius MIR sections to emit during the dumping process. | ||
fn emit_polonius_mir<'tcx>( | ||
tcx: TyCtxt<'tcx>, | ||
regioncx: &RegionInferenceContext<'tcx>, | ||
closure_region_requirements: &Option<ClosureRegionRequirements<'tcx>>, | ||
borrow_set: &BorrowSet<'tcx>, | ||
localized_outlives_constraints: &LocalizedOutlivesConstraintSet, | ||
pass_where: PassWhere, | ||
out: &mut dyn io::Write, | ||
) -> io::Result<()> { | ||
// Emit the regular NLL front-matter | ||
crate::nll::emit_nll_mir( | ||
tcx, | ||
regioncx, | ||
closure_region_requirements, | ||
borrow_set, | ||
pass_where.clone(), | ||
out, | ||
)?; | ||
|
||
let liveness = regioncx.liveness_constraints(); | ||
|
||
// Add localized outlives constraints | ||
match pass_where { | ||
PassWhere::BeforeCFG => { | ||
if localized_outlives_constraints.outlives.len() > 0 { | ||
writeln!(out, "| Localized constraints")?; | ||
|
||
for constraint in &localized_outlives_constraints.outlives { | ||
let LocalizedOutlivesConstraint { source, from, target, to } = constraint; | ||
let from = liveness.location_from_point(*from); | ||
let to = liveness.location_from_point(*to); | ||
writeln!(out, "| {source:?} at {from:?} -> {target:?} at {to:?}")?; | ||
} | ||
writeln!(out, "|")?; | ||
} | ||
} | ||
_ => {} | ||
} | ||
|
||
Ok(()) | ||
} |
Oops, something went wrong.