From 6843f31467cf830ba2cce0ea35cfa897f6aeb9ca Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Dec 2024 16:36:17 +0100 Subject: [PATCH] Don't use `Free` variables internally, substitute at the end --- charon-ml/src/generated/Generated_Types.ml | 30 ++++++++---- charon/Charon.toml | 10 ++-- charon/src/ast/krate.rs | 19 ++++++++ charon/src/ast/types/vars.rs | 29 +++++++---- charon/src/ast/types_utils.rs | 48 +++++++++++-------- .../charon-driver/translate/translate_ctx.rs | 6 +-- .../translate/translate_functions_to_ullbc.rs | 2 +- charon/src/ids/vector.rs | 12 +++++ charon/src/pretty/formatter.rs | 2 + charon/src/transform/mod.rs | 3 ++ charon/src/transform/unbind_item_vars.rs | 27 +++++++++++ .../transform/update_closure_signatures.rs | 2 +- charon/tests/ui/hide-marker-traits.out | 22 +++++++++ charon/tests/ui/hide-marker-traits.rs | 17 +++++++ 14 files changed, 177 insertions(+), 52 deletions(-) create mode 100644 charon/src/transform/unbind_item_vars.rs create mode 100644 charon/tests/ui/hide-marker-traits.out create mode 100644 charon/tests/ui/hide-marker-traits.rs diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index a4d5289ed..619debede 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -56,18 +56,26 @@ and de_bruijn_id = int (** Type-level variable. Variables are bound in groups. Each item has a top-level binding group in its `generic_params` - field, and then inner binders are possible using the `RegionBinder` type. Each variable is - linked to exactly one binder. The `Id` then identifies the specific variable among all those - bound in that group. - - We distinguish the top-level (item-level) binder from others: a `Free` variable indicates a - variable bound at the item level; a `Bound` variable indicates a variable bound at an inner - binder, using a de Bruijn index (i.e. counting binders from the innermost out). - - This distinction is not necessary (we could use bound variables only) but is practical. + field, and then inner binders are possible using the `RegionBinder` and `Binder` types. + Each variable is linked to exactly one binder. The `Id` then identifies the specific variable + among all those bound in that group. For instance, we have the following: ```text + fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {} + ^^^^^^ ^^ ^ ^ ^^ ^ ^ ^ + | inner binder | | inner binder | | | + top-level binder | | | | | + Bound(1, b) | Bound(2, b) | Bound(0, d) + | | + Bound(0, c) Bound(1, c) + ``` + + To make consumption easier for projects that don't do heavy substitution, a micro-pass at the + end changes the variables bound at the top-level (i.e. in the `GenericParams` of items) to be + `Free`. This is an optional pass, we may add a flag to deactivate it. The example above + becomes: + ```text fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {} ^^^^^^ ^^ ^ ^ ^^ ^ ^ ^ | inner binder | | inner binder | | | @@ -83,7 +91,9 @@ and 'a0 de_bruijn_var = | Bound of de_bruijn_id * 'a0 (** A variable attached to the nth binder, counting from the innermost. *) | Free of 'a0 - (** A variable attached to the outermost binder (the one on the item). *) + (** A variable attached to the outermost binder (the one on the item). As explained above, This + is not used in charon internals, only as a micro-pass before exporting the crate data. + *) and type_var_id = TypeVarId.id and const_generic_var_id = ConstGenericVarId.id diff --git a/charon/Charon.toml b/charon/Charon.toml index 58df40e8e..320be2244 100644 --- a/charon/Charon.toml +++ b/charon/Charon.toml @@ -9,13 +9,13 @@ include = [ "alloc::alloc::Global", "alloc::string::String", "alloc::vec::Vec", + "core::cmp::Ordering", + "core::ops::control_flow::ControlFlow", "core::option::Option", - "std::path::PathBuf", - "crate::options::CliOpts", "crate::ast", - "crate::ast::krate", "crate::ast::expressions", "crate::ast::gast", + "crate::ast::krate", "crate::ast::llbc_ast", "crate::ast::meta", "crate::ast::names", @@ -23,6 +23,8 @@ include = [ "crate::ast::ullbc_ast", "crate::ast::values", "crate::ids::vector::Vector", - "crate::transform::reorder_decls::GDeclarationGroup", + "crate::options::CliOpts", "crate::transform::reorder_decls::DeclarationGroup", + "crate::transform::reorder_decls::GDeclarationGroup", + "std::path::PathBuf", ] diff --git a/charon/src/ast/krate.rs b/charon/src/ast/krate.rs index 82d4fb8db..a3a1b6d8b 100644 --- a/charon/src/ast/krate.rs +++ b/charon/src/ast/krate.rs @@ -175,6 +175,15 @@ impl TranslatedCrate { .iter() .flat_map(|id| Some((*id, self.get_item(*id)?))) } + pub fn all_items_mut(&mut self) -> impl Iterator> { + self.type_decls + .iter_mut() + .map(AnyTransItemMut::Type) + .chain(self.fun_decls.iter_mut().map(AnyTransItemMut::Fun)) + .chain(self.global_decls.iter_mut().map(AnyTransItemMut::Global)) + .chain(self.trait_decls.iter_mut().map(AnyTransItemMut::TraitDecl)) + .chain(self.trait_impls.iter_mut().map(AnyTransItemMut::TraitImpl)) + } } impl<'ctx> AnyTransItem<'ctx> { @@ -223,6 +232,16 @@ impl<'ctx> AnyTransItem<'ctx> { } impl<'ctx> AnyTransItemMut<'ctx> { + pub fn as_ref(&self) -> AnyTransItem<'_> { + match self { + AnyTransItemMut::Type(d) => AnyTransItem::Type(d), + AnyTransItemMut::Fun(d) => AnyTransItem::Fun(d), + AnyTransItemMut::Global(d) => AnyTransItem::Global(d), + AnyTransItemMut::TraitDecl(d) => AnyTransItem::TraitDecl(d), + AnyTransItemMut::TraitImpl(d) => AnyTransItem::TraitImpl(d), + } + } + /// The generic parameters of this item. pub fn generic_params(&mut self) -> &mut GenericParams { match self { diff --git a/charon/src/ast/types/vars.rs b/charon/src/ast/types/vars.rs index 6f2b517aa..655a9d992 100644 --- a/charon/src/ast/types/vars.rs +++ b/charon/src/ast/types/vars.rs @@ -28,15 +28,9 @@ pub struct DeBruijnId { /// Type-level variable. /// /// Variables are bound in groups. Each item has a top-level binding group in its `generic_params` -/// field, and then inner binders are possible using the `RegionBinder` type. Each variable is -/// linked to exactly one binder. The `Id` then identifies the specific variable among all those -/// bound in that group. -/// -/// We distinguish the top-level (item-level) binder from others: a `Free` variable indicates a -/// variable bound at the item level; a `Bound` variable indicates a variable bound at an inner -/// binder, using a de Bruijn index (i.e. counting binders from the innermost out). -/// -/// This distinction is not necessary (we could use bound variables only) but is practical. +/// field, and then inner binders are possible using the `RegionBinder` and `Binder` types. +/// Each variable is linked to exactly one binder. The `Id` then identifies the specific variable +/// among all those bound in that group. /// /// For instance, we have the following: /// ```text @@ -44,6 +38,20 @@ pub struct DeBruijnId { /// ^^^^^^ ^^ ^ ^ ^^ ^ ^ ^ /// | inner binder | | inner binder | | | /// top-level binder | | | | | +/// Bound(1, b) | Bound(2, b) | Bound(0, d) +/// | | +/// Bound(0, c) Bound(1, c) +/// ``` +/// +/// To make consumption easier for projects that don't do heavy substitution, a micro-pass at the +/// end changes the variables bound at the top-level (i.e. in the `GenericParams` of items) to be +/// `Free`. This is an optional pass, we may add a flag to deactivate it. The example above +/// becomes: +/// ```text +/// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {} +/// ^^^^^^ ^^ ^ ^ ^^ ^ ^ ^ +/// | inner binder | | inner binder | | | +/// top-level binder | | | | | /// Free(b) | Free(b) | Bound(0, d) /// | | /// Bound(0, c) Bound(1, c) @@ -54,7 +62,8 @@ pub struct DeBruijnId { pub enum DeBruijnVar { /// A variable attached to the nth binder, counting from the innermost. Bound(DeBruijnId, Id), - /// A variable attached to the outermost binder (the one on the item). + /// A variable attached to the outermost binder (the one on the item). As explained above, This + /// is not used in charon internals, only as a micro-pass before exporting the crate data. Free(Id), } diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs index 3eabb9324..af00faee1 100644 --- a/charon/src/ast/types_utils.rs +++ b/charon/src/ast/types_utils.rs @@ -74,27 +74,36 @@ impl GenericParams { GenericArgs { regions: self .regions - .iter_indexed() - .map(|(id, _)| Region::Var(DeBruijnVar::free(id))) - .collect(), + .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::new_at_zero(id))), types: self .types - .iter_indexed() - .map(|(id, _)| TyKind::TypeVar(DeBruijnVar::free(id)).into_ty()) - .collect(), + .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::new_at_zero(id)).into_ty()), const_generics: self .const_generics - .iter_indexed() - .map(|(id, _)| ConstGeneric::Var(DeBruijnVar::free(id))) - .collect(), - trait_refs: self - .trait_clauses - .iter_indexed() - .map(|(id, clause)| TraitRef { - kind: TraitRefKind::Clause(DeBruijnVar::free(id)), - trait_decl_ref: clause.trait_.clone(), - }) - .collect(), + .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::new_at_zero(id))), + trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef { + kind: TraitRefKind::Clause(DeBruijnVar::new_at_zero(id)), + trait_decl_ref: clause.trait_.clone(), + }), + } + } + + /// Like `identity_args`, but uses free variables instead of bound ones. + pub fn free_identity_args(&self) -> GenericArgs { + GenericArgs { + regions: self + .regions + .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::free(id))), + types: self + .types + .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::free(id)).into_ty()), + const_generics: self + .const_generics + .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::free(id))), + trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef { + kind: TraitRefKind::Clause(DeBruijnVar::free(id)), + trait_decl_ref: clause.trait_.clone(), + }), } } } @@ -588,10 +597,7 @@ impl<'a> SubstVisitor<'a> { } fn should_subst(&self, var: DeBruijnVar) -> Option { - match var { - DeBruijnVar::Free(id) => Some(id), - DeBruijnVar::Bound(..) => None, - } + var.bound_at_depth(self.binder_depth) } fn enter_poly_trait_decl_ref(&mut self, _: &mut PolyTraitDeclRef) { diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 59ace804c..a4e145adf 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -1085,11 +1085,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { /// Make a `DeBruijnVar`, where we use `Free` for the outermost binder and `Bound` for the /// others. fn bind_var(&self, dbid: usize, varid: Id) -> DeBruijnVar { - if dbid == self.binding_levels.len() - 1 { - DeBruijnVar::free(varid) - } else { - DeBruijnVar::bound(DeBruijnId::new(dbid), varid) - } + DeBruijnVar::bound(DeBruijnId::new(dbid), varid) } pub(crate) fn lookup_bound_region( 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 48ac1a1fc..2d9e48e27 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 @@ -1509,7 +1509,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> { .innermost_generics_mut() .regions .push_with(|index| RegionVar { index, name: None }); - let r = Region::Var(DeBruijnVar::free(rid)); + let r = Region::Var(DeBruijnVar::new_at_zero(rid)); let mutability = if kind == ClosureKind::Fn { RefKind::Shared } else { diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs index 3f2baf626..ac825c4d5 100644 --- a/charon/src/ids/vector.rs +++ b/charon/src/ids/vector.rs @@ -153,6 +153,18 @@ where } } + /// Map each entry to a new one, keeping the same ids. + pub fn map_ref_indexed<'a, U>(&'a self, mut f: impl FnMut(I, &'a T) -> U) -> Vector { + Vector { + vector: self + .vector + .iter_enumerated() + .map(|(i, x_opt)| x_opt.as_ref().map(|x| f(i, x))) + .collect(), + real_len: self.real_len, + } + } + /// Iter over the nonempty slots. pub fn iter(&self) -> impl Iterator + Clone { self.vector.iter().flat_map(|opt| opt.as_ref()) diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs index 87a925a1a..888d969b6 100644 --- a/charon/src/pretty/formatter.rs +++ b/charon/src/pretty/formatter.rs @@ -284,6 +284,7 @@ impl<'a> Formatter for FmtCtx<'a> { None => format!("wrong_region('_{var})"), Some(v) => match &v.name { Some(name) => name.to_string(), + None if dbid == self.generics.len() - 1 => format!("'_{varid}"), None => format!("'_{var}"), }, } @@ -354,6 +355,7 @@ impl<'a> Formatter for FmtCtx<'a> { .and_then(|generics| generics.trait_clauses.get(varid)) { None => format!("missing_clause_var({var})"), + Some(_) if dbid == self.generics.len() - 1 => format!("@TraitClause{varid}"), Some(_) => format!("@TraitClause{var}"), } } diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs index 37a024604..3aed47e3d 100644 --- a/charon/src/transform/mod.rs +++ b/charon/src/transform/mod.rs @@ -24,6 +24,7 @@ pub mod reorder_decls; pub mod simplify_constants; pub mod skip_trait_refs_when_known; pub mod ullbc_to_llbc; +pub mod unbind_item_vars; pub mod update_block_indices; pub mod update_closure_signatures; @@ -118,6 +119,8 @@ pub static LLBC_PASSES: &[Pass] = &[ StructuredBody(&recover_body_comments::Transform), // Check that all supplied generic types match the corresponding generic parameters. NonBody(&check_generics::Check), + // Use `DeBruijnVar::Free` for the variables bound in item signatures. + NonBody(&unbind_item_vars::Check), ]; #[derive(Clone, Copy)] diff --git a/charon/src/transform/unbind_item_vars.rs b/charon/src/transform/unbind_item_vars.rs new file mode 100644 index 000000000..4c542d552 --- /dev/null +++ b/charon/src/transform/unbind_item_vars.rs @@ -0,0 +1,27 @@ +//! Check that all supplied generic types match the corresponding generic parameters. + +use derive_visitor::DriveMut; + +use crate::ast::types_utils::SubstVisitor; + +use super::{ctx::TransformPass, TransformCtx}; + +pub struct Check; +impl TransformPass for Check { + fn transform_ctx(&self, ctx: &mut TransformCtx) { + for mut item in ctx.translated.all_items_mut() { + let args = item.generic_params().free_identity_args(); + let mut visitor = SubstVisitor::new(&args); + item.drive_mut(&mut visitor); + } + for decl in &ctx.translated.fun_decls { + if let Ok(body_id) = decl.body { + if let Some(body) = ctx.translated.bodies.get_mut(body_id) { + let args = decl.signature.generics.free_identity_args(); + let mut visitor = SubstVisitor::new(&args); + body.drive_mut(&mut visitor); + } + } + } + } +} diff --git a/charon/src/transform/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs index b56dfadd8..3187be3ef 100644 --- a/charon/src/transform/update_closure_signatures.rs +++ b/charon/src/transform/update_closure_signatures.rs @@ -25,7 +25,7 @@ impl<'a> InsertRegions<'a> { let index = self .regions .push_with(|index| RegionVar { index, name: None }); - *r = Region::Var(DeBruijnVar::free(index)); + *r = Region::Var(DeBruijnVar::bound(DeBruijnId::new(self.depth), index)); } } diff --git a/charon/tests/ui/hide-marker-traits.out b/charon/tests/ui/hide-marker-traits.out new file mode 100644 index 000000000..034f06886 --- /dev/null +++ b/charon/tests/ui/hide-marker-traits.out @@ -0,0 +1,22 @@ +# Final LLBC before serialization: + +trait test_crate::Idx + +struct test_crate::IndexVec + where + [@TraitClause1]: test_crate::Idx, + = +{ + i: I, +} + +struct test_crate::Vector + where + [@TraitClause1]: test_crate::Idx, + = +{ + vector: test_crate::IndexVec[@TraitClause1], +} + + + diff --git a/charon/tests/ui/hide-marker-traits.rs b/charon/tests/ui/hide-marker-traits.rs new file mode 100644 index 000000000..251770086 --- /dev/null +++ b/charon/tests/ui/hide-marker-traits.rs @@ -0,0 +1,17 @@ +//@ charon-args=--hide-marker-traits +//! Reproduces a crash when substituting variables with the `--hide-marker-traits` option. +trait Idx {} + +pub struct IndexVec +where + I: Idx, +{ + i: I, +} + +pub struct Vector +where + I: Idx, +{ + vector: IndexVec, +}