diff options
| -rw-r--r-- | tests/test_runner/Input.ml | 83 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 22 |
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 () |