Skip to content

Commit 30a0a9b

Browse files
committed
Auto merge of rust-lang#86977 - vakaras:body_with_borrowck_facts, r=nikomatsakis
Enable compiler consumers to obtain mir::Body with Polonius facts. This PR adds a function (``get_body_with_borrowck_facts``) that can be used by compiler consumers to obtain ``mir::Body`` with accompanying borrow checker information. The most important borrow checker information that [our verifier called Prusti](https://github.com/viperproject/prusti-dev) needs is lifetime constraints. I have not found a reasonable way to compute the lifetime constraints on the Prusti side. In the compiler, the constraints are computed during the borrow checking phase and then dropped. This PR adds an additional parameter to the `do_mir_borrowck` function that tells it to return the computed information instead of dropping it. The additionally returned information by `do_mir_borrowck` contains a ``mir::Body`` with non-erased lifetime regions and Polonius facts. I have decided to reuse the Polonius facts because this way I needed fewer changes to the compiler and Polonius facts contains other useful information that we otherwise would need to recompute. Just FYI: up to now, Prusti was obtaining this information by [parsing the compiler logs](https://github.com/viperproject/prusti-dev/blob/b58ced8dfd14ef30582b503d517167ccd771eaff/prusti-interface/src/environment/borrowck/regions.rs#L25-L39). This is not only a hacky approach, but we also reached its limits. r? `@nikomatsakis`
2 parents d83da1d + 9142d6d commit 30a0a9b

File tree

10 files changed

+342
-17
lines changed

10 files changed

+342
-17
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
//! This file provides API for compiler consumers.
2+
3+
use rustc_hir::def_id::LocalDefId;
4+
use rustc_index::vec::IndexVec;
5+
use rustc_infer::infer::TyCtxtInferExt;
6+
use rustc_middle::mir::Body;
7+
use rustc_middle::ty::{self, TyCtxt};
8+
9+
pub use super::{
10+
facts::{AllFacts as PoloniusInput, RustcFacts},
11+
location::{LocationTable, RichLocation},
12+
nll::PoloniusOutput,
13+
BodyWithBorrowckFacts,
14+
};
15+
16+
/// This function computes Polonius facts for the given body. It makes a copy of
17+
/// the body because it needs to regenerate the region identifiers.
18+
///
19+
/// Note:
20+
/// * This function will panic if the required body was already stolen. This
21+
/// can, for example, happen when requesting a body of a `const` function
22+
/// because they are evaluated during typechecking. The panic can be avoided
23+
/// by overriding the `mir_borrowck` query. You can find a complete example
24+
/// that shows how to do this at `src/test/run-make/obtain-borrowck/`.
25+
/// * This function will also panic if computation of Polonius facts
26+
/// (`-Zpolonius` flag) is not enabled.
27+
///
28+
/// * Polonius is highly unstable, so expect regular changes in its signature or other details.
29+
pub fn get_body_with_borrowck_facts<'tcx>(
30+
tcx: TyCtxt<'tcx>,
31+
def: ty::WithOptConstParam<LocalDefId>,
32+
) -> BodyWithBorrowckFacts<'tcx> {
33+
let (input_body, promoted) = tcx.mir_promoted(def);
34+
tcx.infer_ctxt().enter(|infcx| {
35+
let input_body: &Body<'_> = &input_body.borrow();
36+
let promoted: &IndexVec<_, _> = &promoted.borrow();
37+
*super::do_mir_borrowck(&infcx, input_body, promoted, true).1.unwrap()
38+
})
39+
}

compiler/rustc_mir/src/borrow_check/facts.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ use std::io::{BufWriter, Write};
1212
use std::path::Path;
1313

1414
#[derive(Copy, Clone, Debug)]
15-
crate struct RustcFacts;
15+
pub struct RustcFacts;
1616

