diff options
| -rw-r--r-- | charon-pin | 2 | ||||
| -rw-r--r-- | compiler/Extract.ml | 10 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 43 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 6 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 2 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 8 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 2 | ||||
| -rw-r--r-- | compiler/LlbcAstUtils.ml | 7 | ||||
| -rw-r--r-- | compiler/PrePasses.ml | 2 | ||||
| -rw-r--r-- | compiler/Pure.ml | 20 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 1 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/RegionsHierarchy.ml | 5 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 47 | ||||
| -rw-r--r-- | compiler/Translate.ml | 39 | ||||
| -rw-r--r-- | flake.lock | 6 | ||||
| -rw-r--r-- | tests/src/mutually-recursive-traits.lean.out | 12 |
18 files changed, 113 insertions, 105 deletions
@@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -2e74074eaa0528f3203dc1c160ccdba0f44b563a +5c2ae3744ce702d07920d0f536a272aadd396ed9 diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 6c6b7f0e..1fbce7fd 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1258,7 +1258,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) (let name = - if !extract_external_name_patterns && not def.is_local then + if !extract_external_name_patterns && not def.item_meta.is_local then Some def.llbc_name else None in @@ -1433,7 +1433,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) [ comment_pre ^ loop_comment ] in let name = - if !extract_external_name_patterns && not def.is_local then + if !extract_external_name_patterns && not def.item_meta.is_local then Some def.llbc_name else None in @@ -1924,7 +1924,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; let name = - if !extract_external_name_patterns && not global.is_local then + if !extract_external_name_patterns && not global.item_meta.is_local then Some global.llbc_name else None in @@ -2389,7 +2389,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) (let name = - if !extract_external_name_patterns && not decl.is_local then + if !extract_external_name_patterns && not decl.item_meta.is_local then Some decl.llbc_name else None in @@ -2703,7 +2703,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) (let name, generics = - if !extract_external_name_patterns && not impl.is_local then + if !extract_external_name_patterns && not impl.item_meta.is_local then let decl_id = impl.impl_trait.trait_decl_id in let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in let decl_ref = impl.llbc_impl_trait in diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index fb65bd5e..57131dad 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -253,8 +253,9 @@ let empty_names_map : names_map = } (** Small helper to update an LLBC name if the rename attribute has been set *) -let rename_llbc_name (item_meta : Meta.item_meta) (llbc_name : llbc_name) = - match item_meta.rename with +let rename_llbc_name (attr_info : Meta.attr_info) (llbc_name : llbc_name) : + llbc_name = + match attr_info.rename with | Some rename -> let name_prefix = List.tl (List.rev llbc_name) in List.rev (T.PeIdent (rename, Disambiguator.zero) :: name_prefix) @@ -1393,8 +1394,8 @@ let ctx_compute_simple_type_name = ctx_compute_simple_name (** Helper *) let ctx_compute_type_name_no_suffix (ctx : extraction_ctx) - (item_meta : Meta.item_meta) (name : llbc_name) : string = - let name = rename_llbc_name item_meta name in + (item_meta : Types.item_meta) (name : llbc_name) : string = + let name = rename_llbc_name item_meta.attr_info name in flatten_name (ctx_compute_simple_type_name item_meta.span ctx name) (** Provided a basename, compute a type name. @@ -1403,7 +1404,7 @@ let ctx_compute_type_name_no_suffix (ctx : extraction_ctx) for instance field and variant names when we need to add the name of the type as a prefix. *) -let ctx_compute_type_name (item_meta : Meta.item_meta) (ctx : extraction_ctx) +let ctx_compute_type_name (item_meta : Types.item_meta) (ctx : extraction_ctx) (name : llbc_name) = let name = ctx_compute_type_name_no_suffix ctx item_meta name in match backend () with @@ -1424,7 +1425,7 @@ let ctx_compute_type_name (item_meta : Meta.item_meta) (ctx : extraction_ctx) to tuples, meaning generating names by using indices shouldn't be too much of a problem. *) -let ctx_compute_field_name (def : type_decl) (field_meta : Meta.item_meta) +let ctx_compute_field_name (def : type_decl) (field_meta : Meta.attr_info) (ctx : extraction_ctx) (def_name : llbc_name) (field_id : FieldId.id) (field_name : string option) : string = (* If the user did not provide a name, use the field index. *) @@ -1435,7 +1436,7 @@ let ctx_compute_field_name (def : type_decl) (field_meta : Meta.item_meta) let field_name_s = Option.value field_meta.rename ~default:field_name_s in (* Prefix the name with the name of the type, if necessary (some backends don't support field name collisions) *) - let def_name = rename_llbc_name def.item_meta def_name in + let def_name = rename_llbc_name def.item_meta.attr_info def_name in let name = if !Config.record_fields_short_names then if field_name = None then (* TODO: this is a bit ugly *) @@ -1457,7 +1458,7 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl) (variant : variant) : string = (* Replace the name of the variant if the user annotated it with the [rename] attribute. *) let variant = - Option.value variant.item_meta.rename ~default:variant.variant_name + Option.value variant.attr_info.rename ~default:variant.variant_name in match backend () with | FStar | Coq | HOL4 -> @@ -1547,7 +1548,9 @@ let ctx_compute_fun_name (span : Meta.span) (ctx : extraction_ctx) let ctx_compute_trait_decl_name (ctx : extraction_ctx) (trait_decl : trait_decl) : string = - let llbc_name = rename_llbc_name trait_decl.item_meta trait_decl.llbc_name in + let llbc_name = + rename_llbc_name trait_decl.item_meta.attr_info trait_decl.llbc_name + in ctx_compute_type_name trait_decl.item_meta ctx llbc_name let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) @@ -1561,7 +1564,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) Note that if the user provided a [rename] attribute, we simply use that. *) let name = - match trait_impl.item_meta.rename with + match trait_impl.item_meta.attr_info.rename with | None -> let name = let params = trait_impl.llbc_generics in @@ -1569,7 +1572,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) let name = ctx_prepare_name trait_impl.item_meta.span ctx trait_decl.llbc_name in - let name = rename_llbc_name trait_impl.item_meta name in + let name = rename_llbc_name trait_impl.item_meta.attr_info name in trait_name_with_generics_to_simple_name ctx.trans_ctx name params args in flatten_name name @@ -1631,7 +1634,7 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx) let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in let args = clause.clause_generics in trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix - impl_trait_decl.name params args + impl_trait_decl.item_meta.name params args in String.concat "" clause @@ -1814,7 +1817,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx) *) (* The name shouldn't be empty, and its last element should * be an ident *) - let cl = Collections.List.last def.name in + let cl = Collections.List.last def.item_meta.name in name_from_type_ident (TypesUtils.as_ident cl)) | TVar _ -> ( (* TODO: use "t" also for F* *) @@ -2006,7 +2009,7 @@ let ctx_add_generic_params (span : Meta.span) (current_def_name : Types.name) let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = - let name = rename_llbc_name def.item_meta def.llbc_name in + let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in let name = ctx_compute_decreases_proof_name def.item_meta.span ctx def.def_id name def.num_loops def.loop_id @@ -2017,7 +2020,7 @@ let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) : let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx = - let name = rename_llbc_name def.item_meta def.llbc_name in + let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in let name = ctx_compute_termination_measure_name def.item_meta.span ctx def.def_id name def.num_loops def.loop_id @@ -2034,13 +2037,15 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : (* Check if the global corresponds to an assumed global that we should map to a custom definition in our standard library (for instance, happens with "core::num::usize::MAX") *) - match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with + match + match_name_find_opt ctx.trans_ctx def.item_meta.name builtin_globals_map + with | Some name -> (* Yes: register the custom binding *) ctx_add def.item_meta.span decl name ctx | None -> (* Not the case: "standard" registration *) - let name = rename_llbc_name def.item_meta def.name in + let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in let name = ctx_compute_global_name def.item_meta.span ctx name in let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in @@ -2068,7 +2073,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = let item_meta = match def.kind with | TraitItemImpl (_, trait_decl_id, item_name, _) -> ( - if Option.is_some def.item_meta.rename then def.item_meta + if Option.is_some def.item_meta.attr_info.rename then def.item_meta else (* Lookup the declaration. TODO: the trait item impl info should directly give us the id of the method declaration. *) @@ -2099,7 +2104,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = ~default:def.item_meta)) | _ -> def.item_meta in - let llbc_name = rename_llbc_name item_meta def.llbc_name in + let llbc_name = rename_llbc_name item_meta.attr_info def.llbc_name in ctx_compute_fun_name def.item_meta.span ctx llbc_name def.num_loops def.loop_id diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index a242e950..129fdd78 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -782,7 +782,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : FieldId.mapi (fun fid (field : field) -> ( fid, - ctx_compute_field_name def field.item_meta ctx + ctx_compute_field_name def field.attr_info ctx def.llbc_name fid field.field_name )) fields in @@ -1425,8 +1425,8 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) (let name = - if !Config.extract_external_name_patterns && not def.is_local then - Some def.llbc_name + if !Config.extract_external_name_patterns && not def.item_meta.is_local + then Some def.llbc_name else None in extract_comment_with_raw_span ctx fmt diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index e0a86145..d448c173 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -74,7 +74,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) way. *) let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option = let open ExtractBuiltin in - NameMatcherMap.find_opt name_matcher_ctx f.name + NameMatcherMap.find_opt name_matcher_ctx f.item_meta.name (builtin_fun_effects_map ()) in diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 075672fe..afa189e3 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -282,7 +282,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config) (lazy ("evaluate_function_symbolic_synthesize_backward_from_return:" ^ "\n- fname: " - ^ Print.EvalCtx.name_to_string ctx fdef.name + ^ Print.EvalCtx.name_to_string ctx fdef.item_meta.name ^ "\n- back_id: " ^ RegionGroupId.to_string back_id ^ "\n- loop_id: " @@ -526,7 +526,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) let name_to_string () = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) - fdef.name + fdef.item_meta.name in log#ldebug (lazy ("evaluate_function_symbolic: " ^ name_to_string ())); @@ -670,7 +670,7 @@ module Test = struct ("test_unit_function: " ^ Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env decls_ctx) - fdef.name)); + fdef.item_meta.name)); (* Sanity check - *) sanity_check __FILE__ __LINE__ @@ -697,7 +697,7 @@ module Test = struct ("Unit test failed (concrete execution) on: " ^ Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env decls_ctx) - fdef.name) + fdef.item_meta.name) in (* Evaluate the function *) let ctx_resl, _ = eval_function_body config body.body ctx in diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index 1690aa80..c4e37646 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -647,7 +647,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) : ("Attempted to greedily expand a symbolic enumeration with > \ 1 variants (option [greedy_expand_symbolics_with_borrows] \ of [config]): " - ^ name_to_string ctx def.name) + ^ name_to_string ctx def.item_meta.name) | Alias _ | Opaque -> craise __FILE__ __LINE__ span "Attempted to greedily expand an alias or opaque type"); @@ -656,7 +656,7 @@ let greedy_expand_symbolics_with_borrows (config : config) (span : Meta.span) : craise __FILE__ __LINE__ span ("Attempted to greedily expand a recursive definition (option \ [greedy_expand_symbolics_with_borrows] of [config]): " - ^ name_to_string ctx def.name) + ^ name_to_string ctx def.item_meta.name) else expand_symbolic_value_no_branching config span sv None ctx | TAdt ((TTuple | TAssumed TBox), _) | TRef (_, _, _) -> (* Ok *) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 27f503bc..67ac15d9 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1274,7 +1274,7 @@ and eval_transparent_function_call_concrete (config : config) (span : Meta.span) | None -> craise __FILE__ __LINE__ span ("Can't evaluate a call to an opaque function: " - ^ name_to_string ctx def.name) + ^ name_to_string ctx def.item_meta.name) | Some body -> body in (* TODO: we need to normalize the types if we want to correctly support traits *) diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 1053c9ab..e7b85c30 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -46,13 +46,14 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitItemDecl _ -> false | _ -> true) && ((not filter_assumed) - || (not (NameMatcherMap.mem ctx d.name builtin_globals_map)) - && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ()))) + || (not (NameMatcherMap.mem ctx d.item_meta.name builtin_globals_map)) + && not (NameMatcherMap.mem ctx d.item_meta.name (builtin_funs_map ())) + ) in let is_opaque_type (d : type_decl) : bool = d.kind = Opaque && ((not filter_assumed) - || not (NameMatcherMap.mem ctx d.name (builtin_types_map ()))) + || not (NameMatcherMap.mem ctx d.item_meta.name (builtin_types_map ()))) in (* Note that by checking the function bodies we also the globals *) ( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls), diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml index 5cef8b05..6bdf0a01 100644 --- a/compiler/PrePasses.ml +++ b/compiler/PrePasses.ml @@ -482,7 +482,7 @@ let apply_passes (crate : crate) : crate = However, we replace the body of the function, and save an error to report to the user the fact that we will ignore the function body *) let fmt = Print.Crate.crate_to_fmt_env crate in - let name = Print.name_to_string fmt f.name in + let name = Print.name_to_string fmt f.item_meta.name in save_error __FILE__ __LINE__ (Some f.item_meta.span) ("Ignoring the body of '" ^ name ^ "' because of previous error"); { f with body = None } diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 2ff8c272..d273546a 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -355,14 +355,14 @@ and trait_instance_id = type field = { field_name : string option; field_ty : ty; - item_meta : item_meta; + attr_info : attr_info; } [@@deriving show] type variant = { variant_name : string; fields : field list; - item_meta : item_meta; + attr_info : attr_info; } [@@deriving show] @@ -397,7 +397,6 @@ type predicates = { trait_type_constraints : trait_type_constraint list } type type_decl = { def_id : TypeDeclId.id; - is_local : bool; llbc_name : llbc_name; (** The original name coming from the LLBC declaration *) name : string; @@ -405,7 +404,7 @@ type type_decl = { the name used at extraction time will be derived from the llbc_name. *) - item_meta : item_meta; + item_meta : T.item_meta; generics : generic_params; llbc_generics : Types.generic_params; (** We use the LLBC generics to generate "pretty" names, for instance @@ -1097,8 +1096,7 @@ type backend_attributes = { type fun_decl = { def_id : FunDeclId.id; - is_local : bool; - item_meta : item_meta; + item_meta : T.item_meta; kind : item_kind; backend_attributes : backend_attributes; num_loops : int; @@ -1121,9 +1119,9 @@ type fun_decl = { [@@deriving show] type global_decl = { - span : span; def_id : GlobalDeclId.id; - is_local : bool; + span : span; + item_meta : T.item_meta; llbc_name : llbc_name; (** The original LLBC name. *) name : string; (** We use the name only for printing purposes (for debugging): @@ -1142,10 +1140,9 @@ type global_decl = { type trait_decl = { def_id : trait_decl_id; - is_local : bool; llbc_name : llbc_name; name : string; - item_meta : item_meta; + item_meta : T.item_meta; generics : generic_params; llbc_generics : Types.generic_params; (** We use the LLBC generics to generate "pretty" names, for instance @@ -1165,10 +1162,9 @@ type trait_decl = { type trait_impl = { def_id : trait_impl_id; - is_local : bool; llbc_name : llbc_name; name : string; - item_meta : item_meta; + item_meta : T.item_meta; impl_trait : trait_decl_ref; llbc_impl_trait : Types.trait_decl_ref; (** Same remark as for {!field:llbc_generics}. *) diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 543b2bee..dda6a611 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1499,7 +1499,6 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) : let loop_def : fun_decl = { def_id = def.def_id; - is_local = def.is_local; item_meta; kind = def.kind; backend_attributes = def.backend_attributes; diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 5a85628c..d38644c1 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -689,7 +689,6 @@ let trait_decl_get_method (trait_decl : trait_decl) (method_name : string) : let trait_decl_is_empty (trait_decl : trait_decl) : bool = let { def_id = _; - is_local = _; name = _; llbc_name = _; item_meta = _; @@ -711,7 +710,6 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool = let trait_impl_is_empty (trait_impl : trait_impl) : bool = let { def_id = _; - is_local = _; name = _; llbc_name = _; item_meta = _; diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index c608c02e..6c5253b8 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -322,8 +322,9 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) List.map (fun ((fid, d) : FunDeclId.id * fun_decl) -> ( FRegular fid, - (Types.name_to_string env d.name, d.signature, Some d.item_meta.span) - )) + ( Types.name_to_string env d.item_meta.name, + d.signature, + Some d.item_meta.span ) )) (FunDeclId.Map.bindings fun_decls) in let assumed = diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 7aa5c558..13c94bdf 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -542,8 +542,8 @@ let translate_generic_params (span : Meta.span) (generics : T.generic_params) : let translate_field (span : Meta.span) (f : T.field) : field = let field_name = f.field_name in let field_ty = translate_sty span f.field_ty in - let item_meta = f.item_meta in - { field_name; field_ty; item_meta } + let attr_info = f.attr_info in + { field_name; field_ty; attr_info } let translate_fields (span : Meta.span) (fl : T.field list) : field list = List.map (translate_field span) fl @@ -551,8 +551,8 @@ let translate_fields (span : Meta.span) (fl : T.field list) : field list = let translate_variant (span : Meta.span) (v : T.variant) : variant = let variant_name = v.variant_name in let fields = translate_fields span v.fields in - let item_meta = v.item_meta in - { variant_name; fields; item_meta } + let attr_info = v.attr_info in + { variant_name; fields; attr_info } let translate_variants (span : Meta.span) (vl : T.variant list) : variant list = List.map (translate_variant span) vl @@ -583,8 +583,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : ^ "\n")); let env = Print.Contexts.decls_ctx_to_fmt_env ctx in let def_id = def.T.def_id in - let llbc_name = def.name in - let name = Print.Types.name_to_string env def.name in + let llbc_name = def.item_meta.name in + let name = Print.Types.name_to_string env def.item_meta.name in (* Can't translate types with regions for now *) cassert __FILE__ __LINE__ (def.generics.regions = []) @@ -593,11 +593,9 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) : translate_generic_params def.item_meta.span def.generics in let kind = translate_type_decl_kind def.item_meta.span def.T.kind in - let is_local = def.is_local in let item_meta = def.item_meta in { def_id; - is_local; llbc_name; name; item_meta; @@ -1285,7 +1283,8 @@ let translate_fun_sig_from_decl_to_decomposed (decls_ctx : C.decls_ctx) log#ldebug (lazy ("translate_fun_sig_from_decl_to_decomposed:" ^ "\n- name: " - ^ T.show_name fdef.name ^ "\n- sg:\n" ^ show_decomposed_fun_sig sg ^ "\n")); + ^ T.show_name fdef.item_meta.name + ^ "\n- sg:\n" ^ show_decomposed_fun_sig sg ^ "\n")); sg let mk_output_ty_from_effect_info (effect_info : fun_effect_info) (ty : ty) : ty @@ -2184,7 +2183,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let decl = FunDeclId.Map.find fid ctx.fun_ctx.llbc_fun_decls in - match Collections.List.last decl.name with + match Collections.List.last decl.item_meta.name with | PeIdent (s, _) -> s | PeImpl _ -> (* We shouldn't get there *) @@ -2368,7 +2367,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) log#ldebug (lazy ("translate_end_abstraction_synth_input:" ^ "\n- function: " - ^ name_to_string ctx ctx.fun_decl.name + ^ name_to_string ctx ctx.fun_decl.item_meta.name ^ "\n- rg_id: " ^ T.RegionGroupId.to_string rg_id ^ "\n- loop_id: " @@ -3768,12 +3767,12 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = log#ldebug (lazy ("SymbolicToPure.translate_fun_decl: " - ^ name_to_string ctx def.name + ^ name_to_string ctx def.item_meta.name ^ "\n")); (* Translate the declaration *) let def_id = def.def_id in - let llbc_name = def.name in + let llbc_name = def.item_meta.name in let name = name_to_string ctx llbc_name in (* Translate the signature *) let signature = translate_fun_sig_from_decomposed ctx.sg in @@ -3864,7 +3863,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = log#ldebug (lazy ("SymbolicToPure.translate_fun_decl: " - ^ name_to_string ctx def.name + ^ name_to_string ctx def.item_meta.name ^ "\n- inputs: " ^ String.concat ", " (List.map show_var ctx.forward_inputs) ^ "\n- state: " @@ -3894,7 +3893,6 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = let def : fun_decl = { def_id; - is_local = def.is_local; item_meta = def.item_meta; kind = def.kind; backend_attributes; @@ -3921,8 +3919,10 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = try Some (translate_type_decl ctx d) with CFailure (span, _) -> let env = PrintPure.decls_ctx_to_fmt_env ctx in - let name = PrintPure.name_to_string env d.name in - let name_pattern = TranslateCore.name_to_pattern_string ctx d.name in + let name = PrintPure.name_to_string env d.item_meta.name in + let name_pattern = + TranslateCore.name_to_pattern_string ctx d.item_meta.name + in save_error __FILE__ __LINE__ span ("Could not translate type decl '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); @@ -3933,8 +3933,6 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) : trait_decl = let { def_id; - is_local; - name = llbc_name; item_meta; generics = llbc_generics; parent_clauses = llbc_parent_clauses; @@ -3945,6 +3943,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) } : A.trait_decl = trait_decl in + let llbc_name = item_meta.name in let type_infos = ctx.type_ctx.type_infos in let name = Print.Types.name_to_string @@ -3979,7 +3978,6 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) in { def_id; - is_local; llbc_name; name; item_meta; @@ -3998,8 +3996,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) : trait_impl = let { A.def_id; - is_local; - name = llbc_name; item_meta; impl_trait = llbc_impl_trait; generics = llbc_generics; @@ -4011,6 +4007,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) } = trait_impl in + let llbc_name = item_meta.name in let type_infos = ctx.type_ctx.type_infos in let impl_trait = translate_trait_decl_ref trait_impl.item_meta.span @@ -4046,7 +4043,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl) in { def_id; - is_local; llbc_name; name; item_meta; @@ -4067,8 +4063,6 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : let { A.item_meta; def_id; - is_local; - name = llbc_name; generics = llbc_generics; ty; kind; @@ -4076,6 +4070,7 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : } = decl in + let llbc_name = item_meta.name in let name = Print.Types.name_to_string (Print.Contexts.decls_ctx_to_fmt_env ctx) @@ -4088,7 +4083,7 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) : { span = item_meta.span; def_id; - is_local; + item_meta; llbc_name; name; llbc_generics; diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 0474d233..cadf8cbd 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -25,7 +25,8 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : (* Debug *) log#ldebug (lazy - ("translate_function_to_symbolics: " ^ name_to_string trans_ctx fdef.name)); + ("translate_function_to_symbolics: " + ^ name_to_string trans_ctx fdef.item_meta.name)); match fdef.body with | None -> None @@ -47,7 +48,9 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx) pure_fun_translation_no_loops = (* Debug *) log#ldebug - (lazy ("translate_function_to_pure: " ^ name_to_string trans_ctx fdef.name)); + (lazy + ("translate_function_to_pure: " + ^ name_to_string trans_ctx fdef.item_meta.name)); (* Compute the symbolic ASTs, if the function is transparent *) let symbolic_trans = translate_function_to_symbolics trans_ctx fdef in @@ -205,8 +208,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx) Some (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef) with CFailure (span, _) -> - let name = name_to_string trans_ctx fdef.name in - let name_pattern = name_to_pattern_string trans_ctx fdef.name in + let name = name_to_string trans_ctx fdef.item_meta.name in + let name_pattern = name_to_pattern_string trans_ctx fdef.item_meta.name in save_error __FILE__ __LINE__ span ("Could not translate the function '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); @@ -245,8 +248,10 @@ let translate_crate_to_pure (crate : crate) : SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx fdef ) with CFailure (span, _) -> - let name = name_to_string trans_ctx fdef.name in - let name_pattern = name_to_pattern_string trans_ctx fdef.name in + let name = name_to_string trans_ctx fdef.item_meta.name in + let name_pattern = + name_to_pattern_string trans_ctx fdef.item_meta.name + in save_error __FILE__ __LINE__ span ("Could not translate the function signature of '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern @@ -268,8 +273,10 @@ let translate_crate_to_pure (crate : crate) : (fun d -> try Some (SymbolicToPure.translate_trait_decl trans_ctx d) with CFailure (span, _) -> - let name = name_to_string trans_ctx d.name in - let name_pattern = name_to_pattern_string trans_ctx d.name in + let name = name_to_string trans_ctx d.item_meta.name in + let name_pattern = + name_to_pattern_string trans_ctx d.item_meta.name + in save_error __FILE__ __LINE__ span ("Could not translate the trait declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" @@ -284,8 +291,10 @@ let translate_crate_to_pure (crate : crate) : (fun d -> try Some (SymbolicToPure.translate_trait_impl trans_ctx d) with CFailure (span, _) -> - let name = name_to_string trans_ctx d.name in - let name_pattern = name_to_pattern_string trans_ctx d.name in + let name = name_to_string trans_ctx d.item_meta.name in + let name_pattern = + name_to_pattern_string trans_ctx d.item_meta.name + in save_error __FILE__ __LINE__ span ("Could not translate the trait instance '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'" @@ -511,7 +520,9 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let open ExtractBuiltin in let extract = extract - && match_name_find_opt ctx.trans_ctx global.name builtin_globals_map = None + && match_name_find_opt ctx.trans_ctx global.item_meta.name + builtin_globals_map + = None in if extract then (* We don't wrap global declaration groups between calls to functions @@ -522,8 +533,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) let global = try Some (SymbolicToPure.translate_global ctx.trans_ctx global) with CFailure (span, _) -> - let name = name_to_string ctx.trans_ctx global.name in - let name_pattern = name_to_pattern_string ctx.trans_ctx global.name in + let name = name_to_string ctx.trans_ctx global.item_meta.name in + let name_pattern = + name_to_pattern_string ctx.trans_ctx global.item_meta.name + in save_error __FILE__ __LINE__ span ("Could not translate the global declaration '" ^ name ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"); @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1719218135, - "narHash": "sha256-ICbwKLkfAjuIivmruHF6srfn9MBjo/zO+IpLeKtH5d4=", + "lastModified": 1719229989, + "narHash": "sha256-/Eb1xd65HQeZtO7R/XMXA0ibzig7mffOLNGITuG6rVQ=", "owner": "aeneasverif", "repo": "charon", - "rev": "2e74074eaa0528f3203dc1c160ccdba0f44b563a", + "rev": "5c2ae3744ce702d07920d0f536a272aadd396ed9", "type": "github" }, "original": { diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index df80ccc6..bd281a82 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -1,17 +1,17 @@ [[92mInfo[39m ] Imported: tests/llbc/mutually_recursive_traits.llbc -[[91mError[39m] In file Translate.ml, line 813: +[[91mError[39m] In file Translate.ml, line 826: Mutually recursive trait declarations are not supported Uncaught exception: (Failure - "In file Translate.ml, line 813:\ - \nIn file Translate.ml, line 813:\ + "In file Translate.ml, line 826:\ + \nIn file Translate.ml, line 826:\ \nMutually recursive trait declarations are not supported") Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 47, characters 4-76 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 -Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 839, characters 2-52 -Called from Aeneas__Translate.extract_file in file "Translate.ml", line 966, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1515, characters 5-42 +Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 852, characters 2-52 +Called from Aeneas__Translate.extract_file in file "Translate.ml", line 979, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1528, characters 5-42 Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66 |