From d9d0b7cc27abecfefcb22b46333ecdeb9ec397fa Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 May 2024 15:03:37 +0200
Subject: Downgrade the version of dune

---
 tests/test_runner/dune-project | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/dune-project b/tests/test_runner/dune-project
index c614e923..dc352bd0 100644
--- a/tests/test_runner/dune-project
+++ b/tests/test_runner/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.12)
+(lang dune 3.7)
 
 (name aeneas_test_runner)
 
-- 
cgit v1.2.3


From 7935e74a9cedd93e885ab546d5513ea6c31db5ad Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 17:01:03 +0200
Subject: runner: Strongly typed Backend enum

---
 tests/test_runner/dune        |   6 ++
 tests/test_runner/run_test.ml | 144 ++++++++++++++++++++++++------------------
 2 files changed, 88 insertions(+), 62 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 7caf661f..65b0c5fe 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,4 +1,10 @@
 (executable
  (public_name test_runner)
  (libraries core_unix.sys_unix 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/run_test.ml b/tests/test_runner/run_test.ml
index 8aa6347c..2c411c95 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -5,22 +5,38 @@ type runner_env = {
   llbc_dir : string;
 }
 
-(* The data for a specific test to run aeneas on *)
-type aeneas_test_case = {
-  name : string;
-  backend : string;
-  subdir : string;
-  extra_aeneas_options : string list;
-}
+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)
 
 type input_kind = SingleFile | Crate
 
-(* The data for a specific test to generate llbc for *)
-type charon_test_case = {
-  kind : input_kind;
+(* The data for a specific test input *)
+type test_case = {
   name : string;
   path : string;
-  extra_charon_options : string list;
+  input_kind : input_kind;
+  charon_options : string list;
+  aeneas_options : string list BackendMap.t;
+  subdir : string BackendMap.t;
 }
 
 let concat_path = List.fold_left Filename.concat ""
@@ -43,21 +59,26 @@ let run_command args =
   ()
 
 (* Run Aeneas on a specific input with the given options *)
-let run_aeneas (env : runner_env) (case : aeneas_test_case) =
-  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
-  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
+let run_aeneas (env : runner_env) (case : test_case) (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"; case.backend;
+      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str;
     |]
   in
-  let args = Array.append args (Array.of_list case.extra_aeneas_options) 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 : charon_test_case) =
-  match case.kind with
+let run_charon (env : runner_env) (case : test_case) =
+  match case.input_kind with
   | SingleFile ->
       let args =
         [|
@@ -71,16 +92,14 @@ let run_charon (env : runner_env) (case : charon_test_case) =
           env.llbc_dir;
         |]
       in
-      let args = Array.append args (Array.of_list case.extra_charon_options) 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.extra_charon_options)
-          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;
@@ -96,12 +115,13 @@ let run_charon (env : runner_env) (case : charon_test_case) =
 
 (* File-specific options *)
 let aeneas_options_for_test backend test_name =
+  let backend = Backend.to_string backend in
   (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
   let use_fuel =
     match (backend, test_name) with
     | ( "coq",
-        ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main"
-        | "loops" ) ) ->
+        ("arrays" | "betree" | "demo" | "hashmap" | "hashmap_main" | "loops") )
+      ->
         true
     | "fstar", "demo" -> true
     | _ -> false
@@ -112,8 +132,7 @@ let aeneas_options_for_test backend test_name =
     backend = "fstar"
     &&
     match test_name with
-    | "arrays" | "betree_main" | "hashmap" | "hashmap_main" | "loops" | "traits"
-      ->
+    | "arrays" | "betree" | "hashmap" | "hashmap_main" | "loops" | "traits" ->
         true
     | _ -> false
   in
@@ -125,7 +144,7 @@ let aeneas_options_for_test backend test_name =
 
   let extra_options =
     match (backend, test_name) with
