From 2e810aac82cf50b12909f92ce7c9b5fd54228756 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 16 Dec 2024 15:47:48 +0100 Subject: [PATCH 1/3] Correctly handle binders in ml printing --- charon-ml/src/NameMatcher.ml | 3 +- charon-ml/src/PrintLlbcAst.ml | 3 +- charon-ml/src/PrintTypes.ml | 122 +++++++++++++++++++-------------- charon-ml/src/PrintUllbcAst.ml | 3 +- charon-ml/src/PrintUtils.ml | 21 +++--- 5 files changed, 82 insertions(+), 70 deletions(-) diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index fb5345689..9062044de 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -235,8 +235,7 @@ let ctx_to_fmt_env (ctx : ctx) : PrintLlbcAst.fmt_env = global_decls = ctx.global_decls; trait_decls = ctx.trait_decls; trait_impls = ctx.trait_impls; - regions = []; - generics = TypesUtils.empty_generic_params; + generics = []; locals = []; } diff --git a/charon-ml/src/PrintLlbcAst.ml b/charon-ml/src/PrintLlbcAst.ml index ada4838b3..02319463a 100644 --- a/charon-ml/src/PrintLlbcAst.ml +++ b/charon-ml/src/PrintLlbcAst.ml @@ -150,8 +150,7 @@ module Crate = struct global_decls = m.global_decls; trait_decls = m.trait_decls; trait_impls = m.trait_impls; - regions = []; - generics = empty_generic_params; + generics = []; locals = []; } diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index ca3f9c04c..08b1a651f 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -7,9 +7,6 @@ open TypesUtils open GAst open PrintUtils -let type_var_to_string (tv : type_var) : string = tv.name -let const_generic_var_to_string (v : const_generic_var) : string = v.name - let region_var_to_string (rv : region_var) : string = match rv.name with | Some name -> name @@ -37,23 +34,39 @@ let ref_kind_to_string (rk : ref_kind) : string = let builtin_ty_to_string (_ : builtin_ty) : string = "Box" -let trait_clause_id_to_pretty_string (id : trait_clause_id) : string = - "TraitClause@" ^ TraitClauseId.to_string id - -let de_bruijn_var_to_pretty_string show_bound show_free var : string = +let de_bruijn_var_to_pretty_string show_varid var : string = match var with - | Bound (dbid, varid) -> show_de_bruijn_id dbid ^ "_" ^ show_bound varid - | Free varid -> "'" ^ show_free varid + | Bound (dbid, varid) -> show_de_bruijn_id dbid ^ "_" ^ show_varid varid + | Free varid -> show_varid varid let region_db_var_to_pretty_string (var : region_db_var) : string = - "'" ^ de_bruijn_var_to_pretty_string RegionId.to_string RegionId.to_string var + "'" ^ de_bruijn_var_to_pretty_string RegionId.to_string var + +let type_db_var_to_pretty_string (var : type_db_var) : string = + "T@" ^ de_bruijn_var_to_pretty_string TypeVarId.to_string var let type_var_id_to_pretty_string (id : type_var_id) : string = "T@" ^ TypeVarId.to_string id +let type_var_to_string (tv : type_var) : string = tv.name + let const_generic_var_id_to_pretty_string (id : const_generic_var_id) : string = "C@" ^ ConstGenericVarId.to_string id +let const_generic_db_var_to_pretty_string (var : const_generic_db_var) : string + = + "C@" ^ de_bruijn_var_to_pretty_string ConstGenericVarId.to_string var + +let const_generic_var_to_string (v : const_generic_var) : string = v.name + +let trait_clause_id_to_pretty_string (id : trait_clause_id) : string = + "TraitClause@" ^ TraitClauseId.to_string id + +let trait_db_var_to_pretty_string (var : trait_db_var) : string = + "TraitClause@" ^ de_bruijn_var_to_pretty_string TraitClauseId.to_string var + +let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id + let type_decl_id_to_pretty_string (id : type_decl_id) : string = "TypeDecl@" ^ TypeDeclId.to_string id @@ -75,57 +88,64 @@ let variant_id_to_pretty_string (id : variant_id) : string = let field_id_to_pretty_string (id : field_id) : string = "Field@" ^ FieldId.to_string id -let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id +let lookup_var_in_env (env : 'a fmt_env) + (find_in : generic_params -> 'id -> 'b option) (var : 'id de_bruijn_var) : + 'b option = + if List.length env.generics == 0 then None + else + let dbid, varid = + match var with + | Bound (dbid, varid) -> (dbid, varid) + | Free varid -> + let len = List.length env.generics in + let dbid = len - 1 in + (dbid, varid) + in + match List.nth_opt env.generics dbid with + | None -> None + | Some generics -> begin + match find_in generics varid with + | None -> None + | Some r -> Some r + end let region_db_var_to_string (env : 'a fmt_env) (var : region_db_var) : string = - let dbid, varid = - match var with - | Bound (dbid, varid) -> (dbid, varid) - | Free varid -> - let len = List.length env.regions in - let dbid = if len == 0 then 0 else len - 1 in - (dbid, varid) + (* Note that the regions are not necessarily ordered following their indices *) + let find (generics : generic_params) varid = + List.find_opt (fun (v : region_var) -> v.index = varid) generics.regions in - match List.nth_opt env.regions dbid with + match lookup_var_in_env env find var with | None -> region_db_var_to_pretty_string var - | Some regions -> begin - (* Note that the regions are not necessarily ordered following their indices *) - match List.find_opt (fun (r : region_var) -> r.index = varid) regions with - | None -> region_db_var_to_pretty_string var - | Some r -> region_var_to_string r - end + | Some r -> region_var_to_string r let type_db_var_to_string (env : 'a fmt_env) (var : type_db_var) : string = - match var with - | Bound _ -> failwith "bound type variable" - | Free id -> begin - (* Note that the types are not necessarily ordered following their indices *) - match - List.find_opt (fun (x : type_var) -> x.index = id) env.generics.types - with - | None -> type_var_id_to_pretty_string id - | Some x -> type_var_to_string x - end + let find (generics : generic_params) varid = + List.find_opt (fun (v : type_var) -> v.index = varid) generics.types + in + match lookup_var_in_env env find var with + | None -> type_db_var_to_pretty_string var + | Some r -> type_var_to_string r let const_generic_db_var_to_string (env : 'a fmt_env) (var : const_generic_db_var) : string = - match var with - | Bound _ -> failwith "bound const generic variable" - | Free id -> begin - (* Note that the types are not necessarily ordered following their indices *) - match - List.find_opt - (fun (x : const_generic_var) -> x.index = id) - env.generics.const_generics - with - | None -> const_generic_var_id_to_pretty_string id - | Some x -> const_generic_var_to_string x - end + let find (generics : generic_params) varid = + List.find_opt + (fun (v : const_generic_var) -> v.index = varid) + generics.const_generics + in + match lookup_var_in_env env find var with + | None -> const_generic_db_var_to_pretty_string var + | Some r -> const_generic_var_to_string r let trait_db_var_to_string (env : 'a fmt_env) (var : trait_db_var) : string = - match var with - | Bound _ -> failwith "bound trait clause variable" - | Free id -> trait_clause_id_to_pretty_string id + let find (generics : generic_params) varid = + List.find_opt + (fun (v : trait_clause) -> v.clause_id = varid) + generics.trait_clauses + in + match lookup_var_in_env env find var with + | None -> trait_db_var_to_pretty_string var + | Some r -> trait_clause_id_to_pretty_string r.clause_id let region_to_string (env : 'a fmt_env) (r : region) : string = match r with @@ -220,7 +240,7 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string = | RMut -> "*mut " ^ ty_to_string env rty | RShared -> "*const " ^ ty_to_string env rty) | TArrow binder -> - let env = { env with regions = binder.binder_regions :: env.regions } in + let env = fmt_env_push_regions env binder.binder_regions in let inputs, output = binder.binder_value in let inputs = "(" ^ String.concat ", " (List.map (ty_to_string env) inputs) ^ ") -> " diff --git a/charon-ml/src/PrintUllbcAst.ml b/charon-ml/src/PrintUllbcAst.ml index ff8acb88d..de7554678 100644 --- a/charon-ml/src/PrintUllbcAst.ml +++ b/charon-ml/src/PrintUllbcAst.ml @@ -119,8 +119,7 @@ module Crate = struct global_decls = m.global_decls; trait_decls = m.trait_decls; trait_impls = m.trait_impls; - regions = []; - generics = empty_generic_params; + generics = []; locals = []; } in diff --git a/charon-ml/src/PrintUtils.ml b/charon-ml/src/PrintUtils.ml index 70e65106a..ef51d1465 100644 --- a/charon-ml/src/PrintUtils.ml +++ b/charon-ml/src/PrintUtils.ml @@ -19,26 +19,21 @@ type 'fun_body fmt_env = { global_decls : global_decl GlobalDeclId.Map.t; trait_decls : trait_decl TraitDeclId.Map.t; trait_impls : trait_impl TraitImplId.Map.t; - regions : region_var list list; - (** We have a stack of regions, because we can dive into groups of - universally quantified regions (for instance because of the arrow - type). - - Note that the variables in the generics don't need to be ordered following their - indices, i.e., the region var of index 0 doesn't have to be at index 0, - etc. We lookup the variables by checking their id, not their position. + generics : generic_params list; + (** We have a stack of generic parameters, because we can dive into + binders (for instance because of the arrow type). *) - generics : generic_params; - (* We ignore `generics.regions` as they are tracked in `regions` already *) locals : (VarId.id * string option) list; (** The local variables don't need to be ordered (same as the generics) *) } let fmt_env_update_generics_and_preds (env : 'a fmt_env) (generics : generic_params) : 'a fmt_env = - let { regions; _ } : generic_params = generics in - { env with regions = regions :: env.regions; generics } + { env with generics = generics :: env.generics } let fmt_env_push_regions (env : 'a fmt_env) (regions : region_var list) : 'a fmt_env = - { env with regions = regions :: env.regions } + { + env with + generics = { TypesUtils.empty_generic_params with regions } :: env.generics; + } From fcd5a6f20707d394a9ffb93eaf5dc196bd2a238c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2024 10:56:00 +0100 Subject: [PATCH 2/3] Correctly handle binders in name matcher --- charon-ml/src/NameMatcher.ml | 75 ++++++++++++++++++------------------ 1 file changed, 38 insertions(+), 37 deletions(-) diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index 9062044de..26580c91e 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -776,42 +776,53 @@ let mk_name_matcher (ctx : ctx) (c : match_config) (pat : string) : * Helpers to convert names to patterns *) -(* We use this to store the constraints maps (the map from variable - ids to option pattern variable ids) *) -type constraints = { - rmap : var option T.RegionId.Map.t list; - (** Note that we have a stack of maps for the regions *) +(* Maps from variable ids to option pattern variable ids *) +type vars_map = { + rmap : var option T.RegionId.Map.t; tmap : var option T.TypeVarId.Map.t; cmap : var option T.ConstGenericVarId.Map.t; } -let empty_constraints = +let empty_vars_map = { - rmap = [ T.RegionId.Map.empty ]; + rmap = T.RegionId.Map.empty; tmap = T.TypeVarId.Map.empty; cmap = T.ConstGenericVarId.Map.empty; } +(* We use this to store the constraints maps. Note that we have a stack of + maps, with one level per binder. *) +type constraints = vars_map list + +let empty_constraints = [ empty_vars_map ] + let ref_kind_to_pattern (rk : T.ref_kind) : ref_kind = match rk with | RMut -> RMut | RShared -> RShared +let lookup_var_in_maps (m : constraints) + (lookup : 'id -> vars_map -> 'a option option) (var : 'id T.de_bruijn_var) : + 'a option = + let dbid, varid = + match var with + | Bound (dbid, varid) -> (dbid, varid) + | Free varid -> (List.length m - 1, varid) + in + match List.nth_opt m dbid with + | None -> None + | Some map -> ( + match lookup varid map with + | Some r -> r + | None -> None) + let region_to_pattern (m : constraints) (r : T.region) : region = match r with | RVar var -> - let dbid, varid = - match var with - | Bound (dbid, varid) -> (dbid, varid) - | Free varid -> (List.length m.rmap - 1, varid) - in RVar - (match List.nth_opt m.rmap dbid with - | None -> None - | Some rmap -> ( - match T.RegionId.Map.find_opt varid rmap with - | Some r -> r - | None -> None)) + (lookup_var_in_maps m + (fun varid map -> T.RegionId.Map.find_opt varid map.rmap) + var) | RStatic -> RStatic | RErased -> (* We do get there when converting function pointers (when we try to @@ -819,25 +830,15 @@ let region_to_pattern (m : constraints) (r : T.region) : region = RVar None let type_var_to_pattern (m : constraints) (var : T.type_db_var) : var option = - match var with - | Bound _ -> failwith "bound type var" - | Free id -> begin - match T.TypeVarId.Map.find_opt id m.tmap with - | Some v -> v - | None -> None - (* Return the empty pattern *) - end + lookup_var_in_maps m + (fun varid map -> T.TypeVarId.Map.find_opt varid map.tmap) + var let const_generic_var_to_pattern (m : constraints) (var : T.const_generic_db_var) : var option = - match var with - | Bound _ -> failwith "bound const generic var" - | Free id -> begin - match T.ConstGenericVarId.Map.find_opt id m.cmap with - | Some v -> v - | None -> None - (* Return the empty pattern *) - end + lookup_var_in_maps m + (fun varid map -> T.ConstGenericVarId.Map.find_opt varid map.cmap) + var let constraints_map_compute_regions_map (regions : T.region_var list) : var option T.RegionId.Map.t = @@ -859,7 +860,7 @@ let constraints_map_compute_regions_map (regions : T.region_var list) : regions) let compute_constraints_map (generics : T.generic_params) : constraints = - let rmap = [ constraints_map_compute_regions_map generics.regions ] in + let rmap = constraints_map_compute_regions_map generics.regions in let tmap = T.TypeVarId.Map.of_list (List.map @@ -872,12 +873,12 @@ let compute_constraints_map (generics : T.generic_params) : constraints = (fun (x : T.const_generic_var) -> (x.index, Some (VarName x.name))) generics.const_generics) in - { rmap; tmap; cmap } + [ { rmap; tmap; cmap } ] let constraints_map_push_regions_map (m : constraints) (regions : T.region_var list) : constraints = let rmap = constraints_map_compute_regions_map regions in - { m with rmap = rmap :: m.rmap } + { empty_vars_map with rmap } :: m (** Push a regions map to the constraints map, if the group of regions is non-empty - TODO: do something more precise *) From a3a0149226e435cb7dc804cc6f29d0df64ae5020 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Dec 2024 16:36:17 +0100 Subject: [PATCH 3/3] 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 +++++++ charon/tests/ui/traits.out | 16 +++++++ charon/tests/ui/traits.rs | 10 ++++ 16 files changed, 203 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, +} diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out index 6a945f8f8..ef920bc3a 100644 --- a/charon/tests/ui/traits.out +++ b/charon/tests/ui/traits.out @@ -1020,6 +1020,22 @@ fn test_crate::flibidi() return } +trait test_crate::assoc_ty_trait_ref::SliceIndex +{ + parent_clause0 : [@TraitClause0]: core::marker::Sized + type Output +} + +fn test_crate::assoc_ty_trait_ref::index() -> @TraitClause1::Output +where + [@TraitClause0]: core::marker::Sized, + [@TraitClause1]: test_crate::assoc_ty_trait_ref::SliceIndex, +{ + let @0: @TraitClause1::Output; // return + + panic(core::panicking::panic) +} + fn test_crate::{test_crate::TestType[@TraitClause0]}#6::test::TestTrait::test<'_0, Self>(@1: &'_0 (Self)) -> bool trait test_crate::{test_crate::TestType[@TraitClause0]}#6::test::TestTrait diff --git a/charon/tests/ui/traits.rs b/charon/tests/ui/traits.rs index c2ad6efe0..92a7f2783 100644 --- a/charon/tests/ui/traits.rs +++ b/charon/tests/ui/traits.rs @@ -356,3 +356,13 @@ pub fn call<'a, F: Fn(&'a ()) -> Wrapper<(bool, &'a ())>>(_: F) {} pub fn flibidi() -> () { call(flabada); } + +mod assoc_ty_trait_ref { + //! Minimal reproducer for a binder bug + trait SliceIndex { + type Output; + } + fn index() -> I::Output { + todo!() + } +}