runner: Strongly typed Backend enum

3 files changed, 89 insertions, 62 deletions

diff --git a/flake.nix b/flake.nix
index caa29fae..68378954 100644
--- a/flake.nix
+++ b/flake.nix
@@ -80,6 +80,7 @@
           OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors.
           propagatedBuildInputs = (with ocamlPackages; [
             core_unix
+            ppx_deriving
           ]);
         };
 
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"