summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--charon-pin2
-rw-r--r--compiler/Extract.ml10
-rw-r--r--compiler/ExtractBase.ml43
-rw-r--r--compiler/ExtractTypes.ml6
-rw-r--r--compiler/FunsAnalysis.ml2
-rw-r--r--compiler/Interpreter.ml8
-rw-r--r--compiler/InterpreterExpansion.ml4
-rw-r--r--compiler/InterpreterStatements.ml2
-rw-r--r--compiler/LlbcAstUtils.ml7
-rw-r--r--compiler/PrePasses.ml2
-rw-r--r--compiler/Pure.ml20
-rw-r--r--compiler/PureMicroPasses.ml1
-rw-r--r--compiler/PureUtils.ml2
-rw-r--r--compiler/RegionsHierarchy.ml5
-rw-r--r--compiler/SymbolicToPure.ml47
-rw-r--r--compiler/Translate.ml39
-rw-r--r--flake.lock6
-rw-r--r--tests/src/mutually-recursive-traits.lean.out12
18 files changed, 113 insertions, 105 deletions
diff --git a/charon-pin b/charon-pin
index ad45dea7..2621304e 100644
--- a/charon-pin
+++ b/charon-pin
@@ -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 ^ "'");
diff --git a/flake.lock b/flake.lock
index 19263560..73bd300d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -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 @@
[Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
-[Error] In file Translate.ml, line 813:
+[Error] 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