From 6f14e8c699169aa11ea9c106f8cae1ba593569d0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 22 May 2024 15:11:28 +0200
Subject: Add simple test runner

---
 tests/test_runner/.ocamlformat            |  0
 tests/test_runner/aeneas_test_runner.opam | 27 +++++++++++++++++++++++++++
 tests/test_runner/dune                    |  4 ++++
 tests/test_runner/dune-project            | 25 +++++++++++++++++++++++++
 tests/test_runner/run_test.ml             | 30 ++++++++++++++++++++++++++++++
 5 files changed, 86 insertions(+)
 create mode 100644 tests/test_runner/.ocamlformat
 create mode 100644 tests/test_runner/aeneas_test_runner.opam
 create mode 100644 tests/test_runner/dune
 create mode 100644 tests/test_runner/dune-project
 create mode 100644 tests/test_runner/run_test.ml

(limited to 'tests')

diff --git a/tests/test_runner/.ocamlformat b/tests/test_runner/.ocamlformat
new file mode 100644
index 00000000..e69de29b
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
+      ()
+  | _ -> ()
-- 
cgit v1.2.3