From e1708622a753ef140b15aae77092b777c6915cbb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Fri, 3 Jan 2025 12:12:17 +0100
Subject: [PATCH] refactor init and assignment constraints
---
.../src/{ => body}/checked_op_analysis.rs | 0
rr_frontend/translation/src/body/mod.rs | 5 +-
rr_frontend/translation/src/body/signature.rs | 113 ++---
.../translation/src/body/translator.rs | 431 +-----------------
rr_frontend/translation/src/lib.rs | 3 -
.../src/{ => regions}/arg_folder.rs | 6 +
.../translation/src/regions/assignment.rs | 364 +++++++++++++++
.../src/{ => regions}/inclusion_tracker.rs | 73 ++-
rr_frontend/translation/src/regions/init.rs | 275 +++++++++++
rr_frontend/translation/src/regions/mod.rs | 206 ++-------
rr_frontend/translation/src/types/local.rs | 2 +-
11 files changed, 822 insertions(+), 656 deletions(-)
rename rr_frontend/translation/src/{ => body}/checked_op_analysis.rs (100%)
rename rr_frontend/translation/src/{ => regions}/arg_folder.rs (96%)
create mode 100644 rr_frontend/translation/src/regions/assignment.rs
rename rr_frontend/translation/src/{ => regions}/inclusion_tracker.rs (72%)
create mode 100644 rr_frontend/translation/src/regions/init.rs
diff --git a/rr_frontend/translation/src/checked_op_analysis.rs b/rr_frontend/translation/src/body/checked_op_analysis.rs
similarity index 100%
rename from rr_frontend/translation/src/checked_op_analysis.rs
rename to rr_frontend/translation/src/body/checked_op_analysis.rs
diff --git a/rr_frontend/translation/src/body/mod.rs b/rr_frontend/translation/src/body/mod.rs
index 6fa0f359..91e53cf3 100644
--- a/rr_frontend/translation/src/body/mod.rs
+++ b/rr_frontend/translation/src/body/mod.rs
@@ -4,6 +4,8 @@
// If a copy of the BSD-3-clause license was not distributed with this
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
+mod checked_op_analysis;
+
use std::collections::{btree_map, BTreeMap, HashMap, HashSet};
use log::{info, trace, warn};
@@ -22,14 +24,11 @@ use rr_rustc_interface::middle::{mir, ty};
use rr_rustc_interface::{abi, ast, middle};
use typed_arena::Arena;
-use crate::arg_folder::*;
use crate::base::*;
-use crate::checked_op_analysis::CheckedOpLocalAnalysis;
use crate::environment::borrowck::facts;
use crate::environment::polonius_info::PoloniusInfo;
use crate::environment::procedure::Procedure;
use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::inclusion_tracker::*;
use crate::spec_parsers::parse_utils::ParamLookup;
use crate::spec_parsers::verbose_function_spec_parser::{
ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
diff --git a/rr_frontend/translation/src/body/signature.rs b/rr_frontend/translation/src/body/signature.rs
index f0c7542a..ea7e044f 100644
--- a/rr_frontend/translation/src/body/signature.rs
+++ b/rr_frontend/translation/src/body/signature.rs
@@ -25,13 +25,13 @@ use rr_rustc_interface::{abi, ast, middle};
use typed_arena::Arena;
use crate::base::*;
+use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
use crate::body::translator;
-use crate::checked_op_analysis::CheckedOpLocalAnalysis;
use crate::environment::borrowck::facts;
use crate::environment::polonius_info::PoloniusInfo;
use crate::environment::procedure::Procedure;
use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::inclusion_tracker::*;
+use crate::regions::inclusion_tracker::InclusionTracker;
use crate::spec_parsers::parse_utils::ParamLookup;
use crate::spec_parsers::verbose_function_spec_parser::{
ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
@@ -125,7 +125,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
info!("Function generic args: {:?}", params);
let (inputs, output, region_substitution) =
- regions::replace_fnsig_args_with_polonius_vars(env, params, sig);
+ regions::init::replace_fnsig_args_with_polonius_vars(env, params, sig);
info!("inputs: {:?}, output: {:?}", inputs, output);
let (type_scope, trait_attrs) = Self::setup_local_scope(
@@ -265,7 +265,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
}
let (tupled_inputs, output, mut region_substitution) =
- regions::replace_fnsig_args_with_polonius_vars(env, params, sig);
+ regions::init::replace_fnsig_args_with_polonius_vars(env, params, sig);
// Process the lifetime parameters that come from the captures
for r in capture_regions {
@@ -286,7 +286,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
// We need to do some hacks here to find the right Polonius region:
// `r` is the non-placeholder region that the variable gets, but we are
// looking for the corresponding placeholder region
- let r2 = Self::find_placeholder_region_for(r, info).unwrap();
+ let r2 = regions::init::find_placeholder_region_for(r, info).unwrap();
info!("using lifetime {:?} for closure universal", r2);
let lft = info.mk_atomic_region(r2);
@@ -440,7 +440,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
}
let (inputs, output, region_substitution) =
- regions::replace_fnsig_args_with_polonius_vars(env, params, sig);
+ regions::init::replace_fnsig_args_with_polonius_vars(env, params, sig);
info!("inputs: {:?}, output: {:?}", inputs, output);
let mut inclusion_tracker = InclusionTracker::new(info);
@@ -496,10 +496,17 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
if spec_builder.has_spec() {
// add universal constraints
- let universal_constraints = t.get_relevant_universal_constraints();
- info!("univeral constraints: {:?}", universal_constraints);
- for (lft1, lft2) in universal_constraints {
- spec_builder.add_lifetime_constraint(lft1, lft2);
+ {
+ let scope = t.ty_translator.scope.borrow();
+ let universal_constraints = regions::init::get_relevant_universal_constraints(
+ &scope.lifetime_scope,
+ &mut t.inclusion_tracker,
+ t.info,
+ );
+ info!("univeral constraints: {:?}", universal_constraints);
+ for (lft1, lft2) in universal_constraints {
+ spec_builder.add_lifetime_constraint(lft1, lft2);
+ }
}
t.translated_fn.add_function_spec_from_builder(spec_builder);
@@ -567,28 +574,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
}
}
- /// At the start of the function, there's a universal (placeholder) region for reference argument.
- /// These get subsequently relabeled.
- /// Given the relabeled region, find the original placeholder region.
- fn find_placeholder_region_for(r: ty::RegionVid, info: &PoloniusInfo) -> Option<ty::RegionVid> {
- let root_location = Location {
- block: BasicBlock::from_u32(0),
- statement_index: 0,
- };
- let root_point = info.interner.get_point_index(&facts::Point {
- location: root_location,
- typ: facts::PointType::Start,
- });
-
- for (r1, r2, p) in &info.borrowck_in_facts.subset_base {
- if *p == root_point && *r2 == r {
- info!("find placeholder region for: {:?} ⊑ {:?} = r = {:?}", r1, r2, r);
- return Some(*r1);
- }
- }
- None
- }
-
/// Set up the local generic scope of the function, including type parameters, lifetime
/// parameters, and trait constraints.
fn setup_local_scope(
@@ -693,55 +678,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
Ok((type_scope, trait_scope))
}
- /// Filter the "interesting" constraints between universal lifetimes that need to hold
- /// (this does not include the constraints that need to hold for all universal lifetimes,
- /// e.g. that they outlive the function lifetime and are outlived by 'static).
- fn get_relevant_universal_constraints(&mut self) -> Vec<(radium::UniversalLft, radium::UniversalLft)> {
- let info = &self.info;
- let input_facts = &info.borrowck_in_facts;
- let placeholder_subset = &input_facts.known_placeholder_subset;
-
- let root_location = Location {
- block: BasicBlock::from_u32(0),
- statement_index: 0,
- };
- let root_point = self.info.interner.get_point_index(&facts::Point {
- location: root_location,
- typ: facts::PointType::Start,
- });
-
- let mut universal_constraints = Vec::new();
-
- for (r1, r2) in placeholder_subset {
- if let polonius_info::RegionKind::Universal(uk1) = info.get_region_kind(*r1) {
- if let polonius_info::RegionKind::Universal(uk2) = info.get_region_kind(*r2) {
- // if LHS is static, ignore.
- if uk1 == polonius_info::UniversalRegionKind::Static {
- continue;
- }
- // if RHS is the function lifetime, ignore
- if uk2 == polonius_info::UniversalRegionKind::Function {
- continue;
- }
-
- let scope = self.ty_translator.scope.borrow();
- let to_universal = || {
- let x = scope.lifetime_scope.lookup_region_with_kind(uk1, *r2)?;
- let y = scope.lifetime_scope.lookup_region_with_kind(uk2, *r1)?;
- Some((x, y))
- };
- // else, add this constraint
- // for the purpose of this analysis, it is fine to treat it as a dynamic inclusion
- if let Some((x, y)) = to_universal() {
- self.inclusion_tracker.add_dynamic_inclusion(*r1, *r2, root_point);
- universal_constraints.push((x, y));
- };
- }
- }
- }
- universal_constraints
- }
-
/// Process extra requirements annotated on a function spec.
fn process_function_requirements(
fn_builder: &mut radium::FunctionBuilder<'def>,
@@ -792,10 +728,17 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
let mut spec_builder = radium::LiteralFunctionSpecBuilder::new();
// add universal constraints
- let universal_constraints = self.get_relevant_universal_constraints();
- info!("universal constraints: {:?}", universal_constraints);
- for (lft1, lft2) in universal_constraints {
- spec_builder.add_lifetime_constraint(lft1, lft2);
+ {
+ let scope = self.ty_translator.scope.borrow();
+ let universal_constraints = regions::init::get_relevant_universal_constraints(
+ &scope.lifetime_scope,
+ &mut self.inclusion_tracker,
+ self.info,
+ );
+ info!("universal constraints: {:?}", universal_constraints);
+ for (lft1, lft2) in universal_constraints {
+ spec_builder.add_lifetime_constraint(lft1, lft2);
+ }
}
let ty_translator = &self.ty_translator;
diff --git a/rr_frontend/translation/src/body/translator.rs b/rr_frontend/translation/src/body/translator.rs
index b9ef08b0..0adc5e31 100644
--- a/rr_frontend/translation/src/body/translator.rs
+++ b/rr_frontend/translation/src/body/translator.rs
@@ -22,14 +22,13 @@ use rr_rustc_interface::middle::{mir, ty};
use rr_rustc_interface::{abi, ast, middle};
use typed_arena::Arena;
-use crate::arg_folder::*;
use crate::base::*;
-use crate::checked_op_analysis::CheckedOpLocalAnalysis;
+use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
use crate::environment::borrowck::facts;
use crate::environment::polonius_info::PoloniusInfo;
use crate::environment::procedure::Procedure;
use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::inclusion_tracker::*;
+use crate::regions::inclusion_tracker::InclusionTracker;
use crate::spec_parsers::parse_utils::ParamLookup;
use crate::spec_parsers::verbose_function_spec_parser::{
ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
@@ -267,7 +266,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
let return_name = opt_return_name?;
// add lifetime parameters to the map
- let initial_constraints = Self::get_initial_universal_arg_constraints(
+ let initial_constraints = regions::init::get_initial_universal_arg_constraints(
info,
&mut inclusion_tracker,
inputs,
@@ -301,70 +300,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
})
}
- /// Determine initial constraints between universal regions and local place regions.
- /// Returns an initial mapping for the name _map that initializes place regions of arguments
- /// with universals.
- fn get_initial_universal_arg_constraints(
- info: &'a PoloniusInfo<'a, 'tcx>,
- inclusion_tracker: &mut InclusionTracker<'a, 'tcx>,
- _sig_args: &[Ty<'tcx>],
- _local_args: &[Ty<'tcx>],
- ) -> Vec<(polonius_info::AtomicRegion, polonius_info::AtomicRegion)> {
- // Polonius generates a base subset constraint uregion ⊑ pregion.
- // We turn that into pregion = uregion, as we do strong updates at the top-level.
- let input_facts = &info.borrowck_in_facts;
- let subset_base = &input_facts.subset_base;
-
- let root_location = Location {
- block: BasicBlock::from_u32(0),
- statement_index: 0,
- };
- let root_point = info.interner.get_point_index(&facts::Point {
- location: root_location,
- typ: facts::PointType::Start,
- });
-
- // TODO: for nested references, this doesn't really seem to work.
- // Problem is that we don't have constraints for the mapping of nested references.
- // Potentially, we should instead just equalize the types
-
- let mut initial_arg_mapping = Vec::new();
- for (r1, r2, _) in subset_base {
- let lft1 = info.mk_atomic_region(*r1);
- let lft2 = info.mk_atomic_region(*r2);
-
- let polonius_info::AtomicRegion::Universal(polonius_info::UniversalRegionKind::Local, _) = lft1
- else {
- continue;
- };
-
- // this is a constraint we care about here, add it
- if inclusion_tracker.check_inclusion(*r1, *r2, root_point) {
- continue;
- }
-
- inclusion_tracker.add_static_inclusion(*r1, *r2, root_point);
- inclusion_tracker.add_static_inclusion(*r2, *r1, root_point);
-
- assert!(matches!(lft2, polonius_info::AtomicRegion::PlaceRegion(_)));
-
- initial_arg_mapping.push((lft1, lft2));
- }
- initial_arg_mapping
- }
-
- fn get_initial_universal_arg_constraints2(
- sig_args: &[Ty<'tcx>],
- local_args: &[Ty<'tcx>],
- ) -> Vec<(polonius_info::AtomicRegion, polonius_info::AtomicRegion)> {
- // Polonius generates a base subset constraint uregion ⊑ pregion.
- // We turn that into pregion = uregion, as we do strong updates at the top-level.
- assert!(sig_args.len() == local_args.len());
-
- // TODO: implement a bitypefolder to solve this issue.
- Vec::new()
- }
-
/// Generate a string identifier for a Local.
/// Tries to find the Rust source code name of the local, otherwise simply enumerates.
/// `used_names` keeps track of the Rust source code names that have already been used.
@@ -736,72 +671,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
false
}
- fn get_assignment_strong_update_constraints(
- &mut self,
- loc: Location,
- ) -> HashSet<(Region, Region, PointIndex)> {
- let info = &self.info;
- let input_facts = &info.borrowck_in_facts;
- let subset_base = &input_facts.subset_base;
-
- let mut constraints = HashSet::new();
- // Polonius subset constraint are spawned for the midpoint
- let midpoint = self.info.interner.get_point_index(&facts::Point {
- location: loc,
- typ: facts::PointType::Mid,
- });
-
- // for strong update: emit mutual equalities
- // TODO: alternative implementation: structurally compare regions in LHS type and RHS type
- for (s1, s2, point) in subset_base {
- if *point == midpoint {
- let lft1 = self.info.mk_atomic_region(*s1);
- let lft2 = self.info.mk_atomic_region(*s2);
-
- // We only care about inclusions into a place lifetime.
- // Moreover, we want to filter out the universal inclusions which are always
- // replicated at every point.
- if lft2.is_place() && !lft1.is_universal() {
- // take this constraint and the reverse constraint
- constraints.insert((*s1, *s2, *point));
- //constraints.insert((*s2, *s1, *point));
- }
- }
- }
- constraints
- }
-
- fn get_assignment_weak_update_constraints(
- &mut self,
- loc: Location,
- ) -> HashSet<(Region, Region, PointIndex)> {
- let info = &self.info;
- let input_facts = &info.borrowck_in_facts;
- let subset_base = &input_facts.subset_base;
-
- let mut constraints = HashSet::new();
- // Polonius subset constraint are spawned for the midpoint
- let midpoint = self.info.interner.get_point_index(&facts::Point {
- location: loc,
- typ: facts::PointType::Mid,
- });
-
- // for weak updates: should mirror the constraints generated by Polonius
- for (s1, s2, point) in subset_base {
- if *point == midpoint {
- // take this constraint
- // TODO should there be exceptions to this?
-
- if !self.inclusion_tracker.check_inclusion(*s1, *s2, *point) {
- // only add it if it does not hold already, since we will enforce this
- // constraint dynamically.
- constraints.insert((*s1, *s2, *point));
- }
- }
- }
- constraints
- }
-
/// Split the type of a function operand of a call expression to a base type and an instantiation for
/// generics.
fn call_expr_op_split_inst(
@@ -1188,8 +1057,17 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
info!("call has instantiated type {:?}", inst_sig);
// compute the resulting annotations
- let (rhs_annots, pre_stmt_annots, post_stmt_annots) =
- self.get_assignment_annots(loc, destination, output_ty);
+ let lhs_ty = self.get_type_of_place(destination);
+ let lhs_strongly_writeable = !self.check_place_below_reference(destination);
+ let (rhs_annots, pre_stmt_annots, post_stmt_annots) = regions::assignment::get_assignment_annots(
+ self.env,
+ &mut self.inclusion_tracker,
+ &self.ty_translator,
+ loc,
+ lhs_strongly_writeable,
+ lhs_ty,
+ output_ty,
+ );
info!(
"assignment annots after call: expr: {:?}, pre-stmt: {:?}, post-stmt: {:?}",
rhs_annots, pre_stmt_annots, post_stmt_annots
@@ -1515,72 +1393,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
}
}
- /// Generate an annotation on an expression needed to update the region name map.
- fn generate_strong_update_annot(&self, ty: PlaceTy<'tcx>) -> Option<radium::Annotation> {
- let (interesting, tree) = self.generate_strong_update_annot_rec(ty.ty);
- interesting.then(|| radium::Annotation::GetLftNames(tree))
- }
-
- /// Returns a tree for giving names to Coq lifetimes based on RR types.
- /// The boolean indicates whether the tree is "interesting", i.e. whether it names at least one
- /// lifetime.
- fn generate_strong_update_annot_rec(&self, ty: Ty<'tcx>) -> (bool, radium::LftNameTree) {
- // TODO for now this just handles nested references
- match ty.kind() {
- ty::TyKind::Ref(r, ty, _) => match r.kind() {
- ty::RegionKind::ReVar(r) => {
- let name = self.format_region(r);
- let (_, ty_tree) = self.generate_strong_update_annot_rec(*ty);
- (true, radium::LftNameTree::Ref(name, Box::new(ty_tree)))
- },
- _ => {
- panic!("generate_strong_update_annot: expected region variable");
- },
- },
- _ => (false, radium::LftNameTree::Leaf),
- }
- }
-
- /// Generate an annotation to adapt the type of `expr` to `target_ty` from type `current_ty` by
- /// means of shortening lifetimes.
- fn generate_shortenlft_annot(
- &self,
- target_ty: Ty<'tcx>,
- _current_ty: Ty<'tcx>,
- mut expr: radium::Expr,
- ) -> radium::Expr {
- // this is not so different from the strong update annotation
- let (interesting, tree) = self.generate_strong_update_annot_rec(target_ty);
- if interesting {
- expr = radium::Expr::Annot {
- a: radium::Annotation::ShortenLft(tree),
- e: Box::new(expr),
- why: None,
- };
- }
- expr
- }
-
- /// Find all regions that need to outlive a loan region at its point of creation, and
- /// add the corresponding constraints to the inclusion tracker.
- fn get_outliving_regions_on_loan(&mut self, r: Region, loan_point: PointIndex) -> Vec<Region> {
- // get all base subset constraints r' ⊆ r
- let info = &self.info;
- let input_facts = &info.borrowck_in_facts;
- let mut outliving = Vec::new();
-
- let subset_base = &input_facts.subset_base;
- for (r1, r2, p) in subset_base {
- if *p == loan_point && *r2 == r {
- self.inclusion_tracker.add_static_inclusion(*r1, *r2, *p);
- outliving.push(*r1);
- }
- // other subset constraints at this point are due to (for instance) the assignment of
- // the loan to a place and are handled there.
- }
- outliving
- }
-
/// Check if a local is used for a spec closure.
fn is_spec_closure_local(&self, l: Local) -> Result<Option<DefId>, TranslationError<'tcx>> {
// check if we should ignore this
@@ -1596,208 +1408,6 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
.and_then(|m| m.is_ignore().then_some(*did)))
}
- fn region_to_region_vid(r: ty::Region<'tcx>) -> facts::Region {
- match r.kind() {
- ty::RegionKind::ReVar(vid) => vid,
- _ => panic!(),
- }
- }
-
- /// Generate a dynamic inclusion of r1 in r2 at point p. Prepends annotations for doing so to `cont`.
- fn generate_dyn_inclusion(
- &mut self,
- stmt_annots: &mut Vec<radium::Annotation>,
- r1: Region,
- r2: Region,
- p: PointIndex,
- ) {
- // check if inclusion already holds
- if !self.inclusion_tracker.check_inclusion(r1, r2, p) {
- // check if the reverse inclusion already holds
- if self.inclusion_tracker.check_inclusion(r2, r1, p) {
- // our invariant is that this must be a static inclusion
- assert!(self.inclusion_tracker.check_static_inclusion(r2, r1, p));
- self.inclusion_tracker.add_dynamic_inclusion(r1, r2, p);
-
- // we generate an extendlft instruction
- // for this, we need to figure out a path to make this inclusion true, i.e. we need
- // an explanation of why it is syntactically included.
- // TODO: for now, we just assume that r1 ⊑ₗ [r2] (in terms of Coq lifetime inclusion)
- stmt_annots.push(radium::Annotation::ExtendLft(self.format_region(r1)));
- } else {
- self.inclusion_tracker.add_dynamic_inclusion(r1, r2, p);
- // we generate a dynamic inclusion instruction
- // we flip this around because the annotations are talking about lifetimes, which are oriented
- // the other way around.
- stmt_annots
- .push(radium::Annotation::DynIncludeLft(self.format_region(r2), self.format_region(r1)));
- }
- }
- }
-
- /// Generates dynamic inclusions for the set of inclusions in `incls`.
- /// These inclusions should not hold yet.
- /// Skips mutual inclusions -- we cannot interpret these.
- fn generate_dyn_inclusions(
- &mut self,
- incls: &HashSet<(Region, Region, PointIndex)>,
- ) -> Vec<radium::Annotation> {
- // before executing the assignment, first enforce dynamic inclusions
- info!("Generating dynamic inclusions {:?}", incls);
- let mut stmt_annots = Vec::new();
-
- for (r1, r2, p) in incls {
- if incls.contains(&(*r2, *r1, *p)) {
- warn!("Skipping impossible dynamic inclusion {:?} ⊑ {:?} at {:?}", r1, r2, p);
- continue;
- }
-
- self.generate_dyn_inclusion(&mut stmt_annots, *r1, *r2, *p);
- }
-
- stmt_annots
- }
-
- /// Get the annotations due to borrows appearing on the RHS of an assignment.
- fn get_assignment_loan_annots(&mut self, loc: Location, rhs: &Rvalue<'tcx>) -> Vec<radium::Annotation> {
- let mut stmt_annots = Vec::new();
-
- // if we create a new loan here, start a new lifetime for it
- let loan_point = self.info.get_point(loc, facts::PointType::Mid);
- if let Some(loan) = self.info.get_optional_loan_at_location(loc) {
- // TODO: is this fine for aggregates? I suppose, if I create a loan for an
- // aggregate, I want to use the same atomic region for all of its components
- // anyways.
-
- let lft = self.info.atomic_region_of_loan(loan);
- let r = lft.get_region();
-
- // get the static inclusions we need to generate here and add them to the
- // inclusion tracker
- let outliving = self.get_outliving_regions_on_loan(r, loan_point);
-
- // add statement for issuing the loan
- stmt_annots.insert(
- 0,
- radium::Annotation::StartLft(
- self.ty_translator.format_atomic_region(&lft),
- outliving.iter().map(|r| self.format_region(*r)).collect(),
- ),
- );
-
- let a = self.info.get_region_kind(r);
- info!("Issuing loan at {:?} with kind {:?}: {:?}; outliving: {:?}", loc, a, loan, outliving);
- } else if let Rvalue::Ref(region, BorrowKind::Shared, _) = rhs {
- // for shared reborrows, Polonius does not create a new loan, and so the
- // previous case did not match.
- // However, we still need to track the region created for the reborrow in an
- // annotation.
-
- let region = TX::region_to_region_vid(*region);
-
- // find inclusion ?r1 ⊑ region -- we will actually enforce region = r1
- let new_constrs: Vec<(facts::Region, facts::Region)> =
- self.info.get_new_subset_constraints_at_point(loan_point);
- info!("Shared reborrow at {:?} with new constrs: {:?}", region, new_constrs);
- let mut included_region = None;
- for (r1, r2) in &new_constrs {
- if *r2 == region {
- included_region = Some(r1);
- break;
- }
- }
- if let Some(r) = included_region {
- //info!("Found inclusion {:?}⊑ {:?}", r, region);
- stmt_annots.push(radium::Annotation::CopyLftName(
- self.format_region(*r),
- self.format_region(region),
- ));
-
- // also add this to the inclusion checker
- self.inclusion_tracker.add_static_inclusion(*r, region, loan_point);
- } else {
- // This happens e.g. when borrowing from a raw pointer etc.
- info!("Found unconstrained shared borrow for {:?}", region);
- let inferred_constrained = vec![];
-
- // add statement for issuing the loan
- stmt_annots
- .push(radium::Annotation::StartLft(self.format_region(region), inferred_constrained));
- }
- }
-
- stmt_annots
- }
-
- /// Compute the annotations for an assignment: an annotation for the rhs value, and a list of
- /// annotations to prepend to the statement, and a list of annotations to put after the
- /// statement.
- fn get_assignment_annots(
- &mut self,
- loc: Location,
- lhs: &Place<'tcx>,
- _rhs_ty: Ty<'tcx>,
- ) -> (Option<radium::Annotation>, Vec<radium::Annotation>, Vec<radium::Annotation>) {
- // check if the place is strongly writeable
- let strongly_writeable = !self.check_place_below_reference(lhs);
- let plc_ty = self.get_type_of_place(lhs);
-
- let new_dyn_inclusions;
- let expr_annot;
- let stmt_annot;
- if strongly_writeable {
- // we are going to update the region mapping through annotations,
- // and hence put up a barrier for propagation of region constraints
-
- // structurally go over the type and find region variables.
- // for each of the variables, issue a barrier.
- // also track them together with the PlaceItems needed to reach them.
- // from the latter, we can generate the necessary annotations
- let regions = regions::find_region_variables_of_place_type(self.env, plc_ty);
-
- // put up a barrier at the Mid point
- let barrier_point_index = self.info.interner.get_point_index(&facts::Point {
- location: loc,
- typ: facts::PointType::Mid,
- });
- for r in ®ions {
- self.inclusion_tracker.add_barrier(*r, barrier_point_index);
- }
- // get new constraints that should be enforced
- let new_constraints = self.get_assignment_strong_update_constraints(loc);
- stmt_annot = Vec::new();
- for (r1, r2, p) in &new_constraints {
- self.inclusion_tracker.add_static_inclusion(*r1, *r2, *p);
- self.inclusion_tracker.add_static_inclusion(*r2, *r1, *p);
-
- // TODO: use this instead of the expr_annot below
- //stmt_annot.push(
- //radium::Annotation::CopyLftName(
- //self.format_region(*r1),
- //self.format_region(*r2),
- //));
- }
-
- // TODO: get rid of this
- // similarly generate an annotation that encodes these constraints in the RR
- // type system
- expr_annot = self.generate_strong_update_annot(plc_ty);
- //expr_annot = None;
-
- new_dyn_inclusions = HashSet::new();
- } else {
- // need to filter out the constraints that are relevant here.
- // incrementally go through them.
- new_dyn_inclusions = self.get_assignment_weak_update_constraints(loc);
- expr_annot = None;
- stmt_annot = Vec::new();
- }
-
- // First enforce the new inclusions, then do the other annotations
- let new_dyn_inclusions = self.generate_dyn_inclusions(&new_dyn_inclusions);
- (expr_annot, new_dyn_inclusions, stmt_annot)
- }
-
/// Get the regions appearing in a type.
fn get_regions_of_ty(&self, ty: Ty<'tcx>) -> HashSet<ty::RegionVid> {
let mut regions = HashSet::new();
@@ -1938,9 +1548,16 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
let plc_ty = self.get_type_of_place(plc);
let rhs_ty = val.ty(&self.proc.get_mir().local_decls, self.env.tcx());
- let borrow_annots = self.get_assignment_loan_annots(loc, val);
+ let borrow_annots = regions::assignment::get_assignment_loan_annots(
+ &mut self.inclusion_tracker, &self.ty_translator,
+ loc, val);
+
+ let plc_ty = self.get_type_of_place(plc);
+ let plc_strongly_writeable = !self.check_place_below_reference(plc);
let (expr_annot, pre_stmt_annots, post_stmt_annots) =
- self.get_assignment_annots(loc, plc, rhs_ty);
+ regions::assignment::get_assignment_annots(
+ self.env, &mut self.inclusion_tracker, &self.ty_translator,
+ loc, plc_strongly_writeable, plc_ty, rhs_ty);
// TODO; maybe move this to rvalue
let composite_annots = self.get_composite_rvalue_creation_annots(loc, rhs_ty);
@@ -2201,7 +1818,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
})
} else {
info!("Didn't find loan at {:?}: {:?}; region {:?}", loc, rval, region);
- let region = TX::region_to_region_vid(*region);
+ let region = regions::region_to_region_vid(*region);
let lft = self.format_region(region);
Ok(radium::Expr::Borrow {
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index a418aae1..2ab43fcf 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -8,16 +8,13 @@
#![feature(box_patterns)]
#![feature(let_chains)]
#![feature(rustc_private)]
-mod arg_folder;
mod attrs;
mod base;
mod body;
-mod checked_op_analysis;
mod consts;
mod data;
pub mod environment;
mod force_matches_macro;
-mod inclusion_tracker;
mod procedures;
mod regions;
mod search;
diff --git a/rr_frontend/translation/src/arg_folder.rs b/rr_frontend/translation/src/regions/arg_folder.rs
similarity index 96%
rename from rr_frontend/translation/src/arg_folder.rs
rename to rr_frontend/translation/src/regions/arg_folder.rs
index 214ce62e..cd7bee8b 100644
--- a/rr_frontend/translation/src/arg_folder.rs
+++ b/rr_frontend/translation/src/regions/arg_folder.rs
@@ -1,3 +1,9 @@
+// © 2023, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// If a copy of the BSD-3-clause license was not distributed with this
+// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
+
use rr_rustc_interface::middle::ty::visit::*;
use rr_rustc_interface::middle::ty::{self, GenericArg, GenericArgKind, ParamConst, Ty, TyCtxt, TypeFolder};
use rr_rustc_interface::type_ir::fold::{TypeFoldable, TypeSuperFoldable};
diff --git a/rr_frontend/translation/src/regions/assignment.rs b/rr_frontend/translation/src/regions/assignment.rs
new file mode 100644
index 00000000..8676d47c
--- /dev/null
+++ b/rr_frontend/translation/src/regions/assignment.rs
@@ -0,0 +1,364 @@
+// © 2024, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// If a copy of the BSD-3-clause license was not distributed with this
+// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
+
+//! Provides functionality for generating lifetime annotations for assignments.
+
+use std::collections::{BTreeMap, HashMap, HashSet};
+
+use derive_more::{Constructor, Debug};
+use log::{info, warn};
+use rr_rustc_interface::hir::def_id::DefId;
+use rr_rustc_interface::middle::mir::tcx::PlaceTy;
+use rr_rustc_interface::middle::mir::{BasicBlock, BorrowKind, Location, Rvalue};
+use rr_rustc_interface::middle::ty;
+use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind, TypeFoldable};
+use ty::TypeSuperFoldable;
+
+use crate::base::{self, Region};
+use crate::environment::borrowck::facts;
+use crate::environment::polonius_info::PoloniusInfo;
+use crate::environment::{dump_borrowck_info, polonius_info, Environment};
+use crate::regions::arg_folder::ty_instantiate;
+use crate::regions::inclusion_tracker::{self, InclusionTracker};
+use crate::regions::EarlyLateRegionMap;
+use crate::{regions, types};
+
+/// Generate inclusions for a strong update assignment.
+fn get_assignment_strong_update_constraints(
+ inclusion_tracker: &InclusionTracker<'_, '_>,
+ loc: Location,
+) -> HashSet<(Region, Region, base::PointIndex)> {
+ let info = inclusion_tracker.info();
+ let input_facts = &info.borrowck_in_facts;
+ let subset_base = &input_facts.subset_base;
+
+ let mut constraints = HashSet::new();
+ // Polonius subset constraint are spawned for the midpoint
+ let midpoint = info.interner.get_point_index(&facts::Point {
+ location: loc,
+ typ: facts::PointType::Mid,
+ });
+
+ // for strong update: emit mutual equalities
+ // TODO: alternative implementation: structurally compare regions in LHS type and RHS type
+ for (s1, s2, point) in subset_base {
+ if *point == midpoint {
+ let lft1 = info.mk_atomic_region(*s1);
+ let lft2 = info.mk_atomic_region(*s2);
+
+ // We only care about inclusions into a place lifetime.
+ // Moreover, we want to filter out the universal inclusions which are always
+ // replicated at every point.
+ if lft2.is_place() && !lft1.is_universal() {
+ // take this constraint and the reverse constraint
+ constraints.insert((*s1, *s2, *point));
+ //constraints.insert((*s2, *s1, *point));
+ }
+ }
+ }
+ constraints
+}
+
+/// Generate inclusions for a weak update assignment.
+fn get_assignment_weak_update_constraints(
+ inclusion_tracker: &mut InclusionTracker<'_, '_>,
+ loc: Location,
+) -> HashSet<(Region, Region, base::PointIndex)> {
+ let info = inclusion_tracker.info();
+ let input_facts = &info.borrowck_in_facts;
+ let subset_base = &input_facts.subset_base;
+
+ let mut constraints = HashSet::new();
+ // Polonius subset constraint are spawned for the midpoint
+ let midpoint = info.interner.get_point_index(&facts::Point {
+ location: loc,
+ typ: facts::PointType::Mid,
+ });
+
+ // for weak updates: should mirror the constraints generated by Polonius
+ for (s1, s2, point) in subset_base {
+ if *point == midpoint {
+ // take this constraint
+ // TODO should there be exceptions to this?
+
+ if !inclusion_tracker.check_inclusion(*s1, *s2, *point) {
+ // only add it if it does not hold already, since we will enforce this
+ // constraint dynamically.
+ constraints.insert((*s1, *s2, *point));
+ }
+ }
+ }
+ constraints
+}
+
+/// Get all region variables mentioned in a place type.
+fn find_region_variables_of_place_type<'tcx>(env: &Environment<'tcx>, ty: PlaceTy<'tcx>) -> HashSet<Region> {
+ let mut collector = regions::TyRegionCollectFolder::new(env.tcx());
+ if ty.variant_index.is_some() {
+ panic!("find_region_variables_of_place_type: don't support enums");
+ }
+
+ ty.ty.fold_with(&mut collector);
+ collector.get_regions()
+}
+
+/// Compute the annotations for an assignment: an annotation for the rhs value, and a list of
+/// annotations to prepend to the statement, and a list of annotations to put after the
+/// statement.
+pub fn get_assignment_annots<'tcx>(
+ env: &Environment<'tcx>,
+ inclusion_tracker: &mut InclusionTracker<'_, 'tcx>,
+ ty_translator: &types::LocalTX<'_, 'tcx>,
+ loc: Location,
+ lhs_strongly_writeable: bool,
+ lhs_ty: PlaceTy<'tcx>,
+ _rhs_ty: Ty<'tcx>,
+) -> (Option<radium::Annotation>, Vec<radium::Annotation>, Vec<radium::Annotation>) {
+ let info = inclusion_tracker.info();
+ let new_dyn_inclusions;
+ let expr_annot;
+ let stmt_annot;
+ if lhs_strongly_writeable {
+ // we are going to update the region mapping through annotations,
+ // and hence put up a barrier for propagation of region constraints
+
+ // structurally go over the type and find region variables.
+ // for each of the variables, issue a barrier.
+ // also track them together with the PlaceItems needed to reach them.
+ // from the latter, we can generate the necessary annotations
+ let regions = find_region_variables_of_place_type(env, lhs_ty);
+
+ // put up a barrier at the Mid point
+ let barrier_point_index = info.interner.get_point_index(&facts::Point {
+ location: loc,
+ typ: facts::PointType::Mid,
+ });
+ for r in ®ions {
+ inclusion_tracker.add_barrier(*r, barrier_point_index);
+ }
+ // get new constraints that should be enforced
+ let new_constraints = get_assignment_strong_update_constraints(inclusion_tracker, loc);
+ stmt_annot = Vec::new();
+ for (r1, r2, p) in &new_constraints {
+ inclusion_tracker.add_static_inclusion(*r1, *r2, *p);
+ inclusion_tracker.add_static_inclusion(*r2, *r1, *p);
+
+ // TODO: use this instead of the expr_annot below
+ //stmt_annot.push(
+ //radium::Annotation::CopyLftName(
+ //self.format_region(*r1),
+ //self.format_region(*r2),
+ //));
+ }
+
+ // TODO: get rid of this
+ // similarly generate an annotation that encodes these constraints in the RR
+ // type system
+ expr_annot = generate_strong_update_annot(ty_translator, info, lhs_ty);
+ //expr_annot = None;
+
+ new_dyn_inclusions = HashSet::new();
+ } else {
+ // need to filter out the constraints that are relevant here.
+ // incrementally go through them.
+ new_dyn_inclusions = get_assignment_weak_update_constraints(inclusion_tracker, loc);
+ expr_annot = None;
+ stmt_annot = Vec::new();
+ }
+
+ // First enforce the new inclusions, then do the other annotations
+ let new_dyn_inclusions =
+ generate_dyn_inclusion_annots(inclusion_tracker, ty_translator, &new_dyn_inclusions);
+ (expr_annot, new_dyn_inclusions, stmt_annot)
+}
+
+/// Generates dynamic inclusions for the set of inclusions in `incls`.
+/// These inclusions should not hold yet.
+/// Skips mutual inclusions -- we cannot interpret these.
+fn generate_dyn_inclusion_annots<'tcx>(
+ inclusion_tracker: &mut InclusionTracker<'_, 'tcx>,
+ ty_translator: &types::LocalTX<'_, 'tcx>,
+ incls: &HashSet<(Region, Region, base::PointIndex)>,
+) -> Vec<radium::Annotation> {
+ // before executing the assignment, first enforce dynamic inclusions
+ info!("Generating dynamic inclusions {:?}", incls);
+
+ let inclusions = inclusion_tracker.generate_dyn_inclusions(incls);
+
+ inclusions
+ .into_iter()
+ .map(|incl| match incl {
+ inclusion_tracker::DynamicInclusion::ExtendLft(l) => {
+ radium::Annotation::ExtendLft(ty_translator.format_atomic_region(&l))
+ },
+ inclusion_tracker::DynamicInclusion::IncludeLft(l1, l2) => radium::Annotation::DynIncludeLft(
+ ty_translator.format_atomic_region(&l1),
+ ty_translator.format_atomic_region(&l2),
+ ),
+ })
+ .collect()
+}
+
+/// Generate an annotation on an expression needed to update the region name map.
+fn generate_strong_update_annot<'tcx>(
+ ty_translator: &types::LocalTX<'_, 'tcx>,
+ info: &PoloniusInfo<'_, 'tcx>,
+ ty: PlaceTy<'tcx>,
+) -> Option<radium::Annotation> {
+ let (interesting, tree) = generate_strong_update_annot_rec(ty_translator, info, ty.ty);
+ interesting.then(|| radium::Annotation::GetLftNames(tree))
+}
+
+/// Returns a tree for giving names to Coq lifetimes based on RR types.
+/// The boolean indicates whether the tree is "interesting", i.e. whether it names at least one
+/// lifetime.
+fn generate_strong_update_annot_rec<'tcx>(
+ ty_translator: &types::LocalTX<'_, 'tcx>,
+ info: &PoloniusInfo<'_, 'tcx>,
+ ty: Ty<'tcx>,
+) -> (bool, radium::LftNameTree) {
+ // TODO for now this just handles nested references
+ match ty.kind() {
+ ty::TyKind::Ref(r, ty, _) => match r.kind() {
+ ty::RegionKind::ReVar(r) => {
+ let name = ty_translator.format_atomic_region(&info.mk_atomic_region(r));
+ let (_, ty_tree) = generate_strong_update_annot_rec(ty_translator, info, *ty);
+ (true, radium::LftNameTree::Ref(name, Box::new(ty_tree)))
+ },
+ _ => {
+ panic!("generate_strong_update_annot: expected region variable");
+ },
+ },
+ _ => (false, radium::LftNameTree::Leaf),
+ }
+}
+
+/// Generate an annotation to adapt the type of `expr` to `target_ty` from type `current_ty` by
+/// means of shortening lifetimes.
+fn generate_shortenlft_annot<'tcx>(
+ ty_translator: &types::LocalTX<'_, 'tcx>,
+ info: &PoloniusInfo<'_, 'tcx>,
+ target_ty: Ty<'tcx>,
+ _current_ty: Ty<'tcx>,
+ mut expr: radium::Expr,
+) -> radium::Expr {
+ // this is not so different from the strong update annotation
+ let (interesting, tree) = generate_strong_update_annot_rec(ty_translator, info, target_ty);
+ if interesting {
+ expr = radium::Expr::Annot {
+ a: radium::Annotation::ShortenLft(tree),
+ e: Box::new(expr),
+ why: None,
+ };
+ }
+ expr
+}
+
+/// Find all regions that need to outlive a loan region at its point of creation, and
+/// add the corresponding constraints to the inclusion tracker.
+fn get_outliving_regions_on_loan(
+ inclusion_tracker: &mut InclusionTracker<'_, '_>,
+ r: Region,
+ loan_point: base::PointIndex,
+) -> Vec<Region> {
+ // get all base subset constraints r' ⊆ r
+ let info = inclusion_tracker.info();
+ let input_facts = &info.borrowck_in_facts;
+ let mut outliving = Vec::new();
+
+ let subset_base = &input_facts.subset_base;
+ for (r1, r2, p) in subset_base {
+ if *p == loan_point && *r2 == r {
+ inclusion_tracker.add_static_inclusion(*r1, *r2, *p);
+ outliving.push(*r1);
+ }
+ // other subset constraints at this point are due to (for instance) the assignment of
+ // the loan to a place and are handled there.
+ }
+ outliving
+}
+
+/// Get the annotations due to borrows appearing on the RHS of an assignment.
+pub fn get_assignment_loan_annots<'tcx>(
+ inclusion_tracker: &mut InclusionTracker<'_, 'tcx>,
+ ty_translator: &types::LocalTX<'_, 'tcx>,
+ loc: Location,
+ rhs: &Rvalue<'tcx>,
+) -> Vec<radium::Annotation> {
+ let info = inclusion_tracker.info();
+ let mut stmt_annots = Vec::new();
+
+ // if we create a new loan here, start a new lifetime for it
+ let loan_point = info.get_point(loc, facts::PointType::Mid);
+ if let Some(loan) = info.get_optional_loan_at_location(loc) {
+ // TODO: is this fine for aggregates? I suppose, if I create a loan for an
+ // aggregate, I want to use the same atomic region for all of its components
+ // anyways.
+
+ let lft = info.atomic_region_of_loan(loan);
+ let r = lft.get_region();
+
+ // get the static inclusions we need to generate here and add them to the
+ // inclusion tracker
+ let outliving = get_outliving_regions_on_loan(inclusion_tracker, r, loan_point);
+
+ // add statement for issuing the loan
+ stmt_annots.insert(
+ 0,
+ radium::Annotation::StartLft(
+ ty_translator.format_atomic_region(&lft),
+ outliving
+ .iter()
+ .map(|r| ty_translator.format_atomic_region(&info.mk_atomic_region(*r)))
+ .collect(),
+ ),
+ );
+
+ let a = info.get_region_kind(r);
+ info!("Issuing loan at {:?} with kind {:?}: {:?}; outliving: {:?}", loc, a, loan, outliving);
+ } else if let Rvalue::Ref(region, BorrowKind::Shared, _) = rhs {
+ // for shared reborrows, Polonius does not create a new loan, and so the
+ // previous case did not match.
+ // However, we still need to track the region created for the reborrow in an
+ // annotation.
+
+ let region = regions::region_to_region_vid(*region);
+
+ // find inclusion ?r1 ⊑ region -- we will actually enforce region = r1
+ let new_constrs: Vec<(facts::Region, facts::Region)> =
+ info.get_new_subset_constraints_at_point(loan_point);
+ info!("Shared reborrow at {:?} with new constrs: {:?}", region, new_constrs);
+ let mut included_region = None;
+ for (r1, r2) in &new_constrs {
+ if *r2 == region {
+ included_region = Some(r1);
+ break;
+ }
+ }
+ if let Some(r) = included_region {
+ //info!("Found inclusion {:?}⊑ {:?}", r, region);
+ stmt_annots.push(radium::Annotation::CopyLftName(
+ ty_translator.format_atomic_region(&info.mk_atomic_region(*r)),
+ ty_translator.format_atomic_region(&info.mk_atomic_region(region)),
+ ));
+
+ // also add this to the inclusion checker
+ inclusion_tracker.add_static_inclusion(*r, region, loan_point);
+ } else {
+ // This happens e.g. when borrowing from a raw pointer etc.
+ info!("Found unconstrained shared borrow for {:?}", region);
+ let inferred_constrained = vec![];
+
+ // add statement for issuing the loan
+ stmt_annots.push(radium::Annotation::StartLft(
+ ty_translator.format_atomic_region(&info.mk_atomic_region(region)),
+ inferred_constrained,
+ ));
+ }
+ }
+
+ stmt_annots
+}
diff --git a/rr_frontend/translation/src/inclusion_tracker.rs b/rr_frontend/translation/src/regions/inclusion_tracker.rs
similarity index 72%
rename from rr_frontend/translation/src/inclusion_tracker.rs
rename to rr_frontend/translation/src/regions/inclusion_tracker.rs
index 964280cf..46c87c12 100644
--- a/rr_frontend/translation/src/inclusion_tracker.rs
+++ b/rr_frontend/translation/src/regions/inclusion_tracker.rs
@@ -4,8 +4,17 @@
// If a copy of the BSD-3-clause license was not distributed with this
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
+use std::collections::HashSet;
+
+use log::{info, warn};
+
use crate::base::*;
-use crate::environment::polonius_info::PoloniusInfo;
+use crate::environment::polonius_info::{self, PoloniusInfo};
+
+pub enum DynamicInclusion {
+ ExtendLft(polonius_info::AtomicRegion),
+ IncludeLft(polonius_info::AtomicRegion, polonius_info::AtomicRegion),
+}
/// The `InclusionTracker` maintains a set of dynamic lifetime inclusions holding in the `RefinedRust`
/// type system at given program points.
@@ -48,6 +57,10 @@ impl<'a, 'tcx: 'a> InclusionTracker<'a, 'tcx> {
}
}
+ pub const fn info(&self) -> &'a PoloniusInfo<'a, 'tcx> {
+ self.info
+ }
+
/// Add a basic static inclusion fact.
pub fn add_static_inclusion(&mut self, a: Region, b: Region, p: PointIndex) {
self.static_incl_base.push((a, b, p));
@@ -167,4 +180,62 @@ impl<'a, 'tcx: 'a> InclusionTracker<'a, 'tcx> {
}
self.static_incl.as_ref().unwrap().contains(&(r1, r2, p)) || r1 == r2
}
+
+ /// Generate a dynamic inclusion of r1 in r2 at point p. Prepends annotations for doing so to
+ /// `stmt_annots`.
+ fn generate_dyn_inclusion(
+ &mut self,
+ stmt_annots: &mut Vec<DynamicInclusion>,
+ r1: Region,
+ r2: Region,
+ p: PointIndex,
+ ) {
+ // check if inclusion already holds
+ if !self.check_inclusion(r1, r2, p) {
+ // check if the reverse inclusion already holds
+ if self.check_inclusion(r2, r1, p) {
+ // our invariant is that this must be a static inclusion
+ assert!(self.check_static_inclusion(r2, r1, p));
+ self.add_dynamic_inclusion(r1, r2, p);
+
+ // we generate an extendlft instruction
+ // for this, we need to figure out a path to make this inclusion true, i.e. we need
+ // an explanation of why it is syntactically included.
+ // TODO: for now, we just assume that r1 ⊑ₗ [r2] (in terms of Coq lifetime inclusion)
+ stmt_annots.push(DynamicInclusion::ExtendLft(self.info.mk_atomic_region(r1)));
+ } else {
+ self.add_dynamic_inclusion(r1, r2, p);
+ // we generate a dynamic inclusion instruction
+ // we flip this around because the annotations are talking about lifetimes, which are oriented
+ // the other way around.
+ stmt_annots.push(DynamicInclusion::IncludeLft(
+ self.info.mk_atomic_region(r2),
+ self.info.mk_atomic_region(r1),
+ ));
+ }
+ }
+ }
+
+ /// Generates dynamic inclusions for the set of inclusions in `incls`.
+ /// These inclusions should not hold yet.
+ /// Skips mutual inclusions -- we cannot interpret these.
+ pub fn generate_dyn_inclusions(
+ &mut self,
+ incls: &HashSet<(Region, Region, PointIndex)>,
+ ) -> Vec<DynamicInclusion> {
+ // before executing the assignment, first enforce dynamic inclusions
+ info!("Generating dynamic inclusions {:?}", incls);
+ let mut stmt_annots = Vec::new();
+
+ for (r1, r2, p) in incls {
+ if incls.contains(&(*r2, *r1, *p)) {
+ warn!("Skipping impossible dynamic inclusion {:?} ⊑ {:?} at {:?}", r1, r2, p);
+ continue;
+ }
+
+ self.generate_dyn_inclusion(&mut stmt_annots, *r1, *r2, *p);
+ }
+
+ stmt_annots
+ }
}
diff --git a/rr_frontend/translation/src/regions/init.rs b/rr_frontend/translation/src/regions/init.rs
new file mode 100644
index 00000000..d329ff2b
--- /dev/null
+++ b/rr_frontend/translation/src/regions/init.rs
@@ -0,0 +1,275 @@
+// © 2024, The RefinedRust Developers and Contributors
+//
+// This Source Code Form is subject to the terms of the BSD-3-clause License.
+// If a copy of the BSD-3-clause license was not distributed with this
+// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
+
+//! Provides functionality for generating initial lifetime constraints.
+
+use std::collections::{BTreeMap, HashMap, HashSet};
+
+use derive_more::{Constructor, Debug};
+use log::{info, warn};
+use rr_rustc_interface::hir::def_id::DefId;
+use rr_rustc_interface::middle::mir::tcx::PlaceTy;
+use rr_rustc_interface::middle::mir::{BasicBlock, Location};
+use rr_rustc_interface::middle::ty;
+use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind, TypeFoldable};
+use ty::TypeSuperFoldable;
+
+use crate::base::{self, Region};
+use crate::environment::borrowck::facts;
+use crate::environment::polonius_info::PoloniusInfo;
+use crate::environment::{dump_borrowck_info, polonius_info, Environment};
+use crate::regions::arg_folder::ty_instantiate;
+use crate::regions::inclusion_tracker::InclusionTracker;
+use crate::regions::EarlyLateRegionMap;
+
+/// Process the signature of a function by instantiating the region variables with their
+/// Polonius variables.
+/// Returns the argument and return type signature instantiated in this way.
+/// Moreover, returns a `EarlyLateRegionMap` that contains the mapping of indices to Polonius
+/// region variables.
+pub fn replace_fnsig_args_with_polonius_vars<'tcx>(
+ env: &Environment<'tcx>,
+ params: &[ty::GenericArg<'tcx>],
+ sig: ty::Binder<'tcx, ty::FnSig<'tcx>>,
+) -> (Vec<ty::Ty<'tcx>>, ty::Ty<'tcx>, EarlyLateRegionMap) {
+ // a mapping of Polonius region IDs to names
+ let mut universal_lifetimes = BTreeMap::new();
+ let mut lifetime_names = HashMap::new();
+
+ let mut region_substitution_early: Vec<Option<ty::RegionVid>> = Vec::new();
+
+ // we create a substitution that replaces early bound regions with their Polonius
+ // region variables
+ let mut subst_early_bounds: Vec<ty::GenericArg<'tcx>> = Vec::new();
+ let mut num_early_bounds = 0;
+ for a in params {
+ if let ty::GenericArgKind::Lifetime(r) = a.unpack() {
+ // skip over 0 = static
+ let next_id = ty::RegionVid::from_u32(num_early_bounds + 1);
+ let revar = ty::Region::new_var(env.tcx(), next_id);
+ num_early_bounds += 1;
+ subst_early_bounds.push(ty::GenericArg::from(revar));
+
+ region_substitution_early.push(Some(next_id));
+
+ match *r {
+ ty::RegionKind::ReEarlyBound(r) => {
+ let name = base::strip_coq_ident(r.name.as_str());
+ universal_lifetimes.insert(next_id, format!("ulft_{}", name));
+ lifetime_names.insert(name, next_id);
+ },
+ _ => {
+ universal_lifetimes.insert(next_id, format!("ulft_{}", num_early_bounds));
+ },
+ }
+ } else {
+ subst_early_bounds.push(*a);
+ region_substitution_early.push(None);
+ }
+ }
+ let subst_early_bounds = env.tcx().mk_args(&subst_early_bounds);
+
+ info!("Computed early region map {region_substitution_early:?}");
+
+ // add names for late bound region variables
+ let mut num_late_bounds = 0;
+ let mut region_substitution_late = Vec::new();
+ for b in sig.bound_vars() {
+ let next_id = ty::RegionVid::from_u32(num_early_bounds + num_late_bounds + 1);
+
+ let ty::BoundVariableKind::Region(r) = b else {
+ continue;
+ };
+
+ region_substitution_late.push(next_id);
+
+ match r {
+ ty::BoundRegionKind::BrNamed(_, sym) => {
+ let mut region_name = base::strip_coq_ident(sym.as_str());
+ if region_name == "_" {
+ region_name = next_id.as_usize().to_string();
+ universal_lifetimes.insert(next_id, format!("ulft_{}", region_name));
+ } else {
+ universal_lifetimes.insert(next_id, format!("ulft_{}", region_name));
+ lifetime_names.insert(region_name, next_id);
+ }
+ },
+ ty::BoundRegionKind::BrAnon(_) => {
+ universal_lifetimes.insert(next_id, format!("ulft_{}", next_id.as_usize()));
+ },
+ _ => (),
+ }
+
+ num_late_bounds += 1;
+ }
+
+ // replace late-bound region variables by re-enumerating them in the same way as the MIR
+ // type checker does (that this happens in the same way is important to make the names
+ // line up!)
+ let mut next_index = num_early_bounds + 1; // skip over one additional due to static
+ let mut folder = |_| {
+ let cur_index = next_index;
+ next_index += 1;
+ ty::Region::new_var(env.tcx(), ty::RegionVid::from_u32(cur_index))
+ };
+ let (late_sig, _late_region_map) = env.tcx().replace_late_bound_regions(sig, &mut folder);
+
+ // replace early bound variables
+ let inputs: Vec<_> = late_sig
+ .inputs()
+ .iter()
+ .map(|ty| ty_instantiate(*ty, env.tcx(), subst_early_bounds))
+ .collect();
+
+ let output = ty_instantiate(late_sig.output(), env.tcx(), subst_early_bounds);
+
+ info!("Computed late region map {region_substitution_late:?}");
+
+ let region_map = EarlyLateRegionMap::new(
+ region_substitution_early,
+ region_substitution_late,
+ universal_lifetimes,
+ lifetime_names,
+ );
+ (inputs, output, region_map)
+}
+
+/// At the start of the function, there's a universal (placeholder) region for reference argument.
+/// These get subsequently relabeled.
+/// Given the relabeled region, find the original placeholder region.
+pub fn find_placeholder_region_for(r: ty::RegionVid, info: &PoloniusInfo) -> Option<ty::RegionVid> {
+ let root_location = Location {
+ block: BasicBlock::from_u32(0),
+ statement_index: 0,
+ };
+ let root_point = info.interner.get_point_index(&facts::Point {
+ location: root_location,
+ typ: facts::PointType::Start,
+ });
+
+ for (r1, r2, p) in &info.borrowck_in_facts.subset_base {
+ if *p == root_point && *r2 == r {
+ info!("find placeholder region for: {:?} ⊑ {:?} = r = {:?}", r1, r2, r);
+ return Some(*r1);
+ }
+ }
+ None
+}
+
+/// Filter the "interesting" constraints between universal lifetimes that need to hold
+/// (this does not include the constraints that need to hold for all universal lifetimes,
+/// e.g. that they outlive the function lifetime and are outlived by 'static).
+pub fn get_relevant_universal_constraints<'a>(
+ lifetime_scope: &EarlyLateRegionMap,
+ inclusion_tracker: &mut InclusionTracker,
+ info: &'a PoloniusInfo<'a, '_>,
+) -> Vec<(radium::UniversalLft, radium::UniversalLft)> {
+ let input_facts = &info.borrowck_in_facts;
+ let placeholder_subset = &input_facts.known_placeholder_subset;
+
+ let root_location = Location {
+ block: BasicBlock::from_u32(0),
+ statement_index: 0,
+ };
+ let root_point = info.interner.get_point_index(&facts::Point {
+ location: root_location,
+ typ: facts::PointType::Start,
+ });
+
+ let mut universal_constraints = Vec::new();
+
+ for (r1, r2) in placeholder_subset {
+ if let polonius_info::RegionKind::Universal(uk1) = info.get_region_kind(*r1) {
+ if let polonius_info::RegionKind::Universal(uk2) = info.get_region_kind(*r2) {
+ // if LHS is static, ignore.
+ if uk1 == polonius_info::UniversalRegionKind::Static {
+ continue;
+ }
+ // if RHS is the function lifetime, ignore
+ if uk2 == polonius_info::UniversalRegionKind::Function {
+ continue;
+ }
+
+ let to_universal = || {
+ let x = lifetime_scope.lookup_region_with_kind(uk1, *r2)?;
+ let y = lifetime_scope.lookup_region_with_kind(uk2, *r1)?;
+ Some((x, y))
+ };
+ // else, add this constraint
+ // for the purpose of this analysis, it is fine to treat it as a dynamic inclusion
+ if let Some((x, y)) = to_universal() {
+ inclusion_tracker.add_dynamic_inclusion(*r1, *r2, root_point);
+ universal_constraints.push((x, y));
+ };
+ }
+ }
+ }
+ universal_constraints
+}
+
+/// Determine initial constraints between universal regions and local place regions.
+/// Returns an initial mapping for the name _map that initializes place regions of arguments
+/// with universals.
+pub fn get_initial_universal_arg_constraints<'a, 'tcx>(
+ info: &'a PoloniusInfo<'a, 'tcx>,
+ inclusion_tracker: &mut InclusionTracker<'a, 'tcx>,
+ _sig_args: &[Ty<'tcx>],
+ _local_args: &[Ty<'tcx>],
+) -> Vec<(polonius_info::AtomicRegion, polonius_info::AtomicRegion)> {
+ // Polonius generates a base subset constraint uregion ⊑ pregion.
+ // We turn that into pregion = uregion, as we do strong updates at the top-level.
+ let input_facts = &info.borrowck_in_facts;
+ let subset_base = &input_facts.subset_base;
+
+ let root_location = Location {
+ block: BasicBlock::from_u32(0),
+ statement_index: 0,
+ };
+ let root_point = info.interner.get_point_index(&facts::Point {
+ location: root_location,
+ typ: facts::PointType::Start,
+ });
+
+ // TODO: for nested references, this doesn't really seem to work.
+ // Problem is that we don't have constraints for the mapping of nested references.
+ // Potentially, we should instead just equalize the types
+
+ let mut initial_arg_mapping = Vec::new();
+ for (r1, r2, _) in subset_base {
+ let lft1 = info.mk_atomic_region(*r1);
+ let lft2 = info.mk_atomic_region(*r2);
+
+ let polonius_info::AtomicRegion::Universal(polonius_info::UniversalRegionKind::Local, _) = lft1
+ else {
+ continue;
+ };
+
+ // this is a constraint we care about here, add it
+ if inclusion_tracker.check_inclusion(*r1, *r2, root_point) {
+ continue;
+ }
+
+ inclusion_tracker.add_static_inclusion(*r1, *r2, root_point);
+ inclusion_tracker.add_static_inclusion(*r2, *r1, root_point);
+
+ assert!(matches!(lft2, polonius_info::AtomicRegion::PlaceRegion(_)));
+
+ initial_arg_mapping.push((lft1, lft2));
+ }
+ initial_arg_mapping
+}
+
+pub fn get_initial_universal_arg_constraints2<'tcx>(
+ sig_args: &[Ty<'tcx>],
+ local_args: &[Ty<'tcx>],
+) -> Vec<(polonius_info::AtomicRegion, polonius_info::AtomicRegion)> {
+ // Polonius generates a base subset constraint uregion ⊑ pregion.
+ // We turn that into pregion = uregion, as we do strong updates at the top-level.
+ assert!(sig_args.len() == local_args.len());
+
+ // TODO: implement a bitypefolder to solve this issue.
+ Vec::new()
+}
diff --git a/rr_frontend/translation/src/regions/mod.rs b/rr_frontend/translation/src/regions/mod.rs
index e177b1f9..2d0c4dec 100644
--- a/rr_frontend/translation/src/regions/mod.rs
+++ b/rr_frontend/translation/src/regions/mod.rs
@@ -6,74 +6,30 @@
//! Utilities for translating region information.
+mod arg_folder;
+pub mod assignment;
+pub mod inclusion_tracker;
+pub mod init;
+
use std::collections::{BTreeMap, HashMap, HashSet};
+use arg_folder::ty_instantiate;
use derive_more::{Constructor, Debug};
use log::{info, warn};
use rr_rustc_interface::hir::def_id::DefId;
use rr_rustc_interface::middle::mir::tcx::PlaceTy;
+use rr_rustc_interface::middle::mir::{BasicBlock, Location};
use rr_rustc_interface::middle::ty;
use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind, TypeFoldable};
use ty::TypeSuperFoldable;
-use crate::arg_folder::ty_instantiate;
use crate::base::{self, Region};
-use crate::environment::polonius_info::{self, PoloniusInfo};
-use crate::environment::Environment;
-
-/// A `TypeFolder` that finds all regions occurring in a type.
-pub struct TyRegionCollectFolder<'tcx> {
- tcx: TyCtxt<'tcx>,
- regions: HashSet<Region>,
-}
-impl<'tcx> TyRegionCollectFolder<'tcx> {
- pub fn new(tcx: TyCtxt<'tcx>) -> Self {
- TyRegionCollectFolder {
- tcx,
- regions: HashSet::new(),
- }
- }
-
- pub fn get_regions(self) -> HashSet<Region> {
- self.regions
- }
-}
-impl<'tcx> ty::TypeFolder<TyCtxt<'tcx>> for TyRegionCollectFolder<'tcx> {
- fn interner(&self) -> TyCtxt<'tcx> {
- self.tcx
- }
-
- // TODO: handle the case that we pass below binders
- fn fold_binder<T>(&mut self, t: ty::Binder<'tcx, T>) -> ty::Binder<'tcx, T>
- where
- T: ty::TypeFoldable<TyCtxt<'tcx>>,
- {
- t.super_fold_with(self)
- }
-
- fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
- if let ty::RegionKind::ReVar(r) = r.kind() {
- self.regions.insert(r);
- }
-
- r
- }
-}
+use crate::environment::borrowck::facts;
+use crate::environment::polonius_info::PoloniusInfo;
+use crate::environment::{dump_borrowck_info, polonius_info, Environment};
+use crate::regions::inclusion_tracker::InclusionTracker;
/// Collect all the regions appearing in a type.
-pub fn find_region_variables_of_place_type<'tcx>(
- env: &Environment<'tcx>,
- ty: PlaceTy<'tcx>,
-) -> HashSet<Region> {
- let mut collector = TyRegionCollectFolder::new(env.tcx());
- if ty.variant_index.is_some() {
- panic!("find_region_variables_of_place_type: don't support enums");
- }
-
- ty.ty.fold_with(&mut collector);
- collector.get_regions()
-}
-
/// Data structure that maps early and late region indices inside functions to Polonius regions.
#[derive(Constructor, Clone, Debug, Default)]
pub struct EarlyLateRegionMap {
@@ -122,6 +78,10 @@ impl EarlyLateRegionMap {
let vid = self.late_regions.get(idx)?;
self.lookup_region(*vid)
}
+
+ pub fn translate_atomic_region(&self, r: &polonius_info::AtomicRegion) -> radium::Lft {
+ format_atomic_region_direct(r, Some(self))
+ }
}
/// Format the Coq representation of an atomic region.
@@ -148,114 +108,48 @@ pub fn format_atomic_region_direct(
}
}
-/// Process the signature of a function by instantiating the region variables with their
-/// Polonius variables.
-/// Returns the argument and return type signature instantiated in this way.
-/// Moreover, returns a `EarlyLateRegionMap` that contains the mapping of indices to Polonius
-/// region variables.
-pub fn replace_fnsig_args_with_polonius_vars<'tcx>(
- env: &Environment<'tcx>,
- params: &[ty::GenericArg<'tcx>],
- sig: ty::Binder<'tcx, ty::FnSig<'tcx>>,
-) -> (Vec<ty::Ty<'tcx>>, ty::Ty<'tcx>, EarlyLateRegionMap) {
- // a mapping of Polonius region IDs to names
- let mut universal_lifetimes = BTreeMap::new();
- let mut lifetime_names = HashMap::new();
-
- let mut region_substitution_early: Vec<Option<ty::RegionVid>> = Vec::new();
-
- // we create a substitution that replaces early bound regions with their Polonius
- // region variables
- let mut subst_early_bounds: Vec<ty::GenericArg<'tcx>> = Vec::new();
- let mut num_early_bounds = 0;
- for a in params {
- if let ty::GenericArgKind::Lifetime(r) = a.unpack() {
- // skip over 0 = static
- let next_id = ty::RegionVid::from_u32(num_early_bounds + 1);
- let revar = ty::Region::new_var(env.tcx(), next_id);
- num_early_bounds += 1;
- subst_early_bounds.push(ty::GenericArg::from(revar));
-
- region_substitution_early.push(Some(next_id));
+pub fn region_to_region_vid(r: ty::Region<'_>) -> facts::Region {
+ match r.kind() {
+ ty::RegionKind::ReVar(vid) => vid,
+ _ => panic!(),
+ }
+}
- match *r {
- ty::RegionKind::ReEarlyBound(r) => {
- let name = base::strip_coq_ident(r.name.as_str());
- universal_lifetimes.insert(next_id, format!("ulft_{}", name));
- lifetime_names.insert(name, next_id);
- },
- _ => {
- universal_lifetimes.insert(next_id, format!("ulft_{}", num_early_bounds));
- },
- }
- } else {
- subst_early_bounds.push(*a);
- region_substitution_early.push(None);
+/// A `TypeFolder` that finds all regions occurring in a type.
+pub struct TyRegionCollectFolder<'tcx> {
+ tcx: TyCtxt<'tcx>,
+ regions: HashSet<Region>,
+}
+impl<'tcx> TyRegionCollectFolder<'tcx> {
+ pub fn new(tcx: TyCtxt<'tcx>) -> Self {
+ TyRegionCollectFolder {
+ tcx,
+ regions: HashSet::new(),
}
}
- let subst_early_bounds = env.tcx().mk_args(&subst_early_bounds);
-
- info!("Computed early region map {region_substitution_early:?}");
- // add names for late bound region variables
- let mut num_late_bounds = 0;
- let mut region_substitution_late = Vec::new();
- for b in sig.bound_vars() {
- let next_id = ty::RegionVid::from_u32(num_early_bounds + num_late_bounds + 1);
-
- let ty::BoundVariableKind::Region(r) = b else {
- continue;
- };
+ pub fn get_regions(self) -> HashSet<Region> {
+ self.regions
+ }
+}
+impl<'tcx> ty::TypeFolder<TyCtxt<'tcx>> for TyRegionCollectFolder<'tcx> {
+ fn interner(&self) -> TyCtxt<'tcx> {
+ self.tcx
+ }
- region_substitution_late.push(next_id);
+ // TODO: handle the case that we pass below binders
+ fn fold_binder<T>(&mut self, t: ty::Binder<'tcx, T>) -> ty::Binder<'tcx, T>
+ where
+ T: ty::TypeFoldable<TyCtxt<'tcx>>,
+ {
+ t.super_fold_with(self)
+ }
- match r {
- ty::BoundRegionKind::BrNamed(_, sym) => {
- let mut region_name = base::strip_coq_ident(sym.as_str());
- if region_name == "_" {
- region_name = next_id.as_usize().to_string();
- universal_lifetimes.insert(next_id, format!("ulft_{}", region_name));
- } else {
- universal_lifetimes.insert(next_id, format!("ulft_{}", region_name));
- lifetime_names.insert(region_name, next_id);
- }
- },
- ty::BoundRegionKind::BrAnon(_) => {
- universal_lifetimes.insert(next_id, format!("ulft_{}", next_id.as_usize()));
- },
- _ => (),
+ fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
+ if let ty::RegionKind::ReVar(r) = r.kind() {
+ self.regions.insert(r);
}
- num_late_bounds += 1;
+ r
}
-
- // replace late-bound region variables by re-enumerating them in the same way as the MIR
- // type checker does (that this happens in the same way is important to make the names
- // line up!)
- let mut next_index = num_early_bounds + 1; // skip over one additional due to static
- let mut folder = |_| {
- let cur_index = next_index;
- next_index += 1;
- ty::Region::new_var(env.tcx(), ty::RegionVid::from_u32(cur_index))
- };
- let (late_sig, _late_region_map) = env.tcx().replace_late_bound_regions(sig, &mut folder);
-
- // replace early bound variables
- let inputs: Vec<_> = late_sig
- .inputs()
- .iter()
- .map(|ty| ty_instantiate(*ty, env.tcx(), subst_early_bounds))
- .collect();
-
- let output = ty_instantiate(late_sig.output(), env.tcx(), subst_early_bounds);
-
- info!("Computed late region map {region_substitution_late:?}");
-
- let region_map = EarlyLateRegionMap::new(
- region_substitution_early,
- region_substitution_late,
- universal_lifetimes,
- lifetime_names,
- );
- (inputs, output, region_map)
}
diff --git a/rr_frontend/translation/src/types/local.rs b/rr_frontend/translation/src/types/local.rs
index e468d7be..d7b40749 100644
--- a/rr_frontend/translation/src/types/local.rs
+++ b/rr_frontend/translation/src/types/local.rs
@@ -171,7 +171,7 @@ impl<'def, 'tcx> LocalTX<'def, 'tcx> {
/// Format the Coq representation of an atomic region.
pub fn format_atomic_region(&self, r: &polonius_info::AtomicRegion) -> String {
let scope = self.scope.borrow();
- regions::format_atomic_region_direct(r, Some(&scope.lifetime_scope))
+ scope.lifetime_scope.translate_atomic_region(r)
}
/// Normalize a type in the given function environment.
--
GitLab