Core models option update

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

src/extract/Extract.ml

@@ -49,17 +49,45 @@ 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 =
   let type_params = generics.types in
   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<T, A>] 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) ->

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

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;