From a6c9ab139977982f610f3d46e2e2f4c141880c3c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 16:12:15 +0200
Subject: Relax some constraints in the symbolic execution when borrow-checking

---
 compiler/InterpreterLoopsFixedPoint.ml | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 735f3743..0d770e80 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -665,8 +665,8 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
     in
     List.iter end_at_return (fst (eval_loop_body fp));
 
-    (* Check that the sets of abstractions we need to end per region group are pairwise
-     * disjoint *)
+    (* Check that the sets of abstractions we need to end per region group are
+       pairwise disjoint *)
     let aids_union = ref AbstractionId.Set.empty in
     let _ =
       RegionGroupId.Map.iter
@@ -680,8 +680,10 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
         !fp_ended_aids
     in
 
-    (* We also check that all the regions need to end - this is not necessary per
-       se, but if it doesn't happen it is bizarre and worth investigating... *)
+    (* If we generate a translation, we check that all the regions need to end
+       - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating...
+       We need this check for now for technical reasons to make the translation work.
+    *)
     sanity_check __FILE__ __LINE__
       (AbstractionId.Set.equal !aids_union !fp_aids)
       span;
@@ -779,9 +781,11 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
        no region group, and we set them as endable just above).
 
        If [remove_rg_id] is [false], we simply set the abstractions as non-endable
-       to freeze them (we will use the fixed point as starting point for the
-       symbolic execution of the loop body, and we have to make sure the input
-       abstractions are frozen).
+       **when generating a pure translation** to freeze them (we will use the
+       fixed point as starting point for the symbolic execution of the loop body,
+       and we have to make sure the input abstractions are frozen).
+       If we are simply borrow-checking the program, we can set the abstraction
+       as endable.
     *)
     let update_loop_abstractions (remove_rg_id : bool) =
       object
@@ -796,7 +800,13 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
                 if remove_rg_id then Loop (loop_id, None, LoopSynthInput)
                 else abs.kind
               in
-              { abs with can_end = remove_rg_id; kind }
+              (* If we borrow check we can always set the abstraction as
+                 endable. If we generate a pure translation we have a few
+                 more constraints. *)
+              let can_end =
+                if !Config.borrow_check then true else remove_rg_id
+              in
+              { abs with can_end; kind }
           | _ -> abs
       end
     in
-- 
cgit v1.2.3


From 0a0ab7c0e159e736a3187b8121d106ee76651f57 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 16:47:52 +0200
Subject: Relax more checks for borrow-checking

---
 compiler/InterpreterLoopsFixedPoint.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.ml')

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 0d770e80..3760d15a 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -683,9 +683,10 @@ let compute_loop_entry_fixed_point (config : config) (span : Meta.span)
     (* If we generate a translation, we check that all the regions need to end
        - this is not necessary per se, but if it doesn't happen it is bizarre and worth investigating...
        We need this check for now for technical reasons to make the translation work.
+       If we only borrow-check, we can ignore this.
     *)
     sanity_check __FILE__ __LINE__
-      (AbstractionId.Set.equal !aids_union !fp_aids)
+      (!Config.borrow_check || AbstractionId.Set.equal !aids_union !fp_aids)
       span;
 
     (* Merge the abstractions which need to be merged, and compute the map from
-- 
cgit v1.2.3