From d22f5d1ae5155c53b9cd0daf165dccb5d5563c1f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jan 2022 18:36:47 +0100
Subject: Finish implementing eval_local_function_call_symbolic

---
 src/Interpreter.ml | 59 ++++++++++++++++++++++++++++++++++++++++++++----------
 src/Synthesis.ml   |  3 ++-
 src/Values.ml      |  3 ---
 3 files changed, 50 insertions(+), 15 deletions(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ed5c52d3..2192c491 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -442,6 +442,11 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
   in
   { V.value; V.ty }
 
+let apply_proj_borrows_in_context (check_symbolic_no_ended : bool)
+    (ctx : C.eval_ctx) (regions : T.RegionId.set_t) (v : V.typed_value)
+    (ty : T.rty) : C.eval_ctx * V.typed_avalue =
+  raise Unimplemented
+
 (** Convert a symbolic expansion to a value.
 
     If the expansion is a mutable reference expansion, it converts it to a borrow.
@@ -4201,23 +4206,55 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
   let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in
   (* Generate a fresh symbolic value for the result *)
   let res_sv_ty = inst_sg.A.output in
-  let ctx, res_sv =
+  let ctx, res_spc =
     mk_fresh_symbolic_proj_comp T.RegionId.Set.empty res_sv_ty ctx
   in
-  (* Generate the abstractions from the region groups *)
-  let generate_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) :
-      C.eval_ctx * V.abs =
-    raise Unimplemented
+  let res_value = mk_typed_value_from_proj_comp res_spc in
+  let res_av = V.ASymbolic (V.AProjLoans res_spc.V.svalue) in
+  let res_av : V.typed_avalue =
+    { V.value = res_av; V.ty = res_spc.V.svalue.V.sv_ty }
   in
-  let ctx, abs =
-    List.fold_left_map generate_abs ctx inst_sg.A.regions_hierarchy
+  (* Evaluate the input operands *)
+  let ctx, args = eval_operands config ctx args in
+  assert (List.length args = def.A.arg_count);
+  let args_with_rtypes = List.combine args rtype_params in
+  (* Generate the abstractions from the region groups and add them to the context *)
+  let gen_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
+    let abs_id = rg.A.id in
+    let parents =
+      List.fold_left
+        (fun s pid -> V.AbstractionId.Set.add pid s)
+        V.AbstractionId.Set.empty rg.A.parents
+    in
+    let regions =
+      List.fold_left
+        (fun s rid -> T.RegionId.Set.add rid s)
+        T.RegionId.Set.empty rg.A.regions
+    in
+    (* Project over the input values *)
+    let check_symbolic_no_ended = true in
+    let ctx, args_projs =
+      List.fold_left_map
+        (fun ctx (arg, arg_rty) ->
+          apply_proj_borrows_in_context check_symbolic_no_ended ctx regions arg
+            arg_rty)
+        ctx args_with_rtypes
+    in
+    (* Group the input and output values *)
+    let avalues = List.append args_projs [ res_av ] in
+    (* Create the abstraction *)
+    let abs = { V.abs_id; parents; regions; avalues } in
+    (* Insert the abstraction in the context *)
+    let ctx = { ctx with env = Abs abs :: ctx.env } in
+    (* Return *)
+    ctx
   in
-  (* Add the abstractions to the context *)
-  let abs = List.rev (List.map (fun abs -> C.Abs abs) abs) in
-  let ctx = { ctx with C.env = List.append abs ctx.C.env } in
+  let ctx = List.fold_left gen_abs ctx inst_sg.A.regions_hierarchy in
+  (* Move the return value to its destination *)
+  let ctx = assign_to_place config ctx res_value dest in
   (* Synthesis *)
   S.synthesize_local_function_call fid region_params type_params args dest
-    res_sv.V.svalue;
+    res_spc.V.svalue;
   (* Return *)
   ctx
 
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index f317a5f9..60c387d2 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -70,5 +70,6 @@ let synthesize_non_local_function_call (fid : A.assumed_fun_id)
 
 let synthesize_local_function_call (fid : A.FunDefId.id)
     (region_params : T.erased_region list) (type_params : T.ety list)
-    (args : E.operand list) (dest : E.place) (res : V.symbolic_value) : unit =
+    (args : V.typed_value list) (dest : E.place) (res : V.symbolic_value) : unit
+    =
   ()
diff --git a/src/Values.ml b/src/Values.ml
index 001c0347..ae9eb127 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -542,9 +542,6 @@ and typed_avalue = { value : avalue; ty : rty }
 type abs = {
   abs_id : (AbstractionId.id[@opaque]);
   parents : (AbstractionId.set_t[@opaque]);  (** The parent abstractions *)
-  acc_regions : (RegionId.set_t[@opaque]);
-      (** Union of the regions owned by the (transitive) parent abstractions and
-          by the current abstraction. TODO: why do we need those? *)
   regions : (RegionId.set_t[@opaque]);  (** Regions owned by this abstraction *)
   avalues : typed_avalue list;  (** The values in this abstraction *)
 }
-- 
cgit v1.2.3