Add simple test runner

8 files changed, 110 insertions, 6 deletions

diff --git a/.gitignore b/.gitignore
index 7703c3fd..67b16555 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,7 +19,7 @@ _build/
 /charon
 
 # We group everything here
-bin
+/bin
 
 # oasis generated files
 setup.data
diff --git a/Makefile b/Makefile
index c2f42c75..2457bec2 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/flake.nix b/flake.nix
index d380170a..7dd2b7c0 100644
--- a/flake.nix
+++ b/flake.nix
@@ -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
+      ()
+  | _ -> ()