From 3b5057043aff5eac7b0522c3b3281807ffded58a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 26 Nov 2024 11:45:16 +0100 Subject: [PATCH] Clarify binding levels in `BodyTransCtx` --- .../translate/translate_constants.rs | 14 +- .../charon-driver/translate/translate_ctx.rs | 328 ++++++++++-------- .../translate/translate_functions_to_ullbc.rs | 11 +- .../translate/translate_predicates.rs | 15 +- .../translate/translate_traits.rs | 30 +- .../translate/translate_types.rs | 147 ++++---- 6 files changed, 273 insertions(+), 272 deletions(-) diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs index 53180c88..d32ea4e6 100644 --- a/charon/src/bin/charon-driver/translate/translate_constants.rs +++ b/charon/src/bin/charon-driver/translate/translate_constants.rs @@ -149,21 +149,19 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { let arg = self.translate_constant_expr_to_constant_expr(span, arg)?; RawConstantExpr::MutPtr(Box::new(arg)) } - ConstantExprKind::ConstRef { id } => { - let var_id = self.const_generic_vars_map.get(&id.index); - if let Some(var_id) = var_id { - RawConstantExpr::Var(ConstGenericDbVar::free(*var_id)) - } else { + ConstantExprKind::ConstRef { id } => match self.lookup_const_generic_var(id) { + Some(var) => RawConstantExpr::Var(var), + None => { error_or_panic!( self, span, &format!( - "Unexpected error: could not find the const var generic of index {}", - id.index + "Unexpected error: could not find the const generic variable {}", + id.name ) ) } - } + }, ConstantExprKind::FnPtr { def_id: fn_id, generics: substs, diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index f6c2363f..b8ddc109 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -19,7 +19,6 @@ use std::collections::HashMap; use std::collections::{BTreeMap, VecDeque}; use std::fmt; use std::fmt::Debug; -use std::mem; use std::path::{Component, PathBuf}; use std::sync::Arc; @@ -194,6 +193,100 @@ pub struct TranslateCtx<'tcx> { pub cached_item_metas: HashMap, } +/// A level of binding for type-level variables. Each item has a top-level binding level +/// corresponding to the parameters and clauses to the items. We may then encounter inner binding +/// levels in the following cases: +/// - `for<..>` binders in predicates; +/// - `fn<..>` function pointer types; +/// - `dyn Trait` types, represented as `dyn` (TODO); +/// - types in a trait declaration or implementation block (TODO); +/// - methods in a trait declaration or implementation block (TODO). +/// +/// At each level, we store two things: a `GenericParams` that contains the parameters bound at +/// this level, and various maps from the rustc-internal indices to our indices. +#[derive(Default)] +pub(crate) struct BindingLevel { + /// The parameters and predicates bound at this level. + pub params: GenericParams, + /// Rust makes the distinction between early and late-bound region parameters. We do not make + /// this distinction, and merge early and late bound regions. For details, see: + /// https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/ + /// https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/ + /// + /// The map from rust early regions to translated region indices. + pub early_region_vars: std::collections::BTreeMap, + /// The map from rust late/bound regions to translated region indices. + pub bound_region_vars: Vec, + /// The map from rust type variable indices to translated type variable indices. + pub type_vars_map: HashMap, + /// The map from rust const generic variables to translate const generic variable indices. + pub const_generic_vars_map: HashMap, + /// Cache the translation of types. This harnesses the deduplication of `TyKind` that hax does. + pub type_trans_cache: HashMap>, Ty>, +} + +impl BindingLevel { + /// Important: we must push all the early-bound regions before pushing any other region. + pub(crate) fn push_early_region(&mut self, region: hax::EarlyParamRegion) -> RegionId { + let name = super::translate_types::translate_region_name(®ion); + // Check that there are no late-bound regions + assert!( + self.bound_region_vars.is_empty(), + "Early regions must be tralsnated before late ones" + ); + let rid = self + .params + .regions + .push_with(|index| RegionVar { index, name }); + self.early_region_vars.insert(region, rid); + rid + } + + /// Important: we must push all the early-bound regions before pushing any other region. + pub(crate) fn push_bound_region(&mut self, region: hax::BoundRegionKind) -> RegionId { + let name = translate_bound_region_kind_name(®ion); + let rid = self + .params + .regions + .push_with(|index| RegionVar { index, name }); + self.bound_region_vars.push(rid); + rid + } + + pub(crate) fn push_type_var(&mut self, rid: u32, name: String) -> TypeVarId { + let var_id = self.params.types.push_with(|index| TypeVar { index, name }); + self.type_vars_map.insert(rid, var_id); + var_id + } + + pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: LiteralTy, name: String) { + let var_id = self + .params + .const_generics + .push_with(|index| ConstGenericVar { index, name, ty }); + self.const_generic_vars_map.insert(rid, var_id); + } + + /// Translate a binder of regions by appending the stored reguions to the given vector. + pub(crate) fn push_params_from_binder(&mut self, binder: hax::Binder<()>) -> Result<(), Error> { + use hax::BoundVariableKind::*; + for p in binder.bound_vars { + match p { + Region(region) => { + self.push_bound_region(region); + } + Ty(_) => { + panic!("Unexpected locally bound type variable"); + } + Const => { + panic!("Unexpected locally bound const generic variable"); + } + } + } + Ok(()) + } +} + /// A translation context for type/global/function bodies. /// Simply augments the [TranslateCtx] with local variables. /// @@ -216,51 +309,15 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx> { /// aliases, because rust does not enforce correct trait bounds on type aliases. pub error_on_impl_expr_error: bool, - /// The regions. - /// We use DeBruijn indices, so we have a stack of regions. - /// See the comments for [Region::BVar]. - pub region_vars: VecDeque>, - /// The map from rust (free) regions to translated region indices. - /// This contains the early bound regions. - /// - /// Important: - /// ========== - /// Rust makes the distinction between the early bound regions, which - /// are free, and the late-bound regions, which are bound (and use - /// DeBruijn indices). - /// We do not make this distinction, and use bound regions everywhere. - /// This means that we consider the free regions as belonging to the first - /// group of bound regions. - /// - /// The [bound_region_vars] field below takes care of the regions which - /// are bound in the Rustc representation. - pub free_region_vars: std::collections::BTreeMap, - /// The stack of late-bound parameters (can only be lifetimes for now), which - /// use DeBruijn indices (the other parameters use free variables). - /// For explanations about what early-bound and late-bound parameters are, see: - /// https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/ - /// https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/ - /// - /// **Important**: - /// ============== - /// We use DeBruijn indices. See the comments for [Region::Var]. - pub bound_region_vars: VecDeque>, - /// The generic parameters for the item. `regions` must be empty, as regions are handled - /// separately. - pub generic_params: GenericParams, - /// The map from rust type variable indices to translated type variable indices. - pub type_vars_map: HashMap, - /// The map from rust const generic variables to translate const generic - /// variable indices. - pub const_generic_vars_map: HashMap, + /// The stack of generic parameter binders for the current context. Each binder introduces an + /// entry in this stack, with the entry as index `0` being the innermost binder. These + /// parameters are referenced using [`DeBruijnVar`]; see there for details. + pub binding_levels: VecDeque, /// (For traits only) accumulated implied trait clauses. pub parent_trait_clauses: Vector, /// (For traits only) accumulated trait clauses on associated types. pub item_trait_clauses: HashMap>, - /// Cache the translation of types. This harnesses the deduplication of `TyKind` that hax does. - pub type_trans_cache: HashMap>, Ty>, - /// The (regular) variables in the current function body. pub locals: Locals, /// The map from rust variable indices to translated variables indices. @@ -365,10 +422,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { // substs and bounds. In order to properly do so, we introduce // a body translation context. let mut bt_ctx = BodyTransCtx::new(def_id, None, self); - let params = bt_ctx.translate_def_generics(span, &full_def)?; + bt_ctx.translate_def_generics(span, &full_def)?; let ty = bt_ctx.translate_ty(span, &ty)?; ImplElem::Ty(Binder { - params, + params: bt_ctx.into_generics(), skip_binder: ty, }) } @@ -909,15 +966,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { t_ctx, hax_state, error_on_impl_expr_error: true, - region_vars: [Vector::new()].into(), - free_region_vars: Default::default(), - bound_region_vars: Default::default(), - generic_params: Default::default(), - type_vars_map: Default::default(), - const_generic_vars_map: Default::default(), + binding_levels: Default::default(), parent_trait_clauses: Default::default(), item_trait_clauses: Default::default(), - type_trans_cache: Default::default(), locals: Default::default(), vars_map: Default::default(), blocks: Default::default(), @@ -993,69 +1044,74 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { self.t_ctx.register_trait_impl_id(&src, id) } - /// Push a free region. - /// - /// Important: we must push *all* the free regions (which are early-bound - /// regions) before pushing any (late-)bound region. - pub(crate) fn push_free_region(&mut self, r: hax::EarlyParamRegion) -> RegionId { - let name = super::translate_types::translate_region_name(&r); - // Check that there are no late-bound regions - assert!(self.bound_region_vars.is_empty()); - let rid = self.region_vars[0].push_with(|index| RegionVar { index, name }); - self.free_region_vars.insert(r, rid); - rid + pub(crate) fn outermost_binder(&self) -> &BindingLevel { + self.binding_levels.back().unwrap() } - /// Translate a binder of regions by appending the stored reguions to the given vector. - pub(crate) fn register_region_binder( - &mut self, - span: Span, - binder: hax::Binder<()>, - region_vars: &mut Vector, - ) -> Result, Error> { - use hax::BoundVariableKind::*; - binder - .bound_vars - .into_iter() - .map(|p| match p { - Region(region) => { - let name = translate_bound_region_kind_name(®ion); - let id = region_vars.push_with(|index| RegionVar { index, name }); - Ok(id) - } - Ty(_) => { - error_or_panic!(self, span, "Unexpected locally bound type variable"); - } - Const => { - error_or_panic!( - self, - span, - "Unexpected locally bound const generic variable" - ); - } - }) - .try_collect() + pub(crate) fn outermost_binder_mut(&mut self) -> &mut BindingLevel { + self.binding_levels.back_mut().unwrap() } - /// Set the first bound regions group - pub(crate) fn set_first_bound_regions_group( - &mut self, - span: Span, - binder: hax::Binder<()>, - ) -> Result<(), Error> { - assert!(self.bound_region_vars.is_empty()); - assert_eq!(self.region_vars.len(), 1); + pub(crate) fn innermost_binder(&mut self) -> &mut BindingLevel { + self.binding_levels.front_mut().unwrap() + } - // Register the variables - // There may already be lifetimes in the current group. - let mut region_vars = mem::take(&mut self.region_vars[0]); - let var_ids = self.register_region_binder(span, binder, &mut region_vars)?; - self.region_vars[0] = region_vars; - self.bound_region_vars.push_front(var_ids); - // Translation of types depends on bound variables, we must not mix that up. - self.type_trans_cache = Default::default(); + pub(crate) fn lookup_bound_region( + &self, + dbid: hax::DebruijnIndex, + var: hax::BoundVar, + ) -> Option { + let rid = self.binding_levels.get(dbid)?.bound_region_vars.get(var)?; + Some(if dbid == self.binding_levels.len() - 1 { + DeBruijnVar::free(*rid) + } else { + DeBruijnVar::bound(DeBruijnId::new(dbid), *rid) + }) + } - Ok(()) + pub(crate) fn lookup_early_region( + &self, + region: &hax::EarlyParamRegion, + ) -> Option { + // TODO: handle non-top-level full binders. + let id = self.outermost_binder().early_region_vars.get(region)?; + Some(DeBruijnVar::free(*id)) + } + + pub(crate) fn lookup_type_var(&self, param: &hax::ParamTy) -> Option { + // TODO: handle non-top-level full binders. + let id = self.outermost_binder().type_vars_map.get(¶m.index)?; + Some(DeBruijnVar::free(*id)) + } + + pub(crate) fn lookup_const_generic_var( + &self, + param: &hax::ParamConst, + ) -> Option { + // TODO: handle non-top-level full binders. + let id = self + .outermost_binder() + .const_generic_vars_map + .get(¶m.index)?; + Some(DeBruijnVar::free(*id)) + } + + pub(crate) fn lookup_clause_var(&self, id: usize) -> Option { + // TODO: handle non-top-level full binders. + let id = TraitClauseId::from_usize(id); + Some(DeBruijnVar::free(id)) + } + + pub(crate) fn lookup_cached_type( + &self, + cache_key: &HashByAddr>, + ) -> Option { + for bl in self.binding_levels.iter().rev() { + if let Some(ty) = bl.type_trans_cache.get(&cache_key) { + return Some(ty.clone()); + } + } + None } /// Push a group of bound regions and call the continuation. @@ -1063,30 +1119,25 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { /// it contains universally quantified regions). pub(crate) fn translate_region_binder( &mut self, - span: Span, + _span: Span, binder: &hax::Binder, f: F, ) -> Result, Error> where F: FnOnce(&mut Self, &T) -> Result, { - assert!(!self.region_vars.is_empty()); + assert!(!self.binding_levels.is_empty()); + // Register the variables - let mut bound_vars = Vector::new(); - let unit_binder = binder.rebind(()); - let var_ids = self.register_region_binder(span, unit_binder, &mut bound_vars)?; - self.bound_region_vars.push_front(var_ids); - self.region_vars.push_front(bound_vars); - // Translation of types depends on bound variables, we must not mix that up. - let old_ty_cache = std::mem::take(&mut self.type_trans_cache); + let mut binding_level = BindingLevel::default(); + binding_level.push_params_from_binder(binder.rebind(()))?; + self.binding_levels.push_front(binding_level); // Call the continuation. Important: do not short-circuit on error here. let res = f(self, binder.hax_skip_binder_ref()); // Reset - self.bound_region_vars.pop_front(); - let regions = self.region_vars.pop_front().unwrap(); - self.type_trans_cache = old_ty_cache; + let regions = self.binding_levels.pop_front().unwrap().params.regions; // Return res.map(|skip_binder| RegionBinder { @@ -1095,28 +1146,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { }) } - pub(crate) fn push_type_var(&mut self, rid: u32, name: String) -> TypeVarId { - let var_id = self - .generic_params - .types - .push_with(|index| TypeVar { index, name }); - self.type_vars_map.insert(rid, var_id); - var_id - } - pub(crate) fn push_var(&mut self, rid: usize, ty: Ty, name: Option) { let var_id = self.locals.vars.push_with(|index| Var { index, name, ty }); self.vars_map.insert(rid, var_id); } - pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: LiteralTy, name: String) { - let var_id = self - .generic_params - .const_generics - .push_with(|index| ConstGenericVar { index, name, ty }); - self.const_generic_vars_map.insert(rid, var_id); - } - pub(crate) fn fresh_block_id(&mut self, rid: hax::BasicBlock) -> ast::BlockId { // Push to the stack of blocks awaiting translation self.blocks_stack.push_back(rid); @@ -1148,25 +1182,13 @@ impl<'tcx, 'ctx, 'a> IntoFormatter for &'a BodyTransCtx<'tcx, 'ctx> { type C = FmtCtx<'a>; fn into_fmt(self) -> Self::C { - // Translate our generics into a stack of generics. Only the outermost binder has - // non-region parameters. - let mut generics: VecDeque> = self - .region_vars - .iter() - .cloned() - .map(|regions| { - Cow::Owned(GenericParams { - regions, - ..Default::default() - }) - }) - .collect(); - let outermost_generics = generics.back_mut().unwrap().to_mut(); - outermost_generics.types = self.generic_params.types.clone(); - outermost_generics.const_generics = self.generic_params.const_generics.clone(); FmtCtx { translated: Some(&self.t_ctx.translated), - generics, + generics: self + .binding_levels + .iter() + .map(|bl| Cow::Borrowed(&bl.params)) + .collect(), locals: Some(&self.locals), } } diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs index 32d05501..e4e15b8c 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs @@ -1415,7 +1415,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { ) -> Result { let span = item_meta.span; - let mut generics = self.translate_def_generics(span, def)?; + self.translate_def_generics(span, def)?; let signature = match &def.kind { hax::FullDefKind::Closure { args, .. } => &args.sig, @@ -1505,7 +1505,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { match &kind { ClosureKind::FnOnce => state_ty, ClosureKind::Fn | ClosureKind::FnMut => { - let rid = generics + let rid = self + .top_level_generics_mut() .regions .push_with(|index| RegionVar { index, name: None }); let r = Region::Var(DeBruijnVar::free(rid)); @@ -1532,7 +1533,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { }; Ok(FunSig { - generics, + generics: self.top_level_generics().clone(), is_unsafe, is_closure: matches!(&def.kind, hax::FullDefKind::Closure { .. }), closure_info, @@ -1619,7 +1620,7 @@ impl BodyTransCtx<'_, '_> { // const LEN : usize = N; // } // ``` - let generics = self.translate_def_generics(span, def)?; + self.translate_def_generics(span, def)?; // Retrieve the kind let global_kind = self.get_item_kind(span, def)?; @@ -1638,7 +1639,7 @@ impl BodyTransCtx<'_, '_> { Ok(GlobalDecl { def_id, item_meta, - generics, + generics: self.into_generics(), ty, kind: global_kind, init: initializer, diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index d063a1c8..e8a19f2c 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -90,7 +90,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { ctx.translate_trait_predicate(span, trait_pred) })?; let location = match location { - PredicateLocation::Base => &mut self.generic_params.trait_clauses, + PredicateLocation::Base => { + &mut self.top_level_generics_mut().trait_clauses + } PredicateLocation::Parent => &mut self.parent_trait_clauses, PredicateLocation::Item(item_name) => self .item_trait_clauses @@ -110,7 +112,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { let r1 = ctx.translate_region(span, &p.rhs)?; Ok(OutlivesPred(r0, r1)) })?; - self.generic_params.regions_outlive.push(pred); + self.top_level_generics_mut().regions_outlive.push(pred); } ClauseKind::TypeOutlives(p) => { let pred = self.translate_region_binder(span, &pred.kind, |ctx, _| { @@ -118,7 +120,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { let r = ctx.translate_region(span, &p.rhs)?; Ok(OutlivesPred(ty, r)) })?; - self.generic_params.types_outlive.push(pred); + self.top_level_generics_mut().types_outlive.push(pred); } ClauseKind::Projection(p) => { // This is used to express constraints over associated types. @@ -137,7 +139,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { ty, }) })?; - self.generic_params.trait_type_constraints.push(pred); + self.top_level_generics_mut() + .trait_type_constraints + .push(pred); } ClauseKind::ConstArgHasType(..) => { // I don't really understand that one. Why don't they put @@ -248,7 +252,8 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { let mut trait_id = match &impl_source.r#impl { ImplExprAtom::SelfImpl { .. } => TraitRefKind::SelfId, ImplExprAtom::LocalBound { index, .. } => { - TraitRefKind::Clause(DeBruijnVar::free(TraitClauseId::from_usize(*index))) + let var = self.lookup_clause_var(*index).unwrap(); + TraitRefKind::Clause(var) } _ => unreachable!(), }; diff --git a/charon/src/bin/charon-driver/translate/translate_traits.rs b/charon/src/bin/charon-driver/translate/translate_traits.rs index a6df2502..923ecd28 100644 --- a/charon/src/bin/charon-driver/translate/translate_traits.rs +++ b/charon/src/bin/charon-driver/translate/translate_traits.rs @@ -9,6 +9,7 @@ use hax_frontend_exporter as hax; use itertools::Itertools; use rustc_hir::def_id::DefId; use std::collections::HashMap; +use std::mem; use std::sync::Arc; /// The context in which we are translating a clause, used to generate the appropriate ids and @@ -70,7 +71,7 @@ impl BodyTransCtx<'_, '_> { // contain the local trait clauses. The parent clauses are stored in // `self.parent_trait_clauses`. // TODO: Distinguish between required and implied trait clauses? - let generics = self.translate_def_generics(span, def)?; + self.translate_def_generics(span, def)?; // Translate the associated items // We do something subtle here: TODO: explain @@ -102,7 +103,7 @@ impl BodyTransCtx<'_, '_> { // declares them. let gref = GlobalDeclRef { id: self.register_global_decl_id(item_span, rust_item_id), - generics: generics.identity_args(), + generics: self.top_level_generics().identity_args(), }; const_defaults.insert(item_name.clone(), gref); }; @@ -131,21 +132,6 @@ impl BodyTransCtx<'_, '_> { } } - // Debugging: - { - let ctx = self.into_fmt(); - let generic_clauses = generics - .trait_clauses - .iter() - .map(|c| c.fmt_with_ctx(&ctx)) - .collect::>() - .join("\n"); - trace!( - "Trait decl: {:?}:\n- generic.trait_clauses:\n{}\n", - def_id, - generic_clauses - ); - } if item_meta.opacity.is_opaque() { let ctx = self.into_fmt(); self.t_ctx.errors.display_error( @@ -164,8 +150,8 @@ impl BodyTransCtx<'_, '_> { Ok(ast::TraitDecl { def_id, item_meta, - generics, - parent_clauses: self.parent_trait_clauses, + parent_clauses: mem::take(&mut self.parent_trait_clauses), + generics: self.into_generics(), type_clauses, consts, const_defaults, @@ -189,7 +175,7 @@ impl BodyTransCtx<'_, '_> { let span = item_meta.span; - let generics = self.translate_def_generics(span, def)?; + self.translate_def_generics(span, def)?; let hax::FullDefKind::TraitImpl { trait_pred, @@ -265,7 +251,7 @@ impl BodyTransCtx<'_, '_> { // The parameters of the constant are the same as those of the item that // declares them. let generics = match &impl_item.value { - Provided { .. } => generics.identity_args(), + Provided { .. } => self.top_level_generics().identity_args(), _ => implemented_trait.generics.clone(), }; let gref = GlobalDeclRef { id, generics }; @@ -308,7 +294,7 @@ impl BodyTransCtx<'_, '_> { def_id, item_meta, impl_trait: implemented_trait, - generics, + generics: self.into_generics(), parent_trait_refs, type_clauses, consts, diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index eb079650..e483c099 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -4,12 +4,11 @@ use super::translate_ctx::*; use charon_lib::ast::*; use charon_lib::builtins; use charon_lib::common::hash_by_addr::HashByAddr; -use charon_lib::formatter::IntoFormatter; use charon_lib::ids::Vector; -use charon_lib::pretty::FmtWithCtx; use core::convert::*; use hax::Visibility; use hax_frontend_exporter as hax; +use std::collections::HashSet; /// Small helper: we ignore some region names (when they are equal to "'_") fn check_region_name(s: String) -> Option { @@ -46,32 +45,17 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { match ®ion.kind { ReErased => Ok(Region::Erased), ReStatic => Ok(Region::Static), - ReBound(id, br) => { - // See the comments in [BodyTransCtx.bound_vars]: - // - the De Bruijn index identifies the group of variables - // - the var id identifies the variable inside the group - let rid = self - .bound_region_vars - .get(*id) - .expect("Error: missing binder when translating lifetime") - .get(br.var) - .expect("Error: lifetime not found, binders were handled incorrectly"); - let var = if *id == self.region_vars.len() - 1 { - // Late-bound in the signature: we represent it as a free var. - DeBruijnVar::free(*rid) - } else { - DeBruijnVar::bound(DeBruijnId::new(*id), *rid) - }; - Ok(Region::Var(var)) - } - ReEarlyParam(region) => match self.free_region_vars.get(region) { - Some(rid) => Ok(Region::Var(DeBruijnVar::free(*rid))), + ReBound(id, br) => match self.lookup_bound_region(*id, br.var) { + Some(var) => Ok(Region::Var(var)), + None => { + let err = format!("Could not find region: {region:?}"); + error_or_panic!(self, span, err) + } + }, + ReEarlyParam(region) => match self.lookup_early_region(region) { + Some(var) => Ok(Region::Var(var)), None => { - let err = format!( - "Could not find region: {region:?}\n\n\ - Region vars map:\n{:?}\n\nBound region vars:\n{:?}", - self.free_region_vars, self.bound_region_vars - ); + let err = format!("Could not find region: {region:?}"); error_or_panic!(self, span, err) } }, @@ -99,7 +83,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { pub(crate) fn translate_ty(&mut self, span: Span, ty: &hax::Ty) -> Result { trace!("{:?}", ty); let cache_key = HashByAddr(ty.inner().clone()); - if let Some(ty) = self.type_trans_cache.get(&cache_key) { + if let Some(ty) = self.lookup_cached_type(&cache_key) { return Ok(ty.clone()); } @@ -251,16 +235,13 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { trace!("Param"); // Retrieve the translation of the substituted type: - match self.type_vars_map.get(¶m.index) { + match self.lookup_type_var(param) { None => error_or_panic!( self, span, - format!( - "Could not find the type variable {:?} (index: {:?})", - param.name, param.index - ) + format!("Could not find the type variable {:?}", param.name) ), - Some(var_id) => TyKind::TypeVar(DeBruijnVar::Free(*var_id)), + Some(var) => TyKind::TypeVar(var), } } @@ -318,7 +299,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { } }; let ty = kind.into_ty(); - self.type_trans_cache.insert(cache_key, ty.clone()); + self.innermost_binder() + .type_trans_cache + .insert(cache_key, ty.clone()); Ok(ty) } @@ -558,51 +541,56 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { Ok(ScalarValue::from_bits(int_ty, discr.val)) } - /// Sanity check: region names are pairwise distinct (this caused trouble - /// when generating names for the backward functions in Aeneas): at some - /// point, Rustc introduced names equal to `Some("'_")` for the anonymous - /// regions, instead of using `None` (we now check in [translate_region_name] - /// and ignore names equal to "'_"). - pub(crate) fn check_generics(&self) { - let mut s = std::collections::HashSet::new(); - for r in self.region_vars.get(0).unwrap() { - let name = &r.name; - if name.is_some() { - let name = name.as_ref().unwrap(); - assert!( - !s.contains(name), - "Name \"{}\" used for different lifetimes", - name - ); - s.insert(name.clone()); - } - } - } - /// Translate the generics and predicates of this item and its parents. pub(crate) fn translate_def_generics( &mut self, span: Span, def: &hax::FullDef, - ) -> Result { + ) -> Result<(), Error> { + assert!(self.binding_levels.len() == 0); + self.binding_levels.push_back(BindingLevel::default()); self.push_generics_for_def(span, def, false)?; - let mut generic_params = self.generic_params.clone(); - // Sanity checks - self.check_generics(); + assert!(self.binding_levels.len() == 1); + let generic_params = self.top_level_generics(); + + // Sanity check: check the clause ids are consistent. assert!(generic_params .trait_clauses .iter() .enumerate() .all(|(i, c)| c.clause_id.index() == i)); + // Sanity check: region names are pairwise distinct (this caused trouble when generating + // names for the backward functions in Aeneas): at some point, Rustc introduced names equal + // to `Some("'_")` for the anonymous regions, instead of using `None` (we now check in + // [translate_region_name] and ignore names equal to "'_"). + let mut s = HashSet::new(); + for r in &generic_params.regions { + if let Some(name) = &r.name { + assert!( + !s.contains(name), + "Name \"{}\" reused for two different lifetimes", + name + ); + s.insert(name); + } + } - // The regons were tracked separately, we add them back here. - assert!(generic_params.regions.is_empty()); - assert!(self.region_vars.len() == 1); - generic_params.regions = self.region_vars[0].clone(); + Ok(()) + } + + /// At the end of translation, extract the top-level generics. + pub(crate) fn into_generics(mut self) -> GenericParams { + assert!(self.binding_levels.len() == 1); + self.binding_levels.pop_back().unwrap().params + } - trace!("Translated generics: {generic_params:?}"); - Ok(generic_params) + pub(crate) fn top_level_generics(&self) -> &GenericParams { + &self.outermost_binder().params + } + + pub(crate) fn top_level_generics_mut(&mut self) -> &mut GenericParams { + &mut self.outermost_binder_mut().params } /// Add the generics and predicates of this item and its parents to the current context. @@ -717,8 +705,9 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { if let Some(signature) = signature && !is_parent { - let binder = signature.rebind(()); - self.set_first_bound_regions_group(span, binder)?; + let innermost_binder = self.innermost_binder(); + assert!(innermost_binder.bound_region_vars.is_empty()); + innermost_binder.push_params_from_binder(signature.rebind(()))?; } Ok(()) @@ -738,10 +727,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { index: param.index, name: param.name.clone(), }; - let _ = self.push_free_region(region); + let _ = self.innermost_binder().push_early_region(region); } hax::GenericParamDefKind::Type { .. } => { - let _ = self.push_type_var(param.index, param.name.clone()); + let _ = self + .innermost_binder() + .push_type_var(param.index, param.name.clone()); } hax::GenericParamDefKind::Const { ty, .. } => { let span = self.def_span(¶m.def_id); @@ -749,7 +740,11 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { // non-primitive adts, etc. As a result, we can use an empty context. let ty = self.translate_ty(span, ty)?; match ty.kind().as_literal() { - Some(ty) => self.push_const_generic_var(param.index, *ty, param.name.clone()), + Some(ty) => self.innermost_binder().push_const_generic_var( + param.index, + *ty, + param.name.clone(), + ), None => error_or_panic!( self, span, @@ -779,7 +774,7 @@ impl BodyTransCtx<'_, '_> { let span = item_meta.span; // Translate generics and predicates - let generics = self.translate_def_generics(span, def)?; + self.translate_def_generics(span, def)?; // Translate type body let kind = match &def.kind { @@ -807,16 +802,10 @@ impl BodyTransCtx<'_, '_> { let type_def = TypeDecl { def_id: trans_id, item_meta, - generics, + generics: self.into_generics(), kind, }; - trace!( - "{} -> {}", - trans_id.to_string(), - type_def.fmt_with_ctx(&self.into_fmt()) - ); - Ok(type_def) } }