summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-12-09 16:51:40 +0100
committerSon HO2023-02-03 11:21:46 +0100
commite6edaac99fc38fc3cb574db06fe83c7eb32ef37b (patch)
tree8d609e91a58ae729401ff6efb2450e41103367f6
parentc86ecc916f9493bf312aa3f156e07da3bc415e77 (diff)
Merge loop abs so that there is one abs per function input region group
Diffstat (limited to '')
-rw-r--r--compiler/Contexts.ml1
-rw-r--r--compiler/Interpreter.ml11
-rw-r--r--compiler/InterpreterLoops.ml283
-rw-r--r--compiler/PrePasses.ml116
-rw-r--r--compiler/Values.ml30
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;
}]