diff options
| -rw-r--r-- | tests/test_runner/run_test.ml | 182 |
1 files changed, 92 insertions, 90 deletions
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index 2c411c95..e168069b 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -27,18 +27,6 @@ end module BackendMap = Map.Make (Backend) -type input_kind = SingleFile | Crate - -(* The data for a specific test input *) -type test_case = { - name : string; - path : string; - 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 "" let run_command args = @@ -58,61 +46,6 @@ let run_command args = let _ = Unix.waitpid [] pid in () -(* Run Aeneas on a specific input with the given options *) -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"; backend_str; - |] - 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 : test_case) = - match case.input_kind with - | SingleFile -> - let args = - [| - env.charon_path; - "--no-cargo"; - "--input"; - case.path; - "--crate"; - case.name; - "--dest"; - env.llbc_dir; - |] - 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.charon_options) in - (* Run Charon inside the crate *) - let old_pwd = Unix.getcwd () in - Unix.chdir case.path; - run_command args; - Unix.chdir old_pwd - | Some _ -> - (* Crates with dependencies must be generated separately in CI. We skip - here and trust that CI takes care to generate the necessary llbc - file. *) - print_endline - "Warn: IN_CI is set; we skip generating llbc files for whole crates" - ) - (* File-specific options *) let aeneas_options_for_test backend test_name = let backend = Backend.to_string backend in @@ -205,29 +138,98 @@ 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 +(* The data for a specific test input *) +module Input = struct + type kind = SingleFile | Crate + + type t = { + name : string; + path : string; + kind : kind; + charon_options : string list; + aeneas_options : string list BackendMap.t; + subdir : string BackendMap.t; + } + + let build (path : string) : t = + let name = Filename.remove_extension (Filename.basename path) 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 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; kind; charon_options; subdir; aeneas_options } +end + +(* Run Aeneas on a specific input with the given options *) +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 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"; backend_str; + |] in - { path; name; input_kind; charon_options; subdir; aeneas_options } + 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 : Input.t) = + match case.kind with + | SingleFile -> + let args = + [| + env.charon_path; + "--no-cargo"; + "--input"; + case.path; + "--crate"; + case.name; + "--dest"; + env.llbc_dir; + |] + 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.charon_options) in + (* Run Charon inside the crate *) + let old_pwd = Unix.getcwd () in + Unix.chdir case.path; + run_command args; + Unix.chdir old_pwd + | Some _ -> + (* Crates with dependencies must be generated separately in CI. We skip + here and trust that CI takes care to generate the necessary llbc + file. *) + print_endline + "Warn: IN_CI is set; we skip generating llbc files for whole crates" + ) let () = match Array.to_list Sys.argv with @@ -235,7 +237,7 @@ let () = | _exe_path :: charon_path :: aeneas_path :: llbc_dir :: test_path :: aeneas_options -> let runner_env = { charon_path; aeneas_path; llbc_dir } in - let test_case = build_test test_path in + let test_case = Input.build test_path in let test_case = { test_case with |