From b669f7c1228efb362cbb56b95090b24c0611ba7b Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 12:01:31 +0200
Subject: tests: Add a README

---
 tests/README.md | 67 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)
 create mode 100644 tests/README.md

diff --git a/tests/README.md b/tests/README.md
new file mode 100644
index 00000000..4f4f1ff5
--- /dev/null
+++ b/tests/README.md
@@ -0,0 +1,67 @@
+# Aeneas test suite
+
+This folder contains the test suite for Aeneas. It is organized as follows:
+- `test_runner/`: ocaml script that orchestrates the test suite;
+- `src/`: rust files and crates used as test inputs;
+- `llbc/`: temporary directory (ignored by git) that stores intermediate files generated during tests;
+- `coq/`, `fstar/`, `hol4/`, `lean/`: one folder per backend. Each folder contains:
+   - Files generated by Aeneas from our test inputs;
+   - Handwritten proof files.
+
+# Running the test suite
+
+Running the test suite has two parts:
+- The generation of files from rust to each backend. This is done by running `make test` in the
+  project root. This will call the test runner on each file or crate in `tests/src`, which will call
+  `charon` and `aeneas` to generate the backend-specific outputs.
+- The verification of proofs for each backend. This is done by running `make verify` in the project
+  root. It will run each verifier (`fstar`, `lean` etc) on the files in the corresponding folder to
+  verify the correctness of proofs.
+
+CI does both of these things; in particular it checks that we correctly committed the generated
+files.
+
+Important note: at the moment we don't regenerate the `hol4` outputs. We do still check them with
+hol4. This is tracked in https://github.com/AeneasVerif/aeneas/issues/62.
+
+# Adding a new test
+
+Adding a new test is easy: just add a `foo.rs` file or a `foo_crate` folder in `tests/src`. `make
+test` will find the new file and call the test runner on it.
+
+To specify options for how your test should be run, see the next section.
+
+Ideally, any non-trivial change to Aeneas should have an accompanying test that exercises the new
+code. The goal of this test suite is to cover a large portion of what Aeneas can do, so we can work
+on it confidently.
+
+# Passing options to `Aeneas` and `Charon`
+
+The test runner supports setting several options for each test.
+- For single files, it will read comments at the top of the file that start with `//@`;
+- For crates, it will read the `crate_dir/aeneas-test-options` file.
+
+In both cases it supports the same options. Typical options are:
+- `charon-args=--polonius --opaque=betree_utils`: pass these arguments to `charon`;
+- `aeneas-args=-test-trans-units`: pass these arguments to `aeneas` for all backends;
+- `[fstar] aeneas-args=-decreases-clauses -template-clauses`: pass these arguments to `aeneas` for
+  the `fstar` backend;
+- `[coq,lean] skip`: skip the test for the `coq` and `lean` backends;
+- `[fstar] known-failure`: see below;
+- `[coq,fstar] subdir=misc`: store the output in the `misc` subdirectory for these two backends.
+
+For an up-to-date list of options, see comments in the test runner code.
+
+# `known-failure` tests
+
+There's a special kind of test that doesn't generate backend code: `//@ known-failure` tests. These
+are meant to record:
+- Cases that produce an error so we don't forget and can fix them later;
+- Cases that _should_ error, to ensure we correctly raise an error and that the error output is nice.
+
+It is useful to add tests there whenever you find an interesting failure case.
+
+Note however that this is for failures of Aeneas. Tests that cause Charon errors should be submitted
+to the Charon project. `known-failure` tests will not pass if the error occurs within Charon. Note
+also that there is no option for tests that translate successfully but fail to be verified by the
+backend.
-- 
cgit v1.2.3


From 86d0789b5a303f43c0d9bfeff83f37d89750b5d6 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 12:14:08 +0200
Subject: runner: make the backend map a submodule of `Backend`

---
 tests/test_runner/run_test.ml | 84 ++++++++++++++++++++++++-------------------
 1 file changed, 48 insertions(+), 36 deletions(-)

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index c626b4d1..5314752c 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -36,27 +36,34 @@ module Backend = struct
     | Lean -> "lean"
     | FStar -> "fstar"
     | HOL4 -> "hol4"
-end
 
