summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile29
-rw-r--r--flake.nix3
-rw-r--r--tests/test_runner/dune2
-rw-r--r--tests/test_runner/run_test.ml38
4 files changed, 39 insertions, 33 deletions
diff --git a/Makefile b/Makefile
index fccca9b1..8a7701cc 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/flake.nix b/flake.nix
index 9c918ff9..caa29fae 100644
--- a/flake.nix
+++ b/flake.nix
@@ -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"