Use runner to generate llbc

1 files changed, 104 insertions, 20 deletions

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 8b4a4208..d80231d0 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,26 +1,26 @@
 (* Paths to use for tests *)
-type test_env = { aeneas_path : string; llbc_dir : string }
+type aeneas_env = { aeneas_path : string; llbc_dir : string }
 
-(* The data for a specific test to run *)
-type test_case = {
+type charon_env = {
+  charon_path : string;
+  inputs_dir : string;
+  llbc_dir : string;
+}
+
+(* The data for a specific test to run aeneas on *)
+type aeneas_test_case = {
   name : string;
   backend : string;
   subdir : string;
   extra_aeneas_options : string list;
 }
 
-(* Run Aeneas on a specific input with the given options *)
-let run_test env case =
-  let concat_path = List.fold_left Filename.concat "" in
-  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
-  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
-  let args =
-    [|
-      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
-    |]
-  in
-  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
+(* The data for a specific test to generate llbc for *)
+type charon_test_case = { name : string; extra_charon_options : string list }
 
+let concat_path = List.fold_left Filename.concat ""
+
+let run_command args =
   (* Debug arguments *)
   print_string "[test_runner] Running: ";
   Array.iter
@@ -30,15 +30,66 @@ let run_test env case =
     args;
   print_endline "";
 
-  (* Run Aeneas *)
+  (* Run the command *)
   let pid =
-    Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+    Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr
   in
   let _ = Unix.waitpid [] pid in
   ()
 
+(* Run Aeneas on a specific input with the given options *)
+let run_aeneas (env : aeneas_env) (case : aeneas_test_case) =
+  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
+  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
+  let args =
+    [|
+      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
+    |]
+  in
+  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
+  (* Run Aeneas *)
+  run_command args
+
+(* Run Charon on a specific input with the given options *)
+let run_charon (env : charon_env) (case : charon_test_case) =
+  let input_crate = concat_path [ env.inputs_dir; case.name ] in
+  let input_file = input_crate ^ ".rs" in
+  if Sys.file_exists input_file then
+    let args =
+      [|
+        env.charon_path;
+        "--no-cargo";
+        "--input";
+        input_file;
+        "--crate";
+        case.name;
+        "--dest";
+        env.llbc_dir;
+      |]
+    in
+    let args = Array.append args (Array.of_list case.extra_charon_options) in
+    (* Run Charon on the rust file *)
+    run_command args
+  else if Sys.file_exists input_crate then
+    match Sys.getenv_opt "IN_CI" with
+    | None ->
+        let args = [| env.charon_path; "--dest"; env.llbc_dir |] in
+        let args =
+          Array.append args (Array.of_list case.extra_charon_options)
+        in
+        (* Run Charon inside the crate *)
+        Unix.chdir input_crate;
+        run_command args
+    | Some _ ->
+        (* Crates with dependencies must be generated separately in CI. We skip
+           here and trust that CI takes care to generate the necessary llbc
+           file. *)
+        print_endline
+          "Warn: IN_CI is set; we skip generating llbc files for whole crates"
+  else failwith ("Neither " ^ input_file ^ " nor " ^ input_crate ^ " exist.")
+
 (* File-specific options *)
-let test_options backend test_name =
+let aeneas_options_for_test backend test_name =
   (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
   let use_fuel =
     match (backend, test_name) with
@@ -92,6 +143,27 @@ let test_options backend test_name =
   let options = List.append extra_options options in
   options
 
+(* File-specific options *)
+let charon_options_for_test test_name =
+  (* Possible to add `--no-code-duplication` for `hashmap_main` if we use the optimized MIR *)
+  let no_code_dup =
+    match test_name with
+    | "constants" | "external" | "nested_borrows" | "no_nested_borrows"
+    | "paper" ->
+        [ "--no-code-duplication" ]
+    | _ -> []
+  in
+  let extra_options =
+    (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *)
+    match test_name with
+    | "betree_main" ->
+        [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
+    | "hashmap_main" -> [ "--opaque=hashmap_utils" ]
+    | "polonius_list" -> [ "--polonius" ]
+    | _ -> []
+  in
+  List.append no_code_dup extra_options
+
 (* The subdirectory in which to store the outputs. *)
 (* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *)
 let test_subdir backend test_name =
@@ -111,7 +183,7 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options ->
+  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_name :: options ->
       let tests_env = { aeneas_path; llbc_dir } in
       (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
       let backends = [ "coq"; "lean"; "fstar" ] in
@@ -119,11 +191,23 @@ let () =
         (fun backend ->
           let subdir = test_subdir backend test_name in
           let extra_aeneas_options =
-            List.append (test_options backend test_name) options
+            List.append (aeneas_options_for_test backend test_name) options
           in
           let test_case =
             { name = test_name; backend; subdir; extra_aeneas_options }
           in
-          run_test tests_env test_case)
+          run_aeneas tests_env test_case)
         backends
+  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name
+    :: options ->
+      let tests_env = { charon_path; inputs_dir; llbc_dir } in
+      let extra_charon_options =
+        List.append (charon_options_for_test test_name) options
+      in
+      (* FIXME: remove this special case *)
+      let test_name =
+        if test_name = "betree_main" then "betree" else test_name
+      in
+      let test_case = { name = test_name; extra_charon_options } in
+      run_charon tests_env test_case
   | _ -> failwith "Incorrect options passed to test runner"