Merge loop abs so that there is one abs per function input region group

5 files changed, 387 insertions, 54 deletions

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 69c4ec3b..55baa6a4 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -259,6 +259,7 @@ type eval_ctx = {
   type_context : type_context;
   fun_context : fun_context;
   global_context : global_context;
+  region_groups : RegionGroupId.id list;
   type_vars : type_var list;
   env : env;
   ended_regions : RegionId.Set.t;
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index ec1b6260..4b030088 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -29,12 +29,14 @@ let compute_type_fun_global_contexts (m : A.crate) :
 
 let initialize_eval_context (type_context : C.type_context)
     (fun_context : C.fun_context) (global_context : C.global_context)
-    (type_vars : T.type_var list) : C.eval_ctx =
+    (region_groups : T.RegionGroupId.id list) (type_vars : T.type_var list) :
+    C.eval_ctx =
   C.reset_global_counters ();
   {
     C.type_context;
     C.fun_context;
     C.global_context;
+    C.region_groups;
     C.type_vars;
     C.env = [ C.Frame ];
     C.ended_regions = T.RegionId.Set.empty;
@@ -69,9 +71,12 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
    * *)
   let sg = fdef.signature in
   (* Create the context *)
+  let region_groups =
+    List.map (fun (g : T.region_var_group) -> g.id) sg.regions_hierarchy
+  in
   let ctx =
     initialize_eval_context type_context fun_context global_context
-      sg.type_params
+      region_groups sg.type_params
   in
   (* Instantiate the signature *)
   let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in
@@ -312,7 +317,7 @@ module Test = struct
       compute_type_fun_global_contexts crate
     in
     let ctx =
-      initialize_eval_context type_context fun_context global_context []
+      initialize_eval_context type_context fun_context global_context [] []
     in
 
     (* Insert the (uninitialized) local variables *)
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 53005bf3..e68790d4 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -245,7 +245,7 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
 (** Destructure all the new abstractions *)
 let destructure_new_abs (loop_id : V.LoopId.id)
     (old_abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
-  let abs_kind = V.Loop loop_id in
+  let abs_kind = V.Loop (loop_id, None) in
   let can_end = false in
   let destructure_shared_values = true in
   let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
@@ -336,7 +336,7 @@ let collapse_ctx (loop_id : V.LoopId.id)
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
      ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n"));
 
-  let abs_kind = V.Loop loop_id in
+  let abs_kind = V.Loop (loop_id, None) in
   let can_end = false in
   let destructure_shared_values = true in
   let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
@@ -966,7 +966,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
       let abs =
         {
           V.abs_id = C.fresh_abstraction_id ();
-          kind = V.Loop S.loop_id;
+          kind = V.Loop (S.loop_id, None);
           can_end = false;
           parents = V.AbstractionId.Set.empty;
           original_parents = [];
@@ -1020,7 +1020,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
       let abs =
         {
           V.abs_id = C.fresh_abstraction_id ();
-          kind = V.Loop S.loop_id;
+          kind = V.Loop (S.loop_id, None);
           can_end = false;
           parents = V.AbstractionId.Set.empty;
           original_parents = [];
@@ -1124,7 +1124,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
             else raise (ValueMatchFailure (LoanInRight id)))
     | None ->
         (* Convert the value to an abstraction *)
-        let abs_kind = V.Loop S.loop_id in
+        let abs_kind = V.Loop (S.loop_id, None) in
         let can_end = false in
         let destructure_shared_values = true in
         let absl =
@@ -1146,15 +1146,8 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
   let match_avalues _ _ = raise (Failure "Unreachable")
 end
 
-(** Collapse an environment, merging the duplicated borrows/loans.
-
-    This function simply calls {!collapse_ctx} with the proper merging functions.
-
-    We do this because when we join environments, we may introduce duplicated
-    loans and borrows. See the explanations for {!join_ctxs}.
- *)
-let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+let mk_collapse_ctx_merge_duplicate_funs (loop_id : V.LoopId.id)
+    (ctx : C.eval_ctx) : merge_duplicates_funcs =
   (* Rem.: the merge functions raise exceptions (that we catch). *)
   let module S : MatchJoinState = struct
     let ctx = ctx
@@ -1228,15 +1221,30 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
     let value = V.ALoan (V.ASharedLoan (ids, sv, child)) in
     { V.value; ty }
   in
-  let merge_funcs =
-    {
-      merge_amut_borrows;
-      merge_ashared_borrows;
-      merge_amut_loans;
-      merge_ashared_loans;
-    }
-  in
-  try collapse_ctx loop_id (Some merge_funcs) old_ids ctx
+  {
+    merge_amut_borrows;
+    merge_ashared_borrows;
+    merge_amut_loans;
+    merge_ashared_loans;
+  }
+
+let merge_abstractions (loop_id : V.LoopId.id) (abs_kind : V.abs_kind)
+    (can_end : bool) (ctx : C.eval_ctx) (aid0 : V.AbstractionId.id)
+    (aid1 : V.AbstractionId.id) : C.eval_ctx * V.AbstractionId.id =
+  let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in
+  merge_abstractions abs_kind can_end (Some merge_funs) ctx aid0 aid1
+
+(** Collapse an environment, merging the duplicated borrows/loans.
+
+    This function simply calls {!collapse_ctx} with the proper merging functions.
+
+    We do this because when we join environments, we may introduce duplicated
+    loans and borrows. See the explanations for {!join_ctxs}.
+ *)
+let collapse_ctx_with_merge (loop_id : V.LoopId.id) (old_ids : ids_sets)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  let merge_funs = mk_collapse_ctx_merge_duplicate_funs loop_id ctx in
+  try collapse_ctx loop_id (Some merge_funs) old_ids ctx
   with ValueMatchFailure _ -> raise (Failure "Unexpected")
 
 (** Join two contexts.
@@ -1450,6 +1458,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
       C.type_context;
       fun_context;
       global_context;
+      region_groups;
       type_vars;
       env = _;
       ended_regions = ended_regions0;
@@ -1460,6 +1469,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
       C.type_context = _;
       fun_context = _;
       global_context = _;
+      region_groups = _;
       type_vars = _;
       env = _;
       ended_regions = ended_regions1;
@@ -1472,6 +1482,7 @@ let join_ctxs (loop_id : V.LoopId.id) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
         C.type_context;
         fun_context;
         global_context;
+        region_groups;
         type_vars;
         env;
         ended_regions;
@@ -1830,6 +1841,10 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
 
   (* Rem.: this function raises exceptions of type [Distinct] *)
   let match_abstractions (abs0 : V.abs) (abs1 : V.abs) : unit =
+    log#ldebug
+      (lazy
+        ("match_ctxs: match_abstractions: " ^ "\n\n- abs0: " ^ V.show_abs abs0
+       ^ "\n\n- abs0: " ^ V.show_abs abs1));
     let {
       V.abs_id = abs_id0;
       kind = kind0;
@@ -1917,8 +1932,11 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
         (* Continue *)
         match_envs env0' env1'
     | C.Abs abs0 :: env0', C.Abs abs1 :: env1' ->
+        log#ldebug (lazy "ctxs_are_equivalent: match_envs: matching abs");
         (* Same as for the dummy values: there are two cases *)
         if V.AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
+          log#ldebug
+            (lazy "ctxs_are_equivalent: match_envs: matching abs: fixed abs");
           (* Still in the prefix: the abstractions must be the same *)
           assert (abs0 = abs1);
           (* Their ids must be fixed *)
@@ -1927,6 +1945,9 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) (ctx0 : C.eval_ctx)
           (* Continue *)
           match_envs env0' env1')
         else (
+          log#ldebug
+            (lazy
+              "ctxs_are_equivalent: match_envs: matching abs: not fixed abs");
           (* Match the values *)
           match_abstractions abs0 abs1;
           (* Continue *)
@@ -2188,12 +2209,13 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
     ctxs_are_equivalent fixed_ids ctx1 ctx2
   in
   let max_num_iter = Config.loop_fixed_point_max_num_iters in
-  let rec compute_fixed_point (ctx : C.eval_ctx) (i : int) : C.eval_ctx =
+  let rec compute_fixed_point (ctx : C.eval_ctx) (i0 : int) (i : int) :
+      C.eval_ctx =
     if i = 0 then
       raise
         (Failure
-           ("Could not compute a loop fixed point in "
-          ^ string_of_int max_num_iter ^ " iterations"))
+           ("Could not compute a loop fixed point in " ^ string_of_int i0
+          ^ " iterations"))
     else
       (* Evaluate the loop body to register the different contexts upon reentry *)
       let _ = eval_loop_body cf_exit_loop_body ctx in
@@ -2211,35 +2233,206 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
           ^ "\n\n"));
 
       (* Check if we reached a fixed point: if not, iterate *)
-      if equiv_ctxs ctx ctx1 then ctx1 else compute_fixed_point ctx1 (i - 1)
+      if equiv_ctxs ctx ctx1 then ctx1 else compute_fixed_point ctx1 i0 (i - 1)
   in
-  let fp = compute_fixed_point ctx0 max_num_iter in
-  let fixed_ids = compute_fixed_ids (Option.get !ctx_upon_entry) fp in
-  (* For now, all the new abstractions in the fixed-point have the same region
-     group (of id 0): we want each one of them to have a unique region group
-     (because we will translate each one of those abstractions to a pair
-     forward function/backward function).
-  *)
-  let region_map = ref T.RegionId.Map.empty in
-  let get_rid (rid : T.RegionId.id) : T.RegionId.id =
-    if T.RegionId.Set.mem rid fixed_ids.rids then rid
-    else
-      match T.RegionId.Map.find_opt rid !region_map with
-      | Some rid -> rid
+  let fp = compute_fixed_point ctx0 max_num_iter max_num_iter in
+
+  (* Make sure we have exactly one loop abstraction per function region (merge
+     abstractions accordingly) *)
+  let fp =
+    (* List the loop abstractions in the fixed-point, and set all the abstractions
+       as endable *)
+    let fp_aids, add_aid, _mem_aid = V.AbstractionId.Set.mk_stateful_set () in
+
+    let list_loop_abstractions =
+      object
+        inherit [_] C.map_eval_ctx as super
+
+        method! visit_abs env abs =
+          match abs.kind with
+          | Loop (loop_id', _) ->
+              assert (loop_id' = loop_id);
+              add_aid abs.abs_id;
+              { abs with can_end = true }
+          | _ -> super#visit_abs env abs
+      end
+    in
+    let fp = list_loop_abstractions#visit_eval_ctx () fp in
+
+    (* For every input region group:
+     * - evaluate until we get to a [return]
+     * - end the input abstraction corresponding to the input region group
+     * - find which loop abstractions end at that moment
+     *
+     * [fp_ended_aids] links region groups to sets of ended abstractions.
+     *)
+    let fp_ended_aids = ref T.RegionGroupId.Map.empty in
+    let add_ended_aids (rg_id : T.RegionGroupId.id)
+        (aids : V.AbstractionId.Set.t) : unit =
+      match T.RegionGroupId.Map.find_opt rg_id !fp_ended_aids with
       | None ->
-          let nrid = C.fresh_region_id () in
-          region_map := T.RegionId.Map.add rid nrid !region_map;
-          nrid
+          fp_ended_aids := T.RegionGroupId.Map.add rg_id aids !fp_ended_aids
+      | Some aids' ->
+          let aids = V.AbstractionId.Set.union aids aids' in
+          fp_ended_aids := T.RegionGroupId.Map.add rg_id aids !fp_ended_aids
+    in
+    let cf_loop : st_m_fun =
+     fun res ctx ->
+      match res with
+      | Continue _ | Panic ->
+          (* We don't want to generate anything *)
+          None
+      | Break _ ->
+          (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *)
+          raise (Failure "Unreachable")
+      | Unit | EndEnterLoop | EndContinue ->
+          (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
+             For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
+          *)
+          raise (Failure "Unreachable")
+      | Return ->
+          (* Should we consume the return value and pop the frame?
+           * If we check in [Interpreter] that the loop abstraction we end is
+           * indeed the correct one, I think it is sound to under-approximate here
+           * (and it shouldn't make any difference).
+           *)
+          let _ =
+            List.iter
+              (fun rg_id ->
+                (* Lookup the input abstraction - we use the fact that the
+                   abstractions should have been introduced in a specific
+                   order (and we check that it is indeed the case) *)
+                let abs_id =
+                  V.AbstractionId.of_int (T.RegionGroupId.to_int rg_id)
+                in
+                let abs = C.ctx_lookup_abs ctx abs_id in
+                assert (abs.kind = V.SynthInput rg_id);
+                (* End this abstraction *)
+                let ctx =
+                  InterpreterBorrows.end_abstraction_no_synth config abs_id ctx
+                in
+                (* Explore the context, and check which abstractions are not there anymore *)
+                let ids = compute_context_ids ctx in
+                let ended_ids = V.AbstractionId.Set.diff !fp_aids ids.aids in
+                add_ended_aids rg_id ended_ids)
+              ctx.region_groups
+          in
+          (* We don't want to generate anything *)
+          None
+    in
+    let _ = eval_loop_body cf_loop fp in
+
+    (* Check that the sets of abstractions we need to end per region group are pairwise
+     * disjoint *)
+    let aids_union = ref V.AbstractionId.Set.empty in
+    let _ =
+      T.RegionGroupId.Map.iter
+        (fun _ ids ->
+          assert (V.AbstractionId.Set.disjoint !aids_union ids);
+          aids_union := V.AbstractionId.Set.union ids !aids_union)
+        !fp_ended_aids
+    in
+    assert (!aids_union = !fp_aids);
+
+    (* Merge the abstractions which need to be merged *)
+    let fp = ref fp in
+    let _ =
+      T.RegionGroupId.Map.iter
+        (fun rg_id ids ->
+          let ids = V.AbstractionId.Set.elements ids in
+          (* Retrieve the first id of the group *)
+          match ids with
+          | [] ->
+              (* This would be rather unexpected... let's fail for now to see
+                 in which situations this happens *)
+              raise (Failure "Unexpected")
+          | id0 :: ids ->
+              let id0 = ref id0 in
+              (* Add the proper region group into the abstraction *)
+              let abs_kind = V.Loop (loop_id, Some rg_id) in
+              let abs = C.ctx_lookup_abs !fp !id0 in
+              let abs = { abs with V.kind = abs_kind } in
+              let fp', _ = C.ctx_subst_abs !fp !id0 abs in
+              fp := fp';
+              (* Merge all the abstractions into this one *)
+              List.iter
+                (fun id ->
+                  try
+                    let fp', id0' =
+                      merge_abstractions loop_id abs_kind false !fp !id0 id
+                    in
+                    fp := fp';
+                    id0 := id0';
+                    ()
+                  with ValueMatchFailure _ -> raise (Failure "Unexpected"))
+                ids)
+        !fp_ended_aids
+    in
+
+    (* Reset the loop abstracions as not endable *)
+    let list_loop_abstractions (remove_rg_id : bool) =
+      object
+        inherit [_] C.map_eval_ctx as super
+
+        method! visit_abs env abs =
+          match abs.kind with
+          | Loop (loop_id', _) ->
+              assert (loop_id' = loop_id);
+              let kind =
+                if remove_rg_id then V.Loop (loop_id, None) else abs.kind
+              in
+              { abs with can_end = false; kind }
+          | _ -> super#visit_abs env abs
+      end
+    in
+    let update_kinds_can_end (remove_rg_id : bool) ctx =
+      (list_loop_abstractions remove_rg_id)#visit_eval_ctx () ctx
+    in
+    let fp = update_kinds_can_end false !fp in
+
+    (* Check that we still have a fixed point - we simply call [compute_fixed_point]
+       while allowing exactly one iteration to see if it fails *)
+    let _ = compute_fixed_point (update_kinds_can_end true fp) 1 1 in
+
+    (* Return *)
+    fp
   in
+  let fixed_ids = compute_fixed_ids (Option.get !ctx_upon_entry) fp in
+
+  (* Return *)
+  (fp, fixed_ids)
+
+(*
+(** Introduce region groups in the loop abstractions.
+
+    Initially, the new abstractions in the fixed-point have no region group.
+    We want each one of them to have a unique region group (because we will
+    translate each one of those abstractions to a pair forward
+    function/backward function).
+ *)
+let ctx_add_loop_region_groups (loop_id : V.LoopId.id) (fp : C.eval_ctx) :
+    C.eval_ctx =
+  let _, fresh_rid = T.RegionGroupId.fresh_stateful_generator () in
+
   let introduce_fresh_rids =
     object
       inherit [_] C.map_eval_ctx
-      method! visit_region_id _ rid = get_rid rid
+
+      method! visit_abs _ abs =
+        match abs.kind with
+        | Loop (loop_id', rg_id) ->
+            assert (loop_id' = loop_id);
+            assert (rg_id = None);
+            let rg_id = Some (fresh_rid ()) in
+            let kind = V.Loop (loop_id, rg_id) in
+            { abs with V.kind }
+        | _ -> abs
     end
   in
   let fp_env = List.rev (introduce_fresh_rids#visit_env () (List.rev fp.env)) in
   let fp = { fp with env = fp_env } in
-  (fp, fixed_ids)
+  fp
+ *)
 
 (** Split an environment between the fixed abstractions, values, etc. and
     the new abstractions, values, etc.
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 082a81ba..be154539 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -8,6 +8,7 @@ module E = Expressions
 module C = Contexts
 module A = LlbcAst
 module L = Logging
+open Utils
 open LlbcAstUtils
 
 let log = L.pre_passes_log
@@ -55,6 +56,8 @@ let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
     merge branches during the symbolic execution in some quite common cases
     where doing a merge is actually not necessary and leads to an ugly translation.
 
+    TODO: this is useless
+
     For instance, it performs the following transformation:
     {[
       if b {
@@ -145,8 +148,119 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
       ^ "\n"));
   f
 
+(** This pass restructures the control-flow by inserting all the statements
+    which occur after loops *inside* the loops, thus removing the need to
+    have breaks (we later check that we removed all the breaks).
+
+    This is needed because of the way we perform the symbolic execution
+    on the loops for now.
+
+    Rem.: we check that there are no nested loops (all the breaks must break
+    to the first outer loop, and the statements we insert inside the loops
+    mustn't contain breaks themselves).
+
+    For instance, it performs the following transformation:
+    {[
+      loop {
+        if b {
+          ...
+          continue 0;
+        }
+        else {
+          ...
+          break 0;
+        }
+      };
+      x := x + 1;
+      return;
+
+      ~~>
+
+      loop {
+        if b {
+          ...
+          continue 0;
+        }
+        else {
+          ...
+          x := x + 1;
+          return;
+        }
+      };
+    ]}
+ *)
+let remove_loop_breaks (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
+  let f0 = f in
+
+  (* Check that a statement doesn't contain loops, breaks or continues *)
+  let statement_has_no_loop_break_continue (st : A.statement) : bool =
+    let obj =
+      object
+        inherit [_] A.iter_statement
+        method! visit_Loop _ _ = raise Found
+        method! visit_Break _ _ = raise Found
+        method! visit_Continue _ _ = raise Found
+      end
+    in
+    try
+      obj#visit_statement () st;
+      true
+    with Found -> false
+  in
+
+  (* Replace a break statement with another statement (we check that the
+     break statement breaks exactly one level, and that there are no nested
+     loops.
+  *)
+  let replace_breaks_with (st : A.statement) (nst : A.statement) : A.statement =
+    let obj =
+      object
+        inherit [_] A.map_statement as super
+
+        method! visit_Loop entered_loop loop =
+          assert (not entered_loop);
+          super#visit_Loop true loop
+
+        method! visit_Break _ i =
+          assert (i = 0);
+          nst.content
+      end
+    in
+    obj#visit_statement false st
+  in
+
+  (* The visitor *)
+  let obj =
+    object
+      inherit [_] A.map_statement as super
+
+      method! visit_Sequence env st1 st2 =
+        match st1.content with
+        | Loop _ ->
+            assert (statement_has_no_loop_break_continue st2);
+            (replace_breaks_with st1 st2).content
+        | _ -> super#visit_Sequence env st1 st2
+    end
+  in
+
+  (* Map  *)
+  let body =
+    match f.body with
+    | Some body -> Some { body with body = obj#visit_statement () body.body }
+    | None -> None
+  in
+  let f = { f with body } in
+  log#ldebug
+    (lazy
+      ("Before/after [remove_loop_breaks]:\n"
+      ^ Print.Crate.crate_fun_decl_to_string crate f0
+      ^ "\n\n"
+      ^ Print.Crate.crate_fun_decl_to_string crate f
+      ^ "\n"));
+  f
+
 let apply_passes (crate : A.crate) : A.crate =
-  let passes = [ remove_useless_cf_merges crate ] in
+  let passes = [ remove_loop_breaks crate ] in
   let functions =
     List.fold_left (fun fl pass -> List.map pass fl) crate.functions passes
   in
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 6af59087..e737103a 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -920,9 +920,29 @@ type abs_kind =
 
           See the explanations for [SynthInput].
        *)
-  | Loop of LoopId.id  (** The abstraction corresponds to a loop *)
+  | Loop of (LoopId.id * RegionGroupId.id option)
+      (** The abstraction corresponds to a loop.
+
+          The region group id is initially [None].
+          After we computed a fixed point, we give a unique region group
+          identifier for each loop abstraction.
+       *)
 [@@deriving show, ord]
 
+(** Ancestor for {!abs} iter visitor *)
+class ['self] iter_abs_base =
+  object (_self : 'self)
+    inherit [_] iter_typed_avalue
+    method visit_abs_kind : 'env -> abs_kind -> unit = fun _ _ -> ()
+  end
+
+(** Ancestor for {!abs} map visitor *)
+class ['self] map_abs_base =
+  object (_self : 'self)
+    inherit [_] map_typed_avalue
+    method visit_abs_kind : 'env -> abs_kind -> abs_kind = fun _ x -> x
+  end
+
 (** Abstractions model the parts in the borrow graph where the borrowing relations
     have been abstracted because of a function call.
     
@@ -931,8 +951,8 @@ type abs_kind =
 *)
 type abs = {
   abs_id : abstraction_id;
-  kind : (abs_kind[@opaque]);
-  can_end : (bool[@opaque]);
+  kind : abs_kind;
+  can_end : bool;
       (** Controls whether the region can be ended or not.
           
           This allows to "pin" some regions, and is useful when generating
@@ -959,7 +979,7 @@ type abs = {
       {
         name = "iter_abs";
         variety = "iter";
-        ancestors = [ "iter_typed_avalue" ];
+        ancestors = [ "iter_abs_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
@@ -967,7 +987,7 @@ type abs = {
       {
         name = "map_abs";
         variety = "map";
-        ancestors = [ "map_typed_avalue" ];
+        ancestors = [ "map_abs_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]