diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/test_runner/dune | 2 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 124 |
2 files changed, 71 insertions, 55 deletions
diff --git a/tests/test_runner/dune b/tests/test_runner/dune index e8b29d66..1c719532 100644 --- a/tests/test_runner/dune +++ b/tests/test_runner/dune @@ -1,6 +1,6 @@ (executable (public_name test_runner) - (libraries core_unix.sys_unix re unix) + (libraries core_unix.sys_unix re str unix) (preprocess (pps ppx_deriving.show ppx_deriving.ord ppx_sexp_conv)) (name run_test)) diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 25efbcfd..5d77bf9e 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -37,7 +37,26 @@ module Backend = struct | HOL4 -> "hol4" end -module BackendMap = Map.Make (Backend) +module BackendMap = struct + include Map.Make (Backend) + + (* Make a new map with one entry per backend, given by `f` *) + let make (f : Backend.t -> 'a) : 'a t = + List.fold_left + (fun map backend -> add backend (f backend) map) + empty Backend.all + + (* Set this value for all the backends in `backends` *) + let add_each (backends : Backend.t list) (v : 'a) (map : 'a t) : 'a t = + List.fold_left (fun map backend -> add backend v map) map backends + + (* Updates all the backends in `backends` with `f` *) + let update_each (backends : Backend.t list) (f : 'a -> 'a) (map : 'a t) : 'a t + = + List.fold_left + (fun map backend -> update backend (Option.map f) map) + map backends +end let concat_path = List.fold_left Filename.concat "" @@ -85,23 +104,6 @@ let charon_options_for_test test_name = [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ] | _ -> [] -(* 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" -> "betree" - | _, "hashmap_main" -> "hashmap_on_disk" - | "hol4", _ -> "misc-" ^ test_name - | ( _, - ( "bitwise" | "constants" | "external" | "loops" | "no_nested_borrows" - | "paper" | "polonius_list" ) ) -> - "misc" - | _ -> test_name - (* The data for a specific test input *) module Input = struct type kind = SingleFile | Crate @@ -111,20 +113,26 @@ module Input = struct name : string; path : string; kind : kind; - action : action; + actions : action BackendMap.t; charon_options : string list; aeneas_options : string list BackendMap.t; - subdir : string BackendMap.t; + subdirs : string BackendMap.t; } + (* The default subdirectory in which to store the outputs. *) + let default_subdir backend test_name = + match backend with Backend.Lean -> "." | _ -> test_name + (* Parse lines that start `//@`. Each of them modifies the options we use for the test. Supported comments: - `skip`: don't process the file; - `known-failure`: TODO; + - `subdir=...: set the subdirectory in which to store the outputs. + Defaults to nothing for lean and to the test name for other backends; - `charon-args=...`: extra arguments to pass to charon; - `aeneas-args=...`: extra arguments to pass to aeneas; - `[backend,..]...`: where each `backend` is the name of a backend supported by - aeneas; this sets options for these backends only. Only supported for `aeneas-args`. + aeneas; this sets options for these backends only. *) let apply_special_comment comment input = let comment = String.trim comment in @@ -143,13 +151,21 @@ module Input = struct (* 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 action = Skip } - else if comment = "known-failure" then { input with action = KnownFailure } + if comment = "skip" then + { input with actions = BackendMap.add_each backends Skip input.actions } + else if comment = "known-failure" then + { + input with + actions = BackendMap.add_each backends KnownFailure input.actions; + } else if Option.is_some charon_args then let args = Option.get charon_args in let args = String.split_on_char ' ' args in - { input with charon_options = List.append input.charon_options args } + if backends != Backend.all then + failwith "Cannot set per-backend charon-args" + else { 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 @@ -157,39 +173,32 @@ module Input = struct { input with aeneas_options = - List.fold_left - (fun map backend -> - BackendMap.update backend (Option.map add_args) map) - input.aeneas_options backends; + BackendMap.update_each backends add_args input.aeneas_options; } + else if Option.is_some subdir then + let subdir = Option.get subdir in + { input with subdirs = BackendMap.add_each backends subdir input.subdirs } 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. *) let build (path : string) : t = let name = Filename.remove_extension (Filename.basename path) in + let name = Str.global_replace (Str.regexp "-") "_" name in let 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 action = Normal in + let actions = BackendMap.make (fun _ -> Normal) 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 + let subdirs = + BackendMap.make (fun backend -> default_subdir backend name) 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 + BackendMap.make (fun backend -> aeneas_options_for_test backend name) in let input = - { path; name; kind; action; charon_options; subdir; aeneas_options } + { path; name; kind; actions; charon_options; subdirs; aeneas_options } in match kind with | SingleFile -> @@ -212,7 +221,7 @@ let run_aeneas (env : runner_env) (case : Input.t) (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 subdir = BackendMap.find backend case.subdirs 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 @@ -266,7 +275,7 @@ 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 -> ( + :: aeneas_options -> let runner_env = { charon_path; aeneas_path; llbc_dir } in let test_case = Input.build test_path in let test_case = @@ -276,15 +285,22 @@ let () = BackendMap.map (List.append aeneas_options) test_case.aeneas_options; } in - - match test_case.action with - | Skip -> () - | Normal -> - (* Generate the llbc file *) - run_charon runner_env test_case; - (* Process the llbc file for the each backend *) - List.iter - (fun backend -> run_aeneas runner_env test_case backend) - Backend.all - | KnownFailure -> failwith "KnownFailure is unimplemented") + let skip_all = + List.for_all + (fun backend -> + BackendMap.find backend test_case.actions = Input.Skip) + Backend.all + in + if skip_all then () + else ( + (* Generate the llbc file *) + run_charon runner_env test_case; + (* Process the llbc file for the each backend *) + List.iter + (fun backend -> + match BackendMap.find backend test_case.actions with + | Skip -> () + | Normal -> run_aeneas runner_env test_case backend + | KnownFailure -> failwith "KnownFailure is unimplemented") + Backend.all) | _ -> failwith "Incorrect options passed to test runner" |