summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/InterpreterLoops.ml26
1 files changed, 14 insertions, 12 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 027db03e..c55d0853 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -246,7 +246,7 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
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, None, V.LoopSynthInput) in
- let can_end = false in
+ let can_end = true in
let destructure_shared_values = true in
let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
not (V.AbstractionId.Set.mem id old_abs_ids)
@@ -337,7 +337,7 @@ let collapse_ctx (loop_id : V.LoopId.id)
^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n"));
let abs_kind = V.Loop (loop_id, None, LoopSynthInput) in
- let can_end = false in
+ let can_end = true in
let destructure_shared_values = true in
let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
not (V.AbstractionId.Set.mem id old_ids.aids)
@@ -967,7 +967,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
{
V.abs_id = C.fresh_abstraction_id ();
kind = V.Loop (S.loop_id, None, LoopSynthInput);
- can_end = false;
+ can_end = true;
parents = V.AbstractionId.Set.empty;
original_parents = [];
regions = T.RegionId.Set.singleton rid;
@@ -1021,7 +1021,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
{
V.abs_id = C.fresh_abstraction_id ();
kind = V.Loop (S.loop_id, None, LoopSynthInput);
- can_end = false;
+ can_end = true;
parents = V.AbstractionId.Set.empty;
original_parents = [];
regions = T.RegionId.Set.singleton rid;
@@ -1125,7 +1125,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
| None ->
(* Convert the value to an abstraction *)
let abs_kind = V.Loop (S.loop_id, None, LoopSynthInput) in
- let can_end = false in
+ let can_end = true in
let destructure_shared_values = true in
let absl =
convert_value_to_abstractions abs_kind can_end
@@ -2256,8 +2256,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
the shared values) will be preserved.
*)
let fp =
- (* List the loop abstractions in the fixed-point, and set all the abstractions
- as endable *)
+ (* List the loop abstractions in the fixed-point *)
let fp_aids, add_aid, _mem_aid = V.AbstractionId.Set.mk_stateful_set () in
let list_loop_abstractions =
@@ -2269,8 +2268,10 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
| Loop (loop_id', _, kind) ->
assert (loop_id' = loop_id);
assert (kind = V.LoopSynthInput);
+ (* The abstractions introduced so far should be endable *)
+ assert (abs.can_end = true);
add_aid abs.abs_id;
- { abs with can_end = true }
+ abs
| _ -> abs
end
in
@@ -2389,8 +2390,8 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
!fp_ended_aids
in
- (* Reset the loop abstracions as not endable *)
- let list_loop_abstractions (remove_rg_id : bool) =
+ (* Reset the loop abstracions as not endable, and update their kinds *)
+ let update_loop_abstractions (remove_rg_id : bool) =
object
inherit [_] C.map_eval_ctx
@@ -2408,7 +2409,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
end
in
let update_kinds_can_end (remove_rg_id : bool) ctx =
- (list_loop_abstractions remove_rg_id)#visit_eval_ctx () ctx
+ (update_loop_abstractions remove_rg_id)#visit_eval_ctx () ctx
in
let fp = update_kinds_can_end false !fp in
@@ -3050,8 +3051,9 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
| V.Loop (loop_id', rg_id, kind) ->
assert (loop_id' = loop_id);
assert (kind = V.LoopSynthInput);
+ let can_end = false in
let kind = V.Loop (loop_id, rg_id, V.LoopCall) in
- let abs = { abs with kind } in
+ let abs = { abs with kind; can_end } in
super#visit_abs env abs
| _ -> super#visit_abs env abs
end