diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Makefile | 13 | ||||
| -rw-r--r-- | flake.nix | 15 | ||||
| -rw-r--r-- | tests/test_runner/.ocamlformat | 0 | ||||
| -rw-r--r-- | tests/test_runner/aeneas_test_runner.opam | 27 | ||||
| -rw-r--r-- | tests/test_runner/dune | 4 | ||||
| -rw-r--r-- | tests/test_runner/dune-project | 25 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 30 |
8 files changed, 110 insertions, 6 deletions
@@ -19,7 +19,7 @@ _build/ /charon # We group everything here -bin +/bin # oasis generated files setup.data @@ -24,6 +24,9 @@ CHARON_HOME ?= ./charon # change this path for the Nix package. AENEAS_EXE ?= bin/aeneas +# The path to our test runner. +TEST_RUNNER_EXE ?= bin/test_runner + # The user can specify additional translation options for Aeneas. # By default we activate the (expensive) sanity checks. OPTIONS ?= @@ -61,11 +64,16 @@ build-bin: check-charon build-lib: check-charon cd compiler && dune build aeneas.cmxs +.PHONY: build-runner +build-runner: check-charon + cd tests/test_runner && dune build + .PHONY: build-bin-dir -build-bin-dir: build-bin build-lib +build-bin-dir: build-bin build-lib build-runner mkdir -p bin cp -f compiler/_build/default/main.exe bin/aeneas cp -f compiler/_build/default/main.exe bin/aeneas.cmxs + cp -f tests/test_runner/_build/default/run_test.exe bin/test_runner mkdir -p bin/backends/fstar mkdir -p bin/backends/coq cp -rf backends/fstar/*.fst* bin/backends/fstar/ @@ -140,6 +148,7 @@ verify: format: @# `|| `true` because the command returns an error if it changed anything, which we don't care about. cd compiler && dune fmt || true + cd tests/test_runner && dune fmt || true # The commands to run Charon to generate the .llbc files ifeq (, $(REGEN_LLBC)) @@ -148,7 +157,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$* endif # The command to run Aeneas on the proper llbc file -AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BACKEND)/$(SUBDIR) -backend $(BACKEND) $(OPTIONS) +AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) "$(SUBDIR)" $(BACKEND) $(OPTIONS) # Subdirs test-arrays: SUBDIR := arrays @@ -47,6 +47,7 @@ ''; installPhase = "touch $out"; }; + aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; @@ -70,6 +71,15 @@ echo charon.packages.${system}.tests ''; }; + + test_runner = ocamlPackages.buildDunePackage { + pname = "aeneas_test_runner"; + version = "0.1.0"; + duneVersion = "3"; + src = ./tests/test_runner; + OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. + }; + # Run the translation on various files. # Make sure we don't need to recompile the package whenever we make # unnecessary changes - we list the exact files and folders the package @@ -88,9 +98,8 @@ # We need to provide the paths to the Charon tests derivations export CHARON_TEST_DIR=${charon.checks.${system}.tests} - # Copy the Aeneas executable, and update the path to it - cp ${aeneas}/bin/aeneas aeneas - export AENEAS_EXE=./aeneas + export AENEAS_EXE=${aeneas}/bin/aeneas + export TEST_RUNNER_EXE=${test_runner}/bin/test_runner # Copy the tests cp -r tests tests-copy diff --git a/tests/test_runner/.ocamlformat b/tests/test_runner/.ocamlformat new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/tests/test_runner/.ocamlformat diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam new file mode 100644 index 00000000..b57cc9f6 --- /dev/null +++ b/tests/test_runner/aeneas_test_runner.opam @@ -0,0 +1,27 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.1" +authors: ["Son Ho" "Guillaume Boisseau"] +license: "Apache-2.0" +homepage: "https://github.com/AeneasVerif/aeneas" +bug-reports: "https://github.com/AeneasVerif/aeneas/issues" +depends: [ + "ocaml" + "dune" {>= "3.12"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/AeneasVerif/aeneas.git" diff --git a/tests/test_runner/dune b/tests/test_runner/dune new file mode 100644 index 00000000..7da7a96d --- /dev/null +++ b/tests/test_runner/dune @@ -0,0 +1,4 @@ +(executable + (public_name test_runner) + (libraries unix) + (name run_test)) diff --git a/tests/test_runner/dune-project b/tests/test_runner/dune-project new file mode 100644 index 00000000..c614e923 --- /dev/null +++ b/tests/test_runner/dune-project @@ -0,0 +1,25 @@ +(lang dune 3.12) + +(name aeneas_test_runner) + +(version 0.1) + +(generate_opam_files true) + +(source + (uri git+https://github.com/AeneasVerif/aeneas.git)) + +(homepage "https://github.com/AeneasVerif/aeneas") + +(bug_reports "https://github.com/AeneasVerif/aeneas/issues") + +(authors + "Son Ho" + "Guillaume Boisseau") + +(license Apache-2.0) + +(package + (name aeneas_test_runner) + (depends ocaml dune) +) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml new file mode 100644 index 00000000..379abe04 --- /dev/null +++ b/tests/test_runner/run_test.ml @@ -0,0 +1,30 @@ +let concat_path = List.fold_left Filename.concat "" + +let () = + match Array.to_list Sys.argv with + (* Ad-hoc argument passing for now. *) + | _exe_path :: aeneas_path :: tests_dir :: test_name :: subdir :: backend + :: options -> + let input_file = concat_path [ tests_dir; "llbc"; test_name ] ^ ".llbc" in + let dest_dir = concat_path [ "tests"; backend; subdir ] in + let args = + [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |] + in + let args = Array.append args (Array.of_list options) in + + (* Debug arguments *) + print_string "[test_runner] Running: "; + Array.iter + (fun x -> + print_string x; + print_string " ") + args; + print_endline ""; + + (* Run Aeneas *) + let pid = + Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr + in + let _ = Unix.waitpid [] pid in + () + | _ -> () |