-    | _, "betree_main" ->
+    | _, "betree" ->
         [
           "-backward-no-state-update";
           "-test-trans-units";
@@ -172,11 +191,12 @@ let charon_options_for_test test_name =
 (* 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_main" -> "betree"
+  | _, "betree" -> "betree"
   | _, "hashmap_main" -> "hashmap_on_disk"
   | "hol4", _ -> "misc-" ^ test_name
   | ( _,
@@ -185,49 +205,49 @@ let test_subdir backend test_name =
       "misc"
   | _ -> test_name
 
+let build_test (path : string) : test_case =
+  let name = Filename.remove_extension (Filename.basename path) in
+  let input_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 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
+  { path; name; input_kind; charon_options; subdir; aeneas_options }
+
 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_name = Filename.remove_extension (Filename.basename test_path) in
-
-      let charon_kind =
-        if Sys_unix.is_file_exn test_path then SingleFile
-        else if Sys_unix.is_directory_exn test_path then Crate
-        else failwith ("`" ^ test_path ^ "` is not a file or a directory.")
-      in
-      let extra_charon_options = charon_options_for_test test_name in
-      let charon_case =
+      let test_case = build_test test_path in
+      let test_case =
         {
-          path = test_path;
-          name = test_name;
-          kind = charon_kind;
-          extra_charon_options;
+          test_case with
+          aeneas_options =
+            BackendMap.map (List.append aeneas_options) test_case.aeneas_options;
         }
       in
-      (* Generate the llbc file *)
-      run_charon runner_env charon_case;
 
-      (* FIXME: remove this special case *)
-      let test_name =
-        if test_name = "betree" then "betree_main" else test_name
-      in
-      (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
-      let backends = [ "coq"; "lean"; "fstar" ] in
+      (* Generate the llbc file *)
+      run_charon runner_env test_case;
+      (* Process the llbc file for the each backend *)
       List.iter
-        (fun backend ->
-          let subdir = test_subdir backend test_name in
-          let extra_aeneas_options =
-            List.append
-              (aeneas_options_for_test backend test_name)
-              aeneas_options
-          in
-          let aeneas_case =
-            { name = test_name; backend; subdir; extra_aeneas_options }
-          in
-          (* Process the llbc file for the current backend *)
-          run_aeneas runner_env aeneas_case)
-        backends
+        (fun backend -> run_aeneas runner_env test_case backend)
+        Backend.all
   | _ -> failwith "Incorrect options passed to test runner"
-- 
cgit v1.2.3


From 03f9d1767b19fe68c35a5adcf936ac9f39ab7882 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 17:29:05 +0200
Subject: runner: define an Input module

---
 tests/test_runner/run_test.ml | 182 +++++++++++++++++++++---------------------
 1 file changed, 92 insertions(+), 90 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 2c411c95..e168069b 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -27,18 +27,6 @@ end
 
 module BackendMap = Map.Make (Backend)
 
-type input_kind = SingleFile | Crate
-
-(* The data for a specific test input *)
-type test_case = {
-  name : string;
-  path : string;
-  input_kind : input_kind;
-  charon_options : string list;
-  aeneas_options : string list BackendMap.t;
-  subdir : string BackendMap.t;
-}
-
 let concat_path = List.fold_left Filename.concat ""
 
 let run_command args =
@@ -58,61 +46,6 @@ let run_command args =
   let _ = Unix.waitpid [] pid in
   ()
 
-(* Run Aeneas on a specific input with the given options *)
-let run_aeneas (env : runner_env) (case : test_case) (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 : test_case) =
-  match case.input_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"
-      )
-
 (* File-specific options *)
 let aeneas_options_for_test backend test_name =
   let backend = Backend.to_string backend in
@@ -205,29 +138,98 @@ let test_subdir backend test_name =
       "misc"
   | _ -> test_name
 
-let build_test (path : string) : test_case =
-  let name = Filename.remove_extension (Filename.basename path) in
-  let input_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 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
+(* The data for a specific test input *)
+module Input = struct
+  type kind = SingleFile | Crate
+
+  type t = {
+    name : string;
+    path : string;
+    kind : kind;
+    charon_options : string list;
+    aeneas_options : string list BackendMap.t;
+    subdir : string BackendMap.t;
+  }
+
+  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 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
+    { path; name; kind; charon_options; subdir; aeneas_options }
+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
-  { path; name; input_kind; charon_options; subdir; aeneas_options }
+  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
@@ -235,7 +237,7 @@ let () =
   | _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 = build_test test_path in
+      let test_case = Input.build test_path in
       let test_case =
         {
           test_case with
-- 
cgit v1.2.3


From 4d3778bea3112168645efc03308056ec341abb5f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 15:47:20 +0200
Subject: runner: Pass options in special comments

---
 tests/test_runner/dune        |   2 +-
 tests/test_runner/run_test.ml | 189 +++++++++++++++++++++++++-----------------
 2 files changed, 113 insertions(+), 78 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 65b0c5fe..e8b29d66 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,6 +1,6 @@
 (executable
  (public_name test_runner)
- (libraries core_unix.sys_unix unix)
+ (libraries core_unix.sys_unix re unix)
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv))
  (name run_test))
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index e168069b..25efbcfd 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,3 +1,15 @@
+(* 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;
@@ -48,78 +60,30 @@ let run_command args =
 
 (* File-specific options *)
 let aeneas_options_for_test backend test_name =
-  let backend = Backend.to_string backend in
-  (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
-  let use_fuel =
-    match (backend, test_name) with
-    | ( "coq",
-        ("arrays" | "betree" | "demo" | "hashmap" | "hashmap_main" | "loops") )
-      ->
-        true
-    | "fstar", "demo" -> true
-    | _ -> false
-  in
-  let options = if use_fuel then "-use-fuel" :: [] else [] in
-
-  let decrease_template_clauses =
-    backend = "fstar"
-    &&
-    match test_name with
-    | "arrays" | "betree" | "hashmap" | "hashmap_main" | "loops" | "traits" ->
-        true
-    | _ -> false
-  in
-  let options =
-    if decrease_template_clauses then
-      "-decreases-clauses" :: "-template-clauses" :: options
-    else options
-  in
-
-  let extra_options =
-    match (backend, test_name) with
-    | _, "betree" ->
-        [
-          "-backward-no-state-update";
-          "-test-trans-units";
-          "-state";
-          "-split-files";
-        ]
-    | _, "bitwise" -> [ "-test-trans-units" ]
-    | _, "constants" -> [ "-test-trans-units" ]
-    | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ]
-    | _, "hashmap_main" -> [ "-state"; "-split-files" ]
-    | _, "no_nested_borrows" -> [ "-test-trans-units" ]
-    | _, "paper" -> [ "-test-trans-units" ]
-    | _, "polonius_list" -> [ "-test-trans-units" ]
-    | "fstar", "arrays" -> [ "-split-files" ]
-    | "fstar", "loops" -> [ "-split-files" ]
-    (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *)
-    | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ]
-    | _, "hashmap" -> [ "-split-files" ]
-    | _ -> []
-  in
-  let options = List.append extra_options options in
-  options
+  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 =
-  (* Possible to add `--no-code-duplication` for `hashmap_main` if we use the optimized MIR *)
-  let no_code_dup =
-    match test_name with
-    | "constants" | "external" | "nested_borrows" | "no_nested_borrows"
-    | "paper" ->
-        [ "--no-code-duplication" ]
-    | _ -> []
-  in
-  let extra_options =
-    match test_name with
-    | "betree" ->
-        [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
-    | "hashmap_main" -> [ "--opaque=hashmap_utils" ]
-    | "polonius_list" -> [ "--polonius" ]
-    | _ -> []
-  in
-  List.append no_code_dup extra_options
+  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 *)
@@ -141,16 +105,66 @@ let test_subdir backend 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 =
@@ -158,6 +172,7 @@ 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 action = Normal in
     let charon_options = charon_options_for_test name in
     let subdir =
       List.fold_left
@@ -173,7 +188,23 @@ module Input = struct
           BackendMap.add backend opts map)
         BackendMap.empty Backend.all
     in
-    { path; name; kind; charon_options; subdir; aeneas_options }
+    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 *)
@@ -235,7 +266,7 @@ 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 ->
+    :: aeneas_options -> (
       let runner_env = { charon_path; aeneas_path; llbc_dir } in
       let test_case = Input.build test_path in
       let test_case =
@@ -246,10 +277,14 @@ let () =
         }
       in
 
