Make a minimal amount of region APIs public #124893
Merged
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
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 toRegionInferenceContext
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:
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.