diff options
| -rw-r--r-- | Makefile | 33 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 38 |
2 files changed, 28 insertions, 43 deletions
@@ -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" |