From 49c8e42ec3bcfc323e61c5ba0345abeb41372ac4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 14:50:21 +0200
Subject: Implement a BorrowCheck.borrow_check_crate

---
 compiler/Interpreter.ml | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index fb3701f3..81d6ff72 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -489,9 +489,13 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
     - the list of symbolic values introduced for the input values (this is
       useful for the synthesis)
     - the symbolic AST generated by the symbolic execution
+
+   If [synthesize] is [true]: we synthesize the symbolic AST that is used for
+   the translation. Otherwise, we do not (the symbolic execution then simply
+   borrow-checks the function).
  *)
-let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
-    symbolic_value list * SA.expression =
+let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
+    (fdef : fun_decl) : symbolic_value list * SA.expression option =
   (* Debug *)
   let name_to_string () =
     Print.Types.name_to_string
@@ -615,9 +619,13 @@ let evaluate_function_symbolic (ctx : decls_ctx) (fdef : fun_decl) :
       let ctx_resl, cc =
         eval_function_body config (Option.get fdef.body).body ctx
       in
-      let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
-      cc el
-    with CFailure (span, msg) -> Error (span, msg)
+      if synthesize then
+        (* Finish synthesizing *)
+        let el = List.map (fun (ctx, res) -> finish res ctx) ctx_resl in
+        Some (cc el)
+      else None
+    with CFailure (span, msg) ->
+      if synthesize then Some (Error (span, msg)) else None
   in
   (* Return *)
   (input_svs, symbolic)
-- 
cgit v1.2.3


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 ++++++++++++++++++++++++++++++------
 1 file changed, 30 insertions(+), 6 deletions(-)

(limited to 'compiler/Interpreter.ml')

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
-- 
cgit v1.2.3