-
Notifications
You must be signed in to change notification settings - Fork 12.7k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Enable compiler consumers to obtain mir::Body with Polonius facts. #86977
Merged
Merged
Changes from all commits
Commits
Show all changes
7 commits
Select commit
Hold shift + click to select a range
ad2b4f4
Enable compiler consumers to obtain Body with Polonius facts.
vakaras b913a45
Add a test for get_body_with_borrowck_facts.
vakaras d882b51
Move obtain-borrowck to run-make-fulldeps.
vakaras f13396e
Fix typo in a comment.
vakaras e5e6acd
Update compiler/rustc_mir/src/borrow_check/consumers.rs
nikomatsakis 25a7c3b
Fix obtain-borrowck failure on MSVC.
vakaras 9142d6d
Fix obtain-borrowck failure on Windows.
vakaras File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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. | ||
nikomatsakis marked this conversation as resolved.
Show resolved
Hide resolved
|
||
/// | ||
/// * 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(); | ||
nikomatsakis marked this conversation as resolved.
Show resolved
Hide resolved
|
||
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.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
how stable do you hope this API to be ? whether it'd be the polonius facts structure (e.g. relation names, or types), their contents, or the polonius output
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For Prusti, we are upgrading the Rust compiler version twice a month. My hope is that we do not spend more than 3-4 person-hours per upgrade. (Currently, it is about 1 hour on average.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
By the way, Prusti is already using Polonius, but in a very hacky way. So, this PR should only reduce our maintenance efforts.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok.
I'll add this as a point of discussion for next week's polonius sprint (I didn't expect we'd have users that rely on all these polonius implementation details) and probably need to maintain some stability to not break prusti.
(Yeah, I remember you told me you were parsing the fact dumps when we talked with oli on how to improve this.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! However, I would not worry too much because I think that the data we need is fundamental (in the sense that you will not be able to implement the borrow checker without it).
By the way, feel free to tag me on the discussion. I will be happy to comment on whether the planned changes affect us.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I mean more for hypotheticals like changing implementation like we talked about in barcelona: "what if we need to change the whole facts to something other than flat relations", or "don't compute all the loans in all the origins at all points", or "what if we move away from datalog one day" that kinda thing 😅
In the close future I wouldn't worry too much about that, for sure.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In the long term, the goal would be to make Prusti use
optimized_mir
or some other version of MIR that is used by all compiler consumers. Then how Polonius works should not matter anymore.