diff options
author | Son HO | 2024-04-22 11:06:25 +0200 |
---|---|---|
committer | GitHub | 2024-04-22 11:06:25 +0200 |
commit | 1e2fce0e1fa42fa2ba5800332e1fdfcba2294657 (patch) | |
tree | 756865684bdfefd3fd1eb6be482e5fd816aac898 /compiler/Interpreter.ml | |
parent | ad764b07c7a576eb509e08a29868e719fe5d8a84 (diff) | |
parent | 93d6dce8f3d78ad6f2f18ca3e2f58fa605d503cd (diff) |
Merge pull request #151 from AeneasVerif/son/fix-loops2
Fix an issue in the loops fixed point
Diffstat (limited to 'compiler/Interpreter.ml')
-rw-r--r-- | compiler/Interpreter.ml | 31 |
1 files changed, 20 insertions, 11 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index d9af063e..f10c8d3e 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -218,12 +218,14 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) : at the same time the normalization map for the associated types. *) let ctx, inst_sg = - symbolic_instantiate_fun_sig fdef.item_meta.meta ctx fdef.signature regions_hierarchy - fdef.kind + 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.item_meta.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 @@ -299,8 +301,8 @@ 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.item_meta.meta ctx fdef.signature regions_hierarchy - fdef.kind + 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 *) @@ -333,8 +335,8 @@ 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.item_meta.meta ctx abs.regions - abs.ancestors_regions ret_value ret_rty + apply_proj_borrows_on_input_value config fdef.item_meta.meta ctx + abs.regions abs.ancestors_regions ret_value ret_rty in (ctx, [ avalue ]) in @@ -349,7 +351,8 @@ 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.item_meta.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) @@ -534,7 +537,9 @@ 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.item_meta.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)) @@ -584,7 +589,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx) (* 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.item_meta.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)) @@ -668,7 +675,9 @@ module Test = struct | Return -> (* Ok: drop the local variables and finish *) let pop_return_value = true in - pop_frame config fdef.item_meta.meta pop_return_value (fun _ _ -> None) ctx + pop_frame config fdef.item_meta.meta pop_return_value + (fun _ _ -> None) + ctx | _ -> craise __FILE__ __LINE__ fdef.item_meta.meta ("Unit test failed (concrete execution) on: " |