-      (* 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
+      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"
-- 
cgit v1.2.3


From c4af12c1c34406720d8173f2972d4cf1f42f8f5b Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:20:04 +0200
Subject: fix generated file

---
 tests/test_runner/aeneas_test_runner.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam
index b57cc9f6..1539c521 100644
--- a/tests/test_runner/aeneas_test_runner.opam
+++ b/tests/test_runner/aeneas_test_runner.opam
@@ -7,7 +7,7 @@ homepage: "https://github.com/AeneasVerif/aeneas"
 bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
 depends: [
   "ocaml"
-  "dune" {>= "3.12"}
+  "dune" {>= "3.7"}
   "odoc" {with-doc}
 ]
 build: [
-- 
cgit v1.2.3


From 0ebfa7a15f4d7218389488ff8a92206c0d6642ec Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:20:26 +0200
Subject: runner: Allow filenames with dashes

---
 tests/test_runner/dune        | 2 +-
 tests/test_runner/run_test.ml | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index e8b29d66..1c719532 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,6 +1,6 @@
 (executable
  (public_name test_runner)
- (libraries core_unix.sys_unix re unix)
+ (libraries core_unix.sys_unix re str unix)
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv))
  (name run_test))
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 25efbcfd..3bda4e29 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -167,6 +167,7 @@ module Input = struct
   (* 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
-- 
cgit v1.2.3


From ff5c20b1ef1309f3752eaf0ffd2789514a30589d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:09:05 +0200
Subject: runner: Allow per-backend skipping

---
 tests/test_runner/run_test.ml | 65 ++++++++++++++++++++++++++++++-------------
 1 file changed, 46 insertions(+), 19 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 3bda4e29..71e2c32f 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -111,7 +111,7 @@ module Input = struct
     name : string;
     path : string;
     kind : kind;
-    action : action;
+    actions : action BackendMap.t;
     charon_options : string list;
     aeneas_options : string list BackendMap.t;
     subdir : string BackendMap.t;
@@ -124,7 +124,7 @@ module Input = struct
        - `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`.
+            aeneas; this sets options for these backends only.
   *)
   let apply_special_comment comment input =
     let comment = String.trim comment in
