-
Notifications
You must be signed in to change notification settings - Fork 12.7k
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 #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`
- Loading branch information
Showing
10 changed files
with
342 additions
and
17 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,39 @@ | ||
//! This file provides API for compiler consumers. | ||
|
||
use rustc_hir::def_id::LocalDefId; | ||
use rustc_index::vec::IndexVec; | ||
use rustc_infer::infer::TyCtxtInferExt; | ||
use rustc_middle::mir::Body; | ||
use rustc_middle::ty::{self, TyCtxt}; | ||
|
||
pub use super::{ | ||
facts::{AllFacts as PoloniusInput, RustcFacts}, | ||
location::{LocationTable, RichLocation}, | ||
nll::PoloniusOutput, | ||
BodyWithBorrowckFacts, | ||
}; | ||
|
||
/// This function computes Polonius facts for the given body. It makes a copy of | ||
/// the body because it needs to regenerate the region identifiers. | ||
/// | ||
/// Note: | ||
/// * This function will panic if the required body was already stolen. This | ||
/// can, for example, happen when requesting a body of a `const` function | ||
/// because they are evaluated during typechecking. The panic can be avoided | ||
/// by overriding the `mir_borrowck` query. You can find a complete example | ||
/// that shows how to do this at `src/test/run-make/obtain-borrowck/`. | ||
/// * This function will also panic if computation of Polonius facts | ||
/// (`-Zpolonius` flag) is not enabled. | ||
/// | ||
/// * Polonius is highly unstable, so expect regular changes in its signature or other details. | ||
pub fn get_body_with_borrowck_facts<'tcx>( | ||
tcx: TyCtxt<'tcx>, | ||
def: ty::WithOptConstParam<LocalDefId>, | ||
) -> BodyWithBorrowckFacts<'tcx> { | ||
let (input_body, promoted) = tcx.mir_promoted(def); | ||
tcx.infer_ctxt().enter(|infcx| { | ||
let input_body: &Body<'_> = &input_body.borrow(); | ||
let promoted: &IndexVec<_, _> = &promoted.borrow(); | ||
*super::do_mir_borrowck(&infcx, input_body, promoted, true).1.unwrap() | ||
}) | ||
} |
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
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,26 @@ | ||
include ../tools.mk | ||
|
||
# This example shows how to implement a rustc driver that retrieves MIR bodies | ||
# together with the borrow checker information. | ||
|
||
# How to run this | ||
# $ ./x.py test src/test/run-make-fulldeps/obtain-borrowck | ||
|
||
DRIVER_BINARY := "$(TMPDIR)"/driver | ||
SYSROOT := $(shell $(RUSTC) --print sysroot) | ||
|
||
ifdef IS_WINDOWS | ||
LIBSTD := -L "$(SYSROOT)\\lib\\rustlib\\$(TARGET)\\lib" | ||
else | ||
LIBSTD := | ||
endif | ||
|
||
all: | ||
$(RUSTC) driver.rs -o "$(DRIVER_BINARY)" | ||
$(TARGET_RPATH_ENV) "$(DRIVER_BINARY)" --sysroot $(SYSROOT) $(LIBSTD) test.rs -o "$(TMPDIR)/driver_test" > "$(TMPDIR)"/output.stdout | ||
|
||
ifdef RUSTC_BLESS_TEST | ||
cp "$(TMPDIR)"/output.stdout output.stdout | ||
else | ||
$(DIFF) output.stdout "$(TMPDIR)"/output.stdout | ||
endif |
Oops, something went wrong.