Set all options in the test runner

2 files changed, 58 insertions, 51 deletions

diff --git a/Makefile b/Makefile
index 5e8fe7bb..0ceaa558 100644
--- a/Makefile
+++ b/Makefile
@@ -117,7 +117,7 @@ test: build-dev test-all
 test-all: \
 	test-arrays \
 	test-betree_main \
-	ctest-test-betree_main \
+	tfstar-betree_main-special \
 	test-bitwise \
 	test-constants \
 	test-demo \
@@ -157,47 +157,6 @@ endif
 # The command to run Aeneas on the proper llbc file
 AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS)
 
-# Add specific options to some tests
-# TODO: reactivate -test-trans-units for hashmap and hashmap_main
-tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files
-tcoq-arrays: OPTIONS += -use-fuel
-
-test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
-tfstar-betree_main: OPTIONS += -decreases-clauses -template-clauses
-tcoq-betree_main: OPTIONS += -use-fuel
-
-ctest-test-betree_main: OPTIONS += -test-trans-units -state -split-files
-ctest-test-betree_main: OPTIONS += -decreases-clauses -template-clauses
-
-test-bitwise: OPTIONS += -test-trans-units
-
-test-constants: OPTIONS += -test-trans-units
-
-tfstar-demo: OPTIONS += -use-fuel
-tcoq-demo: OPTIONS += -use-fuel
-
-test-external: OPTIONS += -test-trans-units -state -split-files
-
-test-hashmap: OPTIONS += -split-files
-tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
-tcoq-hashmap: OPTIONS += -use-fuel
-tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it
-
-test-hashmap_main: OPTIONS += -state -split-files
-tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
-tcoq-hashmap_main: OPTIONS += -use-fuel
-
-tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files
-tcoq-loops: OPTIONS += -use-fuel
-
-test-no_nested_borrows: OPTIONS += -test-trans-units
-
-test-paper: OPTIONS += -test-trans-units
-
-test-polonius_list: OPTIONS += -test-trans-units
-
-tfstar-traits: OPTIONS += -decreases-clauses -template-clauses
-
 # 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.
@@ -233,15 +192,6 @@ thol4-%:
 	echo Ignoring the $* test for HOL4
 #	$(AENEAS_CMD)
 
-# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`.
-# This generates very ugly code, but is good to test the translation.
-.PHONY: ctest-test-betree_main
-ctest-test-betree_main: test-betree_main
-ctest-test-betree_main: FILE = betree_main-special
-ctest-test-betree_main: BACKEND := fstar
-ctest-test-betree_main:
-	$(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 52ff7276..949d5307 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -21,6 +21,63 @@ let () =
         | _ -> test_name
       in
 
+      (* File-specific options *)
+      (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
+      let use_fuel =
+        match (backend, test_name) with
+        | ( "coq",
+            ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main"
+            | "loops" ) ) ->
+            true
+        | "fstar", "demo" -> true
+        | _ -> false
+      in
+      let options = if use_fuel then "-use-fuel" :: options else options in
+
+      let decrease_template_clauses =
+        backend = "fstar"
+        &&
+        match test_name with
+        | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
+        | "hashmap_main" | "loops" | "traits" ->
+            true
+        | _ -> false
+      in
+      let options =
+        if decrease_template_clauses then
+          "-decreases-clauses" :: "-template-clauses" :: options
+        else options
+      in
+
+      let extra_options =
+        match (backend, test_name) with
+        (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
+        (* This generates very ugly code, but is good to test the translation. *)
+        | _, "betree_main-special" ->
+            [ "-test-trans-units"; "-state"; "-split-files" ]
+        | _, "betree_main" ->
+            [
+              "-backward-no-state-update";
+              "-test-trans-units";
+              "-state";
+              "-split-files";
+            ]
+        | _, "bitwise" -> [ "-test-trans-units" ]
+        | _, "constants" -> [ "-test-trans-units" ]
+        | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ]
+        | _, "hashmap_main" -> [ "-state"; "-split-files" ]
+        | _, "no_nested_borrows" -> [ "-test-trans-units" ]
+        | _, "paper" -> [ "-test-trans-units" ]
+        | _, "polonius_list" -> [ "-test-trans-units" ]
+        | "fstar", "arrays" -> [ "-split-files" ]
+        | "fstar", "loops" -> [ "-split-files" ]
+        (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *)
+        | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ]
+        | _, "hashmap" -> [ "-split-files" ]
+        | _ -> []
+      in
+      let options = List.append extra_options options in
+
       let test_file_name =
         match test_name with
         | "betree_main-special" -> "betree_main"