diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 49c6f3f83..dbabd56ac 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -118,6 +118,12 @@ jobs: "$script" fi + - name: Upload Lean oleans + uses: softprops/action-gh-release@v2 + with: + tag_name: ${{ needs.prepare.outputs.tag_name }} + files: dist_staging/backends/lean/.lake/aeneas-*.tar.gz + - name: Re-package Tarball run: | set -eo pipefail diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean index 76ac61fc8..f45e51c97 100644 --- a/backends/lean/lakefile.lean +++ b/backends/lean/lakefile.lean @@ -5,7 +5,8 @@ open Lake DSL require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.30.0-rc2" -package «aeneas» {} +package «aeneas» where + preferReleaseBuild := true @[default_target] lean_lib «Aeneas» {} diff --git a/scripts/ci-precompile-lean.sh b/scripts/ci-precompile-lean.sh index 36287bb77..d226565e7 100755 --- a/scripts/ci-precompile-lean.sh +++ b/scripts/ci-precompile-lean.sh @@ -13,5 +13,9 @@ fi # required for plugin loading. CI="" lake build +# Pack prebuilt oleans into an archive for Lake's automatic olean download. +# Users who pin to a release tag get these instead of compiling from source. +lake pack + # Delete heavy dependency sources to keep the release archive small. rm -rf .lake/packages diff --git a/src/Config.ml b/src/Config.ml index cb919aeb1..b45ea874a 100644 --- a/src/Config.ml +++ b/src/Config.ml @@ -598,3 +598,14 @@ let max_recdepth = ref 2048 (** If [false], evaluate [drop(p)] as [p := bottom]. Otherwise, evaluate it as a no-op (which means that we do not borrow-check the drops). *) let drop_as_no_op = ref true + +(** For Lean only: disable the Rust core library overrides defined in + [ExtractBuiltinLean.ml]. + + With this flag, references to items such as [core::clone::Clone<[T; N]>] are + extracted using the standard name-mangling scheme rather than the hand-tuned + names like [core.array.CloneArray.clone], and the associated shape overrides + ([keep_params], [can_fail], etc.) are ignored. This is useful when + extracting against a separate Lean library that mirrors the Rust core API + under the standard names. *) +let core_models_lib = ref false diff --git a/src/Main.ml b/src/Main.ml index 8073dba6b..eeacb0a75 100644 --- a/src/Main.ml +++ b/src/Main.ml @@ -211,6 +211,14 @@ let () = collisions with field projectors. Example: the `len` method in `impl \ Struct { fn len(&self) -> usize { ... } }` would be named \ `Struct.impl.len`." ); + ( "-core-models-lib", + Arg.Set core_models_lib, + " For Lean: disable the Rust core library overrides from \ + ExtractBuiltinLean.ml. Items like the `Clone` impl for arrays are \ + extracted using the standard name-mangling scheme rather than \ + hand-tuned names such as `core.array.CloneArray.clone`, and the \ + associated shape overrides (keep_params, can_fail, etc.) are ignored." + ); ( "-all-computable", Arg.Set all_computable, " For Lean: do not insert `noncomputable section` at the top of the \ @@ -457,6 +465,9 @@ let () = if !lean_gen_lakefile && not (backend () = Lean) then fail_with_error "The -lean-default-lakefile option is valid only for the Lean backend"; + if !core_models_lib && not (backend () = Lean) then + fail_with_error + "The -core-models-lib option is valid only for the Lean backend"; if !set_max_heartbeats && not (backend () = Lean) then fail_with_error "The -max-heartbeats option is valid only for the Lean backend"; diff --git a/src/PrePasses.ml b/src/PrePasses.ml index 592098ae1..1bd43e3e2 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -1209,6 +1209,135 @@ let filter_marker_traits (crate : crate) : crate = in visitor#visit_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 + let pat = NameMatcher.parse_pattern "core::cmp::Eq" in + let match_config = + { + NameMatcher.map_vars_to_vars = true; + match_with_trait_decl_refs = Config.match_patterns_with_trait_decl_refs; + } + in + let eq_id = + TraitDeclId.Map.fold + (fun id (decl : trait_decl) acc -> + if + acc = None + && NameMatcher.match_name mctx match_config pat decl.item_meta.name + then Some id + else acc) + crate.trait_decls None + in + match eq_id with + | None -> crate + | Some eq_id -> + (* 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 List.mem m.binder_value.name method_names then + TraitMethodId.Set.add mid acc + else acc) + eq_decl.methods TraitMethodId.Set.empty + in + if TraitMethodId.Set.is_empty filtered_method_ids then crate + else + let trait_decls = + TraitDeclId.Map.update eq_id + (function + | None -> None + | Some (d : trait_decl) -> + Some + { + d with + methods = + TraitMethodId.Map.filter + (fun mid _ -> + not + (TraitMethodId.Set.mem mid filtered_method_ids)) + d.methods; + }) + crate.trait_decls + in + (* Collect fun_decl_ids backing the filtered methods of every [Eq] + trait impl, and strip those methods from the impl's method map. *) + let dropped_fun_decl_ids = ref FunDeclId.Set.empty in + let trait_impls = + TraitImplId.Map.map + (fun (impl : trait_impl) -> + if impl.impl_trait.id <> eq_id then impl + else + let methods = + TraitMethodId.Map.filter + (fun mid (m : fun_decl_ref binder) -> + if TraitMethodId.Set.mem mid filtered_method_ids then begin + dropped_fun_decl_ids := + FunDeclId.Set.add m.binder_value.id + !dropped_fun_decl_ids; + false + end + else true) + impl.methods + in + { impl with methods }) + crate.trait_impls + in + let fun_decls = + FunDeclId.Map.filter + (fun id _ -> not (FunDeclId.Set.mem id !dropped_fun_decl_ids)) + crate.fun_decls + in + let declarations = + List.filter_map + (fun (g : declaration_group) -> + match g with + | FunGroup (NonRecGroup id) -> + if FunDeclId.Set.mem id !dropped_fun_decl_ids then None + else Some g + | FunGroup (RecGroup ids) -> + let ids = + List.filter + (fun id -> + not (FunDeclId.Set.mem id !dropped_fun_decl_ids)) + ids + in + if ids = [] then None else Some (FunGroup (RecGroup ids)) + | MixedGroup g -> ( + let is_dropped (id : item_id) = + match id with + | IdFun id -> FunDeclId.Set.mem id !dropped_fun_decl_ids + | _ -> false + in + match g with + | NonRecGroup id -> + if is_dropped id then None else Some (MixedGroup g) + | RecGroup ids -> + let ids = + List.filter (fun id -> not (is_dropped id)) ids + in + if ids = [] then None + else Some (MixedGroup (RecGroup ids))) + | _ -> Some g) + crate.declarations + in + { crate with trait_decls; trait_impls; fun_decls; declarations } + (* Remove the type aliases from the type declarations and declaration groups *) let filter_type_aliases (crate : crate) : crate = let type_decl_is_alias (ty : type_decl) = @@ -2304,6 +2433,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_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/Translate.ml b/src/Translate.ml index de8040141..a4f6565f9 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -13,6 +13,12 @@ open Parallel (** The local logger *) let log = TranslateCore.log +(** When [-core-models-lib] is on, non-local items are skipped from the main + extracted files (the user is expected to provide them via a separate Lean + library, e.g. [core_models] for [core::*] items). *) +let skip_for_core_models_lib (is_local : bool) : bool = + !Config.core_models_lib && not is_local + (** The result of running the symbolic interpreter on a function: - the list of symbolic values used for the input values - the generated symbolic AST *) @@ -758,6 +764,12 @@ let export_types_group (fmt : Format.formatter) (config : gen_config) if List.exists (fun b -> b) builtin then (* Sanity check *) assert (List.for_all (fun b -> b) builtin) + else if + List.exists + (fun (d : Pure.type_decl) -> + skip_for_core_models_lib d.item_meta.is_local) + defs + then () else if List.exists dont_extract defs then (* Check if we have to ignore declarations *) (* Sanity check *) @@ -838,6 +850,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) && match_name_find_opt ctx.trans_ctx global.item_meta.name (builtin_globals_map ()) = None + && not (skip_for_core_models_lib global.item_meta.is_local) in if extract then ( (* We don't wrap global declaration groups between calls to functions @@ -967,6 +980,12 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config) if List.exists (fun b -> b) builtin then (* Sanity check *) assert (List.for_all (fun b -> b) builtin) + else if + List.exists + (fun (trans : pure_fun_translation) -> + skip_for_core_models_lib trans.f.item_meta.is_local) + pure_ls + then () else (* Utility to check a function has a decrease clause *) let has_decreases_clause (def : Pure.fun_decl) : bool = @@ -1070,7 +1089,10 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config) (TraitDeclId.Map.find_opt trait_decl_id ctx.trans_trait_decls) in (* Check if the trait declaration is builtin, in which case we ignore it *) - if not (trait_decl_is_builtin ctx trait_decl_id) then ( + if + (not (trait_decl_is_builtin ctx trait_decl_id)) + && not (skip_for_core_models_lib trait_decl.item_meta.is_local) + then ( let ctx = { ctx with trait_decl_id = Some trait_decl.def_id } in if extract_decl then ( Extract.extract_trait_decl ctx fmt trait_decl; @@ -1088,7 +1110,10 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config) [%silent_unwrap_opt_span] None (TraitImplId.Map.find_opt trait_impl_id ctx.trans_trait_impls) in - if not (trait_impl_is_builtin ctx trait_impl_id) then ( + if + (not (trait_impl_is_builtin ctx trait_impl_id)) + && not (skip_for_core_models_lib trait_impl.item_meta.is_local) + then ( Extract.extract_trait_impl ctx fmt ~is_rec trait_impl; EmitJson.record_trait_impl_if_enabled ctx trait_impl) @@ -1343,12 +1368,19 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) Printf.fprintf out "Module %s.\n" fi.module_name | Lean -> Printf.fprintf out "import Aeneas\n"; + if !Config.core_models_lib then Printf.fprintf out "import CoreModels\n"; (* Add the custom imports *) List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_imports; (* Add the custom includes *) List.iter (fun m -> Printf.fprintf out "import %s\n" m) fi.custom_includes; (* Always open the Primitives namespace *) - Printf.fprintf out "open Aeneas Aeneas.Std Result ControlFlow Error\n"; + if !Config.core_models_lib then begin + Printf.fprintf out "open CoreModels Aeneas\n"; + Printf.fprintf out "open Aeneas.Std hiding namespace core alloc\n"; + Printf.fprintf out "open Result ControlFlow Error\n" + end + else + Printf.fprintf out "open Aeneas Aeneas.Std Result ControlFlow Error\n"; (* It happens that we generate duplicated namespaces, like `betree.betree`. We deactivate the linter for this, because otherwise it leads to too much noise. *) diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 52a676c11..45e16ef97 100644 --- a/src/extract/Extract.ml +++ b/src/extract/Extract.ml @@ -23,11 +23,188 @@ let generic_args_to_string (ctx : extraction_ctx) = let texpr_to_string (ctx : extraction_ctx) = PrintPure.texpr_to_string (extraction_ctx_to_fmt_env ctx) false "" " " +(** Under [-core-models-lib], detect type parameters and trait clauses left + dangling by Charon's [hide_allocator] pass (which strips the [A] parameter + from [Vec], [Box], etc. and removes the [core::alloc::Allocator] trait + declaration but leaves the function-level [A] and [A: Clone]-style clauses + in place). + + A type parameter is dropped iff it is unused in the function's inputs, + output, and predicates. A trait clause is dropped iff every type variable it + references is itself being dropped (i.e., it is "orphan" — only constraining + dropped parameters). The "used" set is saturated through trait clauses so + that a parameter pulled in by a kept clause is itself kept. + + [scan]: caller-supplied closure that gets invoked with a visitor and may + visit any extra structures (e.g. a trait_impl's [impl_trait] / + [parent_trait_refs]) so their type variables also count as used. Pass a + no-op closure when there is nothing extra to scan. + + [extra_trait_decl_refs] / [extra_trait_refs]: caller-supplied additional + things to scan for used type variables. Trait impls in particular have no + function-style inputs; instead, the type variables they bind appear in + [impl_trait] and the parent trait refs, which the caller passes here. + + Returns [None] if nothing needs filtering. *) +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] 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 (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 + List.iter (body_visitor#visit_ty ()) inputs; + (match output with + | Some o -> body_visitor#visit_ty () o + | None -> ()); + body_visitor#visit_predicates () preds; + List.iter (body_visitor#visit_trait_decl_ref ()) extra_trait_decl_refs; + List.iter (body_visitor#visit_trait_ref ()) extra_trait_refs; + let clause_tvars (c : Pure.trait_param) : Pure.TypeVarId.Set.t = + let s = ref Pure.TypeVarId.Set.empty in + let v = + 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 + v#visit_trait_param () c; + !s + in + let rec saturate () = + let changed = ref false in + List.iter + (fun (c : Pure.trait_param) -> + let tvars = clause_tvars c in + if + Pure.TypeVarId.Set.exists + (fun id -> Pure.TypeVarId.Set.mem id !used) + tvars + then + Pure.TypeVarId.Set.iter + (fun id -> + if not (Pure.TypeVarId.Set.mem id !used) then begin + used := Pure.TypeVarId.Set.add id !used; + changed := true + end) + tvars) + trait_clauses; + if !changed then saturate () + in + saturate (); + let unused_set = + List.fold_left + (fun acc (p : Pure.type_param) -> + if Pure.TypeVarId.Set.mem p.index !used then acc + else Pure.TypeVarId.Set.add p.index acc) + Pure.TypeVarId.Set.empty type_params + in + let is_orphan_clause (c : Pure.trait_param) : bool = + let tvars = clause_tvars c in + (not (Pure.TypeVarId.Set.is_empty tvars)) + && Pure.TypeVarId.Set.for_all + (fun id -> Pure.TypeVarId.Set.mem id unused_set) + tvars + in + let any_orphan = List.exists is_orphan_clause trait_clauses in + let any_unused = not (Pure.TypeVarId.Set.is_empty unused_set) in + if (not any_orphan) && not any_unused then None + else + let keep_params = + List.map + (fun (p : Pure.type_param) -> + not (Pure.TypeVarId.Set.mem p.index unused_set)) + type_params + in + let keep_trait_clauses = + List.map (fun c -> not (is_orphan_clause c)) trait_clauses + in + Some (keep_params, keep_trait_clauses) + (** Compute the names for all the pure functions generated from a rust function. *) let extract_fun_decl_register_names (ctx : extraction_ctx) (has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) : extraction_ctx = + let maybe_register_allocator_filter (ctx : extraction_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 ~type_args_filter sg.generics sg.inputs + (Some sg.output) sg.preds + with + | None -> ctx + | Some (keep_params, keep_trait_clauses) -> + let ctx = + if FunDeclId.Map.mem def.f.def_id ctx.funs_filter_type_args_map then + ctx + else + { + ctx with + funs_filter_type_args_map = + FunDeclId.Map.add def.f.def_id keep_params + ctx.funs_filter_type_args_map; + } + in + if FunDeclId.Map.mem def.f.def_id ctx.funs_filter_trait_clauses_map + then ctx + else + { + ctx with + funs_filter_trait_clauses_map = + FunDeclId.Map.add def.f.def_id keep_trait_clauses + ctx.funs_filter_trait_clauses_map; + } + in (* Use the builtin names if necessary *) match def.f.builtin_info with | Some info -> @@ -54,11 +231,13 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) } | _ -> ctx in + let ctx = maybe_register_allocator_filter ctx in let f = def.f in let fun_id = (Pure.FunId (FRegular f.def_id), f.loop_id) in ctx_add f.item_meta.span (FunId (FromLlbc fun_id)) info.extract_name ctx | None -> (* Not builtin *) + let ctx = maybe_register_allocator_filter ctx in (* Register the decrease clauses, if necessary *) let register_decreases ctx def = if has_decreases_clause def then @@ -278,7 +457,7 @@ let fun_builtin_filter_types_trait_clauses (ty_to_string : 'a -> string) match FunDeclId.Map.find_opt id ctx.funs_filter_trait_clauses_map with | None -> Result.Ok clauses | Some filter -> - if List.length filter <> List.length types then ( + if List.length filter <> List.length clauses then ( let decl = [%silent_unwrap_opt_span] None (ctx_lookup_fun_decl_info ctx id) in @@ -2969,6 +3148,52 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) in (ctx, Some builtin_info) in + (* Under [-core-models-lib], drop dangling allocator-shaped type params and + orphan trait clauses (same heuristic as for functions). Trait impls have + no "inputs"; the type variables they bind show up in [impl_trait], its + parent trait refs, the associated types it implements, and so on. We + pass all of those as extra scan context so they don't get wrongly + classified as unused. *) + let 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 ~type_args_filter + trait_impl.generics assoc_tys None trait_impl.preds + with + | None -> ctx + | Some (keep_params, keep_trait_clauses) -> + let ctx = + if + TraitImplId.Map.mem trait_impl.def_id + ctx.trait_impls_filter_type_args_map + then ctx + else + { + ctx with + trait_impls_filter_type_args_map = + TraitImplId.Map.add trait_impl.def_id keep_params + ctx.trait_impls_filter_type_args_map; + } + in + if + TraitImplId.Map.mem trait_impl.def_id + ctx.trait_impls_filter_trait_clauses_map + then ctx + else + { + ctx with + trait_impls_filter_trait_clauses_map = + TraitImplId.Map.add trait_impl.def_id keep_trait_clauses + ctx.trait_impls_filter_trait_clauses_map; + } + in (* Everything is taken care of by {!extract_trait_decl_register_names} *but* the name of the implementation itself *) diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml index 8de01388d..a036d28d6 100644 --- a/src/extract/ExtractBase.ml +++ b/src/extract/ExtractBase.ml @@ -1920,8 +1920,27 @@ let ctx_compute_trait_impl_name_raw (ctx : extraction_ctx) in [%ldebug "trait_name: " ^ trait_name]; - (* Put together *) - let name = flatten_name [ self_name; "Insts"; trait_name ] in + (* Put together. Under [-core-models-lib], non-local trait impls + get prefixed with the Rust crate they originate from (matching + the convention used for non-impl items, where the crate is the + leading namespace component). For local impls, the local crate + is stripped, as elsewhere. We also skip the prefix if the self + type's name already starts with that crate (the ADT case), + which would otherwise yield a duplicated crate component. *) + let name_parts = [ self_name; "Insts"; trait_name ] in + let name_parts = + if !core_models_lib && not trait_impl.item_meta.is_local then + match trait_impl.item_meta.name with + | PeIdent (crate, _) :: _ -> + let already_prefixed = + self_name = crate + || String.starts_with ~prefix:(crate ^ ".") self_name + in + if already_prefixed then name_parts else crate :: name_parts + | _ -> name_parts + else name_parts + in + let name = flatten_name name_parts in [%ldebug "Final name: " ^ name]; name) | Some name -> name diff --git a/src/extract/ExtractBuiltin.ml b/src/extract/ExtractBuiltin.ml index 6e28b984b..f76049e16 100644 --- a/src/extract/ExtractBuiltin.ml +++ b/src/extract/ExtractBuiltin.ml @@ -43,7 +43,7 @@ let builtin_globals () : Pure.builtin_global_info list = unit_metadata; ]; ] - @ mk_lean_only lean_builtin_consts) + @ mk_lean_only_unless_core_models_lib lean_builtin_consts) let mk_builtin_globals_map () : Pure.builtin_global_info NameMatcherMap.t = NameMatcherMap.of_list @@ -170,7 +170,7 @@ let builtin_types () : Pure.builtin_type_info list = ]); }; ]) - @ mk_lean_only lean_builtin_types + @ mk_lean_only_unless_core_models_lib lean_builtin_types let mk_builtin_types_map () = NameMatcherMap.of_list @@ -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 @@ -324,7 +345,7 @@ let builtin_trait_decls_info () = (* Copy *) mk_trait "core::marker::Copy" ~parent_clauses:[ "cloneInst" ] (); ] - @ mk_lean_only lean_builtin_trait_decls + @ mk_lean_only_unless_core_models_lib lean_builtin_trait_decls let mk_builtin_trait_decls_map () = NameMatcherMap.of_list @@ -420,90 +441,96 @@ let builtin_trait_impls_info () : (pattern * Pure.builtin_trait_impl_info) list fmt "core::clone::Clone" ~extract_name:(Some "core::clone::CloneBool") (); ] - @ mk_lean_only lean_builtin_trait_impls - (* From *) - @ List.map - (fun ty -> - fmt - ("core::convert::From<" ^ ty ^ ", bool>") - ~extract_name: - (Some - ("core.convert.From" - ^ StringUtils.capitalize_first_letter ty - ^ "Bool")) - ()) - all_int_names - (* From *) - @ List.map - (fun (big, small) -> - fmt - ("core::convert::From<" ^ big ^ ", " ^ small ^ ">") - ~extract_name: - (Some - ("core.convert.From" - ^ StringUtils.capitalize_first_letter big - ^ StringUtils.capitalize_first_letter small)) - ()) - int_and_smaller_list - (* Clone *) - @ List.map - (fun ty -> - fmt - ("core::clone::Clone<" ^ ty ^ ">") - ~extract_name: - (Some ("core.clone.Clone" ^ StringUtils.capitalize_first_letter ty)) - ()) - all_int_names - (* Copy *) - @ List.map - (fun ty -> - fmt - ("core::marker::Copy<" ^ ty ^ ">") - ~extract_name: - (Some ("core.marker.Copy" ^ StringUtils.capitalize_first_letter ty)) - ()) - all_int_names - (* PartialEq *) - @ List.map - (fun ty -> - fmt - ("core::cmp::PartialEq<" ^ ty ^ "," ^ ty ^ ">") - ~extract_name: - (Some ("core.cmp.PartialEq" ^ StringUtils.capitalize_first_letter ty)) - ()) - all_int_names - (* Eq *) - @ List.map - (fun ty -> - fmt - ("core::cmp::Eq<" ^ ty ^ ">") - ~extract_name: - (Some ("core.cmp.Eq" ^ StringUtils.capitalize_first_letter ty)) - ()) - all_int_names - (* PartialOrd *) - @ List.map - (fun ty -> - fmt - ("core::cmp::PartialOrd<" ^ ty ^ "," ^ ty ^ ">") - ~extract_name: - (Some - ("core.cmp.PartialOrd" ^ StringUtils.capitalize_first_letter ty)) - ()) - all_int_names - (* Ord *) - @ List.map - (fun ty -> - fmt - ("core::cmp::Ord<" ^ ty ^ ">") - ~extract_name: - (Some ("core.cmp.Ord" ^ StringUtils.capitalize_first_letter ty)) - ()) - all_int_names - (* Default *) - @ List.map - (fun ty -> fmt ("core::default::Default<" ^ ty ^ ">") ()) - all_int_names + @ mk_lean_only_unless_core_models_lib lean_builtin_trait_impls + @ unless_core_models_lib + ((* From *) + List.map + (fun ty -> + fmt + ("core::convert::From<" ^ ty ^ ", bool>") + ~extract_name: + (Some + ("core.convert.From" + ^ StringUtils.capitalize_first_letter ty + ^ "Bool")) + ()) + all_int_names + (* From *) + @ List.map + (fun (big, small) -> + fmt + ("core::convert::From<" ^ big ^ ", " ^ small ^ ">") + ~extract_name: + (Some + ("core.convert.From" + ^ StringUtils.capitalize_first_letter big + ^ StringUtils.capitalize_first_letter small)) + ()) + int_and_smaller_list + (* Clone *) + @ List.map + (fun ty -> + fmt + ("core::clone::Clone<" ^ ty ^ ">") + ~extract_name: + (Some + ("core.clone.Clone" ^ StringUtils.capitalize_first_letter ty)) + ()) + all_int_names + (* Copy *) + @ List.map + (fun ty -> + fmt + ("core::marker::Copy<" ^ ty ^ ">") + ~extract_name: + (Some + ("core.marker.Copy" ^ StringUtils.capitalize_first_letter ty)) + ()) + all_int_names + (* PartialEq *) + @ List.map + (fun ty -> + fmt + ("core::cmp::PartialEq<" ^ ty ^ "," ^ ty ^ ">") + ~extract_name: + (Some + ("core.cmp.PartialEq" + ^ StringUtils.capitalize_first_letter ty)) + ()) + all_int_names + (* Eq *) + @ List.map + (fun ty -> + fmt + ("core::cmp::Eq<" ^ ty ^ ">") + ~extract_name: + (Some ("core.cmp.Eq" ^ StringUtils.capitalize_first_letter ty)) + ()) + all_int_names + (* PartialOrd *) + @ List.map + (fun ty -> + fmt + ("core::cmp::PartialOrd<" ^ ty ^ "," ^ ty ^ ">") + ~extract_name: + (Some + ("core.cmp.PartialOrd" + ^ StringUtils.capitalize_first_letter ty)) + ()) + all_int_names + (* Ord *) + @ List.map + (fun ty -> + fmt + ("core::cmp::Ord<" ^ ty ^ ">") + ~extract_name: + (Some ("core.cmp.Ord" ^ StringUtils.capitalize_first_letter ty)) + ()) + all_int_names + (* Default *) + @ List.map + (fun ty -> fmt ("core::default::Default<" ^ ty ^ ">") ()) + all_int_names) let mk_builtin_trait_impls_map () = let m = NameMatcherMap.of_list (builtin_trait_impls_info ()) in @@ -583,81 +610,89 @@ let mk_builtin_funs () : (pattern * Pure.builtin_fun_info) list = funs) all_int_names) in - List.flatten - (List.map - (fun op -> - mk_scalar_fun - (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op) - (fun ty -> StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op) - ~can_fail:false ()) - [ "add"; "sub"; "mul"; "div"; "rem" ]) - (* From *) - @ mk_scalar_fun - (fun ty -> - "core::convert::num::{core::convert::From<" ^ ty ^ ", bool>}::from") - (fun ty -> - "core.convert.num.From" - ^ StringUtils.capitalize_first_letter ty - ^ "Bool.from") - ~can_fail:false () - (* From *) - @ List.map - (fun (big, small) -> - mk_fun - ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small - ^ ">}::from") - ~extract_name: - (Some - ("core.convert.num.From" - ^ StringUtils.capitalize_first_letter big - ^ StringUtils.capitalize_first_letter small - ^ ".from")) - ~can_fail:false ()) - int_and_smaller_list - (* Leading zeros *) - @ mk_scalar_fun - (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros") - (fun ty -> - "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros") - ~can_fail:false () - (* to_le_bytes *) - @ mk_scalar_fun - (fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes") - (fun ty -> - "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes") - ~can_fail:false () - (* to_be_bytes *) - @ mk_scalar_fun - (fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes") - (fun ty -> - "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes") - ~can_fail:false () - (* from_le_bytes *) - @ mk_scalar_fun - (fun ty -> "core::num::{" ^ ty ^ "}::from_le_bytes") - (fun ty -> - "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".from_le_bytes") - ~can_fail:false () - (* from_be_bytes *) - @ mk_scalar_fun - (fun ty -> "core::num::{" ^ ty ^ "}::from_be_bytes") - (fun ty -> - "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".from_be_bytes") - ~can_fail:false () - (* Clone *) - @ mk_funs - (fun fn -> "core::clone::impls::{core::clone::Clone}::" ^ fn) - (fun fn -> "core.clone.impls.CloneBool." ^ fn) - [ (false, "clone"); (false, "clone_from") ] - (* Clone *) - @ mk_scalar_funs - (fun ty fn -> - "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::" ^ fn) - (fun ty fn -> - "core.clone.impls.Clone" - ^ StringUtils.capitalize_first_letter ty - ^ "." ^ fn) - [ (false, "clone"); (false, "clone_from") ] + unless_core_models_lib + (List.flatten + (List.map + (fun op -> + mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op) + (fun ty -> + StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op) + ~can_fail:false ()) + [ "add"; "sub"; "mul"; "div"; "rem" ]) + (* From *) + @ mk_scalar_fun + (fun ty -> + "core::convert::num::{core::convert::From<" ^ ty ^ ", bool>}::from") + (fun ty -> + "core.convert.num.From" + ^ StringUtils.capitalize_first_letter ty + ^ "Bool.from") + ~can_fail:false () + (* From *) + @ List.map + (fun (big, small) -> + mk_fun + ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small + ^ ">}::from") + ~extract_name: + (Some + ("core.convert.num.From" + ^ StringUtils.capitalize_first_letter big + ^ StringUtils.capitalize_first_letter small + ^ ".from")) + ~can_fail:false ()) + int_and_smaller_list + (* Leading zeros *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros") + (fun ty -> + "core.num." + ^ StringUtils.capitalize_first_letter ty + ^ ".leading_zeros") + ~can_fail:false () + (* to_le_bytes *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes") + (fun ty -> + "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes") + ~can_fail:false () + (* to_be_bytes *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes") + (fun ty -> + "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes") + ~can_fail:false () + (* from_le_bytes *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::from_le_bytes") + (fun ty -> + "core.num." + ^ StringUtils.capitalize_first_letter ty + ^ ".from_le_bytes") + ~can_fail:false () + (* from_be_bytes *) + @ mk_scalar_fun + (fun ty -> "core::num::{" ^ ty ^ "}::from_be_bytes") + (fun ty -> + "core.num." + ^ StringUtils.capitalize_first_letter ty + ^ ".from_be_bytes") + ~can_fail:false () + (* Clone *) + @ mk_funs + (fun fn -> "core::clone::impls::{core::clone::Clone}::" ^ fn) + (fun fn -> "core.clone.impls.CloneBool." ^ fn) + [ (false, "clone"); (false, "clone_from") ] + (* Clone *) + @ mk_scalar_funs + (fun ty fn -> + "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::" ^ fn) + (fun ty fn -> + "core.clone.impls.Clone" + ^ StringUtils.capitalize_first_letter ty + ^ "." ^ fn) + [ (false, "clone"); (false, "clone_from") ]) (* Definitions not for Lean *) @ mk_not_lean [ @@ -795,7 +830,7 @@ let mk_builtin_funs () : (pattern * Pure.builtin_fun_info) list = (); ] (* Lean-only definitions *) - @ mk_lean_only + @ mk_lean_only_unless_core_models_lib ((* PartialEq, Eq, PartialOrd, Ord *) mk_scalar_funs (fun ty fun_name -> diff --git a/src/extract/ExtractBuiltinCore.ml b/src/extract/ExtractBuiltinCore.ml index 60961bddc..ecc9b92d9 100644 --- a/src/extract/ExtractBuiltinCore.ml +++ b/src/extract/ExtractBuiltinCore.ml @@ -39,6 +39,26 @@ let mk_lean_only (funs : 'a list) : 'a list = | Lean -> funs | _ -> [] +(** Like [mk_lean_only], but additionally returns [[]] when the + [-core-models-lib] CLI option is on. Used to disable the Rust core library + overrides defined in [ExtractBuiltinLean.ml] (both the hand-tuned extract + names and the associated shape overrides such as [keep_params] and + [can_fail]). *) +let mk_lean_only_unless_core_models_lib (funs : 'a list) : 'a list = + match backend () with + | Lean -> if !core_models_lib then [] else funs + | _ -> [] + +(** Returns [[]] when the [-core-models-lib] CLI option is on, otherwise returns + the input list unchanged. Used to disable Rust core library overrides that + produce hand-tuned, Lean-style flat names (e.g. + [core.convert.num.FromU16U8.from]) and the associated shape overrides (e.g. + [~can_fail:false]) for sections that are otherwise applied to all backends. + The flag is rejected on non-Lean backends, so this only ever affects Lean. +*) +let unless_core_models_lib (funs : 'a list) : 'a list = + if !core_models_lib then [] else funs + let mk_not_lean (funs : 'a list) : 'a list = match backend () with | Lean -> [] diff --git a/src/symbolic/SymbolicToPureTypes.ml b/src/symbolic/SymbolicToPureTypes.ml index 603e5b21f..3c8ec0bb3 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;