mirror of
https://github.com/rust-lang/rust.git
synced 2025-02-10 14:02:57 +00:00
Rollup merge of #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.
This commit is contained in:
commit
ebeedf05cb
@ -1326,14 +1326,20 @@ impl<'tcx> RegionInferenceContext<'tcx> {
|
||||
})
|
||||
}
|
||||
|
||||
// Evaluate whether `sup_region == sub_region`.
|
||||
fn eval_equal(&self, r1: RegionVid, r2: RegionVid) -> bool {
|
||||
/// Evaluate whether `sup_region == sub_region`.
|
||||
///
|
||||
/// Panics if called before `solve()` executes,
|
||||
// This is `pub` because it's used by unstable external borrowck data users, see `consumers.rs`.
|
||||
pub fn eval_equal(&self, r1: RegionVid, r2: RegionVid) -> bool {
|
||||
self.eval_outlives(r1, r2) && self.eval_outlives(r2, r1)
|
||||
}
|
||||
|
||||
// Evaluate whether `sup_region: sub_region`.
|
||||
/// Evaluate whether `sup_region: sub_region`.
|
||||
///
|
||||
/// Panics if called before `solve()` executes,
|
||||
// This is `pub` because it's used by unstable external borrowck data users, see `consumers.rs`.
|
||||
#[instrument(skip(self), level = "debug", ret)]
|
||||
fn eval_outlives(&self, sup_region: RegionVid, sub_region: RegionVid) -> bool {
|
||||
pub fn eval_outlives(&self, sup_region: RegionVid, sub_region: RegionVid) -> bool {
|
||||
debug!(
|
||||
"sup_region's value = {:?} universal={:?}",
|
||||
self.region_value_str(sup_region),
|
||||
@ -2246,7 +2252,10 @@ impl<'tcx> RegionInferenceContext<'tcx> {
|
||||
}
|
||||
|
||||
/// Access to the SCC constraint graph.
|
||||
pub(crate) fn constraint_sccs(&self) -> &Sccs<RegionVid, ConstraintSccIndex> {
|
||||
/// This can be used to quickly under-approximate the regions which are equal to each other
|
||||
/// and their relative orderings.
|
||||
// This is `pub` because it's used by unstable external borrowck data users, see `consumers.rs`.
|
||||
pub fn constraint_sccs(&self) -> &Sccs<RegionVid, ConstraintSccIndex> {
|
||||
self.constraint_sccs.as_ref()
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user