Let the runner choose which backends to use

2 files changed, 28 insertions, 43 deletions

diff --git a/Makefile b/Makefile
index 0ceaa558..506dec5e 100644
--- a/Makefile
+++ b/Makefile
@@ -117,7 +117,7 @@ test: build-dev test-all
 test-all: \
 	test-arrays \
 	test-betree_main \
-	tfstar-betree_main-special \
+	test-betree_main-special \
 	test-bitwise \
 	test-constants \
 	test-demo \
@@ -154,9 +154,6 @@ else
 CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$*
 endif
 
-# The command to run Aeneas on the proper llbc file
-AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS)
-
 # Generic rules to extract the LLBC from a rust file
 # We use the rules in Charon's Makefile to generate the .llbc files: the options
 # vary with the test files.
@@ -164,34 +161,14 @@ AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKE
 gen-llbc-%:
 	$(CHARON_CMD)
 
-# Generic rules to test the translation of an LLBC file.
+# Translate the given llbc file to available backends. The test runner decides
+# which backends to use and sets test-specific options.
 .PHONY: test-%
 test-%: FILE = $*
-test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
+test-%: gen-llbc-%
+	$(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(OPTIONS)
 	echo "# Test $* done"
 
-.PHONY: tfstar-%
-tfstar-%: BACKEND := fstar
-tfstar-%:
-	$(AENEAS_CMD)
-
-.PHONY: tcoq-%
-tcoq-%: BACKEND := coq
-tcoq-%:
-	$(AENEAS_CMD)
-
-.PHONY: tlean-%
-tlean-%: BACKEND := lean
-tlean-%:
-	$(AENEAS_CMD)
-
-# TODO: reactivate HOL4 once traits are parameterized by their associated types
-.PHONY: thol4-%
-thol4-%: BACKEND := hol4
-thol4-%:
-	echo Ignoring the $* test for HOL4
-#	$(AENEAS_CMD)
-
 # Nix - TODO: add the lean tests
 .PHONY: nix
 nix:
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 1ec2d1c8..52619c4a 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -116,20 +116,28 @@ 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 :: backend :: options ->
-      let subdir = test_subdir backend test_name in
-      let options = List.append (test_options backend test_name) options in
-
-      let test_file_name =
+  | _exe_path :: 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 =
         match test_name with
-        | "betree_main-special" -> "betree_main"
-        | _ -> test_name
+        | "betree_main-special" -> [ "fstar" ]
+        | _ -> [ "coq"; "lean"; "fstar" ]
       in
-      run_test { aeneas_path; llbc_dir }
-        {
-          name = test_file_name;
-          backend;
-          subdir;
-          extra_aeneas_options = options;
-        }
-  | _ -> ()
+      List.iter
+        (fun backend ->
+          let subdir = test_subdir backend test_name in
+          let extra_aeneas_options =
+            List.append (test_options backend test_name) options
+          in
+          let test_file_name =
+            match test_name with
+            | "betree_main-special" -> "betree_main"
+            | _ -> test_name
+          in
+          let test_case =
+            { name = test_file_name; backend; subdir; extra_aeneas_options }
+          in
+          run_test tests_env test_case)
+        backends
+  | _ -> failwith "Incorrect options passed to test runner"