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/src/betree/aeneas-test-options |  4 ++++
 tests/test_runner/run_test.ml        | 40 +++++++++---------------------------
 2 files changed, 14 insertions(+), 30 deletions(-)
 create mode 100644 tests/src/betree/aeneas-test-options

(limited to 'tests')

diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options
new file mode 100644
index 00000000..c71e01df
--- /dev/null
+++ b/tests/src/betree/aeneas-test-options
@@ -0,0 +1,4 @@
+charon-args=--polonius --opaque=betree_utils
+aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
+[coq] aeneas-args=-use-fuel
+[fstar] aeneas-args=-decreases-clauses -template-clauses
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