summaryrefslogtreecommitdiff
path: root/tests/test_runner
diff options
context:
space:
mode:
authorNadrieril2024-05-23 17:01:03 +0200
committerNadrieril2024-05-24 16:11:59 +0200
commit7935e74a9cedd93e885ab546d5513ea6c31db5ad (patch)
tree6f231079c905423479b4a63354c2a2e124843059 /tests/test_runner
parent24fc188af7032b8119cb7504965b82216e2bbf6b (diff)
runner: Strongly typed Backend enum
Diffstat (limited to '')
-rw-r--r--tests/test_runner/dune6
-rw-r--r--tests/test_runner/run_test.ml144
2 files changed, 88 insertions, 62 deletions
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"