-module BackendMap = struct
-  include Map.Make (Backend)
+  module Map = struct
+    (* Hack to be able to include things from the parent module with the same names *)
+    type backend_t = t
 
-  (* Make a new map with one entry per backend, given by `f` *)
-  let make (f : Backend.t -> 'a) : 'a t =
-    List.fold_left
-      (fun map backend -> add backend (f backend) map)
-      empty Backend.all
+    let backend_compare = compare
 
-  (* Set this value for all the backends in `backends` *)
-  let add_each (backends : Backend.t list) (v : 'a) (map : 'a t) : 'a t =
-    List.fold_left (fun map backend -> add backend v map) map backends
+    include Map.Make (struct
+      type t = backend_t
 
-  (* Updates all the backends in `backends` with `f` *)
-  let update_each (backends : Backend.t list) (f : 'a -> 'a) (map : 'a t) : 'a t
-      =
-    List.fold_left
-      (fun map backend -> update backend (Option.map f) map)
-      map backends
+      let compare = backend_compare
+    end)
+
+    (* Make a new map with one entry per backend, given by `f` *)
+    let make (f : backend_t -> 'a) : 'a t =
+      List.fold_left (fun map backend -> add backend (f backend) map) empty all
+
+    (* Set this value for all the backends in `backends` *)
+    let add_each (backends : backend_t list) (v : 'a) (map : 'a t) : 'a t =
+      List.fold_left (fun map backend -> add backend v map) map backends
+
+    (* Updates all the backends in `backends` with `f` *)
+    let update_each (backends : backend_t list) (f : 'a -> 'a) (map : 'a t) :
+        'a t =
+      List.fold_left
+        (fun map backend -> update backend (Option.map f) map)
+        map backends
+  end
 end
 
 let concat_path = List.fold_left Filename.concat ""
@@ -109,12 +116,12 @@ module Input = struct
     name : string;
     path : string;
     kind : kind;
-    actions : action BackendMap.t;
+    actions : action Backend.Map.t;
     charon_options : string list;
-    aeneas_options : string list BackendMap.t;
-    subdirs : string BackendMap.t;
+    aeneas_options : string list Backend.Map.t;
+    subdirs : string Backend.Map.t;
     (* Whether to store the command output to a file. Only available for known-failure tests. *)
-    check_output : bool BackendMap.t;
+    check_output : bool Backend.Map.t;
   }
 
   (* The default subdirectory in which to store the outputs. *)
@@ -152,16 +159,16 @@ module Input = struct
     let subdir = Core.String.chop_prefix comment ~prefix:"subdir=" in
 
     if comment = "skip" then
-      { input with actions = BackendMap.add_each backends Skip input.actions }
+      { input with actions = Backend.Map.add_each backends Skip input.actions }
     else if comment = "known-failure" then
       {
         input with
-        actions = BackendMap.add_each backends KnownFailure input.actions;
+        actions = Backend.Map.add_each backends KnownFailure input.actions;
       }
     else if comment = "no-check-output" then
       {
         input with
-        check_output = BackendMap.add_each backends false input.check_output;
+        check_output = Backend.Map.add_each backends false input.check_output;
       }
     else if Option.is_some charon_args then
       let args = Option.get charon_args in
@@ -176,11 +183,14 @@ module Input = struct
       {
         input with
         aeneas_options =
-          BackendMap.update_each backends add_args input.aeneas_options;
+          Backend.Map.update_each backends add_args input.aeneas_options;
       }
     else if Option.is_some subdir then
       let subdir = Option.get subdir in
-      { input with subdirs = BackendMap.add_each backends subdir input.subdirs }
+      {
+        input with
+        subdirs = Backend.Map.add_each backends subdir input.subdirs;
+      }
     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. *)
@@ -192,12 +202,12 @@ module Input = struct
       else if Sys_unix.is_directory_exn path then Crate
       else failwith ("`" ^ path ^ "` is not a file or a directory.")
     in
-    let actions = BackendMap.make (fun _ -> Normal) in
+    let actions = Backend.Map.make (fun _ -> Normal) in
     let subdirs =
-      BackendMap.make (fun backend -> default_subdir backend name)
+      Backend.Map.make (fun backend -> default_subdir backend name)
     in
-    let aeneas_options = BackendMap.make (fun _ -> []) in
-    let check_output = BackendMap.make (fun _ -> true) in
+    let aeneas_options = Backend.Map.make (fun _ -> []) in
+    let check_output = Backend.Map.make (fun _ -> true) in
     let input =
       {
         path;
@@ -240,11 +250,11 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   let output_file =
     Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
   in
-  let subdir = BackendMap.find backend case.subdirs in
+  let subdir = Backend.Map.find backend case.subdirs in
   let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in
-  let aeneas_options = BackendMap.find backend case.aeneas_options in
-  let action = BackendMap.find backend case.actions in
-  let check_output = BackendMap.find backend case.check_output in
+  let aeneas_options = Backend.Map.find backend case.aeneas_options in
+  let action = Backend.Map.find backend case.actions in
+  let check_output = Backend.Map.find backend case.check_output in
 
   (* Build the command *)
   let args =
@@ -332,13 +342,15 @@ let () =
         {
           test_case with
           aeneas_options =
-            BackendMap.map (List.append aeneas_options) test_case.aeneas_options;
+            Backend.Map.map
+              (List.append aeneas_options)
+              test_case.aeneas_options;
         }
       in
       let skip_all =
         List.for_all
           (fun backend ->
-            BackendMap.find backend test_case.actions = Input.Skip)
+            Backend.Map.find backend test_case.actions = Input.Skip)
           Backend.all
       in
       if skip_all then ()
-- 
cgit v1.2.3


From ec03335a473ffdf9371210e8558c691ea69d212d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 12:18:52 +0200
Subject: runner: Split up into multiple files

---
 tests/README.md               |   2 +-
 tests/test_runner/Backend.ml  |  47 ++++++++++
 tests/test_runner/Input.ml    | 129 +++++++++++++++++++++++++++
 tests/test_runner/Utils.ml    |  12 +++
 tests/test_runner/dune        |   3 +-
 tests/test_runner/run_test.ml | 196 ------------------------------------------
 6 files changed, 191 insertions(+), 198 deletions(-)
 create mode 100644 tests/test_runner/Backend.ml
 create mode 100644 tests/test_runner/Input.ml
 create mode 100644 tests/test_runner/Utils.ml

diff --git a/tests/README.md b/tests/README.md
index 4f4f1ff5..f68b509f 100644
--- a/tests/README.md
+++ b/tests/README.md
@@ -50,7 +50,7 @@ In both cases it supports the same options. Typical options are:
 - `[fstar] known-failure`: see below;
 - `[coq,fstar] subdir=misc`: store the output in the `misc` subdirectory for these two backends.
 
-For an up-to-date list of options, see comments in the test runner code.
+For an up-to-date list of options, see comments in `tests/test_runner/Input.ml`.
 
 # `known-failure` tests
 
diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml
new file mode 100644
index 00000000..d21a46fc
--- /dev/null
+++ b/tests/test_runner/Backend.ml
@@ -0,0 +1,47 @@
+(*** Define the backends we support as an enum *)
+
+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"
+
+module Map = struct
+  (* Hack to be able to include things from the parent module with the same names *)
+  type backend_t = t
+
+  let backend_compare = compare
+
+  include Map.Make (struct
+    type t = backend_t
+
+    let compare = backend_compare
+  end)
+
+  (* Make a new map with one entry per backend, given by `f` *)
+  let make (f : backend_t -> 'a) : 'a t =
+    List.fold_left (fun map backend -> add backend (f backend) map) empty all
+
+  (* Set this value for all the backends in `backends` *)
+  let add_each (backends : backend_t list) (v : 'a) (map : 'a t) : 'a t =
+    List.fold_left (fun map backend -> add backend v map) map backends
+
+  (* Updates all the backends in `backends` with `f` *)
+  let update_each (backends : backend_t list) (f : 'a -> 'a) (map : 'a t) : 'a t
+      =
+    List.fold_left
+      (fun map backend -> update backend (Option.map f) map)
+      map backends
+end
diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml
new file mode 100644
index 00000000..dbb69a47
--- /dev/null
+++ b/tests/test_runner/Input.ml
@@ -0,0 +1,129 @@
+(*** The data for a specific test input *)
+
+type kind = SingleFile | Crate
+type action = Normal | Skip | KnownFailure
+
+type t = {
+  name : string;
+  path : string;
+  kind : kind;
+  actions : action Backend.Map.t;
+  charon_options : string list;
+  aeneas_options : string list Backend.Map.t;
+  subdirs : string Backend.Map.t;
+  (* Whether to store the command output to a file. Only available for known-failure tests. *)
+  check_output : bool Backend.Map.t;
+}
+
+(* The default subdirectory in which to store the outputs. *)
+let default_subdir backend test_name =
+  match backend with Backend.Lean -> "." | _ -> test_name
+
+(* 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;
+     - `subdir=...: set the subdirectory in which to store the outputs.
+          Defaults to nothing for lean and to the test name for other backends;
+     - `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.
+*)
+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
+  let subdir = Core.String.chop_prefix comment ~prefix:"subdir=" in
+
+  if comment = "skip" then
+    { input with actions = Backend.Map.add_each backends Skip input.actions }
+  else if comment = "known-failure" then
+    {
+      input with
+      actions = Backend.Map.add_each backends KnownFailure input.actions;
+    }
+  else if comment = "no-check-output" then
+    {
+      input with
+      check_output = Backend.Map.add_each backends false input.check_output;
+    }
+  else if Option.is_some charon_args then
+    let args = Option.get charon_args in
+    let args = String.split_on_char ' ' args in
+    if backends != Backend.all then
+      failwith "Cannot set per-backend charon-args"
+    else { 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 =
+        Backend.Map.update_each backends add_args input.aeneas_options;
+    }
+  else if Option.is_some subdir then
+    let subdir = Option.get subdir in
+    { input with subdirs = Backend.Map.add_each backends subdir input.subdirs }
+  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 name = Str.global_replace (Str.regexp "-") "_" name 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 actions = Backend.Map.make (fun _ -> Normal) in
+  let subdirs = Backend.Map.make (fun backend -> default_subdir backend name) in
+  let aeneas_options = Backend.Map.make (fun _ -> []) in
+  let check_output = Backend.Map.make (fun _ -> true) in
+  let input =
+    {
+      path;
+      name;
+      kind;
+      actions;
+      charon_options = [];
+      subdirs;
+      aeneas_options;
+      check_output;
+    }
+  in
+  (* For crates, we store the special comments in a separate file. *)
+  let crate_config_file = Filename.concat path "aeneas-test-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 =
+        Utils.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 when Sys.file_exists crate_config_file ->
+      let special_comments = Core.In_channel.read_lines crate_config_file in
+      List.fold_left
+        (fun input comment -> apply_special_comment comment input)
+        input special_comments
+  | Crate -> input
diff --git a/tests/test_runner/Utils.ml b/tests/test_runner/Utils.ml
new file mode 100644
index 00000000..79be617c
--- /dev/null
+++ b/tests/test_runner/Utils.ml
@@ -0,0 +1,12 @@
+(*** 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
diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 6bb3f7b2..52688d14 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -3,7 +3,8 @@
  (libraries core_unix core_unix.filename_unix core_unix.sys_unix re str unix)
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv))
- (name run_test))
+ (name run_test)
+ (modules Backend Input Utils run_test))
 
 (env
  (dev
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 5314752c..e8dd38bb 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,15 +1,3 @@
-(* 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;
@@ -18,54 +6,6 @@ type runner_env = {
   dest_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"
-
-  module Map = struct
-    (* Hack to be able to include things from the parent module with the same names *)
-    type backend_t = t
-
-    let backend_compare = compare
-
-    include Map.Make (struct
-      type t = backend_t
-
-      let compare = backend_compare
-    end)
-
-    (* Make a new map with one entry per backend, given by `f` *)
-    let make (f : backend_t -> 'a) : 'a t =
-      List.fold_left (fun map backend -> add backend (f backend) map) empty all
-
-    (* Set this value for all the backends in `backends` *)
-    let add_each (backends : backend_t list) (v : 'a) (map : 'a t) : 'a t =
-      List.fold_left (fun map backend -> add backend v map) map backends
-
-    (* Updates all the backends in `backends` with `f` *)
-    let update_each (backends : backend_t list) (f : 'a -> 'a) (map : 'a t) :
-        'a t =
-      List.fold_left
-        (fun map backend -> update backend (Option.map f) map)
-        map backends
-  end
-end
-
 let concat_path = List.fold_left Filename.concat ""
 
 module Command = struct
@@ -107,142 +47,6 @@ module Command = struct
     | Failure -> ()
 end
 
-(* 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;
-    actions : action Backend.Map.t;
-    charon_options : string list;
-    aeneas_options : string list Backend.Map.t;
-    subdirs : string Backend.Map.t;
-    (* Whether to store the command output to a file. Only available for known-failure tests. *)
-    check_output : bool Backend.Map.t;
-  }
-
-  (* The default subdirectory in which to store the outputs. *)
-  let default_subdir backend test_name =
-    match backend with Backend.Lean -> "." | _ -> test_name
-
-  (* 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;
-       - `subdir=...: set the subdirectory in which to store the outputs.
-            Defaults to nothing for lean and to the test name for other backends;
-       - `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.
-  *)
-  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
-    let subdir = Core.String.chop_prefix comment ~prefix:"subdir=" in
-
-    if comment = "skip" then
-      { input with actions = Backend.Map.add_each backends Skip input.actions }
-    else if comment = "known-failure" then
-      {
-        input with
-        actions = Backend.Map.add_each backends KnownFailure input.actions;
-      }
-    else if comment = "no-check-output" then
-      {
-        input with
-        check_output = Backend.Map.add_each backends false input.check_output;
-      }
-    else if Option.is_some charon_args then
-      let args = Option.get charon_args in
-      let args = String.split_on_char ' ' args in
-      if backends != Backend.all then
-        failwith "Cannot set per-backend charon-args"
-      else { 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 =
-          Backend.Map.update_each backends add_args input.aeneas_options;
-      }
-    else if Option.is_some subdir then
-      let subdir = Option.get subdir in
-      {
-        input with
-        subdirs = Backend.Map.add_each backends subdir input.subdirs;
-      }
-    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 name = Str.global_replace (Str.regexp "-") "_" name 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 actions = Backend.Map.make (fun _ -> Normal) in
-    let subdirs =
-      Backend.Map.make (fun backend -> default_subdir backend name)
-    in
-    let aeneas_options = Backend.Map.make (fun _ -> []) in
-    let check_output = Backend.Map.make (fun _ -> true) in
-    let input =
-      {
-        path;
-        name;
-        kind;
-        actions;
-        charon_options = [];
-        subdirs;
-        aeneas_options;
-        check_output;
-      }
-    in
-    (* For crates, we store the special comments in a separate file. *)
-    let crate_config_file = Filename.concat path "aeneas-test-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 when Sys.file_exists crate_config_file ->
-        let special_comments = Core.In_channel.read_lines crate_config_file in
-        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) =
   let backend_str = Backend.to_string backend in
-- 
cgit v1.2.3


From 14d9ca2ddf5ccb350d3bd87ca14a7b7468398e9c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 28 May 2024 13:52:12 +0200
Subject: runner: Factor out backend-specific options

---
 tests/test_runner/Input.ml    | 83 ++++++++++++++++++++++---------------------
 tests/test_runner/run_test.ml | 22 +++++++-----
 2 files changed, 56 insertions(+), 49 deletions(-)

diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml
index dbb69a47..960ffe8d 100644
--- a/tests/test_runner/Input.ml
+++ b/tests/test_runner/Input.ml
@@ -3,16 +3,22 @@
 type kind = SingleFile | Crate
 type action = Normal | Skip | KnownFailure
 
+(* Options that can be set for a specific backend *)
+type per_backend = {
+  action : action;
+  aeneas_options : string list;
+  subdir : string;
+  (* Whether to store the command output to a file. Only available for known-failure tests. *)
+  check_output : bool;
+}
+
+(* The data for a specific test input *)
 type t = {
   name : string;
   path : string;
   kind : kind;
-  actions : action Backend.Map.t;
   charon_options : string list;
-  aeneas_options : string list Backend.Map.t;
-  subdirs : string Backend.Map.t;
-  (* Whether to store the command output to a file. Only available for known-failure tests. *)
-  check_output : bool Backend.Map.t;
+  per_backend : per_backend Backend.Map.t;
 }
 
 (* The default subdirectory in which to store the outputs. *)
@@ -44,41 +50,42 @@ let apply_special_comment comment input =
         (String.trim rest, backends)
     | None -> (comment, Backend.all)
   in
+  (* Apply `f` to the selected backends *)
+  let per_backend f =
+    {
+      input with
+      per_backend = Backend.Map.update_each backends f input.per_backend;
+    }
+  in
+  (* Assert that this option is not available to be set per-backend *)
+  let assert_no_backend option_name =
+    if backends != Backend.all then
+      failwith ("Cannot set the `" ^ option_name ^ "` option per-backend")
+  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
   let subdir = Core.String.chop_prefix comment ~prefix:"subdir=" in
 
-  if comment = "skip" then
-    { input with actions = Backend.Map.add_each backends Skip input.actions }
+  if comment = "skip" then per_backend (fun x -> { x with action = Skip })
   else if comment = "known-failure" then
-    {
-      input with
-      actions = Backend.Map.add_each backends KnownFailure input.actions;
-    }
+    per_backend (fun x -> { x with action = KnownFailure })
   else if comment = "no-check-output" then
-    {
-      input with
-      check_output = Backend.Map.add_each backends false input.check_output;
-    }
-  else if Option.is_some charon_args then
+    per_backend (fun x -> { x with check_output = false })
+  else if Option.is_some charon_args then (
     let args = Option.get charon_args in
     let args = String.split_on_char ' ' args in
-    if backends != Backend.all then
-      failwith "Cannot set per-backend charon-args"
-    else { input with charon_options = List.append input.charon_options args }
+    assert_no_backend "charon-args";
+    { 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 =
-        Backend.Map.update_each backends add_args input.aeneas_options;
-    }
+    per_backend (fun x ->
+        { x with aeneas_options = List.append x.aeneas_options args })
   else if Option.is_some subdir then
     let subdir = Option.get subdir in
-    { input with subdirs = Backend.Map.add_each backends subdir input.subdirs }
+    per_backend (fun x -> { x with subdir })
   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. *)
@@ -90,22 +97,16 @@ let build (path : string) : t =
     else if Sys_unix.is_directory_exn path then Crate
     else failwith ("`" ^ path ^ "` is not a file or a directory.")
   in
-  let actions = Backend.Map.make (fun _ -> Normal) in
-  let subdirs = Backend.Map.make (fun backend -> default_subdir backend name) in
-  let aeneas_options = Backend.Map.make (fun _ -> []) in
-  let check_output = Backend.Map.make (fun _ -> true) in
-  let input =
-    {
-      path;
-      name;
-      kind;
-      actions;
-      charon_options = [];
-      subdirs;
-      aeneas_options;
-      check_output;
-    }
+  let per_backend =
+    Backend.Map.make (fun backend ->
+        {
+          action = Normal;
+          subdir = default_subdir backend name;
+          aeneas_options = [];
+          check_output = true;
+        })
   in
+  let input = { path; name; kind; charon_options = []; per_backend } in
   (* For crates, we store the special comments in a separate file. *)
   let crate_config_file = Filename.concat path "aeneas-test-options" in
   match kind with
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index e8dd38bb..c17c17be 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -54,11 +54,12 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   let output_file =
     Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
   in
-  let subdir = Backend.Map.find backend case.subdirs in
+  let per_backend = Backend.Map.find backend case.per_backend in
+  let subdir = per_backend.subdir in
+  let check_output = per_backend.check_output in
+  let aeneas_options = per_backend.aeneas_options in
+  let action = per_backend.action in
   let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in
-  let aeneas_options = Backend.Map.find backend case.aeneas_options in
-  let action = Backend.Map.find backend case.actions in
-  let check_output = Backend.Map.find backend case.check_output in
 
   (* Build the command *)
   let args =
@@ -145,16 +146,21 @@ let () =
       let test_case =
         {
           test_case with
-          aeneas_options =
+          per_backend =
             Backend.Map.map
-              (List.append aeneas_options)
-              test_case.aeneas_options;
+              (fun x ->
+                {
+                  x with
+                  Input.aeneas_options =
+                    List.append aeneas_options x.Input.aeneas_options;
+                })
+              test_case.per_backend;
         }
       in
       let skip_all =
         List.for_all
           (fun backend ->
-            Backend.Map.find backend test_case.actions = Input.Skip)
+            (Backend.Map.find backend test_case.per_backend).action = Input.Skip)
           Backend.all
       in
       if skip_all then ()
-- 
cgit v1.2.3


From 87d5a08f44b46657026a99c154bcec4a733f221d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 May 2024 10:37:17 +0200
Subject: Improve the tests README

---
 tests/Makefile  |  6 +++---
 tests/README.md | 30 +++++++++++++++++++-----------
 2 files changed, 22 insertions(+), 14 deletions(-)

diff --git a/tests/Makefile b/tests/Makefile
index ff4baaba..a911e037 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,6 +1,6 @@
 .PHONY: all
-all: test-fstar test-coq test-lean test-hol4
+all: verify-fstar verify-coq verify-lean verify-hol4
 
-.PHONY: test-%
-test-%:
+.PHONY: verify-%
+verify-%:
 	cd $* && $(MAKE) all
diff --git a/tests/README.md b/tests/README.md
index f68b509f..c9ca0047 100644
--- a/tests/README.md
+++ b/tests/README.md
@@ -8,23 +8,26 @@ This folder contains the test suite for Aeneas. It is organized as follows:
    - Files generated by Aeneas from our test inputs;
    - Handwritten proof files.
 
-# Running the test suite
+## Running the test suite
 
 Running the test suite has two parts:
-- The generation of files from rust to each backend. This is done by running `make test` in the
+- We generate files from rust to each backend. This is done by running `make test` in the
   project root. This will call the test runner on each file or crate in `tests/src`, which will call
   `charon` and `aeneas` to generate the backend-specific outputs.
-- The verification of proofs for each backend. This is done by running `make verify` in the project
-  root. It will run each verifier (`fstar`, `lean` etc) on the files in the corresponding folder to
-  verify the correctness of proofs.
+- We check that the generated output is valid code by parsing it and type-checking it with the
+  relevant verifier (Lean, Coq, F*, etc.), and replay the hand-written proofs which use it as
+  a dependency. This is done by running `make verify` in the project root. 
 
-CI does both of these things; in particular it checks that we correctly committed the generated
-files.
+To generate the output of a single test, run `make test-<file_name>`, e.g. `make test-loops.rs` or
+`make test-betree`. To verify the output for a single backend, run `make verify-<backend>` inside the
+`tests/` folder, e.g. `make verify-coq`.
 
-Important note: at the moment we don't regenerate the `hol4` outputs. We do still check them with
+CI does both of these things; it also checks that we committed all the generated files.
+
+Important note: at the moment we don't regenerate the HOL4 outputs. We do still check them with
 hol4. This is tracked in https://github.com/AeneasVerif/aeneas/issues/62.
 
-# Adding a new test
+## Adding a new test
 
 Adding a new test is easy: just add a `foo.rs` file or a `foo_crate` folder in `tests/src`. `make
 test` will find the new file and call the test runner on it.
@@ -35,7 +38,7 @@ Ideally, any non-trivial change to Aeneas should have an accompanying test that
 code. The goal of this test suite is to cover a large portion of what Aeneas can do, so we can work
 on it confidently.
 
-# Passing options to `Aeneas` and `Charon`
+## Passing options to `Aeneas` and `Charon`
 
 The test runner supports setting several options for each test.
 - For single files, it will read comments at the top of the file that start with `//@`;
@@ -52,13 +55,18 @@ In both cases it supports the same options. Typical options are:
 
 For an up-to-date list of options, see comments in `tests/test_runner/Input.ml`.
 
-# `known-failure` tests
+## `known-failure` tests
 
 There's a special kind of test that doesn't generate backend code: `//@ known-failure` tests. These
 are meant to record:
 - Cases that produce an error so we don't forget and can fix them later;
 - Cases that _should_ error, to ensure we correctly raise an error and that the error output is nice.
 
+We record the output of the `aeneas` call in `test-file.out` alongside the original `test-file.rs`.
+This file must be committed like the rest of the test outputs. (Note: sometimes the output will be
+different between your local machine and CI, e.g. because release build changed a stacktrace. In
+that case we don't record the output, which is done with `//@ no-check-output`).
+
 It is useful to add tests there whenever you find an interesting failure case.
 
 Note however that this is for failures of Aeneas. Tests that cause Charon errors should be submitted
-- 
cgit v1.2.3