Merge pull request #233 from AeneasVerif/son/borrow-check

Add a `-borrow-check` option

1 files changed, 20 insertions, 9 deletions

diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 735f3743..3760d15a 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,10 +680,13 @@ 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.
+       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
@@ -779,9 +782,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 +801,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