Use runner to generate llbc

3 files changed, 126 insertions, 84 deletions

diff --git a/Makefile b/Makefile
index b9aaf97c..fccca9b1 100644
--- a/Makefile
+++ b/Makefile
@@ -19,8 +19,7 @@ TEST_RUNNER_EXE ?= $(PWD)/bin/test_runner
 CHARON_EXE ?= $(PWD)/charon/bin/charon
 
 # The user can specify additional translation options for Aeneas.
-# In CI we activate the (expensive) sanity checks.
-OPTIONS ?=
+AENEAS_OPTIONS ?=
 CHARON_OPTIONS ?=
 
 # The directory thta contains the rust source files for tests.
@@ -28,7 +27,7 @@ INPUTS_DIR ?= tests/src
 # The directory where to look for the .llbc files.
 LLBC_DIR ?= $(PWD)/tests/llbc
 
-# In CI, we enforce formatting and we don't regenerate llbc files.
+# In CI, we enforce formatting and activate the (expensive) sanity checks.
 IN_CI ?=
 
 ####################################
@@ -169,53 +168,19 @@ verify:
 
 ifdef IN_CI
 # In CI we do extra sanity checks.
-test-%: OPTIONS += -checks
+test-%: AENEAS_OPTIONS += -checks
+else
+test-%: check-charon
 endif
 
-# Translate the given llbc file to available backends. The test runner decides
+# Translate the given rust file to available backends. The test runner decides
 # which backends to use and sets test-specific options.
 .PHONY: test-%
-test-%: TEST_NAME = $*
-test-%: $(LLBC_DIR)/%.llbc
-	$(TEST_RUNNER_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(TEST_NAME) $(OPTIONS)
+test-%:
+	$(TEST_RUNNER_EXE) charon $(CHARON_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(CHARON_OPTIONS)
+	$(TEST_RUNNER_EXE) aeneas $(AENEAS_EXE) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS)
 	echo "# Test $* done"
 
-#  List the `.rs` files in `$(INPUTS_DIR)/`
-INDIVIDUAL_RUST_SRCS = $(wildcard $(INPUTS_DIR)/*.rs)
-# We test all rust files except this one.
-INDIVIDUAL_RUST_SRCS := $(filter-out $(INPUTS_DIR)/hashmap_utils.rs, $(INDIVIDUAL_RUST_SRCS))
-# List the corresponding llbc files.
-INDIVIDUAL_LLBCS := $(subst $(INPUTS_DIR)/,$(LLBC_DIR)/,$(patsubst %.rs,%.llbc,$(INDIVIDUAL_RUST_SRCS)))
-
-.PHONY: generate-llbc
-# This depends on `llbc/<file>.llbc` for each `$(INPUTS_DIR)/<file>.rs` we care about, plus the whole-crate test.
-generate-llbc: $(INDIVIDUAL_LLBCS) $(LLBC_DIR)/betree_main.llbc
-
-$(LLBC_DIR)/hashmap_main.llbc: CHARON_OPTIONS += --opaque=hashmap_utils
-$(LLBC_DIR)/nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication
-$(LLBC_DIR)/no_nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication
-$(LLBC_DIR)/paper.llbc: CHARON_OPTIONS += --no-code-duplication
-$(LLBC_DIR)/constants.llbc: CHARON_OPTIONS += --no-code-duplication
-$(LLBC_DIR)/external.llbc: CHARON_OPTIONS += --no-code-duplication
-$(LLBC_DIR)/polonius_list.llbc: CHARON_OPTIONS += --polonius
-# Possible to add `--no-code-duplication` if we use the optimized MIR
-$(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main
-
-ifndef IN_CI
-$(LLBC_DIR)/%.llbc: check-charon
-
-$(LLBC_DIR)/%.llbc:
-	$(CHARON_EXE) --no-cargo --input $(INPUTS_DIR)/$*.rs --crate $* $(CHARON_OPTIONS) --dest $(LLBC_DIR)
-# Special rule for the whole-crate test.
-$(LLBC_DIR)/betree_main.llbc:
-	cd $(INPUTS_DIR)/betree && $(CHARON_EXE) $(CHARON_OPTIONS) --dest $(LLBC_DIR)
-else
-$(LLBC_DIR)/%.llbc:
-	@echo 'ERROR: llbc files should be built separately in CI'
-	@false
-endif
-
-
 # =============================================================================
 # Nix
 # =============================================================================
diff --git a/flake.nix b/flake.nix
index 26689af0..9c918ff9 100644
--- a/flake.nix
+++ b/flake.nix
@@ -80,6 +80,9 @@
           OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors.
         };
 
+        # This test is a full crate with dependencies. We generate the
+        # corresponding llbc file here; this function takes care of cargo
+        # dependencies for us.
         betree-llbc = charon.extractCrateWithCharon.${system} {
           name = "betree";
           src = ./tests/src/betree;
@@ -89,22 +92,6 @@
             ./target/debug/betree
           '';
         };
-        input-llbcs = pkgs.runCommand "input-llbcs"
-          {
-            src = ./tests/src;
-            makefile = ./Makefile;
-            buildInputs = [ charon.packages.${system}.rustToolchain charon.packages.${system}.charon ];
-          } ''
-          # Copy the betree output file
-          mkdir -p $out
-          cp ${betree-llbc}/llbc/betree_main.llbc $out
-
-          mkdir tests
-          cp -r $src tests/src
-          cp $makefile Makefile
-          # Generate the llbc files
-          CHARON_EXE="charon" INPUTS_DIR="tests/src" LLBC_DIR="$out" make generate-llbc
-        '';
 
         # Run the translation on various files.
         # Make sure we don't need to recompile the package whenever we make
@@ -118,19 +105,25 @@
               path == toString ./Makefile
               || pkgs.lib.hasPrefix (toString ./compiler) path
               || pkgs.lib.hasPrefix (toString ./backends) path
-              || pkgs.lib.hasPrefix (toString ./tests) path;
+              || (pkgs.lib.hasPrefix (toString ./tests) path
+              && !pkgs.lib.hasSuffix ".llbc" path);
           };
+          buildInputs = [ charon.packages.${system}.rustToolchain ];
           buildPhase = ''
-            export LLBC_DIR=${input-llbcs}
             export AENEAS_EXE=${aeneas}/bin/aeneas
+            export CHARON_EXE=${charon.packages.${system}.charon}/bin/charon
             export TEST_RUNNER_EXE=${test_runner}/bin/test_runner
 
+            mkdir llbc
+            export LLBC_DIR=llbc
+            # Copy over the llbc file we can't generate ourselves.
+            cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR
+
             # Copy the tests
             cp -r tests tests-copy
+            make clean-generated-aeneas
 
             # Run the tests with extra sanity checks enabled
-            # Remark: we could remove the file
-            make clean-generated-aeneas
             IN_CI=1 make test-all -j $NIX_BUILD_CORES
 
             # Check that there are no differences between the generated tests
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"