diff options
| -rw-r--r-- | Makefile | 29 | ||||
| -rw-r--r-- | flake.nix | 3 | ||||
| -rw-r--r-- | tests/test_runner/dune | 2 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 38 |
4 files changed, 39 insertions, 33 deletions
@@ -145,27 +145,24 @@ test: build-dev test-all betree-tests betree-tests: cd $(INPUTS_DIR)/betree && $(MAKE) test -.PHONY: test-all -test-all: \ - test-arrays \ - test-betree_main \ - test-bitwise \ - test-constants \ - test-demo \ - test-external \ - test-hashmap \ - test-hashmap_main \ - test-loops \ - test-no_nested_borrows \ - test-paper \ - test-polonius_list \ - test-traits - # Verify the F* files generated by the translation .PHONY: verify verify: cd tests && $(MAKE) all +# List the files and directories in `INPUTS_DIR` +INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*) +# Remove the directory prefix, replace with `test-` +INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST)) +# Remove some tests we don't want to run. +# FIXME: move this information to the file itself +INPUTS_LIST := $(filter-out test-hashmap_utils.rs,$(INPUTS_LIST)) +INPUTS_LIST := $(filter-out test-nested_borrows.rs,$(INPUTS_LIST)) + +# Run all the tests we found. +.PHONY: test-all +test-all: $(INPUTS_LIST) + ifdef IN_CI # In CI we do extra sanity checks. test-%: AENEAS_OPTIONS += -checks @@ -78,6 +78,9 @@ duneVersion = "3"; src = ./tests/test_runner; OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. + propagatedBuildInputs = (with ocamlPackages; [ + core_unix + ]); }; # This test is a full crate with dependencies. We generate the diff --git a/tests/test_runner/dune b/tests/test_runner/dune index 7da7a96d..7caf661f 100644 --- a/tests/test_runner/dune +++ b/tests/test_runner/dune @@ -1,4 +1,4 @@ (executable (public_name test_runner) - (libraries unix) + (libraries core_unix.sys_unix unix) (name run_test)) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index d80231d0..688c81ae 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -16,7 +16,11 @@ type aeneas_test_case = { } (* The data for a specific test to generate llbc for *) -type charon_test_case = { name : string; extra_charon_options : string list } +type charon_test_case = { + name : string; + path : string; + extra_charon_options : string list; +} let concat_path = List.fold_left Filename.concat "" @@ -52,15 +56,14 @@ let run_aeneas (env : aeneas_env) (case : aeneas_test_case) = (* 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 input_path = concat_path [ env.inputs_dir; case.path ] in + if Sys_unix.is_file_exn input_path then let args = [| env.charon_path; "--no-cargo"; "--input"; - input_file; + input_path; "--crate"; case.name; "--dest"; @@ -70,7 +73,7 @@ let run_charon (env : charon_env) (case : charon_test_case) = 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 + else if Sys.is_directory input_path then match Sys.getenv_opt "IN_CI" with | None -> let args = [| env.charon_path; "--dest"; env.llbc_dir |] in @@ -78,7 +81,7 @@ let run_charon (env : charon_env) (case : charon_test_case) = Array.append args (Array.of_list case.extra_charon_options) in (* Run Charon inside the crate *) - Unix.chdir input_crate; + Unix.chdir input_path; run_command args | Some _ -> (* Crates with dependencies must be generated separately in CI. We skip @@ -86,7 +89,7 @@ let run_charon (env : charon_env) (case : charon_test_case) = 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.") + else failwith ("`" ^ input_path ^ "` is not a file or a directory.") (* File-specific options *) let aeneas_options_for_test backend test_name = @@ -154,9 +157,8 @@ let charon_options_for_test test_name = | _ -> [] in let extra_options = - (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *) match test_name with - | "betree_main" -> + | "betree" -> [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] | "hashmap_main" -> [ "--opaque=hashmap_utils" ] | "polonius_list" -> [ "--polonius" ] @@ -183,8 +185,13 @@ let test_subdir backend test_name = let () = match Array.to_list Sys.argv with (* Ad-hoc argument passing for now. *) - | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_name :: options -> + | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_path :: options -> let tests_env = { aeneas_path; llbc_dir } in + let test_name = Filename.remove_extension test_path in + (* FIXME: remove this special case *) + let test_name = + if test_name = "betree" then "betree_main" else test_name + in (* TODO: reactivate HOL4 once traits are parameterized by their associated types *) let backends = [ "coq"; "lean"; "fstar" ] in List.iter @@ -198,16 +205,15 @@ let () = in run_aeneas tests_env test_case) backends - | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name + | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_path :: options -> let tests_env = { charon_path; inputs_dir; llbc_dir } in + let test_name = Filename.remove_extension test_path 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 + let test_case = + { name = test_name; path = test_path; extra_charon_options } in - let test_case = { name = test_name; extra_charon_options } in run_charon tests_env test_case | _ -> failwith "Incorrect options passed to test runner" |