Add `can_end` in `abs` and use it for the return abs when generating the

backward functions

5 files changed, 59 insertions, 33 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index f6ae268d..cbbf2b2e 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -86,9 +86,10 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
     in
     (ctx, avalues)
   in
+  let region_can_end _ = true in
   let ctx =
     create_push_abstractions_from_abs_region_groups call_id V.SynthInput
-      inst_sg.A.regions_hierarchy compute_abs_avalues ctx
+      inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
   in
   (* Split the variables between return var, inputs and remaining locals *)
   let body = Option.get fdef.body in
@@ -127,6 +128,21 @@ let evaluate_function_symbolic_synthesize_backward_from_return
   (* Move the return value out of the return variable *)
   let cf_pop_frame = ctx_pop_frame config in
 
+  (* We need to find the parents regions/abstractions of the region we
+   * will end - this will allow us to, first, mark the other return
+   * regions as non-endable, and, second, end those parent regions in
+   * proper order. *)
+  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
+
   (* Insert the return value in the return abstractions (by applying
    * borrow projections) *)
   let cf_consume_ret ret_value ctx =
@@ -139,10 +155,20 @@ let evaluate_function_symbolic_synthesize_backward_from_return
       in
       (ctx, [ avalue ])
     in
-    (* Initialize and insert the abstractions in the context *)
+
+    (* Initialize and insert the abstractions in the context.
+     *
+     * We take care of disallowing ending the return regions which we
+     * shouldn't end (see the documentation of the `can_end` field of [abs]
+     * for more information. *)
+    let parent_and_current_rgs = T.RegionGroupId.Set.add back_id parent_rgs in
+    let region_can_end rid =
+      T.RegionGroupId.Set.mem rid parent_and_current_rgs
+    in
+    assert (region_can_end back_id);
     let ctx =
       create_push_abstractions_from_abs_region_groups ret_call_id V.SynthRet
-        ret_inst_sg.A.regions_hierarchy compute_abs_avalues ctx
+        ret_inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
     in
 
     (* We now need to end the proper *input* abstractions - pay attention
@@ -150,17 +176,6 @@ let evaluate_function_symbolic_synthesize_backward_from_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
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index f5f3a8fa..26374bf7 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -985,6 +985,9 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids)
   (* Lookup the abstraction *)
   let abs = C.ctx_lookup_abs ctx abs_id in
 
+  (* Check that we can end the abstraction *)
+  assert abs.can_end;
+
   (* End the parent abstractions first *)
   let cc = end_abstractions config chain abs.parents in
   let cc =
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index e2775a1d..585fa828 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -677,9 +677,13 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
  
     Create abstractions (with no avalues, which have to be inserted afterwards)
     from a list of abs region groups.
+    
+    [region_can_end]: gives the region groups from which we generate functions
+    which can end or not.
  *)
 let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
-    (kind : V.abs_kind) (rgl : A.abs_region_group list) : V.abs list =
+    (kind : V.abs_kind) (rgl : A.abs_region_group list)
+    (region_can_end : T.RegionGroupId.id -> bool) : 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:
@@ -714,6 +718,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
     let ancestors_regions_union_current_regions =
       T.RegionId.Set.union ancestors_regions regions
     in
+    let can_end = region_can_end back_id in
     abs_to_ancestors_regions :=
       V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
         !abs_to_ancestors_regions;
@@ -723,6 +728,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
       call_id;
       back_id;
       kind;
+      can_end;
       parents;
       original_parents;
       regions;
@@ -737,6 +743,9 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
 
     Create a list of abstractions from a list of regions groups, and insert
     them in the context.
+
+    [region_can_end]: gives the region groups from which we generate functions
+    which can end or not.
     
     [compute_abs_avalues]: this function must compute, given an initialized,
     empty (i.e., with no avalues) abstraction, compute the avalues which
@@ -746,12 +755,14 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
 *)
 let create_push_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
     (kind : V.abs_kind) (rgl : A.abs_region_group list)
