diff options
| -rw-r--r-- | Makefile | 53 | ||||
| -rw-r--r-- | flake.nix | 33 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 124 |
3 files changed, 126 insertions, 84 deletions
@@ -19,8 +19,7 @@ TEST_RUNNER_EXE ?= $(PWD)/bin/test_runner CHARON_EXE ?= $(PWD)/charon/bin/charon # The user can specify additional translation options for Aeneas. -# In CI we activate the (expensive) sanity checks. -OPTIONS ?= +AENEAS_OPTIONS ?= CHARON_OPTIONS ?= # The directory thta contains the rust source files for tests. @@ -28,7 +27,7 @@ INPUTS_DIR ?= tests/src # The directory where to look for the .llbc files. LLBC_DIR ?= $(PWD)/tests/llbc -# In CI, we enforce formatting and we don't regenerate llbc files. +# In CI, we enforce formatting and activate the (expensive) sanity checks. IN_CI ?= #################################### @@ -169,53 +168,19 @@ verify: ifdef IN_CI # In CI we do extra sanity checks. -test-%: OPTIONS += -checks +test-%: AENEAS_OPTIONS += -checks +else +test-%: check-charon endif -# Translate the given llbc file to available backends. The test runner decides +# Translate the given rust file to available backends. The test runner decides # which backends to use and sets test-specific options. .PHONY: test-% -test-%: TEST_NAME = $* -test-%: $(LLBC_DIR)/%.llbc - $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(TEST_NAME) $(OPTIONS) +test-%: + $(TEST_RUNNER_EXE) charon $(CHARON_EXE) $(INPUTS_DIR) $(LLBC_DIR) "$*" $(CHARON_OPTIONS) + $(TEST_RUNNER_EXE) aeneas $(AENEAS_EXE) $(LLBC_DIR) "$*" $(AENEAS_OPTIONS) echo "# Test $* done" -# List the `.rs` files in `$(INPUTS_DIR)/` -INDIVIDUAL_RUST_SRCS = $(wildcard $(INPUTS_DIR)/*.rs) -# We test all rust files except this one. -INDIVIDUAL_RUST_SRCS := $(filter-out $(INPUTS_DIR)/hashmap_utils.rs, $(INDIVIDUAL_RUST_SRCS)) -# List the corresponding llbc files. -INDIVIDUAL_LLBCS := $(subst $(INPUTS_DIR)/,$(LLBC_DIR)/,$(patsubst %.rs,%.llbc,$(INDIVIDUAL_RUST_SRCS))) - -.PHONY: generate-llbc -# This depends on `llbc/<file>.llbc` for each `$(INPUTS_DIR)/<file>.rs` we care about, plus the whole-crate test. -generate-llbc: $(INDIVIDUAL_LLBCS) $(LLBC_DIR)/betree_main.llbc - -$(LLBC_DIR)/hashmap_main.llbc: CHARON_OPTIONS += --opaque=hashmap_utils -$(LLBC_DIR)/nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/no_nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/paper.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/constants.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/external.llbc: CHARON_OPTIONS += --no-code-duplication -$(LLBC_DIR)/polonius_list.llbc: CHARON_OPTIONS += --polonius -# Possible to add `--no-code-duplication` if we use the optimized MIR -$(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main - -ifndef IN_CI -$(LLBC_DIR)/%.llbc: check-charon - -$(LLBC_DIR)/%.llbc: - $(CHARON_EXE) --no-cargo --input $(INPUTS_DIR)/$*.rs --crate $* $(CHARON_OPTIONS) --dest $(LLBC_DIR) -# Special rule for the whole-crate test. -$(LLBC_DIR)/betree_main.llbc: - cd $(INPUTS_DIR)/betree && $(CHARON_EXE) $(CHARON_OPTIONS) --dest $(LLBC_DIR) -else -$(LLBC_DIR)/%.llbc: - @echo 'ERROR: llbc files should be built separately in CI' - @false -endif - - # ============================================================================= # Nix # ============================================================================= @@ -80,6 +80,9 @@ OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. }; + # This test is a full crate with dependencies. We generate the + # corresponding llbc file here; this function takes care of cargo + # dependencies for us. betree-llbc = charon.extractCrateWithCharon.${system} { name = "betree"; src = ./tests/src/betree; @@ -89,22 +92,6 @@ ./target/debug/betree ''; }; - input-llbcs = pkgs.runCommand "input-llbcs" - { - src = ./tests/src; - makefile = ./Makefile; - buildInputs = [ charon.packages.${system}.rustToolchain charon.packages.${system}.charon ]; - } '' - # Copy the betree output file - mkdir -p $out - cp ${betree-llbc}/llbc/betree_main.llbc $out - - mkdir tests - cp -r $src tests/src - cp $makefile Makefile - # Generate the llbc files - CHARON_EXE="charon" INPUTS_DIR="tests/src" LLBC_DIR="$out" make generate-llbc - ''; # Run the translation on various files. # Make sure we don't need to recompile the package whenever we make @@ -118,19 +105,25 @@ path == toString ./Makefile || pkgs.lib.hasPrefix (toString ./compiler) path || pkgs.lib.hasPrefix (toString ./backends) path - || pkgs.lib.hasPrefix (toString ./tests) path; + || (pkgs.lib.hasPrefix (toString ./tests) path + && !pkgs.lib.hasSuffix ".llbc" path); }; + buildInputs = [ charon.packages.${system}.rustToolchain ]; buildPhase = '' - export LLBC_DIR=${input-llbcs} export AENEAS_EXE=${aeneas}/bin/aeneas + export CHARON_EXE=${charon.packages.${system}.charon}/bin/charon export TEST_RUNNER_EXE=${test_runner}/bin/test_runner + mkdir llbc + export LLBC_DIR=llbc + # Copy over the llbc file we can't generate ourselves. + cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR + # Copy the tests cp -r tests tests-copy + make clean-generated-aeneas # Run the tests with extra sanity checks enabled - # Remark: we could remove the file - make clean-generated-aeneas IN_CI=1 make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 8b4a4208..d80231d0 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -1,26 +1,26 @@ (* Paths to use for tests *) -type test_env = { aeneas_path : string; llbc_dir : string } +type aeneas_env = { aeneas_path : string; llbc_dir : string } -(* The data for a specific test to run *) -type test_case = { +type charon_env = { + charon_path : string; + inputs_dir : string; + llbc_dir : string; +} + +(* The data for a specific test to run aeneas on *) +type aeneas_test_case = { name : string; backend : string; subdir : string; extra_aeneas_options : string list; } -(* Run Aeneas on a specific input with the given options *) -let run_test env case = - let concat_path = List.fold_left Filename.concat "" in - let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in - let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in - let args = - [| - env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend; - |] - in - let args = Array.append args (Array.of_list case.extra_aeneas_options) in +(* The data for a specific test to generate llbc for *) +type charon_test_case = { name : string; extra_charon_options : string list } +let concat_path = List.fold_left Filename.concat "" + +let run_command args = (* Debug arguments *) print_string "[test_runner] Running: "; Array.iter @@ -30,15 +30,66 @@ let run_test env case = args; print_endline ""; - (* Run Aeneas *) + (* Run the command *) let pid = - Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr + Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr in let _ = Unix.waitpid [] pid in () +(* Run Aeneas on a specific input with the given options *) +let run_aeneas (env : aeneas_env) (case : aeneas_test_case) = + let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in + let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in + let args = + [| + env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend; + |] + in + let args = Array.append args (Array.of_list case.extra_aeneas_options) in + (* Run Aeneas *) + run_command args + +(* 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 args = + [| + env.charon_path; + "--no-cargo"; + "--input"; + input_file; + "--crate"; + case.name; + "--dest"; + env.llbc_dir; + |] + in + 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 + match Sys.getenv_opt "IN_CI" with + | None -> + let args = [| env.charon_path; "--dest"; env.llbc_dir |] in + let args = + Array.append args (Array.of_list case.extra_charon_options) + in + (* Run Charon inside the crate *) + Unix.chdir input_crate; + run_command args + | Some _ -> + (* Crates with dependencies must be generated separately in CI. We skip + here and trust that CI takes care to generate the necessary llbc + 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.") + (* File-specific options *) -let test_options backend test_name = +let aeneas_options_for_test backend test_name = (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *) let use_fuel = match (backend, test_name) with @@ -92,6 +143,27 @@ let test_options backend test_name = let options = List.append extra_options options in options +(* File-specific options *) +let charon_options_for_test test_name = + (* Possible to add `--no-code-duplication` for `hashmap_main` if we use the optimized MIR *) + let no_code_dup = + match test_name with + | "constants" | "external" | "nested_borrows" | "no_nested_borrows" + | "paper" -> + [ "--no-code-duplication" ] + | _ -> [] + in + let extra_options = + (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *) + match test_name with + | "betree_main" -> + [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] + | "hashmap_main" -> [ "--opaque=hashmap_utils" ] + | "polonius_list" -> [ "--polonius" ] + | _ -> [] + in + List.append no_code_dup extra_options + (* The subdirectory in which to store the outputs. *) (* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *) let test_subdir backend test_name = @@ -111,7 +183,7 @@ 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 :: options -> + | _exe_path :: "aeneas" :: 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 = [ "coq"; "lean"; "fstar" ] in @@ -119,11 +191,23 @@ let () = (fun backend -> let subdir = test_subdir backend test_name in let extra_aeneas_options = - List.append (test_options backend test_name) options + List.append (aeneas_options_for_test backend test_name) options in let test_case = { name = test_name; backend; subdir; extra_aeneas_options } in - run_test tests_env test_case) + run_aeneas tests_env test_case) backends + | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name + :: options -> + let tests_env = { charon_path; inputs_dir; llbc_dir } 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 + in + let test_case = { name = test_name; extra_charon_options } in + run_charon tests_env test_case | _ -> failwith "Incorrect options passed to test runner" |