Implement a BorrowCheck.borrow_check_crate

6 files changed, 54 insertions, 10 deletions

diff --git a/compiler/BorrowCheck.ml b/compiler/BorrowCheck.ml
new file mode 100644
index 00000000..52f42c37
--- /dev/null
+++ b/compiler/BorrowCheck.ml
@@ -0,0 +1,28 @@
+open Interpreter
+open LlbcAst
+
+(** The local logger *)
+let log = Logging.borrow_check_log
+
+(** Borrow-check a crate.
+
+    Note that we don't return anything: if we find borrow-checking errors,
+    we register them and print them later.
+ *)
+let borrow_check_crate (crate : crate) : unit =
+  (* Debug *)
+  log#ldebug (lazy "translate_crate_to_pure");
+
+  (* Compute the translation context *)
+  let trans_ctx = compute_contexts crate in
+
+  (* Borrow-check *)
+  let borrow_check_fun (fdef : fun_decl) : unit =
+    match fdef.body with
+    | None -> ()
+    | Some _ ->
+        let synthesize = false in
+        let _ = evaluate_function_symbolic synthesize trans_ctx fdef in
+        ()
+  in
+  List.iter borrow_check_fun (FunDeclId.Map.values crate.fun_decls)
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)
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 9b8019b2..620c5fb5 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -15,6 +15,9 @@ let regions_hierarchy_log = L.get_logger "MainLogger.RegionsHierarchy"
 (** Logger for Translate *)
 let translate_log = L.get_logger "MainLogger.Translate"
 
+(** Logger for BorrowCheck *)
+let borrow_check_log = L.get_logger "MainLogger.BorrowCheck"
+
 (** Logger for Contexts *)
 let contexts_log = L.get_logger "MainLogger.Contexts"
 
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 557a3993..1bf9196a 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -309,8 +309,9 @@ let () =
          (* Test the unit functions with the concrete interpreter *)
          if !test_unit_functions then Test.test_unit_functions m;
 
-         (* Translate the functions *)
-         Aeneas.Translate.translate_crate filename dest_dir m
+         (* Translate or borrow-check the crate *)
+         if !borrow_check then Aeneas.BorrowCheck.borrow_check_crate m
+         else Aeneas.Translate.translate_crate filename dest_dir m
        with Errors.CFailure (_, _) ->
          (* In theory it shouldn't happen, but there may be uncaught errors -
             note that we let the [Failure] exceptions go through (they are
@@ -323,7 +324,9 @@ let () =
           (* Reverse the list of error messages so that we print them from the
              earliest to the latest. *)
           (List.rev !Errors.error_list);
-        exit 1);
+        exit 1)
+      else if !borrow_check then
+        log#linfo (lazy "Crate successfully borrow-checked");
 
       (* Print total elapsed time *)
       log#linfo
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 690bff5c..2bc9bb25 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -31,8 +31,9 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
   | None -> None
   | Some _ ->
       (* Evaluate *)
-      let inputs, symb = evaluate_function_symbolic trans_ctx fdef in
-      Some (inputs, symb)
+      let synthesize = true in
+      let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
+      Some (inputs, Option.get symb)
 
 (** Translate a function, by generating its forward and backward translations.
 
diff --git a/compiler/dune b/compiler/dune
index 6bdfd153..f987faec 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -14,6 +14,7 @@
  (modules
   AssociatedTypes
   Assumed
+  BorrowCheck
   Collections
   Config
   ConstStrings