rapx/verify/vm/
region.rs

1//! Region (lifetime) helpers shared by the VM and the property checker.
2
3use rustc_hir::def_id::DefId;
4use rustc_middle::ty::{EarlyParamRegion, GenericParamDefKind, Region, RegionKind, Ty, TyCtxt};
5
6/// Resolve a lifetime name from a contract (e.g. `"a"`, `"static"`) to a
7/// concrete `Region`. `name` is the raw ident, without the leading `'`.
8pub(crate) fn resolve_region_name<'tcx>(
9    tcx: TyCtxt<'tcx>,
10    def_id: DefId,
11    name: &str,
12) -> Option<Region<'tcx>> {
13    if name == "static" || name == "static_lifetime" {
14        return Some(tcx.lifetimes.re_static);
15    }
16    let ticked = format!("'{name}");
17    let generics = tcx.generics_of(def_id);
18    for param in &generics.own_params {
19        if matches!(param.kind, GenericParamDefKind::Lifetime)
20            && (param.name.as_str() == name || param.name.as_str() == ticked.as_str())
21        {
22            return Some(Region::new_early_param(
23                tcx,
24                EarlyParamRegion {
25                    index: param.index,
26                    name: param.name,
27                },
28            ));
29        }
30    }
31    None
32}
33
34/// Whether `src` outlives `ret` (`src: ret`).
35///
36/// `'static` and reflexivity are handled structurally; declared where-clauses
37/// (`'a: 'b`) are resolved via rustc's `FreeRegionMap` (which also computes the
38/// transitive closure). Anything else is treated as *not* outlives.
39pub(crate) fn region_outlives<'tcx>(
40    tcx: TyCtxt<'tcx>,
41    def_id: DefId,
42    src: Region<'tcx>,
43    ret: Region<'tcx>,
44) -> bool {
45    match (src.kind(), ret.kind()) {
46        (RegionKind::ReStatic, _) => true,
47        (_, RegionKind::ReStatic) => false,
48        _ => {
49            if src == ret {
50                return true;
51            }
52            if !src.is_free() || !ret.is_free() {
53                return false;
54            }
55            free_region_outlives(tcx, def_id, src, ret)
56        }
57    }
58}
59
60/// Consult the function's declared outlives constraints (where-clauses) via
61/// rustc's `FreeRegionMap`, which records `'a: 'b` bounds and their transitive
62/// closure. `sub_free_regions(r_a, r_b)` tests `r_a <= r_b` (i.e. `r_b: r_a`),
63/// so `src: ret` is `sub_free_regions(ret, src)`.
64fn free_region_outlives<'tcx>(
65    tcx: TyCtxt<'tcx>,
66    def_id: DefId,
67    src: Region<'tcx>,
68    ret: Region<'tcx>,
69) -> bool {
70    use rustc_data_structures::fx::FxHashSet;
71    use rustc_infer::infer::outlives::env::OutlivesEnvironment;
72
73    let param_env = tcx.param_env(def_id);
74    let env = OutlivesEnvironment::from_normalized_bounds(
75        param_env,
76        Vec::new(),
77        std::iter::empty(),
78        FxHashSet::default(),
79    );
80    env.free_region_map().sub_free_regions(tcx, ret, src)
81}
82
83/// Whether `src_region` provably outlives the reference region of `self_ty`
84/// via the type's own well-formedness.  A reference parameter `&'r SliceHost<'s>`
85/// requires its pointee's regions to outlive `'r` (`'s: 'r`), which the
86/// where-clause-only [`region_outlives`] cannot see.  Complements it with the
87/// implied outlives components of `self_ty`.
88pub(crate) fn region_outlives_implied<'tcx>(
89    tcx: TyCtxt<'tcx>,
90    src_region: Region<'tcx>,
91    self_ty: Ty<'tcx>,
92) -> bool {
93    use rustc_data_structures::smallvec::SmallVec;
94    use rustc_middle::ty::outlives::{Component, push_outlives_components};
95
96    let mut out: SmallVec<[Component<TyCtxt<'tcx>>; 4]> = SmallVec::new();
97    push_outlives_components(tcx, self_ty, &mut out);
98    out.iter()
99        .any(|c| matches!(c, Component::Region(r) if *r == src_region))
100}
101
102/// The function's signature with late-bound regions liberated to free
103/// `ReLateParam`s, so reference regions are comparable (MIR erases them to
104/// `ReErased`).
105fn liberate_fn_sig<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> rustc_middle::ty::FnSig<'tcx> {
106    let fn_sig = tcx.fn_sig(def_id).instantiate_identity();
107    #[cfg(rapx_ge_99)]
108    let fn_sig = fn_sig.skip_norm_wip();
109    tcx.liberate_late_bound_regions(def_id, fn_sig)
110}
111
112/// The reference region of `def_id`'s return type (`&'r T` → `Some('r)`).
113pub(crate) fn fn_return_region<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option<Region<'tcx>> {
114    use rustc_middle::ty::TyKind;
115    match liberate_fn_sig(tcx, def_id).output().kind() {
116        TyKind::Ref(region, _, _) => Some(*region),
117        _ => None,
118    }
119}
120
121/// The type of `def_id`'s argument at `index`.
122pub(crate) fn fn_arg_ty<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, index: usize) -> Option<Ty<'tcx>> {
123    liberate_fn_sig(tcx, def_id).inputs().get(index).copied()
124}
rapx/verify/vm/region.rs

rapx/verify/vm/
region.rs
