From cd9ed7e816f76119a321a8e2185e5244ad1d111a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 22:48:00 +0100
Subject: Make good progress on generating the symbolic AST for the backward
 functions

---
 src/Interpreter.ml           | 112 ++++++++++++++++++++++++++++++++++---------
 src/InterpreterStatements.ml |  74 +++++++++++++++++++++-------
 2 files changed, 146 insertions(+), 40 deletions(-)

(limited to 'src')

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
-- 
cgit v1.2.3