Make a minimal amount of region APIs public #124893
Merged
Conversation
This file contains hidden or 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
rustbot
added
S-waiting-on-review
|
Please leave a brief comment on each of these functions, since if they're public API it would be nice if they're documented. And also leave a regular (internal) comment like |
xldenis
force-pushed
the
public-region-apis
branch
from
202e3ed to
2808040
Compare
xldenis
force-pushed
the
public-region-apis
branch
from
2808040 to
d4c6c77
Compare
|
I've promoted the existing comments to doc comments and added internal comments documenting why the apis are public. |
|
@bors r+ rollup |
bors
added
S-waiting-on-bors
bors
added a commit
to rust-lang-ci/rust
that referenced
this pull request
May 9, 2024
…iaskrgr Rollup of 5 pull requests Successful merges: - rust-lang#124893 (Make a minimal amount of region APIs public) - rust-lang#124919 (Add `ErrorGuaranteed` to `Recovered::Yes` and use it more.) - rust-lang#124923 (interpret/miri: better errors on failing offset_from) - rust-lang#124924 (chore: remove repetitive words) - rust-lang#124926 (Make `#![feature]` suggestion MaybeIncorrect) r? `@ghost` `@rustbot` modify labels: rollup
rust-timer
added a commit
to rust-lang-ci/rust
that referenced
this pull request
May 9, 2024
Rollup merge of rust-lang#124893 - xldenis:public-region-apis, r=lcnr Make a minimal amount of region APIs public Tools like Creusot, Prusti or Gillian-Rust need to access information about the loans and regions that exist in MIR programs. While `rustc` provides information about loans, there is currently no public way to reason about the regions present in a MIR program. In particular, we to know which regions are actually equal to each other and which ones outlive each other. Currently, `rustc` provides access to `RegionInferenceContext` but the public api hides that last portion of the information. This PR proposes to make a few apis public, allowing verifiers to reason about the lifetimes present in Rust programs: - [eval_equal](https://doc.rust-lang.org/beta/nightly-rustc/rustc_borrowck/region_infer/struct.RegionInferenceContext.html#method.eval_equal) - [eval_outlives](https://doc.rust-lang.org/beta/nightly-rustc/rustc_borrowck/region_infer/struct.RegionInferenceContext.html#method.eval_outlives) - (Optional) [constraint_sccs](https://doc.rust-lang.org/beta/nightly-rustc/rustc_borrowck/region_infer/struct.RegionInferenceContext.html#method.constraint_sccs) The first two functions would allow us to compare regions and from this we can construct the set of `RegionVid` which are actually equal to each other, and then recover the inclusions between those regions, while the second allows for more direct, but _low level_ access to that information.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
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.
Tools like Creusot, Prusti or Gillian-Rust need to access information about the loans and regions that exist in MIR programs. While
rustcprovides information about loans, there is currently no public way to reason about the regions present in a MIR program. In particular, we to know which regions are actually equal to each other and which ones outlive each other. Currently,rustcprovides access toRegionInferenceContextbut the public api hides that last portion of the information.This PR proposes to make a few apis public, allowing verifiers to reason about the lifetimes present in Rust programs:
The first two functions would allow us to compare regions and from this we can construct the set of
RegionVidwhich are actually equal to each other, and then recover the inclusions between those regions, while the second allows for more direct, but low level access to that information.