+    (region_can_end : T.RegionGroupId.id -> bool)
     (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
+      region_can_end
   in
 
   (* Compute and add the avalues to the abstractions, the insert the abstractions
@@ -1152,9 +1163,10 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     in
     (* Actually initialize and insert the abstractions *)
     let call_id = C.fresh_fun_call_id () in
+    let region_can_end _ = true in
     let ctx =
       create_push_abstractions_from_abs_region_groups call_id V.FunCall
-        inst_sg.A.regions_hierarchy compute_abs_avalues ctx
+        inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
     in
 
     (* Apply the continuation *)
diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml
index 84e8e00f..0e679fca 100644
--- a/src/LlbcAstUtils.ml
+++ b/src/LlbcAstUtils.ml
@@ -7,7 +7,6 @@ let statement_has_loops (st : statement) : bool =
   let obj =
     object
       inherit [_] iter_statement
-
       method! visit_Loop _ _ = raise Found
     end
   in
@@ -38,6 +37,8 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     We don't do that in an efficient manner, but it doesn't matter.
     
     TODO: rename to "list_ancestors_..."
+
+    This list *doesn't* include the current region.
  *)
 let rec list_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) :
     T.RegionGroupId.Set.t =
diff --git a/src/Values.ml b/src/Values.ml
index 4e45db03..4585b443 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -6,13 +6,9 @@ open Types
  * inside abstractions) *)
 
 module VarId = IdGen ()
-
 module BorrowId = IdGen ()
-
 module SymbolicValueId = IdGen ()
-
 module AbstractionId = IdGen ()
-
 module FunCallId = IdGen ()
 
 (** A variable *)
@@ -83,13 +79,9 @@ type symbolic_value = {
 class ['self] iter_typed_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
-
     method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
-
     method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
-
     method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> ()
-
     method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
   end
 
@@ -228,7 +220,6 @@ and typed_value = { value : value; ty : ety }
 class ['self] iter_typed_value =
   object (_self : 'self)
     inherit [_] iter_typed_value_visit_mvalue
-
     method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
   end
 
@@ -236,7 +227,6 @@ class ['self] iter_typed_value =
 class ['self] map_typed_value =
   object (_self : 'self)
     inherit [_] map_typed_value_visit_mvalue
-
     method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
   end
 
@@ -275,7 +265,6 @@ type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show]
 class ['self] iter_aproj_base =
   object (_self : 'self)
     inherit [_] iter_typed_value
-
     method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
 
     method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
@@ -286,7 +275,6 @@ class ['self] iter_aproj_base =
 class ['self] map_aproj_base =
   object (_self : 'self)
     inherit [_] map_typed_value
-
     method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
 
     method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
@@ -374,9 +362,7 @@ type region = RegionVarId.id Types.region [@@deriving show]
 class ['self] iter_typed_avalue_base =
   object (_self : 'self)
     inherit [_] iter_aproj
-
     method visit_id : 'env -> BorrowId.id -> unit = fun _ _ -> ()
-
     method visit_region : 'env -> region -> unit = fun _ _ -> ()
 
     method visit_abstract_shared_borrows
@@ -388,9 +374,7 @@ class ['self] iter_typed_avalue_base =
 class ['self] map_typed_avalue_base =
   object (_self : 'self)
     inherit [_] map_aproj
-
     method visit_id : 'env -> BorrowId.id -> BorrowId.id = fun _ id -> id
-
     method visit_region : 'env -> region -> region = fun _ r -> r
 
     method visit_abstract_shared_borrows
@@ -798,6 +782,17 @@ type abs = {
           the symbolic AST, generated by the symbolic execution.
        *)
   kind : (abs_kind[@opaque]);
+  can_end : (bool[@opaque]);
+      (** Controls whether the region can be ended or not.
+          
+          This allows to "pin" some regions, and is useful when generating
+          backward functions.
+          
+          For instance, if we have: `fn f<'a, 'b>(...) -> (&'a mut T, &'b mut T)`,
+          when generating the backward function for 'a, we have to make sure we
+          don't need to end the return region for 'b (if it is the case, it means
+          the function doesn't borrow check).
+       *)
   parents : (AbstractionId.Set.t[@opaque]);  (** The parent abstractions *)
   original_parents : (AbstractionId.id list[@opaque]);
       (** The original list of parents, ordered. This is used for synthesis. *)