diff options
| -rw-r--r-- | src/Interpreter.ml | 112 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 74 |
2 files changed, 146 insertions, 40 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 617f6211..c7cdc329 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,12 +1,15 @@ +open Cps +open InterpreterUtils +open InterpreterProjectors +open InterpreterBorrows +open InterpreterExpressions +open InterpreterStatements +open CfimAstUtils module L = Logging module T = Types module A = CfimAst module M = Modules module SA = SymbolicAst -open Cps -open InterpreterUtils -open InterpreterExpressions -open InterpreterStatements (** The local logger *) let log = L.interpreter_log @@ -65,24 +68,18 @@ let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) let call_id = C.fresh_fun_call_id () in assert (call_id = V.FunCallId.zero); - let empty_absl = - create_empty_abstractions_from_abs_region_groups call_id V.SynthInput - inst_sg.A.regions_hierarchy - in - (* Add the avalues to the abstractions and insert them in the context *) - let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = + let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) : + C.eval_ctx * V.typed_avalue list = (* Project over the values - we use *loan* projectors, as explained above *) let avalues = List.map (mk_aproj_loans_value_from_symbolic_value abs.regions) input_svs in - (* Insert the avalues in the abstraction *) - let abs = { abs with avalues } in - (* Insert the abstraction in the context *) - let ctx = { ctx with env = Abs abs :: ctx.env } in - (* Return *) - ctx + (ctx, avalues) + in + let ctx = + create_push_abstractions_from_abs_region_groups call_id V.SynthInput + inst_sg.A.regions_hierarchy compute_abs_avalues ctx in - let ctx = List.fold_left insert_abs ctx empty_absl in (* Split the variables between return var, inputs and remaining locals *) let ret_var = List.hd fdef.locals in let input_vars, local_vars = @@ -98,6 +95,78 @@ let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : (* Return *) ctx +(** Small helper. + +*) +let evaluate_function_symbolic_synthesize_backward_from_return + (config : C.config) (m : M.cfim_module) (fdef : A.fun_def) + (inst_sg : A.inst_fun_sig) (back_id : T.RegionGroupId.id) (ctx : C.eval_ctx) + : SA.expression option = + (* 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 + * region ids for the return abstractions. *) + let sg = fdef.signature in + let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in + let ret_inst_sg = instantiate_fun_sig type_params sg in + let ret_rty = ret_inst_sg.output in + (* Move the return value out of the return variable *) + let cf_move_ret = move_return_value config in + + (* Insert the return value in the return abstractions (by applying + * borrow projections) *) + let cf_consume_ret ret_value ctx = + let ret_call_id = C.fresh_fun_call_id () in + let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) : + C.eval_ctx * V.typed_avalue list = + let ctx, avalue = + apply_proj_borrows_on_input_value config ctx abs.regions + abs.ancestors_regions ret_value ret_rty + in + (ctx, [ avalue ]) + in + (* Initialize and insert the abstractions in the context *) + let ctx = + create_push_abstractions_from_abs_region_groups ret_call_id V.SynthRet + ret_inst_sg.A.regions_hierarchy compute_abs_avalues ctx + in + + (* We now need to end the proper *input* abstractions - pay attention + * to the fact that we end the *input* abstractions, not the *return* + * abstractions (of course, the corresponding return abstractions will + * automatically be ended, because they consumed values coming from the + * input abstractions...) *) + let parent_rgs = list_parent_region_groups sg back_id in + let parent_input_abs_ids = + T.RegionGroupId.mapi + (fun rg_id rg -> + if T.RegionGroupId.Set.mem rg_id parent_rgs then Some rg.T.id + else None) + inst_sg.regions_hierarchy + in + let parent_input_abs_ids = + List.filter_map (fun x -> x) parent_input_abs_ids + in + (* End the parent abstractions and the current abstraction - note that we + * end them in an order which follows the regions hierarchy: it should lead + * to generated code which has a better consistency between the parent + * and children backward functions *) + let current_abs_id = + (T.RegionGroupId.nth inst_sg.regions_hierarchy back_id).id + in + 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 [] id cf) + cf target_abs_ids + in + (* Generate the Return node *) + let cf_return : m_fun = fun _ -> Some (SA.Return None) in + (* Apply *) + cf_end_target_abs cf_return ctx + in + cf_move_ret cf_consume_ret ctx + (** Evaluate a function with the symbolic interpreter *) let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) (m : M.cfim_module) (fid : A.FunDefId.id) @@ -133,10 +202,7 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) | None -> (* Forward translation *) (* Move the return value *) - let ret_vid = V.VarId.zero in - let cf_move = - eval_operand config (E.Move (mk_place_from_var_id ret_vid)) - in + let cf_move = move_return_value config in (* Generate the Return node *) let cf_return ret_value : m_fun = fun _ -> Some (SA.Return ret_value) @@ -144,7 +210,9 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool) (* Apply *) cf_move cf_return ctx | Some back_id -> - (* Backward translation *) raise Errors.Unimplemented + (* Backward translation *) + evaluate_function_symbolic_synthesize_backward_from_return config + m fdef inst_sg back_id ctx else None | Panic -> (* Note that as we explore all the execution branches, one of diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 78770adb..c7e67f0a 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -245,6 +245,13 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id) | A.BoxFree, [], [ _ ] -> mk_unit_ty | _ -> failwith "Inconsistent state" +let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun + = + fun ctx -> + let ret_vid = V.VarId.zero in + let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in + cc cf ctx + (** Pop the current frame. Drop all the local variables but the return variable, move the return @@ -280,7 +287,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun = ^ "]")); (* Move the return value out of the return variable *) - let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in + let cc = move_return_value config in (* Sanity check *) let cc = comp_check_value cc (fun ret_value ctx -> @@ -655,6 +662,41 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) (* Apply *) T.RegionGroupId.mapi create_abs rgl +(** Helper. + + Create a list of abstractions from a list of regions groups, and insert + them in the context. + + [compute_abs_avalues]: this function must compute, given an initialized, + empty (i.e., with no avalues) abstraction, compute the avalues which + should be inserted in this abstraction before we insert it in the context. + Note that this function may update the context: it is necessary when + computing borrow projections, for instance. +*) +let create_push_abstractions_from_abs_region_groups (call_id : V.FunCallId.id) + (kind : V.abs_kind) (rgl : A.abs_region_group list) + (compute_abs_avalues : + V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list) + (ctx : C.eval_ctx) : C.eval_ctx = + (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) + let empty_absl = + create_empty_abstractions_from_abs_region_groups call_id kind rgl + in + + (* Compute and add the avalues to the abstractions, the insert the abstractions + * in the context. *) + let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = + (* Compute the values to insert in the abstraction *) + let ctx, avalues = compute_abs_avalues abs ctx in + (* Add the avalues to the abstraction *) + let abs = { abs with avalues } in + (* Insert the abstraction in the context *) + let ctx = { ctx with env = Abs abs :: ctx.env } in + (* Return *) + ctx + in + List.fold_left insert_abs ctx empty_absl + (** Evaluate a statement *) let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = fun cf ctx -> @@ -972,15 +1014,12 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg)) args); - (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *) - let call_id = C.fresh_fun_call_id () in - let empty_absl = - create_empty_abstractions_from_abs_region_groups call_id V.FunCall - inst_sg.A.regions_hierarchy - in - - (* Add the avalues to the abstractions and insert them in the context *) - let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx = + (* Initialize the abstractions and push them in the context. + * First, we define the function which, given an initialized, empty + * abstraction, computes the avalues which should be inserted inside. + *) + let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) : + C.eval_ctx * V.typed_avalue list = (* Project over the input values *) let ctx, args_projs = List.fold_left_map @@ -990,15 +1029,14 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) ctx args_with_rtypes in (* Group the input and output values *) - let avalues = List.append args_projs [ ret_av abs.regions ] in - (* Add the avalues to the abstraction *) - let abs = { abs with avalues } in - (* Insert the abstraction in the context *) - let ctx = { ctx with env = Abs abs :: ctx.env } in - (* Return *) - ctx + (ctx, List.append args_projs [ ret_av abs.regions ]) + in + (* Actually initialize and insert the abstractions *) + let call_id = C.fresh_fun_call_id () in + let ctx = + create_push_abstractions_from_abs_region_groups call_id V.FunCall + inst_sg.A.regions_hierarchy compute_abs_avalues ctx in - let ctx = List.fold_left insert_abs ctx empty_absl in (* Apply the continuation *) let expr = cf ctx in |