summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/test_runner/Input.ml83
-rw-r--r--tests/test_runner/run_test.ml22
2 files changed, 56 insertions, 49 deletions
diff --git a/tests/test_runner/Input.ml b/tests/test_runner/Input.ml
index dbb69a47..960ffe8d 100644
--- a/tests/test_runner/Input.ml
+++ b/tests/test_runner/Input.ml
@@ -3,16 +3,22 @@
type kind = SingleFile | Crate
type action = Normal | Skip | KnownFailure
+(* Options that can be set for a specific backend *)
+type per_backend = {
+ action : action;
+ aeneas_options : string list;
+ subdir : string;
+ (* Whether to store the command output to a file. Only available for known-failure tests. *)
+ check_output : bool;
+}
+
+(* The data for a specific test input *)
type t = {
name : string;
path : string;
kind : kind;
- actions : action Backend.Map.t;
charon_options : string list;
- aeneas_options : string list Backend.Map.t;
- subdirs : string Backend.Map.t;
- (* Whether to store the command output to a file. Only available for known-failure tests. *)
- check_output : bool Backend.Map.t;
+ per_backend : per_backend Backend.Map.t;
}
(* The default subdirectory in which to store the outputs. *)
@@ -44,41 +50,42 @@ let apply_special_comment comment input =
(String.trim rest, backends)
| None -> (comment, Backend.all)
in
+ (* Apply `f` to the selected backends *)
+ let per_backend f =
+ {
+ input with
+ per_backend = Backend.Map.update_each backends f input.per_backend;
+ }
+ in
+ (* Assert that this option is not available to be set per-backend *)
+ let assert_no_backend option_name =
+ if backends != Backend.all then
+ failwith ("Cannot set the `" ^ option_name ^ "` option per-backend")
+ in
+
(* Parse the other options *)
let charon_args = Core.String.chop_prefix comment ~prefix:"charon-args=" in
let aeneas_args = Core.String.chop_prefix comment ~prefix:"aeneas-args=" in
let subdir = Core.String.chop_prefix comment ~prefix:"subdir=" in
- if comment = "skip" then
- { input with actions = Backend.Map.add_each backends Skip input.actions }
+ if comment = "skip" then per_backend (fun x -> { x with action = Skip })
else if comment = "known-failure" then
- {
- input with
- actions = Backend.Map.add_each backends KnownFailure input.actions;
- }
+ per_backend (fun x -> { x with action = KnownFailure })
else if comment = "no-check-output" then
- {
- input with
- check_output = Backend.Map.add_each backends false input.check_output;
- }
- else if Option.is_some charon_args then
+ per_backend (fun x -> { x with check_output = false })
+ else if Option.is_some charon_args then (
let args = Option.get charon_args in
let args = String.split_on_char ' ' args in
- if backends != Backend.all then
- failwith "Cannot set per-backend charon-args"
- else { input with charon_options = List.append input.charon_options args }
+ assert_no_backend "charon-args";
+ { input with charon_options = List.append input.charon_options args })
else if Option.is_some aeneas_args then
let args = Option.get aeneas_args in
let args = String.split_on_char ' ' args in
- let add_args opts = List.append opts args in
- {
- input with
- aeneas_options =
- Backend.Map.update_each backends add_args input.aeneas_options;
- }
+ per_backend (fun x ->
+ { x with aeneas_options = List.append x.aeneas_options args })
else if Option.is_some subdir then
let subdir = Option.get subdir in
- { input with subdirs = Backend.Map.add_each backends subdir input.subdirs }
+ per_backend (fun x -> { x with subdir })
else failwith ("Unrecognized special comment: `" ^ comment ^ "`")
(* Given a path to a rust file or crate, gather the details and options about how to build the test. *)
@@ -90,22 +97,16 @@ let build (path : string) : t =
else if Sys_unix.is_directory_exn path then Crate
else failwith ("`" ^ path ^ "` is not a file or a directory.")
in
- let actions = Backend.Map.make (fun _ -> Normal) in
- let subdirs = Backend.Map.make (fun backend -> default_subdir backend name) in
- let aeneas_options = Backend.Map.make (fun _ -> []) in
- let check_output = Backend.Map.make (fun _ -> true) in
- let input =
- {
- path;
- name;
- kind;
- actions;
- charon_options = [];
- subdirs;
- aeneas_options;
- check_output;
- }
+ let per_backend =
+ Backend.Map.make (fun backend ->
+ {
+ action = Normal;
+ subdir = default_subdir backend name;
+ aeneas_options = [];
+ check_output = true;
+ })
in
+ let input = { path; name; kind; charon_options = []; per_backend } in
(* For crates, we store the special comments in a separate file. *)
let crate_config_file = Filename.concat path "aeneas-test-options" in
match kind with
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index e8dd38bb..c17c17be 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -54,11 +54,12 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
let output_file =
Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
in
- let subdir = Backend.Map.find backend case.subdirs in
+ let per_backend = Backend.Map.find backend case.per_backend in
+ let subdir = per_backend.subdir in
+ let check_output = per_backend.check_output in
+ let aeneas_options = per_backend.aeneas_options in
+ let action = per_backend.action in
let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in
- let aeneas_options = Backend.Map.find backend case.aeneas_options in
- let action = Backend.Map.find backend case.actions in
- let check_output = Backend.Map.find backend case.check_output in
(* Build the command *)
let args =
@@ -145,16 +146,21 @@ let () =
let test_case =
{
test_case with
- aeneas_options =
+ per_backend =
Backend.Map.map
- (List.append aeneas_options)
- test_case.aeneas_options;
+ (fun x ->
+ {
+ x with
+ Input.aeneas_options =
+ List.append aeneas_options x.Input.aeneas_options;
+ })
+ test_case.per_backend;
}
in
let skip_all =
List.for_all
(fun backend ->
- Backend.Map.find backend test_case.actions = Input.Skip)
+ (Backend.Map.find backend test_case.per_backend).action = Input.Skip)
Backend.all
in
if skip_all then ()