Skip to content

Commit b84ab57

Browse files
authored
Rollup merge of #111840 - voidc:borrowck-consumers, r=oli-obk
Expose more information in `get_body_with_borrowck_facts` Verification tools for Rust such as, for example, Creusot or Prusti would benefit from having access to more information computed by the borrow checker. As a first step in that direction, #86977 added the `get_body_with_borrowck_facts` API, allowing compiler consumers to obtain a `mir::Body` with accompanying borrow checker information. At RustVerify 2023, multiple people working on verification tools expressed their need for a more comprehensive API. While eventually borrow information could be part of Stable MIR, in the meantime, this PR proposes a more limited approach, extending the existing `get_body_with_borrowck_facts` API. In summary, we propose the following changes: - Permit obtaining the borrow-checked body without necessarily running Polonius - Return the `BorrowSet` and the `RegionInferenceContext` in `BodyWithBorrowckFacts` - Provide a way to compute the `borrows_out_of_scope_at_location` map - Make some helper methods public This is similar to #108328 but smaller in scope. `@smoelius` Do you think these changes would also be sufficient for your needs? r? `@oli-obk` cc `@JonasAlaif`
2 parents a9a4c9b + 8dac074 commit b84ab57

File tree

9 files changed

+144
-66
lines changed

9 files changed

+144
-66
lines changed

compiler/rustc_borrowck/src/borrow_set.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ pub struct BorrowSet<'tcx> {
3030
/// Map from local to all the borrows on that local.
3131
pub local_map: FxIndexMap<mir::Local, FxIndexSet<BorrowIndex>>,
3232

33-
pub(crate) locals_state_at_exit: LocalsStateAtExit,
33+
pub locals_state_at_exit: LocalsStateAtExit,
3434
}
3535

