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

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

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/.ocamlformat b/tests/test_runner/.ocamlformat
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam
new file mode 100644
index 00000000..b57cc9f6
--- /dev/null
+++ b/tests/test_runner/aeneas_test_runner.opam
@@ -0,0 +1,27 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "0.1"
+authors: ["Son Ho" "Guillaume Boisseau"]
+license: "Apache-2.0"
+homepage: "https://github.com/AeneasVerif/aeneas"
+bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
+depends: [
+  "ocaml"
+  "dune" {>= "3.12"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/AeneasVerif/aeneas.git"
diff --git a/tests/test_runner/dune b/tests/test_runner/dune
new file mode 100644
index 00000000..7da7a96d
--- /dev/null
+++ b/tests/test_runner/dune
@@ -0,0 +1,4 @@
+(executable
+ (public_name test_runner)
+ (libraries unix)
+ (name run_test))
diff --git a/tests/test_runner/dune-project b/tests/test_runner/dune-project
new file mode 100644
index 00000000..c614e923
--- /dev/null
+++ b/tests/test_runner/dune-project
@@ -0,0 +1,25 @@
+(lang dune 3.12)
+
+(name aeneas_test_runner)
+
+(version 0.1)
+
+(generate_opam_files true)
+
+(source
+ (uri git+https://github.com/AeneasVerif/aeneas.git))
+
+(homepage "https://github.com/AeneasVerif/aeneas")
+
+(bug_reports "https://github.com/AeneasVerif/aeneas/issues")
+
+(authors
+  "Son Ho"
+  "Guillaume Boisseau")
+
+(license Apache-2.0)
+
+(package
+ (name aeneas_test_runner)
+ (depends ocaml dune)
+)
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
new file mode 100644
index 00000000..379abe04
--- /dev/null
+++ b/tests/test_runner/run_test.ml
@@ -0,0 +1,30 @@
+let concat_path = List.fold_left Filename.concat ""
+
+let () =
+  match Array.to_list Sys.argv with
+  (* Ad-hoc argument passing for now. *)
+  | _exe_path :: aeneas_path :: tests_dir :: test_name :: subdir :: backend
+    :: options ->
+      let input_file = concat_path [ tests_dir; "llbc"; test_name ] ^ ".llbc" in
+      let dest_dir = concat_path [ "tests"; backend; subdir ] in
+      let args =
+        [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |]
+      in
+      let args = Array.append args (Array.of_list options) in
+
+      (* Debug arguments *)
+      print_string "[test_runner] Running: ";
+      Array.iter
+        (fun x ->
+          print_string x;
+          print_string " ")
+        args;
+      print_endline "";
+
+      (* Run Aeneas *)
+      let pid =
+        Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+      in
+      let _ = Unix.waitpid [] pid in
+      ()
+  | _ -> ()
-- 
cgit v1.2.3


From 6ae8cde046530371345863f04d84be32b2a757bf Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 22 May 2024 18:57:19 +0200
Subject: Move the subdirectory selection to the test runner

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

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 379abe04..52ff7276 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -3,9 +3,32 @@ let concat_path = List.fold_left Filename.concat ""
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: aeneas_path :: tests_dir :: test_name :: subdir :: backend
-    :: options ->
-      let input_file = concat_path [ tests_dir; "llbc"; test_name ] ^ ".llbc" in
+  | _exe_path :: aeneas_path :: tests_dir :: test_name :: backend :: options ->
+      (* Reproduces the file layout that was set by the Makefile. FIXME: cleanup *)
+      let subdir =
+        match (backend, test_name) with
+        | "lean", "demo" -> "Demo"
+        | "lean", _ -> "."
+        | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
+        | _, "betree_main" -> "betree"
+        | _, "betree_main-special" -> "betree_back_stateful"
+        | _, "hashmap_main" -> "hashmap_on_disk"
+        | "hol4", _ -> "misc-" ^ test_name
+        | ( _,
+            ( "bitwise" | "constants" | "external" | "loops"
+            | "no_nested_borrows" | "paper" | "polonius_list" ) ) ->
+            "misc"
+        | _ -> test_name
+      in
+
+      let test_file_name =
+        match test_name with
+        | "betree_main-special" -> "betree_main"
+        | _ -> test_name
+      in
+      let input_file =
+        concat_path [ tests_dir; "llbc"; test_file_name ] ^ ".llbc"
+      in
       let dest_dir = concat_path [ "tests"; backend; subdir ] in
       let args =
         [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |]
-- 
cgit v1.2.3


From a9471e615e03d6fa0bc1594176fe504c9a3c88ae Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 22 May 2024 19:23:03 +0200
Subject: Set all options in the test runner

---
 tests/test_runner/run_test.ml | 57 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 52ff7276..949d5307 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -21,6 +21,63 @@ let () =
         | _ -> test_name
       in
 
+      (* File-specific options *)
+      (* 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" ) ) ->
+            true
+        | "fstar", "demo" -> true
+        | _ -> false
+      in
+      let options = if use_fuel then "-use-fuel" :: options else options in
+
+      let decrease_template_clauses =
+        backend = "fstar"
+        &&
+        match test_name with
+        | "arrays" | "betree_main" | "betree_main-special" | "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
+        (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
+        (* This generates very ugly code, but is good to test the translation. *)
+        | _, "betree_main-special" ->
+            [ "-test-trans-units"; "-state"; "-split-files" ]
+        | _, "betree_main" ->
+            [
+              "-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
+
       let test_file_name =
         match test_name with
         | "betree_main-special" -> "betree_main"
-- 
cgit v1.2.3


From 9e834db4174a900845199ccb189b575a20f11eda Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 09:58:36 +0200
Subject: Cleanup test runner

---
 tests/test_runner/run_test.ml | 223 +++++++++++++++++++++++-------------------
 1 file changed, 124 insertions(+), 99 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 949d5307..1ec2d1c8 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,110 +1,135 @@
-let concat_path = List.fold_left Filename.concat ""
+(* Paths to use for tests *)
+type test_env = { aeneas_path : string; llbc_dir : string }
 
-let () =
-  match Array.to_list Sys.argv with
-  (* Ad-hoc argument passing for now. *)
-  | _exe_path :: aeneas_path :: tests_dir :: test_name :: backend :: options ->
-      (* Reproduces the file layout that was set by the Makefile. FIXME: cleanup *)
-      let subdir =
-        match (backend, test_name) with
-        | "lean", "demo" -> "Demo"
-        | "lean", _ -> "."
-        | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
-        | _, "betree_main" -> "betree"
-        | _, "betree_main-special" -> "betree_back_stateful"
-        | _, "hashmap_main" -> "hashmap_on_disk"
-        | "hol4", _ -> "misc-" ^ test_name
-        | ( _,
-            ( "bitwise" | "constants" | "external" | "loops"
-            | "no_nested_borrows" | "paper" | "polonius_list" ) ) ->
-            "misc"
-        | _ -> test_name
-      in
+(* The data for a specific test to run *)
+type test_case = {
+  name : string;
+  backend : string;
+  subdir : string;
+  extra_aeneas_options : string list;
+}
 
-      (* File-specific options *)
-      (* 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" ) ) ->
-            true
-        | "fstar", "demo" -> true
-        | _ -> false
-      in
-      let options = if use_fuel then "-use-fuel" :: options else options in
+(* Run Aeneas on a specific input with the given options *)
+let run_test env case =
+  let concat_path = List.fold_left Filename.concat "" in
+  let input_file = concat_path [ env.llbc_dir; "llbc"; case.name ] ^ ".llbc" in
+  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
+  let args =
+    [|
+      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
+    |]
+  in
+  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
 
-      let decrease_template_clauses =
-        backend = "fstar"
-        &&
-        match test_name with
-        | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
-        | "hashmap_main" | "loops" | "traits" ->
-            true
-        | _ -> false
-      in
-      let options =
-        if decrease_template_clauses then
-          "-decreases-clauses" :: "-template-clauses" :: options
-        else options
-      in
+  (* Debug arguments *)
+  print_string "[test_runner] Running: ";
+  Array.iter
+    (fun x ->
+      print_string x;
+      print_string " ")
+    args;
+  print_endline "";
 
-      let extra_options =
-        match (backend, test_name) with
-        (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
-        (* This generates very ugly code, but is good to test the translation. *)
-        | _, "betree_main-special" ->
-            [ "-test-trans-units"; "-state"; "-split-files" ]
-        | _, "betree_main" ->
-            [
-              "-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
+  (* Run Aeneas *)
+  let pid =
+    Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+  in
+  let _ = Unix.waitpid [] pid in
+  ()
+
+(* File-specific options *)
+let test_options backend test_name =
+  (* 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" ) ) ->
+        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_main" | "betree_main-special" | "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
+    (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
+    (* This generates very ugly code, but is good to test the translation. *)
+    | _, "betree_main-special" ->
+        [ "-test-trans-units"; "-state"; "-split-files" ]
+    | _, "betree_main" ->
+        [
+          "-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
+
+(* 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 =
+  match (backend, test_name) with
+  | "lean", "demo" -> "Demo"
+  | "lean", _ -> "."
+  | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
+  | _, "betree_main" -> "betree"
+  | _, "betree_main-special" -> "betree_back_stateful"
+  | _, "hashmap_main" -> "hashmap_on_disk"
+  | "hol4", _ -> "misc-" ^ test_name
+  | ( _,
+      ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows"
+      | "paper" | "polonius_list" ) ) ->
+      "misc"
+  | _ -> test_name
+
+let () =
+  match Array.to_list Sys.argv with
+  (* Ad-hoc argument passing for now. *)
+  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: backend :: options ->
+      let subdir = test_subdir backend test_name in
+      let options = List.append (test_options backend test_name) options in
 
       let test_file_name =
         match test_name with
         | "betree_main-special" -> "betree_main"
         | _ -> test_name
       in
-      let input_file =
-        concat_path [ tests_dir; "llbc"; test_file_name ] ^ ".llbc"
-      in
-      let dest_dir = concat_path [ "tests"; backend; subdir ] in
-      let args =
-        [| aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend |]
-      in
-      let args = Array.append args (Array.of_list options) in
-
-      (* Debug arguments *)
-      print_string "[test_runner] Running: ";
-      Array.iter
-        (fun x ->
-          print_string x;
-          print_string " ")
-        args;
-      print_endline "";
-
-      (* Run Aeneas *)
-      let pid =
-        Unix.create_process aeneas_path args Unix.stdin Unix.stdout Unix.stderr
-      in
-      let _ = Unix.waitpid [] pid in
-      ()
+      run_test { aeneas_path; llbc_dir }
+        {
+          name = test_file_name;
+          backend;
+          subdir;
+          extra_aeneas_options = options;
+        }
   | _ -> ()
-- 
cgit v1.2.3


From b953b89f9739c6703c49667781f5509b1b2a3898 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 10:05:04 +0200
Subject: Let the runner choose which backends to use

---
 tests/test_runner/run_test.ml | 38 +++++++++++++++++++++++---------------
 1 file changed, 23 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 1ec2d1c8..52619c4a 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -116,20 +116,28 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: backend :: options ->
-      let subdir = test_subdir backend test_name in
-      let options = List.append (test_options backend test_name) options in
-
-      let test_file_name =
+  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options ->
+      let tests_env = { aeneas_path; llbc_dir } in
+      (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
+      let backends =
         match test_name with
-        | "betree_main-special" -> "betree_main"
-        | _ -> test_name
+        | "betree_main-special" -> [ "fstar" ]
+        | _ -> [ "coq"; "lean"; "fstar" ]
       in
-      run_test { aeneas_path; llbc_dir }
-        {
-          name = test_file_name;
-          backend;
-          subdir;
-          extra_aeneas_options = options;
-        }
-  | _ -> ()
+      List.iter
+        (fun backend ->
+          let subdir = test_subdir backend test_name in
+          let extra_aeneas_options =
+            List.append (test_options backend test_name) options
+          in
+          let test_file_name =
+            match test_name with
+            | "betree_main-special" -> "betree_main"
+            | _ -> test_name
+          in
+          let test_case =
+            { name = test_file_name; backend; subdir; extra_aeneas_options }
+          in
+          run_test tests_env test_case)
+        backends
+  | _ -> failwith "Incorrect options passed to test runner"
-- 
cgit v1.2.3


From b8bdf14f3e4b25578d107160161f5bd2b548a113 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 14:06:51 +0200
Subject: Remove secondary betree test

Opened https://github.com/AeneasVerif/aeneas/issues/196 to remember to
add a more adequate replacement test.
---
 tests/test_runner/run_test.ml | 22 ++++------------------
 1 file changed, 4 insertions(+), 18 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 52619c4a..d3fe8836 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -55,8 +55,8 @@ let test_options backend test_name =
     backend = "fstar"
     &&
     match test_name with
-    | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
-    | "hashmap_main" | "loops" | "traits" ->
+    | "arrays" | "betree_main" | "hashmap" | "hashmap_main" | "loops" | "traits"
+      ->
         true
     | _ -> false
   in
@@ -68,10 +68,6 @@ let test_options backend test_name =
 
   let extra_options =
     match (backend, test_name) with
-    (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
-    (* This generates very ugly code, but is good to test the translation. *)
-    | _, "betree_main-special" ->
-        [ "-test-trans-units"; "-state"; "-split-files" ]
     | _, "betree_main" ->
         [
           "-backward-no-state-update";
@@ -104,7 +100,6 @@ let test_subdir backend test_name =
   | "lean", _ -> "."
   | _, ("arrays" | "demo" | "hashmap" | "traits") -> test_name
   | _, "betree_main" -> "betree"
-  | _, "betree_main-special" -> "betree_back_stateful"
   | _, "hashmap_main" -> "hashmap_on_disk"
   | "hol4", _ -> "misc-" ^ test_name
   | ( _,
@@ -119,24 +114,15 @@ let () =
   | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options ->
       let tests_env = { aeneas_path; llbc_dir } in
       (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
-      let backends =
-        match test_name with
-        | "betree_main-special" -> [ "fstar" ]
-        | _ -> [ "coq"; "lean"; "fstar" ]
-      in
+      let backends = [ "coq"; "lean"; "fstar" ] in
       List.iter
         (fun backend ->
           let subdir = test_subdir backend test_name in
           let extra_aeneas_options =
             List.append (test_options backend test_name) options
           in
-          let test_file_name =
-            match test_name with
-            | "betree_main-special" -> "betree_main"
-            | _ -> test_name
-          in
           let test_case =
-            { name = test_file_name; backend; subdir; extra_aeneas_options }
+            { name = test_name; backend; subdir; extra_aeneas_options }
           in
           run_test tests_env test_case)
         backends
-- 
cgit v1.2.3


From 4ce3e9c7c11744abae52d7a3ae1a3962395784be Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 10:41:10 +0200
Subject: Import test suite from charon

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

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index d3fe8836..8b4a4208 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -12,7 +12,7 @@ type test_case = {
 (* Run Aeneas on a specific input with the given options *)
 let run_test env case =
   let concat_path = List.fold_left Filename.concat "" in
-  let input_file = concat_path [ env.llbc_dir; "llbc"; case.name ] ^ ".llbc" in
+  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
   let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
   let args =
     [|
-- 
cgit v1.2.3


From 3a380f990d0f202ee19bd163726ff5fc63181ae7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 14:38:50 +0200
Subject: Use runner to generate llbc

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

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 8b4a4208..d80231d0 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,26 +1,26 @@
 (* Paths to use for tests *)
-type test_env = { aeneas_path : string; llbc_dir : string }
+type aeneas_env = { aeneas_path : string; llbc_dir : string }
 
-(* The data for a specific test to run *)
-type test_case = {
+type charon_env = {
+  charon_path : string;
+  inputs_dir : string;
+  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;
 }
 
-(* Run Aeneas on a specific input with the given options *)
-let run_test env case =
-  let concat_path = List.fold_left Filename.concat "" in
-  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
-  let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
-  let args =
-    [|
-      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
-    |]
-  in
-  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
+(* The data for a specific test to generate llbc for *)
+type charon_test_case = { name : string; extra_charon_options : string list }
 
+let concat_path = List.fold_left Filename.concat ""
+
+let run_command args =
   (* Debug arguments *)
   print_string "[test_runner] Running: ";
   Array.iter
@@ -30,15 +30,66 @@ let run_test env case =
     args;
   print_endline "";
 
-  (* Run Aeneas *)
+  (* Run the command *)
   let pid =
-    Unix.create_process env.aeneas_path args Unix.stdin Unix.stdout Unix.stderr
+    Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr
   in
   let _ = Unix.waitpid [] pid in
   ()
 
+(* Run Aeneas on a specific input with the given options *)
+let run_aeneas (env : aeneas_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 args =
+    [|
+      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; case.backend;
+    |]
+  in
+  let args = Array.append args (Array.of_list case.extra_aeneas_options) in
+  (* Run Aeneas *)
+  run_command args
+
+(* Run Charon on a specific input with the given options *)
+let run_charon (env : charon_env) (case : charon_test_case) =
+  let input_crate = concat_path [ env.inputs_dir; case.name ] in
+  let input_file = input_crate ^ ".rs" in
+  if Sys.file_exists input_file then
+    let args =
+      [|
+        env.charon_path;
+        "--no-cargo";
+        "--input";
+        input_file;
+        "--crate";
+        case.name;
+        "--dest";
+        env.llbc_dir;
+      |]
+    in
+    let args = Array.append args (Array.of_list case.extra_charon_options) in
+    (* Run Charon on the rust file *)
+    run_command args
+  else if Sys.file_exists input_crate then
+    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
+        (* Run Charon inside the crate *)
+        Unix.chdir input_crate;
+        run_command args
+    | 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"
+  else failwith ("Neither " ^ input_file ^ " nor " ^ input_crate ^ " exist.")
+
 (* File-specific options *)
-let test_options backend test_name =
+let aeneas_options_for_test backend test_name =
   (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
   let use_fuel =
     match (backend, test_name) with
@@ -92,6 +143,27 @@ let test_options backend test_name =
   let options = List.append extra_options options in
   options
 
+(* 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 =
+    (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *)
+    match test_name with
+    | "betree_main" ->
+        [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
+    | "hashmap_main" -> [ "--opaque=hashmap_utils" ]
+    | "polonius_list" -> [ "--polonius" ]
+    | _ -> []
+  in
+  List.append no_code_dup extra_options
+
 (* 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 =
@@ -111,7 +183,7 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: aeneas_path :: llbc_dir :: test_name :: options ->
+  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_name :: options ->
       let tests_env = { aeneas_path; llbc_dir } in
       (* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
       let backends = [ "coq"; "lean"; "fstar" ] in
@@ -119,11 +191,23 @@ let () =
         (fun backend ->
           let subdir = test_subdir backend test_name in
           let extra_aeneas_options =
-            List.append (test_options backend test_name) options
+            List.append (aeneas_options_for_test backend test_name) options
           in
           let test_case =
             { name = test_name; backend; subdir; extra_aeneas_options }
           in
-          run_test tests_env test_case)
+          run_aeneas tests_env test_case)
         backends
+  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name
+    :: options ->
+      let tests_env = { charon_path; inputs_dir; llbc_dir } in
+      let extra_charon_options =
+        List.append (charon_options_for_test test_name) options
+      in
+      (* FIXME: remove this special case *)
+      let test_name =
+        if test_name = "betree_main" then "betree" else test_name
+      in
+      let test_case = { name = test_name; extra_charon_options } in
+      run_charon tests_env test_case
   | _ -> failwith "Incorrect options passed to test runner"
-- 
cgit v1.2.3


From ca045d57b6cc3fc700efe07bfc257231edf814e5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 15:37:01 +0200
Subject: Auto-detect test cases

---
 tests/test_runner/dune        |  2 +-
 tests/test_runner/run_test.ml | 38 ++++++++++++++++++++++----------------
 2 files changed, 23 insertions(+), 17 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 7da7a96d..7caf661f 100644
--- a/tests/test_runner/dune
+++ b/tests/test_runner/dune
@@ -1,4 +1,4 @@
 (executable
  (public_name test_runner)
- (libraries unix)
+ (libraries core_unix.sys_unix unix)
  (name run_test))
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index d80231d0..688c81ae 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -16,7 +16,11 @@ type aeneas_test_case = {
 }
 
 (* The data for a specific test to generate llbc for *)
-type charon_test_case = { name : string; extra_charon_options : string list }
+type charon_test_case = {
+  name : string;
+  path : string;
+  extra_charon_options : string list;
+}
 
 let concat_path = List.fold_left Filename.concat ""
 
@@ -52,15 +56,14 @@ let run_aeneas (env : aeneas_env) (case : aeneas_test_case) =
 
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : charon_env) (case : charon_test_case) =
-  let input_crate = concat_path [ env.inputs_dir; case.name ] in
-  let input_file = input_crate ^ ".rs" in
-  if Sys.file_exists input_file then
+  let input_path = concat_path [ env.inputs_dir; case.path ] in
+  if Sys_unix.is_file_exn input_path then
     let args =
       [|
         env.charon_path;
         "--no-cargo";
         "--input";
-        input_file;
+        input_path;
         "--crate";
         case.name;
         "--dest";
@@ -70,7 +73,7 @@ let run_charon (env : charon_env) (case : charon_test_case) =
     let args = Array.append args (Array.of_list case.extra_charon_options) in
     (* Run Charon on the rust file *)
     run_command args
-  else if Sys.file_exists input_crate then
+  else if Sys.is_directory input_path then
     match Sys.getenv_opt "IN_CI" with
     | None ->
         let args = [| env.charon_path; "--dest"; env.llbc_dir |] in
@@ -78,7 +81,7 @@ let run_charon (env : charon_env) (case : charon_test_case) =
           Array.append args (Array.of_list case.extra_charon_options)
         in
         (* Run Charon inside the crate *)
-        Unix.chdir input_crate;
+        Unix.chdir input_path;
         run_command args
     | Some _ ->
         (* Crates with dependencies must be generated separately in CI. We skip
@@ -86,7 +89,7 @@ let run_charon (env : charon_env) (case : charon_test_case) =
            file. *)
         print_endline
           "Warn: IN_CI is set; we skip generating llbc files for whole crates"
-  else failwith ("Neither " ^ input_file ^ " nor " ^ input_crate ^ " exist.")
+  else failwith ("`" ^ input_path ^ "` is not a file or a directory.")
 
 (* File-specific options *)
 let aeneas_options_for_test backend test_name =
@@ -154,9 +157,8 @@ let charon_options_for_test test_name =
     | _ -> []
   in
   let extra_options =
-    (* $(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main *)
     match test_name with
-    | "betree_main" ->
+    | "betree" ->
         [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
     | "hashmap_main" -> [ "--opaque=hashmap_utils" ]
     | "polonius_list" -> [ "--polonius" ]
@@ -183,8 +185,13 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_name :: options ->
+  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_path :: options ->
       let tests_env = { aeneas_path; llbc_dir } in
+      let test_name = Filename.remove_extension test_path in
+      (* 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
       List.iter
@@ -198,16 +205,15 @@ let () =
           in
           run_aeneas tests_env test_case)
         backends
-  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_name
+  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_path
     :: options ->
       let tests_env = { charon_path; inputs_dir; llbc_dir } in
+      let test_name = Filename.remove_extension test_path in
       let extra_charon_options =
         List.append (charon_options_for_test test_name) options
       in
-      (* FIXME: remove this special case *)
-      let test_name =
-        if test_name = "betree_main" then "betree" else test_name
+      let test_case =
+        { name = test_name; path = test_path; extra_charon_options }
       in
-      let test_case = { name = test_name; extra_charon_options } in
       run_charon tests_env test_case
   | _ -> failwith "Incorrect options passed to test runner"
-- 
cgit v1.2.3


From d37a302762fef4ea91b88f0ca8feb73612ff5382 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 15:46:45 +0200
Subject: runner: Do both steps of generation at once

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

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 688c81ae..5eff95af 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -1,8 +1,7 @@
 (* Paths to use for tests *)
-type aeneas_env = { aeneas_path : string; llbc_dir : string }
-
-type charon_env = {
+type runner_env = {
   charon_path : string;
+  aeneas_path : string;
   inputs_dir : string;
   llbc_dir : string;
 }
@@ -42,7 +41,7 @@ let run_command args =
   ()
 
 (* Run Aeneas on a specific input with the given options *)
-let run_aeneas (env : aeneas_env) (case : aeneas_test_case) =
+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 args =
@@ -55,7 +54,7 @@ let run_aeneas (env : aeneas_env) (case : aeneas_test_case) =
   run_command args
 
 (* Run Charon on a specific input with the given options *)
-let run_charon (env : charon_env) (case : charon_test_case) =
+let run_charon (env : runner_env) (case : charon_test_case) =
   let input_path = concat_path [ env.inputs_dir; case.path ] in
   if Sys_unix.is_file_exn input_path then
     let args =
@@ -81,8 +80,10 @@ let run_charon (env : charon_env) (case : charon_test_case) =
           Array.append args (Array.of_list case.extra_charon_options)
         in
         (* Run Charon inside the crate *)
+        let old_pwd = Unix.getcwd () in
         Unix.chdir input_path;
-        run_command args
+        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
@@ -185,9 +186,18 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: "aeneas" :: aeneas_path :: llbc_dir :: test_path :: options ->
-      let tests_env = { aeneas_path; llbc_dir } in
+  | _exe_path :: charon_path :: aeneas_path :: inputs_dir :: llbc_dir
+    :: test_path :: aeneas_options ->
+      let runner_env = { charon_path; aeneas_path; inputs_dir; llbc_dir } in
       let test_name = Filename.remove_extension test_path in
+
+      let extra_charon_options = charon_options_for_test test_name in
+      let charon_case =
+        { name = test_name; path = test_path; extra_charon_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
@@ -198,22 +208,14 @@ let () =
         (fun backend ->
           let subdir = test_subdir backend test_name in
           let extra_aeneas_options =
-            List.append (aeneas_options_for_test backend test_name) options
+            List.append
+              (aeneas_options_for_test backend test_name)
+              aeneas_options
           in
-          let test_case =
+          let aeneas_case =
             { name = test_name; backend; subdir; extra_aeneas_options }
           in
-          run_aeneas tests_env test_case)
+          (* Process the llbc file for the current backend *)
+          run_aeneas runner_env aeneas_case)
         backends
-  | _exe_path :: "charon" :: charon_path :: inputs_dir :: llbc_dir :: test_path
-    :: options ->
-      let tests_env = { charon_path; inputs_dir; llbc_dir } in
-      let test_name = Filename.remove_extension test_path in
-      let extra_charon_options =
-        List.append (charon_options_for_test test_name) options
-      in
-      let test_case =
-        { name = test_name; path = test_path; extra_charon_options }
-      in
-      run_charon tests_env test_case
   | _ -> failwith "Incorrect options passed to test runner"
-- 
cgit v1.2.3


From 41f78066da5cc10af6312ab1bef71e45ff460688 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 23 May 2024 16:18:40 +0200
Subject: runner: Use full path and use an enum for crate vs file

---
 tests/test_runner/run_test.ml | 96 ++++++++++++++++++++++++-------------------
 1 file changed, 54 insertions(+), 42 deletions(-)

(limited to 'tests/test_runner')

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 5eff95af..8aa6347c 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -2,7 +2,6 @@
 type runner_env = {
   charon_path : string;
   aeneas_path : string;
-  inputs_dir : string;
   llbc_dir : string;
 }
 
@@ -14,8 +13,11 @@ type aeneas_test_case = {
   extra_aeneas_options : string list;
 }
 
+type input_kind = SingleFile | Crate
+
 (* The data for a specific test to generate llbc for *)
 type charon_test_case = {
+  kind : input_kind;
   name : string;
   path : string;
   extra_charon_options : string list;
@@ -55,42 +57,42 @@ let run_aeneas (env : runner_env) (case : aeneas_test_case) =
 
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : runner_env) (case : charon_test_case) =
-  let input_path = concat_path [ env.inputs_dir; case.path ] in
-  if Sys_unix.is_file_exn input_path then
-    let args =
-      [|
-        env.charon_path;
-        "--no-cargo";
-        "--input";
-        input_path;
-        "--crate";
-        case.name;
-        "--dest";
-        env.llbc_dir;
-      |]
-    in
-    let args = Array.append args (Array.of_list case.extra_charon_options) in
-    (* Run Charon on the rust file *)
-    run_command args
-  else if Sys.is_directory input_path then
-    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
-        (* Run Charon inside the crate *)
-        let old_pwd = Unix.getcwd () in
-        Unix.chdir input_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"
-  else failwith ("`" ^ input_path ^ "` is not a file or a directory.")
+  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.extra_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
+          (* 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 =
@@ -186,14 +188,24 @@ let test_subdir backend test_name =
 let () =
   match Array.to_list Sys.argv with
   (* Ad-hoc argument passing for now. *)
-  | _exe_path :: charon_path :: aeneas_path :: inputs_dir :: llbc_dir
-    :: test_path :: aeneas_options ->
-      let runner_env = { charon_path; aeneas_path; inputs_dir; llbc_dir } in
-      let test_name = Filename.remove_extension test_path in
+  | _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 =
-        { name = test_name; path = test_path; extra_charon_options }
+        {
+          path = test_path;
+          name = test_name;
+          kind = charon_kind;
+          extra_charon_options;
+        }
       in
       (* Generate the llbc file *)
       run_charon runner_env charon_case;
-- 
cgit v1.2.3


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