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/Interpreter.ml                | 36 ++++++++++++++++++++++++++++------
 compiler/InterpreterLoopsFixedPoint.ml | 26 ++++++++++++++++--------
 compiler/InterpreterLoopsMatchCtxs.ml  |  5 ++++-
 compiler/Print.ml                      |  3 ++-
 4 files changed, 54 insertions(+), 16 deletions(-)

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 81d6ff72..b2e55841 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -362,6 +362,11 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
       ctx)
     else ctx
   in
+  log#ldebug
+    (lazy
+      ("evaluate_function_symbolic_synthesize_backward_from_return: (after \
+        putting the return value in the proper abstraction)\n" ^ "\n- ctx:\n"
+      ^ Print.Contexts.eval_ctx_to_string ~span:(Some fdef.item_meta.span) ctx));
 
   (* We now need to end the proper *input* abstractions - pay attention
    * to the fact that we end the *input* abstractions, not the *return*
@@ -418,7 +423,28 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
                }
              ]}
           *)
-          (None, false)
+          (* If we are borrow-checking: end the synth input abstraction to
+             check there is no borrow-checking issue.
+             Otherwise, do nothing.
+
+             We need this check because of the following:
+             {[
+               fn loop_reborrow_mut1<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 {
+                   let mut x = 0;
+                   while x > 0 {
+                       x += 1;
+                   }
+                   if x > 0 {
+                       a
+                   } else {
+                       b // Failure
+                   }
+               }
+             ]}
+             (remark: this is slightly ad-hoc, and we won't need to do that
+              once we make the handling of loops more general).
+          *)
+          if !Config.borrow_check then (Some fun_abs_id, true) else (None, false)
       | Some abs -> (Some abs.abs_id, false)
   in
   log#ldebug
@@ -619,11 +645,9 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
       let ctx_resl, cc =
         eval_function_body config (Option.get fdef.body).body ctx
       in
-      if synthesize then
-        (* Finish synthesizing *)
-        let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
-        Some (cc el)
-      else None
+      let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
+      (* Finish synthesizing *)
+      if synthesize then Some (cc el) else None
     with CFailure (span, msg) ->
       if synthesize then Some (Error (span, msg)) else None
   in
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
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 3f7c023e..a1c0841a 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -1956,7 +1956,10 @@ let match_ctx_with_target (config : config) (span : Meta.span)
         | Loop (loop_id', rg_id, kind) ->
             sanity_check __FILE__ __LINE__ (loop_id' = loop_id) span;
             sanity_check __FILE__ __LINE__ (kind = LoopSynthInput) span;
-            let can_end = false in
+            (* If we borrow-check: we can set the abstractions as endable.
+               If we synthesize we have to constrain the region abstractions
+               a bit. *)
+            let can_end = !Config.borrow_check in
             let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in
             let abs = { abs with kind; can_end } in
             super#visit_abs env abs
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 7495d6bf..8bd709d0 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -309,13 +309,14 @@ module Values = struct
     let kind =
       if verbose then "[kind:" ^ abs_kind_to_string abs.kind ^ "]" else ""
     in
+    let can_end = if abs.can_end then "{endable}" else "{frozen}" in
     indent ^ "abs@"
     ^ AbstractionId.to_string abs.abs_id
     ^ kind ^ "{parents="
     ^ AbstractionId.Set.to_string None abs.parents
     ^ "}" ^ "{regions="
     ^ RegionId.Set.to_string None abs.regions
-    ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
+    ^ "}" ^ can_end ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}"
 
   let inst_fun_sig_to_string (env : fmt_env) (sg : LlbcAst.inst_fun_sig) :
       string =
-- 
cgit v1.2.3