Enable compiler consumers to obtain mir::Body with Polonius facts. #86977

vakaras · 2021-07-08T14:41:38Z

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 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. This is not only a hacky approach, but we also reached its limits.

r? @nikomatsakis

compiler/rustc_mir/src/borrow_check/consumers.rs

nikomatsakis

r=me but we need a comment somewhere about overriding borrow_check query for now (eventually we should find a better solution)

compiler/rustc_mir/src/borrow_check/consumers.rs

nikomatsakis · 2021-07-21T20:03:22Z

Hmm, actually, I wonder if we can think about how to test this?

nikomatsakis · 2021-07-21T20:03:43Z

I'd be ok to land without tests, but it would be nice to have a "working example" (that tests the corner case, too!) that we can point people at. Maybe add it to a run-make test?

nikomatsakis · 2021-07-21T20:04:11Z

Mildly revising my opinion. I think I would like such a test before landing, but it doesn't have to deeply inspect the facts or anything.

vakaras · 2021-07-22T20:07:37Z

Mildly revising my opinion. I think I would like such a test before landing, but it doesn't have to deeply inspect the facts or anything.

I have added a test that just calls the function and in this way checks that it does not panic.

By the way, I did not find a good example on which I could base my Makefile (is there a test that checks that it is possible to create a custom driver?), so would be good to check it more carefully.

lqd · 2021-07-22T20:18:26Z

compiler/rustc_mir/src/borrow_check/consumers.rs

@@ -0,0 +1,37 @@
+//! This file provides API for compiler consumers.


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

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.)

By the way, Prusti is already using Polonius, but in a very hacky way. So, this PR should only reduce our maintenance efforts.

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.)

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.

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.

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.

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.

src/test/run-make/obtain-borrowck/driver.rs

src/test/run-make-fulldeps/obtain-borrowck/Makefile

compiler/rustc_mir/src/borrow_check/consumers.rs

nikomatsakis · 2021-07-30T12:13:52Z

@bors r+

bors · 2021-07-30T12:13:53Z

📌 Commit e5e6acd has been approved by nikomatsakis

bors · 2021-07-31T01:59:15Z

⌛ Testing commit e5e6acd with merge 3fbd225b9e340a1c2aee3a4a1eb315d027082b51...

bors · 2021-07-31T03:00:15Z

💔 Test failed - checks-actions

vakaras · 2021-08-17T14:25:56Z

The test succeeds now for me with build=x86_64-pc-windows-gnu.

nikomatsakis · 2021-08-17T14:43:18Z

@bors r+

bors · 2021-08-17T14:43:20Z

📌 Commit 9142d6d has been approved by nikomatsakis

bors · 2021-08-17T19:08:35Z

⌛ Testing commit 9142d6d with merge 30a0a9b...

bors · 2021-08-17T21:49:11Z

☀️ Test successful - checks-actions
Approved by: nikomatsakis
Pushing 30a0a9b to master...

willcrichton · 2021-08-18T03:02:43Z

It seems like the exported facts reference a number of data types that are private to rustc. For example, BodyWithBorrowckFacts::input_facts::outlives has type (RegionVid, RegionVid, LocationIndex) and LocationIndex is a private type within rustc_mir::borrow_check::location::LocationIndex. Should this PR be extended to publicly expose any data type contained within BodyWithBorrowckFacts?

vakaras · 2021-08-18T07:34:14Z

It seems like the exported facts reference a number of data types that are private to rustc. For example, BodyWithBorrowckFacts::input_facts::outlives has type (RegionVid, RegionVid, LocationIndex) and LocationIndex is a private type within rustc_mir::borrow_check::location::LocationIndex. Should this PR be extended to publicly expose any data type contained within BodyWithBorrowckFacts?

I had a version of Prusti that passes our tests with this PR. Let me check whether something went wrong.

willcrichton · 2021-08-18T16:13:45Z

@vakaras I also was able to use this PR to extract the first two fields of the outlives-constraints. So it's not broken per se. But I can't explicitly reference the type of the third field of the outlives-constraint tuple. I'm a bit surprised this isn't a "private type in public interface" error -- I'm guessing because there's some levels of indirections through generics and associated types?

See: https://github.com/willcrichton/flowistry/blob/master/src/slicing/mod.rs#L275-L283

vakaras · 2021-08-18T17:41:54Z

@vakaras I also was able to use this PR to extract the first two fields of the outlives-constraints. So it's not broken per se. But I can't explicitly reference the type of the third field of the outlives-constraint tuple. I'm a bit surprised this isn't a "private type in public interface" error -- I'm guessing because there's some levels of indirections through generics and associated types?

