diff --git a/src/PrePasses.ml b/src/PrePasses.ml index cd2a73db0..09bfd942f 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -1209,14 +1209,15 @@ let filter_marker_traits (crate : crate) : crate = in visitor#visit_crate () crate -(** Under [-core-models-lib], remove the [assert_receiver_is_total_eq] method - from the [core::cmp::Eq] trait declaration, from any impls of [Eq], and drop - the corresponding function declarations. This is a Rust-only, - [#[doc(hidden)]] method with an empty default body that Aeneas's own - standard library handles via a hand-tuned override; an external library like - [core_models] doesn't model it, so emitting an impl field for it would not - typecheck against [core_models]'s [Eq] structure. *) -let filter_eq_assert_receiver_method (crate : crate) : crate = +(** Under [-core-models-lib], remove the [Eq] marker method (named + [assert_fields_are_eq] in current rustc, formerly + [assert_receiver_is_total_eq]) from the [core::cmp::Eq] trait declaration, + from any impls of [Eq], and drop the corresponding function declarations. + This is a Rust-only, [#[doc(hidden)]] method with an empty default body that + Aeneas's own standard library handles via a hand-tuned override; an external + library like [core_models] doesn't model it, so emitting an impl field for + it would not typecheck against [core_models]'s [Eq] structure. *) +let filter_eq_assert_fields_method (crate : crate) : crate = if not !Config.core_models_lib then crate else let mctx = NameMatcher.ctx_from_crate crate in @@ -1240,12 +1241,17 @@ let filter_eq_assert_receiver_method (crate : crate) : crate = match eq_id with | None -> crate | Some eq_id -> - let method_name = "assert_receiver_is_total_eq" in + (* The method is named [assert_fields_are_eq] in current rustc; older + versions called it [assert_receiver_is_total_eq]. Match either so the + pass is robust across charon updates. *) + let method_names = + [ "assert_fields_are_eq"; "assert_receiver_is_total_eq" ] + in let eq_decl = TraitDeclId.Map.find eq_id crate.trait_decls in let filtered_method_ids = TraitMethodId.Map.fold (fun mid (m : trait_method binder) acc -> - if m.binder_value.name = method_name then + if List.mem m.binder_value.name method_names then TraitMethodId.Set.add mid acc else acc) eq_decl.methods TraitMethodId.Set.empty @@ -2424,7 +2430,7 @@ let apply_passes (crate : crate) : crate = in let crate = { crate with fun_decls } in let crate = strip_unnecessary_target_suffixes crate in - let crate = filter_eq_assert_receiver_method crate in + let crate = filter_eq_assert_fields_method crate in let crate = filter_marker_traits crate in let crate = filter_type_aliases crate in let crate = replace_static crate in diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 914fe549a..4f42b718d 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -49,6 +49,7 @@ let texpr_to_string (ctx : extraction_ctx) = let compute_allocator_filter ?(extra_trait_decl_refs : Pure.trait_decl_ref list = []) ?(extra_trait_refs : Pure.trait_ref list = []) + ?(type_args_filter : Pure.type_decl_id -> bool list option = fun _ -> None) (generics : Pure.generic_params) (inputs : Pure.ty list) (output : Pure.ty option) (preds : Pure.predicates) : (bool list * bool list) option = @@ -56,10 +57,37 @@ let compute_allocator_filter let trait_clauses = generics.trait_clauses in if type_params = [] then None else + (* When visiting a type application of an ADT whose own allocator parameter + is being filtered (e.g. [IntoIter T A] -> [IntoIter T]), we must not count + the type variables that only appear in the dropped argument positions as + "used". Otherwise an allocator parameter that only shows up in, say, the + output type [IntoIter] would be wrongly kept. *) + let visit_filtered_ty_args (self : _) (env : unit) (type_id : Pure.type_id) + (generics : Pure.generic_args) : bool = + match type_id with + | TAdtId id -> ( + match type_args_filter id with + | Some keep when List.length keep = List.length generics.types -> + List.iter2 + (fun b ty -> if b then self#visit_ty env ty) + keep generics.types; + List.iter (self#visit_const_generic env) generics.const_generics; + List.iter (self#visit_trait_ref env) generics.trait_refs; + true + | _ -> false) + | _ -> false + in let used = ref Pure.TypeVarId.Set.empty in let body_visitor = - object - inherit [_] Pure.iter_type_decl + object (self) + inherit [_] Pure.iter_type_decl as super + + method! visit_ty env t = + match t with + | Pure.TAdt (type_id, generics) + when visit_filtered_ty_args self env type_id generics -> () + | _ -> super#visit_ty env t + method! visit_type_var_id _ id = used := Pure.TypeVarId.Set.add id !used end in @@ -73,8 +101,15 @@ let compute_allocator_filter let clause_tvars (c : Pure.trait_param) : Pure.TypeVarId.Set.t = let s = ref Pure.TypeVarId.Set.empty in let v = - object - inherit [_] Pure.iter_type_decl + object (self) + inherit [_] Pure.iter_type_decl as super + + method! visit_ty env t = + match t with + | Pure.TAdt (type_id, generics) + when visit_filtered_ty_args self env type_id generics -> () + | _ -> super#visit_ty env t + method! visit_type_var_id _ id = s := Pure.TypeVarId.Set.add id !s end in @@ -140,8 +175,12 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) if not !Config.core_models_lib then ctx else let sg = def.f.signature in + let type_args_filter id = + TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map + in match - compute_allocator_filter sg.generics sg.inputs (Some sg.output) sg.preds + compute_allocator_filter ~type_args_filter sg.generics sg.inputs + (Some sg.output) sg.preds with | None -> ctx | Some (keep_params, keep_trait_clauses) -> @@ -3127,11 +3166,14 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) if not !Config.core_models_lib then ctx else let assoc_tys = List.map (fun (_, _, ty) -> ty) trait_impl.types in + let type_args_filter id = + TypeDeclId.Map.find_opt id ctx.types_filter_type_args_map + in match compute_allocator_filter ~extra_trait_decl_refs:[ trait_impl.impl_trait ] - ~extra_trait_refs:trait_impl.parent_trait_refs trait_impl.generics - assoc_tys None trait_impl.preds + ~extra_trait_refs:trait_impl.parent_trait_refs ~type_args_filter + trait_impl.generics assoc_tys None trait_impl.preds with | None -> ctx | Some (keep_params, keep_trait_clauses) -> diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index 86f5be0e5..f76049e16 100644 --- a/src/extract/ExtractBuiltin.ml +++ b/src/extract/ExtractBuiltin.ml @@ -180,6 +180,27 @@ let mk_builtin_types_map () = let builtin_types_map = mk_memoized mk_builtin_types_map +(** Map from rust type name to its builtin info, restricted to the types that + carry a [keep_params] filter (i.e. types from which Charon's + [hide_allocator] pass leaves a dangling allocator type parameter, such as + [alloc::vec::into_iter::IntoIter]). + + Unlike {!builtin_types_map}, this map is *not* emptied under + [-core-models-lib]: even when the builtin type overrides are disabled, we + still need to drop the dangling allocator type parameter so that the + extracted types match the [core_models] library, which models them without + an allocator (e.g. [IntoIter T] rather than [IntoIter T Global]). *) +let mk_builtin_types_keep_params_map () = + NameMatcherMap.of_list + (List.filter_map + (fun (info : Pure.builtin_type_info) -> + match info.keep_params with + | Some _ -> Some (info.rust_name, info) + | None -> None) + lean_builtin_types) + +let builtin_types_keep_params_map = mk_memoized mk_builtin_types_keep_params_map + let int_and_smaller_list : (string * string) list = let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in let int_names = List.rev [ "i8"; "i16"; "i32"; "i64"; "i128" ] in diff --git a/src/symbolic/SymbolicToPureTypes.ml b/src/symbolic/SymbolicToPureTypes.ml index d35b6d67a..95371ae65 100644 --- a/src/symbolic/SymbolicToPureTypes.ml +++ b/src/symbolic/SymbolicToPureTypes.ml @@ -311,6 +311,21 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : match_name_find_opt ctx def.item_meta.name (ExtractBuiltin.builtin_types_map ()) in + (* Under [-core-models-lib] the builtin type overrides are disabled, so the + lookup above returns [None]. We still need the allocator [keep_params] of + types like [IntoIter] so that the dangling allocator type parameter (left + by Charon's [hide_allocator] pass) is filtered out, matching the + [core_models] library. Recover it from the dedicated, non-disabled map. + This only carries [keep_params]; the extract name still comes from the + standard name mangling (which, for these types, coincides with the builtin + name anyway). *) + let builtin_info = + if Option.is_some builtin_info || not !Config.core_models_lib then + builtin_info + else + match_name_find_opt ctx def.item_meta.name + (ExtractBuiltin.builtin_types_keep_params_map ()) + in { def_id; name;