Skip to content
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

Expose more information in get_body_with_borrowck_facts #111840

Merged
merged 6 commits into from
May 25, 2023

Conversation

voidc
Copy link
Contributor

@voidc voidc commented May 22, 2023

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

@rustbot rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue. labels May 22, 2023
Copy link
Contributor

@oli-obk oli-obk left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These changes look reasonable to me. I cannot promise we'll keep the API around, but I do not foresee this being a maintenance issue for us, so likely some form of it will keep getting provided.

compiler/rustc_borrowck/src/lib.rs Outdated Show resolved Hide resolved
compiler/rustc_borrowck/src/lib.rs Show resolved Hide resolved
compiler/rustc_borrowck/src/lib.rs Outdated Show resolved Hide resolved
@smoelius
Copy link
Contributor

smoelius commented May 23, 2023

@smoelius Do you think these changes would also be sufficient for your needs?

I think they might. They look very similar to some local changes that I have. Thank you very much for the ping.

@oli-obk
Copy link
Contributor

oli-obk commented May 23, 2023

please rebase, then we can land this

@rust-log-analyzer

This comment has been minimized.

@rust-log-analyzer

This comment has been minimized.

@oli-obk
Copy link
Contributor

oli-obk commented May 23, 2023

@bors r+

@bors
Copy link
Contributor

bors commented May 23, 2023

📌 Commit 6a8112e1f8c02d89fe78667209183f570c502fac has been approved by oli-obk

It is now in the queue for this repository.

@bors 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 May 23, 2023
@rust-log-analyzer

This comment has been minimized.

@JonasAlaif
Copy link
Contributor

@voidc would it be possible to slightly extend this and make the constraints field of RegionInferenceContext here public, along with the corresponding OutlivesConstraintSet struct definition and its fn outlives. This seems like a small change to be able to get all of the OutlivesConstraints out, which already happen to be public.

@smoelius
Copy link
Contributor

smoelius commented May 24, 2023

Sorry if it's not my place to chime in, but will the right commit be pushed? (I can't tell from the queue.)

I think @voidc intends for it to be 8dac074.

But that was pushed after @oli-obk approved.

@oli-obk
Copy link
Contributor

oli-obk commented May 24, 2023

The moment a change is done to a PR it is taken off the queue, so nothing is happening for now until I actually review and r+ it again

@JonasAlaif
Copy link
Contributor

I think that the PR should be ready to merge again now, but let's wait for confirmation from @voidc

@voidc
Copy link
Contributor Author

voidc commented May 24, 2023

Yes, the PR is ready

@rustbot ready

@rustbot rustbot added the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label May 24, 2023
@oli-obk
Copy link
Contributor

oli-obk commented May 24, 2023

@bors r+

@bors
Copy link
Contributor

bors commented May 24, 2023

📌 Commit 8dac074 has been approved by oli-obk

It is now in the queue for this repository.

@bors bors removed the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label May 24, 2023
bors added a commit to rust-lang-ci/rust that referenced this pull request May 25, 2023
…earth

Rollup of 5 pull requests

Successful merges:

 - rust-lang#111741 (Use `ObligationCtxt` in custom type ops)
 - rust-lang#111840 (Expose more information in `get_body_with_borrowck_facts`)
 - rust-lang#111876 (Roll compiler_builtins to 0.1.92)
 - rust-lang#111912 (Use `Option::is_some_and` and `Result::is_ok_and` in the compiler  )
 - rust-lang#111915 (libtest: Improve error when missing `-Zunstable-options`)

r? `@ghost`
`@rustbot` modify labels: rollup
@bors bors merged commit b84ab57 into rust-lang:master May 25, 2023
@rustbot rustbot added this to the 1.71.0 milestone May 25, 2023
@lqd
Copy link
Member

lqd commented May 26, 2023

This seems like a small change to be able to get all of the OutlivesConstraints out, which already happen to be public.

Depending on what you want to achieve, I don't believe OutlivesConstraints would be enough to have a somewhat "complete outlives graph" view of things, since they will not contain member constraints whenever opaque types are involved. (They're not separate in the NLL MIR dump, nor visible in the graphviz region and SCC graphs, and neither present in the polonius input facts IIRC)

pub trait T {}

struct S<'a>(&'a ());

impl<'a> T for S<'a> {}

fn foo() -> impl T {
    let x = ();
    S(&x) //~ ERROR `x` does not live long enough
}
error[E0597]: `x` does not live long enough
  --> test.rs:9:7
   |
8  |     let x = ();
   |         - binding `x` declared here
9  |     S(&x) //~ ERROR `x` does not live long enough
   |     --^^-
   |     | |
   |     | borrowed value does not live long enough
   |     opaque type requires that `x` is borrowed for `'static`
10 | }
   | - `x` dropped here while still borrowed

The constraints field won't have an outlives constraint flowing into 'static here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

8 participants