@@ -144,12 +144,28 @@ module Input = struct
     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 }
+    if comment = "skip" then
+      {
+        input with
+        actions =
+          List.fold_left
+            (fun map backend -> BackendMap.add backend Skip map)
+            input.actions backends;
+      }
+    else if comment = "known-failure" then
+      {
+        input with
+        actions =
+          List.fold_left
+            (fun map backend -> BackendMap.add backend KnownFailure map)
+            input.actions backends;
+      }
     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 }
+      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
@@ -173,7 +189,11 @@ 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 action = Normal in
+    let actions =
+      List.fold_left
+        (fun map backend -> BackendMap.add backend Normal map)
+        BackendMap.empty Backend.all
+    in
     let charon_options = charon_options_for_test name in
     let subdir =
       List.fold_left
@@ -190,7 +210,7 @@ module Input = struct
         BackendMap.empty Backend.all
     in
     let input =
-      { path; name; kind; action; charon_options; subdir; aeneas_options }
+      { path; name; kind; actions; charon_options; subdir; aeneas_options }
     in
     match kind with
     | SingleFile ->
@@ -267,7 +287,7 @@ 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 -> (
+    :: aeneas_options ->
       let runner_env = { charon_path; aeneas_path; llbc_dir } in
       let test_case = Input.build test_path in
       let test_case =
@@ -277,15 +297,22 @@ let () =
             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")
+      let skip_all =
+        List.for_all
+          (fun backend ->
+            BackendMap.find backend test_case.actions = Input.Skip)
+          Backend.all
+      in
+      if skip_all then ()
+      else (
+        (* Generate the llbc file *)
+        run_charon runner_env test_case;
+        (* Process the llbc file for the each backend *)
+        List.iter
+          (fun backend ->
+            match BackendMap.find backend test_case.actions with
+            | Skip -> ()
+            | Normal -> run_aeneas runner_env test_case backend
+            | KnownFailure -> failwith "KnownFailure is unimplemented")
+          Backend.all)
   | _ -> failwith "Incorrect options passed to test runner"
-- 
cgit v1.2.3


From c1892d14fc9ec728422f05dbb9de13ee92984734 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:45:45 +0200
Subject: runner: Factor out useful `BackendMap` operations

---
 tests/test_runner/run_test.ml | 59 +++++++++++++++++++------------------------
 1 file changed, 26 insertions(+), 33 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 71e2c32f..39330a77 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -37,7 +37,26 @@ module Backend = struct
     | HOL4 -> "hol4"
 end
 
-module BackendMap = Map.Make (Backend)
+module BackendMap = struct
+  include Map.Make (Backend)
+
+  (* 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
+
+  (* 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
 
 let concat_path = List.fold_left Filename.concat ""
 
@@ -145,20 +164,11 @@ module Input = struct
     let aeneas_args = Core.String.chop_prefix comment ~prefix:"aeneas-args=" in
 
     if comment = "skip" then
-      {
-        input with
-        actions =
-          List.fold_left
-            (fun map backend -> BackendMap.add backend Skip map)
-            input.actions backends;
-      }
+      { input with actions = BackendMap.add_each backends Skip input.actions }
     else if comment = "known-failure" then
       {
         input with
-        actions =
-          List.fold_left
-            (fun map backend -> BackendMap.add backend KnownFailure map)
-            input.actions backends;
+        actions = BackendMap.add_each backends KnownFailure input.actions;
       }
     else if Option.is_some charon_args then
       let args = Option.get charon_args in
@@ -173,10 +183,7 @@ module Input = struct
       {
         input with
         aeneas_options =
-          List.fold_left
-            (fun map backend ->
-              BackendMap.update backend (Option.map add_args) map)
-            input.aeneas_options backends;
+          BackendMap.update_each backends add_args input.aeneas_options;
       }
     else failwith ("Unrecognized special comment: `" ^ comment ^ "`")
 
@@ -189,25 +196,11 @@ 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 =
-      List.fold_left
-        (fun map backend -> BackendMap.add backend Normal map)
-        BackendMap.empty Backend.all
-    in
+    let actions = BackendMap.make (fun _ -> 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 subdir = BackendMap.make (fun backend -> test_subdir backend name) 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
+      BackendMap.make (fun backend -> aeneas_options_for_test backend name)
     in
     let input =
       { path; name; kind; actions; charon_options; subdir; aeneas_options }
-- 
cgit v1.2.3


From 093ebced6d22f6b805147783c978af13a7a03caa Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 16:51:54 +0200
Subject: runner: Specify subdirectory in magic comments

---
 tests/test_runner/run_test.ml | 31 ++++++++++++++++---------------
 1 file changed, 16 insertions(+), 15 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 39330a77..8f356365 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -104,21 +104,16 @@ let charon_options_for_test test_name =
       [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
   | _ -> []
 
-(* The subdirectory in which to store the outputs. *)
+(* The default 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"
+  | Backend.Lean, _ -> "."
   | _, "hashmap_main" -> "hashmap_on_disk"
-  | "hol4", _ -> "misc-" ^ test_name
-  | ( _,
-      ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows"
-      | "paper" | "polonius_list" ) ) ->
-      "misc"
+  | ( Backend.HOL4,
+      ( "constants" | "external" | "loops" | "no_nested_borrows" | "paper"
+      | "polonius_list" ) ) ->
+      "misc-" ^ test_name
   | _ -> test_name
 
 (* The data for a specific test input *)
@@ -133,13 +128,15 @@ module Input = struct
     actions : action BackendMap.t;
     charon_options : string list;
     aeneas_options : string list BackendMap.t;
-    subdir : string BackendMap.t;
+    subdirs : 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;
+       - `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
@@ -162,6 +159,7 @@ module Input = struct
     (* 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 = BackendMap.add_each backends Skip input.actions }
@@ -185,6 +183,9 @@ module Input = struct
         aeneas_options =
           BackendMap.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 }
     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. *)
@@ -198,12 +199,12 @@ module Input = struct
     in
     let actions = BackendMap.make (fun _ -> Normal) in
     let charon_options = charon_options_for_test name in
-    let subdir = BackendMap.make (fun backend -> test_subdir backend name) in
+    let subdirs = BackendMap.make (fun backend -> test_subdir backend name) in
     let aeneas_options =
       BackendMap.make (fun backend -> aeneas_options_for_test backend name)
     in
     let input =
-      { path; name; kind; actions; charon_options; subdir; aeneas_options }
+      { path; name; kind; actions; charon_options; subdirs; aeneas_options }
     in
     match kind with
     | SingleFile ->
@@ -226,7 +227,7 @@ 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 subdir = BackendMap.find backend case.subdirs 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
-- 
cgit v1.2.3


From 3adbe18d36df3767e98f30b760ccd9c6ace640ad Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 17:01:16 +0200
Subject: Rename some subdirectories for consistency

---
 tests/test_runner/run_test.ml | 20 +++++++-------------
 1 file changed, 7 insertions(+), 13 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 8f356365..5d77bf9e 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -104,18 +104,6 @@ let charon_options_for_test test_name =
       [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
   | _ -> []
 
-(* The default 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 =
-  match (backend, test_name) with
-  | Backend.Lean, _ -> "."
-  | _, "hashmap_main" -> "hashmap_on_disk"
-  | ( Backend.HOL4,
-      ( "constants" | "external" | "loops" | "no_nested_borrows" | "paper"
-      | "polonius_list" ) ) ->
-      "misc-" ^ test_name
-  | _ -> test_name
-
 (* The data for a specific test input *)
 module Input = struct
   type kind = SingleFile | Crate
@@ -131,6 +119,10 @@ module Input = struct
     subdirs : string BackendMap.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;
@@ -199,7 +191,9 @@ module Input = struct
     in
     let actions = BackendMap.make (fun _ -> Normal) in
     let charon_options = charon_options_for_test name in
-    let subdirs = BackendMap.make (fun backend -> test_subdir backend name) in
+    let subdirs =
+      BackendMap.make (fun backend -> default_subdir backend name)
+    in
     let aeneas_options =
       BackendMap.make (fun backend -> aeneas_options_for_test backend name)
     in
-- 
cgit v1.2.3


From aee6dc227c4ed041bbbae7cf38729a4b1a3a6869 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 10:48:07 +0200
Subject: runner: Correctly catch command exit status

---
 tests/test_runner/dune        |  2 +-
 tests/test_runner/run_test.ml | 67 +++++++++++++++++++++++++------------------
 2 files changed, 40 insertions(+), 29 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 1c719532..c38e009c 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,6 +1,6 @@
 (executable
  (public_name test_runner)
- (libraries core_unix.sys_unix re str unix)
+ (libraries core_unix core_unix.sys_unix re str unix)
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv))
  (name run_test))
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 5d77bf9e..a5a89317 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -60,24 +60,37 @@ end
 
 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 "";
+module Command = struct
+  type t = { args : string array }
+  type status = Success | Failure
 
-  (* Run the command *)
-  let pid =
-    Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr
-  in
-  let _ = Unix.waitpid [] pid in
-  ()
+  let make (args : string list) : t = { args = Array.of_list args }
+  let to_string (cmd : t) = Core.String.concat_array ~sep:" " cmd.args
+
+  (* Run the command and returns its exit status. *)
+  let run (cmd : t) : status =
+    let command_str = to_string cmd in
+    print_endline ("[test_runner] Running: " ^ command_str);
+
+    (* Run the command *)
+    let pid =
+      Unix.create_process cmd.args.(0) cmd.args Unix.stdin Unix.stdout
+        Unix.stderr
+    in
+    let status = Core_unix.waitpid (Core.Pid.of_int pid) in
+    match status with
+    | Ok () -> Success
+    | Error (`Exit_non_zero _) -> Failure
+    | Error (`Signal _) ->
+        failwith ("Command `" ^ command_str ^ "` exited incorrectly.")
+
+  (* Run the command and aborts the program if the command failed. *)
+  let run_command_expecting_success cmd =
+    match run cmd with
+    | Success -> ()
+    | Failure -> failwith ("Command `" ^ to_string cmd ^ "` failed.")
+end
 
-(* File-specific options *)
 let aeneas_options_for_test backend test_name =
   if test_name = "betree" then
     let options =
@@ -226,20 +239,18 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   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;
-    |]
+    [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ]
   in
-  let args = Array.append args (Array.of_list aeneas_options) in
+  let args = List.append args aeneas_options in
   (* Run Aeneas *)
-  run_command args
+  Command.run_command_expecting_success (Command.make 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";
@@ -248,20 +259,20 @@ let run_charon (env : runner_env) (case : Input.t) =
           case.name;
           "--dest";
           env.llbc_dir;
-        |]
+        ]
       in
-      let args = Array.append args (Array.of_list case.charon_options) in
+      let args = List.append args case.charon_options in
       (* Run Charon on the rust file *)
-      run_command args
+      Command.run_command_expecting_success (Command.make 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
+          let args = [ env.charon_path; "--dest"; env.llbc_dir ] in
+          let args = List.append args case.charon_options in
           (* Run Charon inside the crate *)
           let old_pwd = Unix.getcwd () in
           Unix.chdir case.path;
-          run_command args;
+          Command.run_command_expecting_success (Command.make args);
           Unix.chdir old_pwd
       | Some _ ->
           (* Crates with dependencies must be generated separately in CI. We skip
-- 
cgit v1.2.3


From 9c09789c26dd8142b8a29b42e250a685aa983e58 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 11:22:37 +0200
Subject: runner: Support negative tests

---
 tests/test_runner/dune        |  2 +-
 tests/test_runner/run_test.ml | 70 +++++++++++++++++++++++++++++++------------
 2 files changed, 52 insertions(+), 20 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index c38e009c..6bb3f7b2 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,6 +1,6 @@
 (executable
  (public_name test_runner)
- (libraries core_unix core_unix.sys_unix re str unix)
+ (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))
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index a5a89317..7a52b6f3 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -15,6 +15,7 @@ type runner_env = {
   charon_path : string;
   aeneas_path : string;
   llbc_dir : string;
+  dest_dir : string;
 }
 
 module Backend = struct
@@ -61,10 +62,12 @@ end
 let concat_path = List.fold_left Filename.concat ""
 
 module Command = struct
-  type t = { args : string array }
+  type t = { args : string array; redirect_out : Unix.file_descr option }
   type status = Success | Failure
 
-  let make (args : string list) : t = { args = Array.of_list args }
+  let make (args : string list) : t =
+    { args = Array.of_list args; redirect_out = None }
+
   let to_string (cmd : t) = Core.String.concat_array ~sep:" " cmd.args
 
   (* Run the command and returns its exit status. *)
@@ -73,10 +76,8 @@ module Command = struct
     print_endline ("[test_runner] Running: " ^ command_str);
 
     (* Run the command *)
-    let pid =
-      Unix.create_process cmd.args.(0) cmd.args Unix.stdin Unix.stdout
-        Unix.stderr
-    in
+    let out = Option.value cmd.redirect_out ~default:Unix.stdout in
+    let pid = Unix.create_process cmd.args.(0) cmd.args Unix.stdin out out in
     let status = Core_unix.waitpid (Core.Pid.of_int pid) in
     match status with
     | Ok () -> Success
@@ -89,6 +90,14 @@ module Command = struct
     match run cmd with
     | Success -> ()
     | Failure -> failwith ("Command `" ^ to_string cmd ^ "` failed.")
+
+  (* Run the command and aborts the program if the command succeeded. *)
+  let run_command_expecting_failure cmd =
+    match run cmd with
+    | Success ->
+        failwith
+          ("Command `" ^ to_string cmd ^ "` succeeded but was expected to fail.")
+    | Failure -> ()
 end
 
 let aeneas_options_for_test backend test_name =
@@ -232,18 +241,43 @@ 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 backend_str = Backend.to_string backend in
   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 output_file =
+    Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
+  in
   let subdir = BackendMap.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 backend_str = Backend.to_string backend in
-  let dest_dir = concat_path [ "tests"; backend_str; subdir ] in
+  let action = BackendMap.find backend case.actions in
+
+  (* Build the command *)
   let args =
     [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ]
   in
-  let args = List.append args aeneas_options in
+  let abort_on_error =
+    match action with
+    | Skip | Normal -> []
+    | KnownFailure -> [ "-abort-on-error" ]
+  in
+  let args = List.concat [ args; aeneas_options; abort_on_error ] in
+  let cmd = Command.make args in
+  (* Remove leftover files if they're not needed anymore *)
+  (match action with
+  | (Skip | Normal) when Sys.file_exists output_file -> Sys.remove output_file
+  | _ -> ());
   (* Run Aeneas *)
-  Command.run_command_expecting_success (Command.make args)
+  match action with
+  | Skip -> ()
+  | Normal -> Command.run_command_expecting_success cmd
+  | KnownFailure ->
+      let out =
+        Core_unix.openfile ~mode:[ O_CREAT; O_TRUNC; O_WRONLY ] output_file
+      in
+      let cmd = { cmd with redirect_out = Some out } in
+      Command.run_command_expecting_failure cmd;
+      Unix.close out
 
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : runner_env) (case : Input.t) =
@@ -267,7 +301,9 @@ let run_charon (env : runner_env) (case : Input.t) =
   | Crate -> (
       match Sys.getenv_opt "IN_CI" with
       | None ->
-          let args = [ env.charon_path; "--dest"; env.llbc_dir ] in
+          let args =
+            [ env.charon_path; "--dest"; Filename_unix.realpath env.llbc_dir ]
+          in
           let args = List.append args case.charon_options in
           (* Run Charon inside the crate *)
           let old_pwd = Unix.getcwd () in
@@ -287,7 +323,9 @@ let () =
   (* 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 runner_env =
+        { charon_path; aeneas_path; llbc_dir; dest_dir = "tests" }
+      in
       let test_case = Input.build test_path in
       let test_case =
         {
@@ -307,11 +345,5 @@ let () =
         (* Generate the llbc file *)
         run_charon runner_env test_case;
         (* Process the llbc file for the each backend *)
-        List.iter
-          (fun backend ->
-            match BackendMap.find backend test_case.actions with
-            | Skip -> ()
-            | Normal -> run_aeneas runner_env test_case backend
-            | KnownFailure -> failwith "KnownFailure is unimplemented")
-          Backend.all)
+        List.iter (run_aeneas runner_env test_case) Backend.all)
   | _ -> failwith "Incorrect options passed to test runner"
-- 
cgit v1.2.3


From fb16d0af4caacd2c9a3463f6d2b455209b755697 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 14:34:12 +0200
Subject: runner: Add `no-check-output` option for unstable outputs

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

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 7a52b6f3..1c885d4b 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -139,6 +139,8 @@ module Input = struct
     charon_options : string list;
     aeneas_options : string list BackendMap.t;
     subdirs : string BackendMap.t;
+    (* Whether to store the command output to a file. Only available for known-failure tests. *)
+    check_output : bool BackendMap.t;
   }
 
   (* The default subdirectory in which to store the outputs. *)
@@ -182,6 +184,11 @@ module Input = struct
         input with
         actions = BackendMap.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;
+      }
     else if Option.is_some charon_args then
       let args = Option.get charon_args in
       let args = String.split_on_char ' ' args in
@@ -219,8 +226,18 @@ module Input = struct
     let aeneas_options =
       BackendMap.make (fun backend -> aeneas_options_for_test backend name)
     in
+    let check_output = BackendMap.make (fun _ -> true) in
     let input =
-      { path; name; kind; actions; charon_options; subdirs; aeneas_options }
+      {
+        path;
+        name;
+        kind;
+        actions;
+        charon_options;
+        subdirs;
+        aeneas_options;
+        check_output;
+      }
     in
     match kind with
     | SingleFile ->
@@ -251,6 +268,7 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   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
 
   (* Build the command *)
   let args =
@@ -264,21 +282,27 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   let args = List.concat [ args; aeneas_options; abort_on_error ] in
   let cmd = Command.make args in
   (* Remove leftover files if they're not needed anymore *)
-  (match action with
-  | (Skip | Normal) when Sys.file_exists output_file -> Sys.remove output_file
-  | _ -> ());
+  if
+    Sys.file_exists output_file
+    &&
+    match action with
+    | Skip | Normal -> true
+    | KnownFailure when not check_output -> true
+    | _ -> false
+  then Sys.remove output_file;
   (* Run Aeneas *)
   match action with
   | Skip -> ()
   | Normal -> Command.run_command_expecting_success cmd
   | KnownFailure ->
       let out =
-        Core_unix.openfile ~mode:[ O_CREAT; O_TRUNC; O_WRONLY ] output_file
+        if check_output then
+          Core_unix.openfile ~mode:[ O_CREAT; O_TRUNC; O_WRONLY ] output_file
+        else Core_unix.openfile ~mode:[ O_WRONLY ] "/dev/null"
       in
       let cmd = { cmd with redirect_out = Some out } in
       Command.run_command_expecting_failure cmd;
       Unix.close out
-
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : runner_env) (case : Input.t) =
   match case.kind with
-- 
cgit v1.2.3


From f77e3f9cbe2ea7abeb4be815bdbf33d0c98076c2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 13:28:28 +0200
Subject: tests: Rename betree_main -> betree

---
 tests/test_runner/run_test.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 1c885d4b..a7b83e88 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -122,8 +122,7 @@ let aeneas_options_for_test backend test_name =
 (* File-specific options *)
 let charon_options_for_test test_name =
   match test_name with
-  | "betree" ->
-      [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
+  | "betree" -> [ "--polonius"; "--opaque=betree_utils" ]
   | _ -> []
 
 (* The data for a specific test input *)
@@ -257,10 +256,8 @@ 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 backend_str = Backend.to_string backend in
-  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 input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
   let output_file =
     Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
   in
-- 
cgit v1.2.3


From 9cc69020773cc77965a6faa6f0d46f179de3d8b8 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 17:22:07 +0200
Subject: runner: Store options for crate tests in a separate file

---
 tests/test_runner/run_test.ml | 40 ++++++++++------------------------------
 1 file changed, 10 insertions(+), 30 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index a7b83e88..c626b4d1 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -100,31 +100,6 @@ module Command = struct
     | Failure -> ()
 end
 
-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" ]
-  | _ -> []
-
 (* The data for a specific test input *)
 module Input = struct
   type kind = SingleFile | Crate
@@ -218,13 +193,10 @@ module Input = struct
       else failwith ("`" ^ path ^ "` is not a file or a directory.")
     in
     let actions = BackendMap.make (fun _ -> Normal) in
-    let charon_options = charon_options_for_test name in
     let subdirs =
       BackendMap.make (fun backend -> default_subdir backend name)
     in
-    let aeneas_options =
-      BackendMap.make (fun backend -> aeneas_options_for_test backend name)
-    in
+    let aeneas_options = BackendMap.make (fun _ -> []) in
     let check_output = BackendMap.make (fun _ -> true) in
     let input =
       {
@@ -232,12 +204,14 @@ module Input = struct
         name;
         kind;
         actions;
-        charon_options;
+        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
@@ -251,6 +225,11 @@ module Input = struct
         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
 
@@ -300,6 +279,7 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
       let cmd = { cmd with redirect_out = Some out } in
       Command.run_command_expecting_failure cmd;
       Unix.close out
+
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : runner_env) (case : Input.t) =
   match case.kind with
-- 
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(-)

(limited to 'tests/test_runner')

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/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 ------------------------------------------
 5 files changed, 190 insertions(+), 197 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

(limited to 'tests/test_runner')

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(-)

(limited to 'tests/test_runner')

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