runner: Support negative tests

2 files changed, 52 insertions, 20 deletions

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"