Factorize initialize_symbolic_context_for_fun and

eval_function_call_symbolic_from_inst_sig and make minor modifications

3 files changed, 69 insertions, 58 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index b938fe90..f38cb66e 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -69,42 +69,23 @@ module Test = struct
     let input_svs =
       List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
     in
-    (* Create the abstractions and insert them in 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 values - we use *loan* projectors, as explained above *)
       let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in
-      (* Create the abstraction *)
-      let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } 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
     in
-    let ctx = List.fold_left create_abs ctx inst_sg.regions_hierarchy 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 =
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 *)
diff --git a/src/Values.ml b/src/Values.ml
index 53851cea..bcb08dc8 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -564,7 +564,8 @@ type abs = {
   parents : (AbstractionId.set_t[@opaque]);  (** The parent abstractions *)
   regions : (RegionId.set_t[@opaque]);  (** Regions owned by this abstraction *)
   ancestors_regions : (RegionId.set_t[@opaque]);
-      (** Union of the regions owned by this abstraction and its ancestors *)
+      (** Union of the regions owned by this abstraction's ancestors (not
+          including the regions of this abstraction itself) *)
   avalues : typed_avalue list;  (** The values in this abstraction *)
 }
 [@@deriving