1717
impl polonius_engine::FactTypes for RustcFacts {
1818
type Origin = RegionVid;
@@ -22,7 +22,7 @@ impl polonius_engine::FactTypes for RustcFacts {
2222
type Path = MovePathIndex;
2323
}
2424

25-
crate type AllFacts = PoloniusFacts<RustcFacts>;
25+
pub type AllFacts = PoloniusFacts<RustcFacts>;
2626

2727
crate trait AllFactsExt {
2828
/// Returns `true` if there is a need to gather `AllFacts` given the

compiler/rustc_mir/src/borrow_check/location.rs

+6-6
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ use rustc_middle::mir::{BasicBlock, Body, Location};
1212
/// granularity through outlives relations; however, the rich location
1313
/// table serves another purpose: it compresses locations from
1414
/// multiple words into a single u32.
15-
crate struct LocationTable {
15+
pub struct LocationTable {
1616
num_points: usize,
1717
statements_before_block: IndexVec<BasicBlock, usize>,
1818
}
@@ -24,7 +24,7 @@ rustc_index::newtype_index! {
2424
}
2525

2626
#[derive(Copy, Clone, Debug)]
27-
crate enum RichLocation {
27+
pub enum RichLocation {
2828
Start(Location),
2929
Mid(Location),
3030
}
@@ -48,23 +48,23 @@ impl LocationTable {
4848
Self { num_points, statements_before_block }
4949
}
5050

51-
crate fn all_points(&self) -> impl Iterator<Item = LocationIndex> {
51+
pub fn all_points(&self) -> impl Iterator<Item = LocationIndex> {
5252
(0..self.num_points).map(LocationIndex::new)
5353
}
5454

55-
crate fn start_index(&self, location: Location) -> LocationIndex {
55+
pub fn start_index(&self, location: Location) -> LocationIndex {
5656
let Location { block, statement_index } = location;
5757
let start_index = self.statements_before_block[block];
5858
LocationIndex::new(start_index + statement_index * 2)
5959
}
6060

61-
crate fn mid_index(&self, location: Location) -> LocationIndex {
61+
pub fn mid_index(&self, location: Location) -> LocationIndex {
6262
let Location { block, statement_index } = location;
6363
let start_index = self.statements_before_block[block];
6464
LocationIndex::new(start_index + statement_index * 2 + 1)
6565
}
6666

67-
crate fn to_location(&self, index: LocationIndex) -> RichLocation {
67+
pub fn to_location(&self, index: LocationIndex) -> RichLocation {
6868
let point_index = index.index();
6969

7070
// Find the basic block. We have a vector with the

compiler/rustc_mir/src/borrow_check/mod.rs

+51-7
Original file line numberDiff line numberDiff line change
@@ -42,12 +42,14 @@ use self::diagnostics::{AccessKind, RegionName};
4242
use self::location::LocationTable;
4343
use self::prefixes::PrefixSet;
4444
use self::MutateMode::{JustWrite, WriteAndRead};
45+
use facts::AllFacts;
4546

4647
use self::path_utils::*;
4748

4849
mod borrow_set;
4950
mod constraint_generation;
5051
mod constraints;
52+
pub mod consumers;
5153
mod def_use;
5254
mod diagnostics;
5355
mod facts;
@@ -108,22 +110,33 @@ fn mir_borrowck<'tcx>(
108110
let opt_closure_req = tcx.infer_ctxt().with_opaque_type_inference(def.did).enter(|infcx| {
109111
let input_body: &Body<'_> = &input_body.borrow();
110112
let promoted: &IndexVec<_, _> = &promoted.borrow();
111-
do_mir_borrowck(&infcx, input_body, promoted)
113+
do_mir_borrowck(&infcx, input_body, promoted, false).0
112114
});
113115
debug!("mir_borrowck done");
114116

115117
tcx.arena.alloc(opt_closure_req)
116118
}
117119

120+
/// Perform the actual borrow checking.
121+
///
122+
/// If `return_body_with_facts` is true, then return the body with non-erased
123+
/// region ids on which the borrow checking was performed together with Polonius
124+
/// facts.
118125
fn do_mir_borrowck<'a, 'tcx>(
119126
infcx: &InferCtxt<'a, 'tcx>,
120127
input_body: &Body<'tcx>,
121128
input_promoted: &IndexVec<Promoted, Body<'tcx>>,
122-
) -> BorrowCheckResult<'tcx> {
129+
return_body_with_facts: bool,
130+
) -> (BorrowCheckResult<'tcx>, Option<Box<BodyWithBorrowckFacts<'tcx>>>) {
123131
let def = input_body.source.with_opt_param().as_local().unwrap();
124132

125133
debug!("do_mir_borrowck(def = {:?})", def);
126134

135+
assert!(
136+
!return_body_with_facts || infcx.tcx.sess.opts.debugging_opts.polonius,
137+
"borrowck facts can be requested only when Polonius is enabled"
138+
);
139+
127140
let tcx = infcx.tcx;
128141
let param_env = tcx.param_env(def.did);
129142
let id = tcx.hir().local_def_id_to_hir_id(def.did);
@@ -169,12 +182,14 @@ fn do_mir_borrowck<'a, 'tcx>(
169182
// requires first making our own copy of the MIR. This copy will
170183
// be modified (in place) to contain non-lexical lifetimes. It
171184
// will have a lifetime tied to the inference context.
172-
let mut body = input_body.clone();
185+
let mut body_owned = input_body.clone();
173186
let mut promoted = input_promoted.clone();
174-
let free_regions = nll::replace_regions_in_mir(infcx, param_env, &mut body, &mut promoted);
175-
let body = &body; // no further changes
187+
let free_regions =
188+
nll::replace_regions_in_mir(infcx, param_env, &mut body_owned, &mut promoted);
189+
let body = &body_owned; // no further changes
176190

177-
let location_table = &LocationTable::new(&body);
191+
let location_table_owned = LocationTable::new(body);
192+
let location_table = &location_table_owned;
178193

179194
let mut errors_buffer = Vec::new();
180195
let (move_data, move_errors): (MoveData<'tcx>, Vec<(Place<'tcx>, MoveError<'tcx>)>) =
@@ -202,6 +217,7 @@ fn do_mir_borrowck<'a, 'tcx>(
202217
let nll::NllOutput {
203218
regioncx,
204219
opaque_type_values,
220+
polonius_input,
205221
polonius_output,
206222
opt_closure_req,
207223
nll_errors,
@@ -446,9 +462,37 @@ fn do_mir_borrowck<'a, 'tcx>(
446462
used_mut_upvars: mbcx.used_mut_upvars,
447463
};
448464

465+
let body_with_facts = if return_body_with_facts {
466+
let output_facts = mbcx.polonius_output.expect("Polonius output was not computed");
467+
Some(box BodyWithBorrowckFacts {
468+
body: body_owned,
469+
input_facts: *polonius_input.expect("Polonius input facts were not generated"),
470+
output_facts,
471+
location_table: location_table_owned,
472+
})
473+
} else {
474+
None
475+
};
476+
449477
debug!("do_mir_borrowck: result = {:#?}", result);
450478

451-
result
479+
(result, body_with_facts)
480+
}
481+
482+
/// A `Body` with information computed by the borrow checker. This struct is
483+
/// intended to be consumed by compiler consumers.
484+
///
485+
/// We need to include the MIR body here because the region identifiers must
486+
/// match the ones in the Polonius facts.
487+
pub struct BodyWithBorrowckFacts<'tcx> {
488+
/// A mir body that contains region identifiers.
489+
pub body: Body<'tcx>,
490+
/// Polonius input facts.
491+
pub input_facts: AllFacts,
492+
/// Polonius output facts.
493+
pub output_facts: Rc<self::nll::PoloniusOutput>,
494+
/// The table that maps Polonius points to locations in the table.
495+
pub location_table: LocationTable,
452496
}
453497

454498
crate struct MirBorrowckCtxt<'cx, 'tcx> {

compiler/rustc_mir/src/borrow_check/nll.rs

+4-2
Original file line numberDiff line numberDiff line change
@@ -40,13 +40,14 @@ use crate::borrow_check::{
4040
Upvar,
4141
};
4242

43-
crate type PoloniusOutput = Output<RustcFacts>;
43+
pub type PoloniusOutput = Output<RustcFacts>;
4444

4545
/// The output of `nll::compute_regions`. This includes the computed `RegionInferenceContext`, any
4646
/// closure requirements to propagate, and any generated errors.
4747
crate struct NllOutput<'tcx> {
4848
pub regioncx: RegionInferenceContext<'tcx>,
4949
pub opaque_type_values: VecMap<OpaqueTypeKey<'tcx>, Ty<'tcx>>,
50+
pub polonius_input: Option<Box<AllFacts>>,
5051
pub polonius_output: Option<Rc<PoloniusOutput>>,
5152
pub opt_closure_req: Option<ClosureRegionRequirements<'tcx>>,
5253
pub nll_errors: RegionErrors<'tcx>,
@@ -271,7 +272,7 @@ pub(in crate::borrow_check) fn compute_regions<'cx, 'tcx>(
271272
let def_id = body.source.def_id();
272273

273274
// Dump facts if requested.
274-
let polonius_output = all_facts.and_then(|all_facts| {
275+
let polonius_output = all_facts.as_ref().and_then(|all_facts| {
275276
if infcx.tcx.sess.opts.debugging_opts.nll_facts {
276277
let def_path = infcx.tcx.def_path(def_id);
277278
let dir_path = PathBuf::from(&infcx.tcx.sess.opts.debugging_opts.nll_facts_dir)
@@ -305,6 +306,7 @@ pub(in crate::borrow_check) fn compute_regions<'cx, 'tcx>(
305306
NllOutput {
306307
regioncx,
307308
opaque_type_values: remapped_opaque_tys,
309+
polonius_input: all_facts.map(Box::new),
308310
polonius_output,
309311
opt_closure_req: closure_region_requirements,
310312
nll_errors,

compiler/rustc_mir/src/lib.rs

+3
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,9 @@ mod shim;
4747
pub mod transform;
4848
pub mod util;
4949

50+
// A public API provided for the Rust compiler consumers.
51+
pub use self::borrow_check::consumers;
52+
5053
use rustc_middle::ty::query::Providers;
5154

5255
pub fn provide(providers: &mut Providers) {
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
include ../tools.mk
2+
3+
# This example shows how to implement a rustc driver that retrieves MIR bodies
4+
# together with the borrow checker information.
5+
6+
# How to run this
7+
# $ ./x.py test src/test/run-make-fulldeps/obtain-borrowck
8+
9+
DRIVER_BINARY := "$(TMPDIR)"/driver
10+
SYSROOT := $(shell $(RUSTC) --print sysroot)
11+
12+
ifdef IS_WINDOWS
13+
LIBSTD := -L "$(SYSROOT)\\lib\\rustlib\\$(TARGET)\\lib"
14+
else
15+
LIBSTD :=
16+
endif
17+
18+
all:
19+
$(RUSTC) driver.rs -o "$(DRIVER_BINARY)"
20+
$(TARGET_RPATH_ENV) "$(DRIVER_BINARY)" --sysroot $(SYSROOT) $(LIBSTD) test.rs -o "$(TMPDIR)/driver_test" > "$(TMPDIR)"/output.stdout
21+
22+
ifdef RUSTC_BLESS_TEST
23+
cp "$(TMPDIR)"/output.stdout output.stdout
24+
else
25+
$(DIFF) output.stdout "$(TMPDIR)"/output.stdout
26+
endif

0 commit comments

Comments
 (0)