From c16ad7c78a149d3fd62976f4eb17d07a9c03b8c6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 7 Jan 2022 15:04:11 +0100
Subject: Factorize initialize_symbolic_context_for_fun and
 eval_function_call_symbolic_from_inst_sig and make minor modifications

---
 src/InterpreterStatements.ml | 87 +++++++++++++++++++++++++++++---------------
 1 file changed, 58 insertions(+), 29 deletions(-)

(limited to 'src/InterpreterStatements.ml')

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 03940bb7..917f1265 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -513,6 +513,54 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
   (* Return *)
   (ctx, inst_sig)
 
+(** Helper
+ 
+    Create abstractions (with no avalues, which have to be inserted afterwards)
+    from a list of abs region groups.
+ *)
+let create_empty_abstractions_from_abs_region_groups
+    (rgl : A.abs_region_group list) : V.abs list =
+  (* We use a reference to progressively create a map from abstraction ids
+   * to set of ancestor regions. Note that abs_to_ancestors_regions[abs_id]
+   * returns the union of:
+   * - the regions of the ancestors of abs_id
+   * - the regions of abs_id
+   *)
+  let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+    ref V.AbstractionId.Map.empty
+  in
+  (* Auxiliary function to create one abstraction *)
+  let create_abs (rg : A.abs_region_group) : V.abs =
+    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
+    let ancestors_regions =
+      List.fold_left
+        (fun acc parent_id ->
+          T.RegionId.Set.union acc
+            (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+        T.RegionId.Set.empty rg.A.parents
+    in
+    let ancestors_regions_union_current_regions =
+      T.RegionId.Set.union ancestors_regions regions
+    in
+    abs_to_ancestors_regions :=
+      V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
+        !abs_to_ancestors_regions;
+    (* Create the abstraction *)
+    { V.abs_id; parents; regions; ancestors_regions; avalues = [] }
+  in
+  (* Apply *)
+  List.map create_abs rgl
+
 (** Evaluate a statement *)
 let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
     : (C.eval_ctx * statement_eval_res) eval_result list =
@@ -817,49 +865,30 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       (fun ((arg, rty) : V.typed_value * T.rty) ->
         arg.V.ty = Subst.erase_regions rty)
       args_with_rtypes);
-  (* Create the abstractions from the region groups and add them to the context *)
-  let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
-    ref V.AbstractionId.Map.empty
+  (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+  let empty_absl =
+    create_empty_abstractions_from_abs_region_groups inst_sg.A.regions_hierarchy
   in
-  let create_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
-    let ancestors_regions =
-      List.fold_left
-        (fun acc parent_id ->
-          T.RegionId.Set.union acc
-            (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
-        regions rg.A.parents
-    in
-    abs_to_ancestors_regions :=
-      V.AbstractionId.Map.add abs_id ancestors_regions !abs_to_ancestors_regions;
+  (* 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 =
     (* Project over the input values *)
     let ctx, args_projs =
       List.fold_left_map
         (fun ctx (arg, arg_rty) ->
-          apply_proj_borrows_on_input_value config ctx regions ancestors_regions
-            arg arg_rty)
+          apply_proj_borrows_on_input_value config ctx abs.regions
+            abs.ancestors_regions arg arg_rty)
         ctx args_with_rtypes
     in
     (* Group the input and output values *)
     let avalues = List.append args_projs [ ret_av ] in
-    (* Create the abstraction *)
-    let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } 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
-  let ctx = List.fold_left create_abs ctx inst_sg.A.regions_hierarchy in
+  let ctx = List.fold_left insert_abs ctx empty_absl in
   (* Move the return value to its destination *)
   let ctx = assign_to_place config ctx ret_value dest in
   (* Synthesis *)
-- 
cgit v1.2.3