Merge branch 'main' into afromher/recursive_projectors

5 files changed, 352 insertions, 0 deletions

diff --git a/backends/lean/Base/Arith/Arith.lean b/tests/test_runner/.ocamlformat
index e69de29b..e69de29b 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ 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..e8b29d66
--- /dev/null
+++ b/tests/test_runner/dune
@@ -0,0 +1,10 @@
+(executable
+ (public_name test_runner)
+ (libraries core_unix.sys_unix re unix)
+ (preprocess
+  (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv))
+ (name run_test))
+
+(env
+ (dev
+  (flags :standard -warn-error -5@8-11-14-32-33-20-21-26-27-39)))
diff --git a/tests/test_runner/dune-project b/tests/test_runner/dune-project
new file mode 100644
index 00000000..dc352bd0
--- /dev/null
+++ b/tests/test_runner/dune-project
@@ -0,0 +1,25 @@
+(lang dune 3.7)
+
+(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..25efbcfd
--- /dev/null
+++ b/tests/test_runner/run_test.ml
@@ -0,0 +1,290 @@
+(* Convenience functions *)
+let map_while (f : 'a -> 'b option) (input : 'a list) : 'b list =
+  let _, result =
+    List.fold_left
+      (fun (continue, out) a ->
+        if continue then
+          match f a with None -> (false, out) | Some b -> (true, b :: out)
+        else (continue, out))
+      (true, []) input
+  in
+  List.rev result
+
+(* Paths to use for tests *)
+type runner_env = {
+  charon_path : string;
+  aeneas_path : string;
+  llbc_dir : string;
+}
+
+module Backend = struct
+  type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp]
+
+  (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
+  let all = [ Coq; Lean; FStar ]
+
+  let of_string = function
+    | "coq" -> Coq
+    | "lean" -> Lean
+    | "fstar" -> FStar
+    | "hol4" -> HOL4
+    | backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
+
+  let to_string = function
+    | Coq -> "coq"
+    | Lean -> "lean"
+    | FStar -> "fstar"
+    | HOL4 -> "hol4"
+end
+
+module BackendMap = Map.Make (Backend)
+
+let concat_path = List.fold_left Filename.concat ""
+
+let run_command args =
+  (* Debug arguments *)
+  print_string "[test_runner] Running: ";
+  Array.iter
+    (fun x ->
+      print_string x;
+      print_string " ")
+    args;
+  print_endline "";
+
+  (* Run the command *)
+  let pid =
+    Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr
+  in
+  let _ = Unix.waitpid [] pid in
+  ()
+
+(* File-specific options *)
+let aeneas_options_for_test backend test_name =
+  if test_name = "betree" then
+    let options =
+      [
+        "-backward-no-state-update";
+        "-test-trans-units";
+        "-state";
+        "-split-files";
+      ]
+    in
+    let extra_options =
+      match backend with
+      | Backend.Coq -> [ "-use-fuel" ]
+      | Backend.FStar -> [ "-decreases-clauses"; "-template-clauses" ]
+      | _ -> []
+    in
+    List.append extra_options options
+  else []
+
+(* File-specific options *)
+let charon_options_for_test test_name =
+  match test_name with
+  | "betree" ->
+      [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
+  | _ -> []
+
+(* 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 =
+  let backend = Backend.to_string backend in
+  match (backend, test_name) with
+  | "lean", "demo" -> "Demo"
+  | "lean", _ -> "."
+  | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
+  | _, "betree" -> "betree"
+  | _, "hashmap_main" -> "hashmap_on_disk"
+  | "hol4", _ -> "misc-" ^ test_name
+  | ( _,
+      ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows"
+      | "paper" | "polonius_list" ) ) ->
+      "misc"
+  | _ -> test_name
+
+(* The data for a specific test input *)
+module Input = struct
+  type kind = SingleFile | Crate
+  type action = Normal | Skip | KnownFailure
+
+  type t = {
+    name : string;
+    path : string;
+    kind : kind;
+    action : action;
+    charon_options : string list;
+    aeneas_options : string list BackendMap.t;
+    subdir : string BackendMap.t;
+  }
+
+  (* Parse lines that start `//@`. Each of them modifies the options we use for the test.
+     Supported comments:
+       - `skip`: don't process the file;
+       - `known-failure`: TODO;
+       - `charon-args=...`: extra arguments to pass to charon;
+       - `aeneas-args=...`: extra arguments to pass to aeneas;
+       - `[backend,..]...`: where each `backend` is the name of a backend supported by
+            aeneas; this sets options for these backends only. Only supported for `aeneas-args`.
+  *)
+  let apply_special_comment comment input =
+    let comment = String.trim comment in
+    (* Parse the backends if any *)
+    let re = Re.compile (Re.Pcre.re "^\\[([a-zA-Z,]+)\\](.*)$") in
+    let comment, (backends : Backend.t list) =
+      match Re.exec_opt re comment with
+      | Some groups ->
+          let backends = Re.Group.get groups 1 in
+          let backends = String.split_on_char ',' backends in
+          let backends = List.map Backend.of_string backends in
+          let rest = Re.Group.get groups 2 in
+          (String.trim rest, backends)
+      | None -> (comment, Backend.all)
+    in
+    (* Parse the other options *)
+    let charon_args = Core.String.chop_prefix comment ~prefix:"charon-args=" in
+    let aeneas_args = Core.String.chop_prefix comment ~prefix:"aeneas-args=" in
+
+    if comment = "skip" then { input with action = Skip }
+    else if comment = "known-failure" then { input with action = KnownFailure }
+    else if Option.is_some charon_args then
+      let args = Option.get charon_args in
+      let args = String.split_on_char ' ' args in
+      { input with charon_options = List.append input.charon_options args }
+    else if Option.is_some aeneas_args then
+      let args = Option.get aeneas_args in
+      let args = String.split_on_char ' ' args in
+      let add_args opts = List.append opts args in
+      {
+        input with
+        aeneas_options =
+          List.fold_left
+            (fun map backend ->
+              BackendMap.update backend (Option.map add_args) map)
+            input.aeneas_options backends;
+      }
+    else failwith ("Unrecognized special comment: `" ^ comment ^ "`")
+
+  (* Given a path to a rust file or crate, gather the details and options about how to build the test. *)
+  let build (path : string) : t =
+    let name = Filename.remove_extension (Filename.basename path) in
+    let kind =
+      if Sys_unix.is_file_exn path then SingleFile
+      else if Sys_unix.is_directory_exn path then Crate
+      else failwith ("`" ^ path ^ "` is not a file or a directory.")
+    in
+    let action = Normal in
+    let charon_options = charon_options_for_test name in
+    let subdir =
+      List.fold_left
+        (fun map backend ->
+          let subdir = test_subdir backend name in
+          BackendMap.add backend subdir map)
+        BackendMap.empty Backend.all
+    in
+    let aeneas_options =
+      List.fold_left
+        (fun map backend ->
+          let opts = aeneas_options_for_test backend name in
+          BackendMap.add backend opts map)
+        BackendMap.empty Backend.all
+    in
+    let input =
+      { path; name; kind; action; charon_options; subdir; aeneas_options }
+    in
+    match kind with
+    | SingleFile ->
+        let file_lines = Core.In_channel.read_lines path in
+        (* Extract the special lines. Stop at the first non-special line. *)
+        let special_comments =
+          map_while
+            (fun line -> Core.String.chop_prefix line ~prefix:"//@")
+            file_lines
+        in
+        (* Apply the changes from the special lines to our input. *)
+        List.fold_left
+          (fun input comment -> apply_special_comment comment input)
+          input special_comments
+    | Crate -> input
+end
+
+(* Run Aeneas on a specific input with the given options *)
+let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
+  (* FIXME: remove this special case *)
+  let test_name = if case.name = "betree" then "betree_main" else case.name in
+  let input_file = concat_path [ env.llbc_dir; test_name ] ^ ".llbc" in
+  let subdir = BackendMap.find backend case.subdir in
+  let aeneas_options = BackendMap.find backend case.aeneas_options in
+  let backend_str = Backend.to_string backend in
+  let dest_dir = concat_path [ "tests"; backend_str; subdir ] in
+  let args =
+    [|
+      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str;
+    |]
+  in
+  let args = Array.append args (Array.of_list aeneas_options) in
+  (* Run Aeneas *)
+  run_command args
+
+(* Run Charon on a specific input with the given options *)
+let run_charon (env : runner_env) (case : Input.t) =
+  match case.kind with
+  | SingleFile ->
+      let args =
+        [|
+          env.charon_path;
+          "--no-cargo";
+          "--input";
+          case.path;
+          "--crate";
+          case.name;
+          "--dest";
+          env.llbc_dir;
+        |]
+      in
+      let args = Array.append args (Array.of_list case.charon_options) in
+      (* Run Charon on the rust file *)
+      run_command args
+  | Crate -> (
+      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.charon_options) in
+          (* Run Charon inside the crate *)
+          let old_pwd = Unix.getcwd () in
+          Unix.chdir case.path;
+          run_command args;
+          Unix.chdir old_pwd
+      | 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"
+      )
+
+let () =
+  match Array.to_list Sys.argv with
+  (* Ad-hoc argument passing for now. *)
+  | _exe_path :: charon_path :: aeneas_path :: llbc_dir :: test_path
+    :: aeneas_options -> (
+      let runner_env = { charon_path; aeneas_path; llbc_dir } in
+      let test_case = Input.build test_path in
+      let test_case =
+        {
+          test_case with
+          aeneas_options =
+            BackendMap.map (List.append aeneas_options) test_case.aeneas_options;
+        }
+      in
+
+      match test_case.action with
+      | Skip -> ()
+      | Normal ->
+          (* Generate the llbc file *)
+          run_charon runner_env test_case;
+          (* Process the llbc file for the each backend *)
+          List.iter
+            (fun backend -> run_aeneas runner_env test_case backend)
+            Backend.all
+      | KnownFailure -> failwith "KnownFailure is unimplemented")
+  | _ -> failwith "Incorrect options passed to test runner"