From fa57d8d9d51c93ccefefb0951c67475970e97879 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 8 Apr 2024 15:18:58 +0200 Subject: item_meta --- compiler/Interpreter.ml | 56 ++++++++++++++++++++++++------------------------- 1 file changed, 28 insertions(+), 28 deletions(-) (limited to 'compiler/Interpreter.ml') 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) -- cgit v1.2.3