diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 9 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 6 | ||||
| -rw-r--r-- | compiler/Interpreter.ml | 56 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 12 | ||||
| -rw-r--r-- | compiler/PrePasses.ml | 2 | ||||
| -rw-r--r-- | compiler/RegionsHierarchy.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 66 | ||||
| -rw-r--r-- | compiler/Translate.ml | 6 | ||||
| -rw-r--r-- | compiler/TypesAnalysis.ml | 2 | ||||
| -rw-r--r-- | flake.lock | 24 |
11 files changed, 101 insertions, 85 deletions
@@ -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 @@ -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" |