See: https://github.com/willcrichton/flowistry/blob/master/src/slicing/mod.rs#L275-L283

@willcrichton You need to do that in a slightly round-about way: willcrichton/flowistry#1.

willcrichton · 2021-08-18T17:50:19Z

Ah I see, thanks @vakaras!

willcrichton · 2021-08-19T01:43:18Z

One other question -- when I call get_body_with_borrowck_facts, the input_facts are populated but the output_facts are empty. Is that expected behavior? Do I need to manually call polonius to populate output_facts? I am passing the -Z polonius flag.

vakaras · 2021-08-19T12:24:25Z

It should be populated, but it is possible that I mixed something up.

willcrichton · 2021-08-19T18:06:31Z

I built from master and the issue seems to have been fixed. I think it's just a gap between nightly and master, so false alarm.

…call, r=ecstatic-morse Allow calling `get_body_with_borrowck_facts` without `-Z polonius` For my [static analysis tool](https://github.com/willcrichton/flowistry), I need to access the set of outlives-constraints. Recently, rust-lang#86977 merged a way to access these facts via Polonius. However, the merged implementation requires `-Z polonius` to be provided to use this feature. This uses Polonius for borrow checking on the entire crate, which as described [here](https://rust-lang.zulipchat.com/#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/Polonius.20performance.20in.20a.20rustc.20plugin/near/251301631), is very slow. This PR allows `get_body_with_borrowck_facts` to be called without `-Z polonius`. This is essential for my tool to run in a sensible length of time. This is a temporary patch as the Polonius-related APIs develop -- I can update my code as future changes happen. Additionally, this PR also makes public two APIs that were previously public but then became private after `rustc_mir` got broken up: `rustc_mir_dataflow::framework::graphviz` and `rustc_mir_transform::MirPass`. I need both of these for my analysis tool. (I can break this change into a separate PR if necessary.)

…facts-flag, r=ecstatic-morse Populate liveness facts when calling `get_body_with_borrowck_facts` without `-Z polonius` For a new feature of [Flowistry](https://github.com/willcrichton/flowistry), a static-analysis tool, we need to obtain a `mir::Body`'s liveness facts using `get_body_with_borrowck_facts` (added in rust-lang#86977). We'd like to do this without passing `-Z polonius` as a compiler arg to avoid borrow checking the entire crate. Support for doing this was added in rust-lang#88983, but the Polonius input facts used for liveness analysis are empty. This happens because the liveness input facts are populated in `liveness::generate` depending only on the value of `AllFacts::enabled` (which is toggled via compiler args). This PR propagates the [`use_polonius`](https://github.com/rust-lang/rust/blob/8b09ba6a5d5c644fe0f1c27c7f9c80b334241707/compiler/rustc_borrowck/src/nll.rs#L168) flag to `liveness::generate` to support populating liveness facts without requiring the `-Z polonius` flag. This fix is somewhat patchy - if it'd be better to add more widely-accessible state (like `AllFacts::enabled`) I'd be open to ideas!

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, rust-lang#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 rust-lang#108328 but smaller in scope. `@smoelius` Do you think these changes would also be sufficient for your needs? r? `@oli-obk` cc `@JonasAlaif`

rust-highfive assigned nikomatsakis Jul 8, 2021

rust-highfive added the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label Jul 8, 2021

bjorn3 reviewed Jul 9, 2021

View reviewed changes

compiler/rustc_mir/src/borrow_check/consumers.rs Show resolved Hide resolved

nikomatsakis requested changes Jul 21, 2021

View reviewed changes

compiler/rustc_mir/src/borrow_check/consumers.rs Show resolved Hide resolved

vakaras added 2 commits July 22, 2021 21:57

Enable compiler consumers to obtain Body with Polonius facts.

ad2b4f4

Add a test for get_body_with_borrowck_facts.

b913a45

vakaras force-pushed the body_with_borrowck_facts branch from 9750b60 to b913a45 Compare July 22, 2021 20:00

lqd reviewed Jul 22, 2021

View reviewed changes

Mark-Simulacrum reviewed Jul 22, 2021

View reviewed changes

src/test/run-make/obtain-borrowck/driver.rs Outdated Show resolved Hide resolved

Move obtain-borrowck to run-make-fulldeps.

d882b51

bjorn3 reviewed Jul 23, 2021

View reviewed changes

src/test/run-make-fulldeps/obtain-borrowck/Makefile Outdated Show resolved Hide resolved

Fix typo in a comment.

f13396e

vakaras requested a review from nikomatsakis July 23, 2021 19:29

nikomatsakis requested changes Jul 30, 2021

View reviewed changes

compiler/rustc_mir/src/borrow_check/consumers.rs Show resolved Hide resolved

Update compiler/rustc_mir/src/borrow_check/consumers.rs

e5e6acd

nikomatsakis approved these changes Jul 30, 2021

View reviewed changes

bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Jul 30, 2021

This comment has been minimized.

Sign in to view

bors added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. and removed S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. labels Jul 31, 2021

bors added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. and removed S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. labels Aug 11, 2021

Fix obtain-borrowck failure on Windows.

9142d6d

bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Aug 17, 2021

bors added the merged-by-bors This PR was explicitly merged by bors. label Aug 17, 2021

bors merged commit 30a0a9b into rust-lang:master Aug 17, 2021

rustbot added this to the 1.56.0 milestone Aug 17, 2021

willcrichton mentioned this pull request Sep 15, 2021

Allow calling get_body_with_borrowck_facts without -Z polonius #88983

Merged

connorff mentioned this pull request Feb 2, 2022

Populate liveness facts when calling get_body_with_borrowck_facts without -Z polonius #93603

Merged

voidc mentioned this pull request May 22, 2023

Expose more information in get_body_with_borrowck_facts #111840

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Enable compiler consumers to obtain mir::Body with Polonius facts. #86977

Enable compiler consumers to obtain mir::Body with Polonius facts. #86977

vakaras commented Jul 8, 2021

nikomatsakis left a comment

nikomatsakis commented Jul 21, 2021

nikomatsakis commented Jul 21, 2021

nikomatsakis commented Jul 21, 2021

vakaras commented Jul 22, 2021

lqd Jul 22, 2021

vakaras Jul 22, 2021

vakaras Jul 22, 2021

lqd Jul 22, 2021 •

edited

Loading

vakaras Jul 22, 2021

lqd Jul 22, 2021

vakaras Jul 23, 2021

nikomatsakis commented Jul 30, 2021

bors commented Jul 30, 2021

bors commented Jul 31, 2021

This comment has been minimized.

bors commented Jul 31, 2021

vakaras commented Aug 17, 2021

nikomatsakis commented Aug 17, 2021

bors commented Aug 17, 2021

bors commented Aug 17, 2021

bors commented Aug 17, 2021

willcrichton commented Aug 18, 2021

vakaras commented Aug 18, 2021 •

edited

Loading

willcrichton commented Aug 18, 2021

vakaras commented Aug 18, 2021

willcrichton commented Aug 18, 2021

willcrichton commented Aug 19, 2021 •

edited

Loading

vakaras commented Aug 19, 2021

willcrichton commented Aug 19, 2021

		@@ -0,0 +1,37 @@
		//! This file provides API for compiler consumers.

Enable compiler consumers to obtain mir::Body with Polonius facts. #86977

Enable compiler consumers to obtain mir::Body with Polonius facts. #86977

Conversation

vakaras commented Jul 8, 2021

nikomatsakis left a comment

Choose a reason for hiding this comment

nikomatsakis commented Jul 21, 2021

nikomatsakis commented Jul 21, 2021

nikomatsakis commented Jul 21, 2021

vakaras commented Jul 22, 2021

lqd Jul 22, 2021

Choose a reason for hiding this comment

vakaras Jul 22, 2021

Choose a reason for hiding this comment

vakaras Jul 22, 2021

Choose a reason for hiding this comment

lqd Jul 22, 2021 • edited Loading

Choose a reason for hiding this comment

vakaras Jul 22, 2021

Choose a reason for hiding this comment

lqd Jul 22, 2021

Choose a reason for hiding this comment

vakaras Jul 23, 2021

Choose a reason for hiding this comment

nikomatsakis commented Jul 30, 2021

bors commented Jul 30, 2021

bors commented Jul 31, 2021

This comment has been minimized.

bors commented Jul 31, 2021

vakaras commented Aug 17, 2021

nikomatsakis commented Aug 17, 2021

bors commented Aug 17, 2021

bors commented Aug 17, 2021

bors commented Aug 17, 2021

willcrichton commented Aug 18, 2021

vakaras commented Aug 18, 2021 • edited Loading

willcrichton commented Aug 18, 2021

vakaras commented Aug 18, 2021

willcrichton commented Aug 18, 2021

willcrichton commented Aug 19, 2021 • edited Loading

vakaras commented Aug 19, 2021

willcrichton commented Aug 19, 2021

lqd Jul 22, 2021 •

edited

Loading

vakaras commented Aug 18, 2021 •

edited

Loading

willcrichton commented Aug 19, 2021 •

edited

Loading