3636
impl<'tcx> Index<BorrowIndex> for BorrowSet<'tcx> {
@@ -153,7 +153,7 @@ impl<'tcx> BorrowSet<'tcx> {
153153
self.activation_map.get(&location).map_or(&[], |activations| &activations[..])
154154
}
155155

156-
pub(crate) fn len(&self) -> usize {
156+
pub fn len(&self) -> usize {
157157
self.location_map.len()
158158
}
159159

compiler/rustc_borrowck/src/consumers.rs

+86-9
Original file line numberDiff line numberDiff line change
@@ -3,22 +3,95 @@
33
//! This file provides API for compiler consumers.
44
55
use rustc_hir::def_id::LocalDefId;
6-
use rustc_index::IndexSlice;
6+
use rustc_index::{IndexSlice, IndexVec};
77
use rustc_infer::infer::{DefiningAnchor, TyCtxtInferExt};
8-
use rustc_middle::mir::Body;
8+
use rustc_middle::mir::{Body, Promoted};
99
use rustc_middle::ty::TyCtxt;
10+
use std::rc::Rc;
11+
12+
use crate::borrow_set::BorrowSet;
1013

1114
pub use super::{
15+
constraints::OutlivesConstraint,
16+
dataflow::{calculate_borrows_out_of_scope_at_location, BorrowIndex, Borrows},
1217
facts::{AllFacts as PoloniusInput, RustcFacts},
1318
location::{LocationTable, RichLocation},
1419
nll::PoloniusOutput,
15-
BodyWithBorrowckFacts,
20+
place_ext::PlaceExt,
21+
places_conflict::{places_conflict, PlaceConflictBias},
22+
region_infer::RegionInferenceContext,
1623
};
1724

18-
/// This function computes Polonius facts for the given body. It makes a copy of
19-
/// the body because it needs to regenerate the region identifiers. This function
20-
/// should never be invoked during a typical compilation session due to performance
21-
/// issues with Polonius.
25+
/// Options determining the output behavior of [`get_body_with_borrowck_facts`].
26+
///
27+
/// If executing under `-Z polonius` the choice here has no effect, and everything as if
28+
/// [`PoloniusOutputFacts`](ConsumerOptions::PoloniusOutputFacts) had been selected
29+
/// will be retrieved.
30+
#[derive(Debug, Copy, Clone)]
31+
pub enum ConsumerOptions {
32+
/// Retrieve the [`Body`] along with the [`BorrowSet`](super::borrow_set::BorrowSet)
33+
/// and [`RegionInferenceContext`]. If you would like the body only, use
34+
/// [`TyCtxt::mir_promoted`].
35+
///
36+
/// These can be used in conjunction with [`calculate_borrows_out_of_scope_at_location`].
37+
RegionInferenceContext,
38+
/// The recommended option. Retrieves the maximal amount of information
39+
/// without significant slowdowns.
40+
///
41+
/// Implies [`RegionInferenceContext`](ConsumerOptions::RegionInferenceContext),
42+
/// and additionally retrieve the [`LocationTable`] and [`PoloniusInput`] that
43+
/// would be given to Polonius. Critically, this does not run Polonius, which
44+
/// one may want to avoid due to performance issues on large bodies.
45+
PoloniusInputFacts,
46+
/// Implies [`PoloniusInputFacts`](ConsumerOptions::PoloniusInputFacts),
47+
/// and additionally runs Polonius to calculate the [`PoloniusOutput`].
48+
PoloniusOutputFacts,
49+
}
50+
51+
impl ConsumerOptions {
52+
/// Should the Polonius input facts be computed?
53+
pub(crate) fn polonius_input(&self) -> bool {
54+
matches!(self, Self::PoloniusInputFacts | Self::PoloniusOutputFacts)
55+
}
56+
/// Should we run Polonius and collect the output facts?
57+
pub(crate) fn polonius_output(&self) -> bool {
58+
matches!(self, Self::PoloniusOutputFacts)
59+
}
60+
}
61+
62+
/// A `Body` with information computed by the borrow checker. This struct is
63+
/// intended to be consumed by compiler consumers.
64+
///
65+
/// We need to include the MIR body here because the region identifiers must
66+
/// match the ones in the Polonius facts.
67+
pub struct BodyWithBorrowckFacts<'tcx> {
68+
/// A mir body that contains region identifiers.
69+
pub body: Body<'tcx>,
70+
/// The mir bodies of promoteds.
71+
pub promoted: IndexVec<Promoted, Body<'tcx>>,
72+
/// The set of borrows occurring in `body` with data about them.
73+
pub borrow_set: Rc<BorrowSet<'tcx>>,
74+
/// Context generated during borrowck, intended to be passed to
75+
/// [`calculate_borrows_out_of_scope_at_location`].
76+
pub region_inference_context: Rc<RegionInferenceContext<'tcx>>,
77+
/// The table that maps Polonius points to locations in the table.
78+
/// Populated when using [`ConsumerOptions::PoloniusInputFacts`]
79+
/// or [`ConsumerOptions::PoloniusOutputFacts`].
80+
pub location_table: Option<LocationTable>,
81+
/// Polonius input facts.
82+
/// Populated when using [`ConsumerOptions::PoloniusInputFacts`]
83+
/// or [`ConsumerOptions::PoloniusOutputFacts`].
84+
pub input_facts: Option<Box<PoloniusInput>>,
85+
/// Polonius output facts. Populated when using
86+
/// [`ConsumerOptions::PoloniusOutputFacts`].
87+
pub output_facts: Option<Rc<PoloniusOutput>>,
88+
}
89+
90+
/// This function computes borrowck facts for the given body. The [`ConsumerOptions`]
91+
/// determine which facts are returned. This function makes a copy of the body because
92+
/// it needs to regenerate the region identifiers. It should never be invoked during a
93+
/// typical compilation session due to the unnecessary overhead of returning
94+
/// [`BodyWithBorrowckFacts`].
2295
///
2396
/// Note:
2497
/// * This function will panic if the required body was already stolen. This
@@ -28,10 +101,14 @@ pub use super::{
28101
/// that shows how to do this at `tests/run-make/obtain-borrowck/`.
29102
///
30103
/// * Polonius is highly unstable, so expect regular changes in its signature or other details.
31-
pub fn get_body_with_borrowck_facts(tcx: TyCtxt<'_>, def: LocalDefId) -> BodyWithBorrowckFacts<'_> {
104+
pub fn get_body_with_borrowck_facts(
105+
tcx: TyCtxt<'_>,
106+
def: LocalDefId,
107+
options: ConsumerOptions,
108+
) -> BodyWithBorrowckFacts<'_> {
32109
let (input_body, promoted) = tcx.mir_promoted(def);
33110
let infcx = tcx.infer_ctxt().with_opaque_type_inference(DefiningAnchor::Bind(def)).build();
34111
let input_body: &Body<'_> = &input_body.borrow();
35112
let promoted: &IndexSlice<_, _> = &promoted.borrow();
36-
*super::do_mir_borrowck(&infcx, input_body, promoted, true).1.unwrap()
113+
*super::do_mir_borrowck(&infcx, input_body, promoted, Some(options)).1.unwrap()
37114
}

compiler/rustc_borrowck/src/dataflow.rs

+20-15
Original file line numberDiff line numberDiff line change
@@ -231,27 +231,32 @@ impl<'tcx> OutOfScopePrecomputer<'_, 'tcx> {
231231
}
232232
}
233233

234+
pub fn calculate_borrows_out_of_scope_at_location<'tcx>(
235+
body: &Body<'tcx>,
236+
regioncx: &RegionInferenceContext<'tcx>,
237+
borrow_set: &BorrowSet<'tcx>,
238+
) -> FxIndexMap<Location, Vec<BorrowIndex>> {
239+
let mut prec = OutOfScopePrecomputer::new(body, regioncx);
240+
for (borrow_index, borrow_data) in borrow_set.iter_enumerated() {
241+
let borrow_region = borrow_data.region;
242+
let location = borrow_data.reserve_location;
243+
244+
prec.precompute_borrows_out_of_scope(borrow_index, borrow_region, location);
245+
}
246+
247+
prec.borrows_out_of_scope_at_location
248+
}
249+
234250
impl<'a, 'tcx> Borrows<'a, 'tcx> {
235-
pub(crate) fn new(
251+
pub fn new(
236252
tcx: TyCtxt<'tcx>,
237253
body: &'a Body<'tcx>,
238254
nonlexical_regioncx: &'a RegionInferenceContext<'tcx>,
239255
borrow_set: &'a BorrowSet<'tcx>,
240256
) -> Self {
241-
let mut prec = OutOfScopePrecomputer::new(body, nonlexical_regioncx);
242-
for (borrow_index, borrow_data) in borrow_set.iter_enumerated() {
243-
let borrow_region = borrow_data.region;
244-
let location = borrow_data.reserve_location;
245-
246-
prec.precompute_borrows_out_of_scope(borrow_index, borrow_region, location);
247-
}
248-
249-
Borrows {
250-
tcx,
251-
body,
252-
borrow_set,
253-
borrows_out_of_scope_at_location: prec.borrows_out_of_scope_at_location,
254-
}
257+
let borrows_out_of_scope_at_location =
258+
calculate_borrows_out_of_scope_at_location(body, nonlexical_regioncx, borrow_set);
259+
Borrows { tcx, body, borrow_set, borrows_out_of_scope_at_location }
255260
}
256261

257262
pub fn location(&self, idx: BorrowIndex) -> &Location {

compiler/rustc_borrowck/src/lib.rs

+14-29
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ use crate::session_diagnostics::VarNeedNotMut;
6161
use self::diagnostics::{AccessKind, RegionName};
6262
use self::location::LocationTable;
6363
use self::prefixes::PrefixSet;
64-
use facts::AllFacts;
64+
use consumers::{BodyWithBorrowckFacts, ConsumerOptions};
6565

6666
use self::path_utils::*;
6767

@@ -143,23 +143,23 @@ fn mir_borrowck(tcx: TyCtxt<'_>, def: LocalDefId) -> &BorrowCheckResult<'_> {
143143
tcx.infer_ctxt().with_opaque_type_inference(DefiningAnchor::Bind(hir_owner.def_id)).build();
144144
let input_body: &Body<'_> = &input_body.borrow();
145145
let promoted: &IndexSlice<_, _> = &promoted.borrow();
146-
let opt_closure_req = do_mir_borrowck(&infcx, input_body, promoted, false).0;
146+
let opt_closure_req = do_mir_borrowck(&infcx, input_body, promoted, None).0;
147147
debug!("mir_borrowck done");
148148

149149
tcx.arena.alloc(opt_closure_req)
150150
}
151151

152152
/// Perform the actual borrow checking.
153153
///
154-
/// If `return_body_with_facts` is true, then return the body with non-erased
155-
/// region ids on which the borrow checking was performed together with Polonius
156-
/// facts.
154+
/// Use `consumer_options: None` for the default behavior of returning
155+
/// [`BorrowCheckResult`] only. Otherwise, return [`BodyWithBorrowckFacts`] according
156+
/// to the given [`ConsumerOptions`].
157157
#[instrument(skip(infcx, input_body, input_promoted), fields(id=?input_body.source.def_id()), level = "debug")]
158158
fn do_mir_borrowck<'tcx>(
159159
infcx: &InferCtxt<'tcx>,
160160
input_body: &Body<'tcx>,
161161
input_promoted: &IndexSlice<Promoted, Body<'tcx>>,
162-
return_body_with_facts: bool,
162+
consumer_options: Option<ConsumerOptions>,
163163
) -> (BorrowCheckResult<'tcx>, Option<Box<BodyWithBorrowckFacts<'tcx>>>) {
164164
let def = input_body.source.def_id().expect_local();
165165
debug!(?def);
@@ -240,8 +240,6 @@ fn do_mir_borrowck<'tcx>(
240240
let borrow_set =
241241
Rc::new(BorrowSet::build(tcx, body, locals_are_invalidated_at_exit, &mdpe.move_data));
242242

243-
let use_polonius = return_body_with_facts || infcx.tcx.sess.opts.unstable_opts.polonius;
244-
245243
// Compute non-lexical lifetimes.
246244
let nll::NllOutput {
247245
regioncx,
@@ -261,7 +259,7 @@ fn do_mir_borrowck<'tcx>(
261259
&mdpe.move_data,
262260
&borrow_set,
263261
&upvars,
264-
use_polonius,
262+
consumer_options,
265263
);
266264

267265
// Dump MIR results into a file, if that is enabled. This let us
@@ -441,13 +439,16 @@ fn do_mir_borrowck<'tcx>(
441439
tainted_by_errors,
442440
};
443441

444-
let body_with_facts = if return_body_with_facts {
445-
let output_facts = mbcx.polonius_output.expect("Polonius output was not computed");
442+
let body_with_facts = if consumer_options.is_some() {
443+
let output_facts = mbcx.polonius_output;
446444
Some(Box::new(BodyWithBorrowckFacts {
447445
body: body_owned,
448-
input_facts: *polonius_input.expect("Polonius input facts were not generated"),
446+
promoted,
447+
borrow_set,
448+
region_inference_context: regioncx,
449+
location_table: polonius_input.as_ref().map(|_| location_table_owned),
450+
input_facts: polonius_input,
449451
output_facts,
450-
location_table: location_table_owned,
451452
}))
452453
} else {
453454
None
@@ -458,22 +459,6 @@ fn do_mir_borrowck<'tcx>(
458459
(result, body_with_facts)
459460
}
460461

461-
/// A `Body` with information computed by the borrow checker. This struct is
462-
/// intended to be consumed by compiler consumers.
463-
///
464-
/// We need to include the MIR body here because the region identifiers must
465-
/// match the ones in the Polonius facts.
466-
pub struct BodyWithBorrowckFacts<'tcx> {
467-
/// A mir body that contains region identifiers.
468-
pub body: Body<'tcx>,
469-
/// Polonius input facts.
470-
pub input_facts: AllFacts,
471-
/// Polonius output facts.
472-
pub output_facts: Rc<self::nll::PoloniusOutput>,
473-
/// The table that maps Polonius points to locations in the table.
474-
pub location_table: LocationTable,
475-
}
476-
477462
pub struct BorrowckInferCtxt<'cx, 'tcx> {
478463
pub(crate) infcx: &'cx InferCtxt<'tcx>,
479464
pub(crate) reg_var_to_origin: RefCell<FxIndexMap<ty::RegionVid, RegionCtxt>>,

compiler/rustc_borrowck/src/nll.rs

+9-4
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ use rustc_mir_dataflow::ResultsCursor;
2727
use crate::{
2828
borrow_set::BorrowSet,
2929
constraint_generation,
30+
consumers::ConsumerOptions,
3031
diagnostics::RegionErrors,
3132
facts::{AllFacts, AllFactsExt, RustcFacts},
3233
invalidation,
@@ -165,10 +166,14 @@ pub(crate) fn compute_regions<'cx, 'tcx>(
165166
move_data: &MoveData<'tcx>,
166167
borrow_set: &BorrowSet<'tcx>,
167168
upvars: &[Upvar<'tcx>],
168-
use_polonius: bool,
169+
consumer_options: Option<ConsumerOptions>,
169170
) -> NllOutput<'tcx> {
171+
let polonius_input = consumer_options.map(|c| c.polonius_input()).unwrap_or_default()
172+
|| infcx.tcx.sess.opts.unstable_opts.polonius;
173+
let polonius_output = consumer_options.map(|c| c.polonius_output()).unwrap_or_default()
174+
|| infcx.tcx.sess.opts.unstable_opts.polonius;
170175
let mut all_facts =
171-
(use_polonius || AllFacts::enabled(infcx.tcx)).then_some(AllFacts::default());
176+
(polonius_input || AllFacts::enabled(infcx.tcx)).then_some(AllFacts::default());
172177

173178
let universal_regions = Rc::new(universal_regions);
174179

@@ -189,7 +194,7 @@ pub(crate) fn compute_regions<'cx, 'tcx>(
189194
move_data,
190195
elements,
191196
upvars,
192-
use_polonius,
197+
polonius_input,
193198
);
194199

195200
if let Some(all_facts) = &mut all_facts {
@@ -284,7 +289,7 @@ pub(crate) fn compute_regions<'cx, 'tcx>(
284289
all_facts.write_to_dir(dir_path, location_table).unwrap();
285290
}
286291

287-
if use_polonius {
292+
if polonius_output {
288293
let algorithm =
289294
env::var("POLONIUS_ALGORITHM").unwrap_or_else(|_| String::from("Hybrid"));
290295
let algorithm = Algorithm::from_str(&algorithm).unwrap();

compiler/rustc_borrowck/src/place_ext.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ use rustc_middle::mir::{Body, Mutability, Place};
77
use rustc_middle::ty::{self, TyCtxt};
88

99
/// Extension methods for the `Place` type.
10-
pub(crate) trait PlaceExt<'tcx> {
10+
pub trait PlaceExt<'tcx> {
1111
/// Returns `true` if we can safely ignore borrows of this place.
1212
/// This is true whenever there is no action that the user can do
1313
/// to the place `self` that would invalidate the borrow. This is true

compiler/rustc_borrowck/src/places_conflict.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,15 +16,15 @@ use std::iter;
1616
/// being run in the calling context, the conservative choice is to assume the compared indices
1717
/// are disjoint (and therefore, do not overlap).
1818
#[derive(Copy, Clone, Debug, Eq, PartialEq)]
19-
pub(crate) enum PlaceConflictBias {
19+
pub enum PlaceConflictBias {
2020
Overlap,
2121
NoOverlap,
2222
}
2323

2424
/// Helper function for checking if places conflict with a mutable borrow and deep access depth.
2525
/// This is used to check for places conflicting outside of the borrow checking code (such as in
2626
/// dataflow).
27-
pub(crate) fn places_conflict<'tcx>(
27+
pub fn places_conflict<'tcx>(
2828
tcx: TyCtxt<'tcx>,
2929
body: &Body<'tcx>,
3030
borrow_place: Place<'tcx>,

compiler/rustc_borrowck/src/region_infer/mod.rs

+6-1
Original file line numberDiff line numberDiff line change
@@ -585,6 +585,11 @@ impl<'tcx> RegionInferenceContext<'tcx> {
585585
self.universal_regions.to_region_vid(r)
586586
}
587587

588+
/// Returns an iterator over all the outlives constraints.
589+
pub fn outlives_constraints(&self) -> impl Iterator<Item = OutlivesConstraint<'tcx>> + '_ {
590+
self.constraints.outlives().iter().copied()
591+
}
592+
588593
/// Adds annotations for `#[rustc_regions]`; see `UniversalRegions::annotate`.
589594
pub(crate) fn annotate(&self, tcx: TyCtxt<'tcx>, err: &mut Diagnostic) {
590595
self.universal_regions.annotate(tcx, err)
@@ -698,7 +703,7 @@ impl<'tcx> RegionInferenceContext<'tcx> {
698703
#[instrument(skip(self, _body), level = "debug")]
699704
fn propagate_constraints(&mut self, _body: &Body<'tcx>) {
700705
debug!("constraints={:#?}", {
701-
let mut constraints: Vec<_> = self.constraints.outlives().iter().collect();
706+
let mut constraints: Vec<_> = self.outlives_constraints().collect();
702707
constraints.sort_by_key(|c| (c.sup, c.sub));
703708
constraints
704709
.into_iter()

0 commit comments

Comments
 (0)