From 9c09789c26dd8142b8a29b42e250a685aa983e58 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 11:22:37 +0200 Subject: runner: Support negative tests --- tests/test_runner/dune | 2 +- tests/test_runner/run_test.ml | 70 +++++++++++++++++++++++++++++++------------ 2 files changed, 52 insertions(+), 20 deletions(-) (limited to 'tests/test_runner') diff --git a/tests/test_runner/dune b/tests/test_runner/dune index c38e009c..6bb3f7b2 100644 --- a/tests/test_runner/dune +++ b/tests/test_runner/dune @@ -1,6 +1,6 @@ (executable (public_name test_runner) - (libraries core_unix core_unix.sys_unix re str unix) + (libraries core_unix core_unix.filename_unix 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 a5a89317..7a52b6f3 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -15,6 +15,7 @@ type runner_env = { charon_path : string; aeneas_path : string; llbc_dir : string; + dest_dir : string; } module Backend = struct @@ -61,10 +62,12 @@ end let concat_path = List.fold_left Filename.concat "" module Command = struct - type t = { args : string array } + type t = { args : string array; redirect_out : Unix.file_descr option } type status = Success | Failure - let make (args : string list) : t = { args = Array.of_list args } + let make (args : string list) : t = + { args = Array.of_list args; redirect_out = None } + let to_string (cmd : t) = Core.String.concat_array ~sep:" " cmd.args (* Run the command and returns its exit status. *) @@ -73,10 +76,8 @@ module Command = struct print_endline ("[test_runner] Running: " ^ command_str); (* Run the command *) - let pid = - Unix.create_process cmd.args.(0) cmd.args Unix.stdin Unix.stdout - Unix.stderr - in + let out = Option.value cmd.redirect_out ~default:Unix.stdout in + let pid = Unix.create_process cmd.args.(0) cmd.args Unix.stdin out out in let status = Core_unix.waitpid (Core.Pid.of_int pid) in match status with | Ok () -> Success @@ -89,6 +90,14 @@ module Command = struct match run cmd with | Success -> () | Failure -> failwith ("Command `" ^ to_string cmd ^ "` failed.") + + (* Run the command and aborts the program if the command succeeded. *) + let run_command_expecting_failure cmd = + match run cmd with + | Success -> + failwith + ("Command `" ^ to_string cmd ^ "` succeeded but was expected to fail.") + | Failure -> () end let aeneas_options_for_test backend test_name = @@ -232,18 +241,43 @@ 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 backend_str = Backend.to_string backend in 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 output_file = + Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out" + in let subdir = BackendMap.find backend case.subdirs in + let dest_dir = concat_path [ env.dest_dir; backend_str; 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 action = BackendMap.find backend case.actions in + + (* Build the command *) let args = [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ] in - let args = List.append args aeneas_options in + let abort_on_error = + match action with + | Skip | Normal -> [] + | KnownFailure -> [ "-abort-on-error" ] + in + let args = List.concat [ args; aeneas_options; abort_on_error ] in + let cmd = Command.make args in + (* Remove leftover files if they're not needed anymore *) + (match action with + | (Skip | Normal) when Sys.file_exists output_file -> Sys.remove output_file + | _ -> ()); (* Run Aeneas *) - Command.run_command_expecting_success (Command.make args) + match action with + | Skip -> () + | Normal -> Command.run_command_expecting_success cmd + | KnownFailure -> + let out = + Core_unix.openfile ~mode:[ O_CREAT; O_TRUNC; O_WRONLY ] output_file + in + let cmd = { cmd with redirect_out = Some out } in + Command.run_command_expecting_failure cmd; + Unix.close out (* Run Charon on a specific input with the given options *) let run_charon (env : runner_env) (case : Input.t) = @@ -267,7 +301,9 @@ let run_charon (env : runner_env) (case : Input.t) = | Crate -> ( match Sys.getenv_opt "IN_CI" with | None -> - let args = [ env.charon_path; "--dest"; env.llbc_dir ] in + let args = + [ env.charon_path; "--dest"; Filename_unix.realpath env.llbc_dir ] + in let args = List.append args case.charon_options in (* Run Charon inside the crate *) let old_pwd = Unix.getcwd () in @@ -287,7 +323,9 @@ let () = (* 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 runner_env = + { charon_path; aeneas_path; llbc_dir; dest_dir = "tests" } + in let test_case = Input.build test_path in let test_case = { @@ -307,11 +345,5 @@ let () = (* 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) + List.iter (run_aeneas runner_env test_case) Backend.all) | _ -> failwith "Incorrect options passed to test runner" -- cgit v1.2.3