summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore1
-rw-r--r--compiler/ExtractBase.ml9
-rw-r--r--compiler/FunsAnalysis.ml6
-rw-r--r--compiler/Interpreter.ml56
-rw-r--r--compiler/InterpreterStatements.ml12
-rw-r--r--compiler/PrePasses.ml2
-rw-r--r--compiler/RegionsHierarchy.ml2
-rw-r--r--compiler/SymbolicToPure.ml66
-rw-r--r--compiler/Translate.ml6
-rw-r--r--compiler/TypesAnalysis.ml2
-rw-r--r--flake.lock24
11 files changed, 101 insertions, 85 deletions
diff --git a/.gitignore b/.gitignore
index 2d668039..36809c43 100644
--- a/.gitignore
+++ b/.gitignore
@@ -72,7 +72,6 @@ tests/fstar/misc/obj/
nohup.out
.vscode
*#
-*.lock
*.txt
*/.#*
*.smt2
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 656d2f27..8080e08c 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1932,10 +1932,11 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with
| Some name ->
(* Yes: register the custom binding *)
- ctx_add def.meta decl name ctx
+ ctx_add def.item_meta.meta decl name ctx
| None ->
(* Not the case: "standard" registration *)
- let name = ctx_compute_global_name def.meta ctx def.name in
+ let name = ctx_compute_global_name def.item_meta.meta ctx def.name in
+
let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
(* If this is a provided constant (i.e., the default value for a constant
in a trait declaration) we add a suffix. Otherwise there is a clash
@@ -1944,8 +1945,8 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
let suffix =
match def.kind with TraitItemProvided _ -> "_default" | _ -> ""
in
- let ctx = ctx_add def.meta decl (name ^ suffix) ctx in
- let ctx = ctx_add def.meta body (name ^ suffix ^ "_body") ctx in
+ let ctx = ctx_add def.item_meta.meta decl (name ^ suffix) ctx in
+ let ctx = ctx_add def.item_meta.meta body (name ^ suffix ^ "_body") ctx in
ctx
let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index f194d4e5..d98efc8d 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -147,7 +147,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
(* Sanity check: global bodies don't contain stateful calls *)
cassert __FILE__ __LINE__
((not f.is_global_decl_body) || not !stateful)
- f.meta "Global definition containing a stateful call in its body";
+ f.item_meta.meta "Global definition containing a stateful call in its body";
let builtin_info = get_builtin_info f in
let has_builtin_info = builtin_info <> None in
group_has_builtin_info := !group_has_builtin_info || has_builtin_info;
@@ -171,11 +171,11 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in
cassert __FILE__ __LINE__
((not is_global_decl_body) || List.length d = 1)
- (List.hd d).meta
+ (List.hd d).item_meta.meta
"This global definition is in a group of mutually recursive definitions";
cassert __FILE__ __LINE__
((not !group_has_builtin_info) || List.length d = 1)
- (List.hd d).meta
+ (List.hd d).item_meta.meta
"This builtin function belongs to a group of mutually recursive \
definitions";
(* We ignore on purpose functions that cannot fail and consider they *can*
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 769e3144..d9af063e 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -196,12 +196,12 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
(List.for_all
(fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
(sg.output :: sg.inputs))
- fdef.meta "Nested borrows are not supported yet";
+ fdef.item_meta.meta "Nested borrows are not supported yet";
cassert __FILE__ __LINE__
(List.for_all
(fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
(sg.output :: sg.inputs))
- fdef.meta "ADTs containing borrows are not supported yet";
+ fdef.item_meta.meta "ADTs containing borrows are not supported yet";
(* Create the context *)
let regions_hierarchy =
@@ -211,23 +211,23 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
in
let ctx =
- initialize_eval_ctx fdef.meta ctx region_groups sg.generics.types
+ initialize_eval_ctx fdef.item_meta.meta ctx region_groups sg.generics.types
sg.generics.const_generics
in
(* Instantiate the signature. This updates the context because we compute
at the same time the normalization map for the associated types.
*)
let ctx, inst_sg =
- symbolic_instantiate_fun_sig fdef.meta ctx fdef.signature regions_hierarchy
+ symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature regions_hierarchy
fdef.kind
in
(* Create fresh symbolic values for the inputs *)
let input_svs =
- List.map (fun ty -> mk_fresh_symbolic_value fdef.meta ty) inst_sg.inputs
+ List.map (fun ty -> mk_fresh_symbolic_value fdef.item_meta.meta ty) inst_sg.inputs
in
(* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
let call_id = fresh_fun_call_id () in
- sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.meta;
+ sanity_check __FILE__ __LINE__ (call_id = FunCallId.zero) fdef.item_meta.meta;
let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
eval_ctx * typed_avalue list =
(* Project over the values - we use *loan* projectors, as explained above *)
@@ -249,14 +249,14 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
Collections.List.split_at (List.tl body.locals) body.arg_count
in
(* Push the return variable (initialized with ⊥) *)
- let ctx = ctx_push_uninitialized_var fdef.meta ctx ret_var in
+ let ctx = ctx_push_uninitialized_var fdef.item_meta.meta ctx ret_var in
(* Push the input variables (initialized with symbolic values) *)
let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
let ctx =
- ctx_push_vars fdef.meta ctx (List.combine input_vars input_values)
+ ctx_push_vars fdef.item_meta.meta ctx (List.combine input_vars input_values)
in
(* Push the remaining local variables (initialized with ⊥) *)
- let ctx = ctx_push_uninitialized_vars fdef.meta ctx local_vars in
+ let ctx = ctx_push_uninitialized_vars fdef.item_meta.meta ctx local_vars in
(* Return *)
(ctx, input_svs, inst_sg)
@@ -290,7 +290,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
^ "\n- inside_loop: "
^ Print.bool_to_string inside_loop
^ "\n- ctx:\n"
- ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.meta) ctx));
+ ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.item_meta.meta) ctx));
(* We need to instantiate the function signature - to retrieve
* the return type. Note that it is important to re-generate
* an instantiation of the signature, so that we use fresh
@@ -299,13 +299,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
in
let _, ret_inst_sg =
- symbolic_instantiate_fun_sig fdef.meta ctx fdef.signature regions_hierarchy
+ symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature regions_hierarchy
fdef.kind
in
let ret_rty = ret_inst_sg.output in
(* Move the return value out of the return variable *)
let pop_return_value = is_regular_return in
- let cf_pop_frame = pop_frame config fdef.meta pop_return_value in
+ let cf_pop_frame = pop_frame config fdef.item_meta.meta pop_return_value in
(* We need to find the parents regions/abstractions of the region we
* will end - this will allow us to, first, mark the other return
@@ -333,7 +333,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
eval_ctx * typed_avalue list =
let ctx, avalue =
- apply_proj_borrows_on_input_value config fdef.meta ctx abs.regions
+ apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx abs.regions
abs.ancestors_regions ret_value ret_rty
in
(ctx, [ avalue ])
@@ -349,7 +349,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
let region_can_end rid =
RegionGroupId.Set.mem rid parent_and_current_rgs
in
- sanity_check __FILE__ __LINE__ (region_can_end back_id) fdef.meta;
+ sanity_check __FILE__ __LINE__ (region_can_end back_id) fdef.item_meta.meta;
let ctx =
create_push_abstractions_from_abs_region_groups
(fun rg_id -> SynthRet rg_id)
@@ -439,7 +439,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
sanity_check __FILE__ __LINE__
(if Option.is_some loop_id then loop_id = Some loop_id'
else true)
- fdef.meta;
+ fdef.item_meta.meta;
(* Loop abstractions *)
let rg_id' = Option.get rg_id' in
if rg_id' = back_id && inside_loop then
@@ -448,7 +448,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
| Loop (loop_id', _, LoopCall) ->
(* We can end all the loop call abstractions *)
sanity_check __FILE__ __LINE__ (loop_id = Some loop_id')
- fdef.meta;
+ fdef.item_meta.meta;
{ abs with can_end = true }
| SynthInput rg_id' ->
if rg_id' = back_id && end_fun_synth_input then
@@ -468,7 +468,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
let target_abs_ids = List.append parent_input_abs_ids current_abs_id in
let cf_end_target_abs cf =
List.fold_left
- (fun cf id -> end_abstraction config fdef.meta id cf)
+ (fun cf id -> end_abstraction config fdef.item_meta.meta id cf)
cf target_abs_ids
in
(* Generate the Return node *)
@@ -534,7 +534,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
let fwd_e =
(* Pop the frame and retrieve the returned value at the same time*)
let pop_return_value = true in
- let cf_pop = pop_frame config fdef.meta pop_return_value in
+ let cf_pop = pop_frame config fdef.item_meta.meta pop_return_value in
(* Generate the Return node *)
let cf_return ret_value : m_fun =
fun ctx -> Some (SA.Return (ctx, ret_value))
@@ -551,7 +551,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
match res with
| Return -> None
| LoopReturn loop_id -> Some loop_id
- | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable"
in
let is_regular_return = true in
let inside_loop = Option.is_some loop_id in
@@ -577,14 +577,14 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
match res with
| EndEnterLoop _ -> false
| EndContinue _ -> true
- | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable"
in
(* Forward translation *)
let fwd_e =
(* Pop the frame - there is no returned value to pop: in the
translation we will simply call the loop function *)
let pop_return_value = false in
- let cf_pop = pop_frame config fdef.meta pop_return_value in
+ let cf_pop = pop_frame config fdef.item_meta.meta pop_return_value in
(* Generate the Return node *)
let cf_return _ret_value : m_fun =
fun _ctx -> Some (SA.ReturnWithLoop (loop_id, inside_loop))
@@ -618,7 +618,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
* the executions can lead to a panic *)
if synthesize then Some SA.Panic else None
| Unit | Break _ | Continue _ ->
- craise __FILE__ __LINE__ fdef.meta
+ craise __FILE__ __LINE__ fdef.item_meta.meta
("evaluate_function_symbolic failed on: " ^ name_to_string ())
in
@@ -652,14 +652,14 @@ module Test = struct
(* Sanity check - *)
sanity_check __FILE__ __LINE__
(fdef.signature.generics = empty_generic_params)
- fdef.meta;
- sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.meta;
+ fdef.item_meta.meta;
+ sanity_check __FILE__ __LINE__ (body.arg_count = 0) fdef.item_meta.meta;
(* Create the evaluation context *)
- let ctx = initialize_eval_ctx fdef.meta decls_ctx [] [] [] in
+ let ctx = initialize_eval_ctx fdef.item_meta.meta decls_ctx [] [] [] in
(* Insert the (uninitialized) local variables *)
- let ctx = ctx_push_uninitialized_vars fdef.meta ctx body.locals in
+ let ctx = ctx_push_uninitialized_vars fdef.item_meta.meta ctx body.locals in
(* Create the continuation to check the function's result *)
let config = mk_config ConcreteMode in
@@ -668,9 +668,9 @@ module Test = struct
| Return ->
(* Ok: drop the local variables and finish *)
let pop_return_value = true in
- pop_frame config fdef.meta pop_return_value (fun _ _ -> None) ctx
+ pop_frame config fdef.item_meta.meta pop_return_value (fun _ _ -> None) ctx
| _ ->
- craise __FILE__ __LINE__ fdef.meta
+ craise __FILE__ __LINE__ fdef.item_meta.meta
("Unit test failed (concrete execution) on: "
^ Print.Types.name_to_string
(Print.Contexts.decls_ctx_to_fmt_env decls_ctx)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index de89f316..064fff29 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1063,13 +1063,13 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
(* Treat the evaluation of the global as a call to the global body *)
let func = { func = FunId (FRegular global.body); generics } in
let call = { func = FnOpRegular func; args = []; dest } in
- (eval_transparent_function_call_concrete config global.meta global.body
+ (eval_transparent_function_call_concrete config global.item_meta.meta global.body
call)
cf ctx
| SymbolicMode ->
(* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
* defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
- cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.meta
+ cassert __FILE__ __LINE__ (ty_no_regions global.ty) global.item_meta.meta
"Const globals should not contain regions";
(* Instantiate the type *)
(* There shouldn't be any reference to Self *)
@@ -1082,9 +1082,9 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
global.ty
in
- let sval = mk_fresh_symbolic_value global.meta ty in
+ let sval = mk_fresh_symbolic_value global.item_meta.meta ty in
let cc =
- assign_to_place config global.meta
+ assign_to_place config global.item_meta.meta
(mk_typed_value_from_symbolic_value sval)
dest
in
@@ -1368,7 +1368,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
(* Sanity check: same number of inputs *)
sanity_check __FILE__ __LINE__
(List.length call.args = List.length def.signature.inputs)
- def.meta;
+ def.item_meta.meta;
(* Sanity check: no nested borrows, borrows in ADTs, etc. *)
cassert __FILE__ __LINE__
(List.for_all
@@ -1381,7 +1381,7 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
(inst_sg.output :: inst_sg.inputs))
meta "ADTs containing borrows are not supported yet";
(* Evaluate the function call *)
- eval_function_call_symbolic_from_inst_sig config def.meta func def.signature
+ eval_function_call_symbolic_from_inst_sig config def.item_meta.meta func def.signature
regions_hierarchy inst_sg generics trait_method_generics call.args call.dest
cf ctx
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index a46ef79c..c84cd39c 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -446,7 +446,7 @@ let apply_passes (crate : crate) : crate =
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
- save_error __FILE__ __LINE__ (Some f.meta)
+ save_error __FILE__ __LINE__ (Some f.item_meta.meta)
("Ignoring the body of '" ^ name ^ "' because of previous error");
{ f with body = None }
in
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index 713cdef9..c05e9f24 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -323,7 +323,7 @@ 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.meta) ))
+ (Types.name_to_string env d.name, d.signature, Some d.item_meta.meta) ))
(FunDeclId.Map.bindings fun_decls)
in
let assumed =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 15b52237..2fa68329 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -584,16 +584,16 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
let name = Print.Types.name_to_string env def.name in
let { T.regions; types; const_generics; trait_clauses } = def.generics in
(* Can't translate types with regions for now *)
- cassert __FILE__ __LINE__ (regions = []) def.meta
+ cassert __FILE__ __LINE__ (regions = []) def.item_meta.meta
"ADTs containing borrows are not supported yet";
let trait_clauses =
- List.map (translate_trait_clause def.meta) trait_clauses
+ List.map (translate_trait_clause def.item_meta.meta) trait_clauses
in
let generics = { types; const_generics; trait_clauses } in
- let kind = translate_type_decl_kind def.meta def.T.kind in
- let preds = translate_predicates def.meta def.preds in
+ let kind = translate_type_decl_kind def.item_meta.meta def.T.kind in
+ let preds = translate_predicates def.item_meta.meta def.preds in
let is_local = def.is_local in
- let meta = def.meta in
+ let meta = def.item_meta.meta in
{
def_id;
is_local;
@@ -1262,7 +1262,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
let regions_hierarchy =
FunIdMap.find (FRegular fun_id) decls_ctx.fun_ctx.regions_hierarchies
in
- let meta = (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).meta in
+ let meta = (FunDeclId.Map.find fun_id decls_ctx.fun_ctx.fun_decls).item_meta.meta in
translate_fun_sig_with_regions_hierarchy_to_decomposed meta decls_ctx
(FunId (FRegular fun_id)) regions_hierarchy sg input_names
@@ -2186,7 +2186,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
| PeIdent (s, _) -> s
| PeImpl _ ->
(* We shouldn't get there *)
- craise __FILE__ __LINE__ decl.meta "Unexpected")
+ craise __FILE__ __LINE__ decl.item_meta.meta "Unexpected")
in
name ^ "_back"
in
@@ -3839,7 +3839,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
(* Add a match over the fuel, if necessary *)
let body =
if function_decreases_fuel effect_info then
- wrap_in_match_fuel def.meta ctx.fuel0 ctx.fuel body
+ wrap_in_match_fuel def.item_meta.meta ctx.fuel0 ctx.fuel body
else body
in
(* Sanity check *)
@@ -3884,7 +3884,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
(List.for_all
(fun (var, ty) -> (var : var).ty = ty)
(List.combine inputs signature.inputs))
- def.meta;
+ def.item_meta.meta;
Some { inputs; inputs_lvs; body }
in
@@ -3900,7 +3900,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
{
def_id;
is_local = def.is_local;
- meta = def.meta;
+ meta = def.item_meta.meta;
kind = def.kind;
num_loops;
loop_id;
@@ -3938,7 +3938,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
def_id;
is_local;
name = llbc_name;
- meta;
+ item_meta;
generics = llbc_generics;
preds;
parent_clauses = llbc_parent_clauses;
@@ -3955,23 +3955,23 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
(Print.Contexts.decls_ctx_to_fmt_env ctx)
llbc_name
in
- let generics = translate_generic_params trait_decl.meta llbc_generics in
- let preds = translate_predicates trait_decl.meta preds in
+ let generics = translate_generic_params trait_decl.item_meta.meta llbc_generics in
+ let preds = translate_predicates trait_decl.item_meta.meta preds in
let parent_clauses =
- List.map (translate_trait_clause trait_decl.meta) llbc_parent_clauses
+ List.map (translate_trait_clause trait_decl.item_meta.meta) llbc_parent_clauses
in
let consts =
List.map
(fun (name, (ty, id)) ->
- (name, (translate_fwd_ty trait_decl.meta type_infos ty, id)))
+ (name, (translate_fwd_ty trait_decl.item_meta.meta type_infos ty, id)))
consts
in
let types =
List.map
(fun (name, (trait_clauses, ty)) ->
( name,
- ( List.map (translate_trait_clause trait_decl.meta) trait_clauses,
- Option.map (translate_fwd_ty trait_decl.meta type_infos) ty ) ))
+ ( List.map (translate_trait_clause trait_decl.item_meta.meta) trait_clauses,
+ Option.map (translate_fwd_ty trait_decl.item_meta.meta type_infos) ty ) ))
types
in
{
@@ -3979,7 +3979,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
is_local;
llbc_name;
name;
- meta;
+ meta = item_meta.meta;
generics;
llbc_generics;
preds;
@@ -3997,7 +3997,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
A.def_id;
is_local;
name = llbc_name;
- meta;
+ item_meta;
impl_trait = llbc_impl_trait;
generics = llbc_generics;
preds;
@@ -4011,8 +4011,8 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
in
let type_infos = ctx.type_ctx.type_infos in
let impl_trait =
- translate_trait_decl_ref trait_impl.meta
- (translate_fwd_ty trait_impl.meta type_infos)
+ translate_trait_decl_ref trait_impl.item_meta.meta
+ (translate_fwd_ty trait_impl.item_meta.meta type_infos)
llbc_impl_trait
in
let name =
@@ -4020,15 +4020,15 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
(Print.Contexts.decls_ctx_to_fmt_env ctx)
llbc_name
in
- let generics = translate_generic_params trait_impl.meta llbc_generics in
- let preds = translate_predicates trait_impl.meta preds in
+ let generics = translate_generic_params trait_impl.item_meta.meta llbc_generics in
+ let preds = translate_predicates trait_impl.item_meta.meta preds in
let parent_trait_refs =
- List.map (translate_strait_ref trait_impl.meta) parent_trait_refs
+ List.map (translate_strait_ref trait_impl.item_meta.meta) parent_trait_refs
in
let consts =
List.map
(fun (name, (ty, id)) ->
- (name, (translate_fwd_ty trait_impl.meta type_infos ty, id)))
+ (name, (translate_fwd_ty trait_impl.item_meta.meta type_infos ty, id)))
consts
in
let types =
@@ -4036,9 +4036,9 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
(fun (name, (trait_refs, ty)) ->
( name,
( List.map
- (translate_fwd_trait_ref trait_impl.meta type_infos)
+ (translate_fwd_trait_ref trait_impl.item_meta.meta type_infos)
trait_refs,
- translate_fwd_ty trait_impl.meta type_infos ty ) ))
+ translate_fwd_ty trait_impl.item_meta.meta type_infos ty ) ))
types
in
{
@@ -4046,7 +4046,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
is_local;
llbc_name;
name;
- meta;
+ meta = item_meta.meta;
impl_trait;
llbc_impl_trait;
generics;
@@ -4062,7 +4062,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
global_decl =
let {
- A.meta;
+ A.item_meta;
def_id;
is_local;
name = llbc_name;
@@ -4079,11 +4079,11 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
(Print.Contexts.decls_ctx_to_fmt_env ctx)
llbc_name
in
- let generics = translate_generic_params decl.meta llbc_generics in
- let preds = translate_predicates decl.meta preds in
- let ty = translate_fwd_ty decl.meta ctx.type_ctx.type_infos ty in
+ let generics = translate_generic_params decl.item_meta.meta llbc_generics in
+ let preds = translate_predicates decl.item_meta.meta preds in
+ let ty = translate_fwd_ty decl.item_meta.meta ctx.type_ctx.type_infos ty in
{
- meta;
+ meta = item_meta.meta;
def_id;
is_local;
llbc_name;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 9460c5f4..222b3c57 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -127,7 +127,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx)
let ctx =
{
- meta = fdef.meta;
+ meta = fdef.item_meta.meta;
decls_ctx = trans_ctx;
SymbolicToPure.bid = None;
sg;
@@ -179,7 +179,7 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx)
SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx
in
{ ctx with forward_inputs }
- | _ -> craise __FILE__ __LINE__ fdef.meta "Unreachable"
+ | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta "Unreachable"
in
(* Add the backward inputs *)
@@ -486,7 +486,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
let global_decls = ctx.trans_ctx.global_ctx.global_decls in
let global = GlobalDeclId.Map.find id global_decls in
let trans = FunDeclId.Map.find global.body ctx.trans_funs in
- sanity_check __FILE__ __LINE__ (trans.loops = []) global.meta;
+ sanity_check __FILE__ __LINE__ (trans.loops = []) global.item_meta.meta;
let body = trans.f in
let is_opaque = Option.is_none body.Pure.body in
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index e6621c7a..987df6ca 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -289,7 +289,7 @@ let analyze_type_decl (updated : bool ref) (infos : type_infos)
(List.map
(fun v -> List.map (fun f -> f.field_ty) v.fields)
variants)
- | Opaque -> craise __FILE__ __LINE__ def.meta "unreachable"
+ | Opaque -> craise __FILE__ __LINE__ def.item_meta.meta "unreachable"
in
(* Explore the types and accumulate information *)
let type_decl_info = TypeDeclId.Map.find def.def_id infos in
diff --git a/flake.lock b/flake.lock
index 4209cd99..ecc6b267 100644
--- a/flake.lock
+++ b/flake.lock
@@ -3,16 +3,17 @@
"charon": {
"inputs": {
"crane": "crane",
+ "flake-compat": "flake-compat",
"flake-utils": "flake-utils",
"nixpkgs": "nixpkgs",
"rust-overlay": "rust-overlay"
},
"locked": {
- "lastModified": 1713364636,
- "narHash": "sha256-+1qeUEzEz6wPc/0QaXQ6Co3tx8mckOggW8Hjx0qRFHc=",
+ "lastModified": 1713433954,
+ "narHash": "sha256-R3Pb/Z+V5s5neAwlTIhVJ/q3hDC65nLZ8d1ICotSdkM=",
"owner": "aeneasverif",
"repo": "charon",
- "rev": "6267ea774c762a8ca47ce26e66acd6dcc6a0ac6b",
+ "rev": "80ceb481c90f3cda435d5a60944ea7516415b294",
"type": "github"
},
"original": {
@@ -57,6 +58,21 @@
"type": "github"
}
},
+ "flake-compat_2": {
+ "locked": {
+ "lastModified": 1688025799,
+ "narHash": "sha256-ktpB4dRtnksm9F5WawoIkEneh1nrEvuxb5lJFt1iOyw=",
+ "owner": "nix-community",
+ "repo": "flake-compat",
+ "rev": "8bf105319d44f6b9f0d764efa4fdef9f1cc9ba1c",
+ "type": "github"
+ },
+ "original": {
+ "owner": "nix-community",
+ "repo": "flake-compat",
+ "type": "github"
+ }
+ },
"flake-utils": {
"inputs": {
"systems": "systems"
@@ -236,7 +252,7 @@
"root": {
"inputs": {
"charon": "charon",
- "flake-compat": "flake-compat",
+ "flake-compat": "flake-compat_2",
"flake-utils": [
"charon",
"flake-utils"