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`
This commit is contained in:
Manish Goregaokar 2023-05-24 15:05:04 -07:00 committed by GitHub
commit b84ab57f90
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
9 changed files with 144 additions and 66 deletions

View file

@ -61,7 +61,7 @@ use crate::session_diagnostics::VarNeedNotMut;
use self::diagnostics::{AccessKind, RegionName};
use self::location::LocationTable;
use self::prefixes::PrefixSet;
use facts::AllFacts;
use consumers::{BodyWithBorrowckFacts, ConsumerOptions};
use self::path_utils::*;
@ -143,7 +143,7 @@ fn mir_borrowck(tcx: TyCtxt<'_>, def: LocalDefId) -> &BorrowCheckResult<'_> {
tcx.infer_ctxt().with_opaque_type_inference(DefiningAnchor::Bind(hir_owner.def_id)).build();
let input_body: &Body<'_> = &input_body.borrow();
let promoted: &IndexSlice<_, _> = &promoted.borrow();
let opt_closure_req = do_mir_borrowck(&infcx, input_body, promoted, false).0;
let opt_closure_req = do_mir_borrowck(&infcx, input_body, promoted, None).0;
debug!("mir_borrowck done");
tcx.arena.alloc(opt_closure_req)
@ -151,15 +151,15 @@ fn mir_borrowck(tcx: TyCtxt<'_>, def: LocalDefId) -> &BorrowCheckResult<'_> {
/// Perform the actual borrow checking.
///
/// If `return_body_with_facts` is true, then return the body with non-erased
/// region ids on which the borrow checking was performed together with Polonius
/// facts.
/// Use `consumer_options: None` for the default behavior of returning
/// [`BorrowCheckResult`] only. Otherwise, return [`BodyWithBorrowckFacts`] according
/// to the given [`ConsumerOptions`].
#[instrument(skip(infcx, input_body, input_promoted), fields(id=?input_body.source.def_id()), level = "debug")]
fn do_mir_borrowck<'tcx>(
infcx: &InferCtxt<'tcx>,
input_body: &Body<'tcx>,
input_promoted: &IndexSlice<Promoted, Body<'tcx>>,
return_body_with_facts: bool,
consumer_options: Option<ConsumerOptions>,
) -> (BorrowCheckResult<'tcx>, Option<Box<BodyWithBorrowckFacts<'tcx>>>) {
let def = input_body.source.def_id().expect_local();
debug!(?def);
@ -240,8 +240,6 @@ fn do_mir_borrowck<'tcx>(
let borrow_set =
Rc::new(BorrowSet::build(tcx, body, locals_are_invalidated_at_exit, &mdpe.move_data));
let use_polonius = return_body_with_facts || infcx.tcx.sess.opts.unstable_opts.polonius;
// Compute non-lexical lifetimes.
let nll::NllOutput {
regioncx,
@ -261,7 +259,7 @@ fn do_mir_borrowck<'tcx>(
&mdpe.move_data,
&borrow_set,
&upvars,
use_polonius,
consumer_options,
);
// Dump MIR results into a file, if that is enabled. This let us
@ -441,13 +439,16 @@ fn do_mir_borrowck<'tcx>(
tainted_by_errors,
};
let body_with_facts = if return_body_with_facts {
let output_facts = mbcx.polonius_output.expect("Polonius output was not computed");
let body_with_facts = if consumer_options.is_some() {
let output_facts = mbcx.polonius_output;
Some(Box::new(BodyWithBorrowckFacts {
body: body_owned,
input_facts: *polonius_input.expect("Polonius input facts were not generated"),
promoted,
borrow_set,
region_inference_context: regioncx,
location_table: polonius_input.as_ref().map(|_| location_table_owned),
input_facts: polonius_input,
output_facts,
location_table: location_table_owned,
}))
} else {
None
@ -458,22 +459,6 @@ fn do_mir_borrowck<'tcx>(
(result, body_with_facts)
}
/// A `Body` with information computed by the borrow checker. This struct is
/// intended to be consumed by compiler consumers.
///
/// We need to include the MIR body here because the region identifiers must
/// match the ones in the Polonius facts.
pub struct BodyWithBorrowckFacts<'tcx> {
/// A mir body that contains region identifiers.
pub body: Body<'tcx>,
/// Polonius input facts.
pub input_facts: AllFacts,
/// Polonius output facts.
pub output_facts: Rc<self::nll::PoloniusOutput>,
/// The table that maps Polonius points to locations in the table.
pub location_table: LocationTable,
}
pub struct BorrowckInferCtxt<'cx, 'tcx> {
pub(crate) infcx: &'cx InferCtxt<'tcx>,
pub(crate) reg_var_to_origin: RefCell<FxIndexMap<ty::RegionVid, RegionCtxt>>,