Merge pull request #209 from AeneasVerif/negative-tests

2 files changed, 108 insertions, 41 deletions

diff --git a/tests/test_runner/dune b/tests/test_runner/dune
index 1c719532..6bb3f7b2 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 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 5d77bf9e..1c885d4b 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
@@ -60,24 +61,45 @@ end
 
 let concat_path = List.fold_left Filename.concat ""
 
-let run_command args =
-  (* Debug arguments *)
-  print_string "[test_runner] Running: ";
-  Array.iter
-    (fun x ->
-      print_string x;
-      print_string " ")
-    args;
-  print_endline "";
+module Command = struct
+  type t = { args : string array; redirect_out : Unix.file_descr option }
+  type status = Success | Failure
 
-  (* Run the command *)
-  let pid =
-    Unix.create_process args.(0) args Unix.stdin Unix.stdout Unix.stderr
-  in
-  let _ = Unix.waitpid [] pid in
-  ()
+  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. *)
+  let run (cmd : t) : status =
+    let command_str = to_string cmd in
+    print_endline ("[test_runner] Running: " ^ command_str);
+
+    (* Run the command *)
+    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
+    | Error (`Exit_non_zero _) -> Failure
+    | Error (`Signal _) ->
+        failwith ("Command `" ^ command_str ^ "` exited incorrectly.")
+
+  (* Run the command and aborts the program if the command failed. *)
+  let run_command_expecting_success cmd =
+    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
 
-(* File-specific options *)
 let aeneas_options_for_test backend test_name =
   if test_name = "betree" then
     let options =
@@ -117,6 +139,8 @@ module Input = struct
     charon_options : string list;
     aeneas_options : string list BackendMap.t;
     subdirs : string BackendMap.t;
+    (* Whether to store the command output to a file. Only available for known-failure tests. *)
+    check_output : bool BackendMap.t;
   }
 
   (* The default subdirectory in which to store the outputs. *)
@@ -160,6 +184,11 @@ module Input = struct
         input with
         actions = BackendMap.add_each backends KnownFailure input.actions;
       }
+    else if comment = "no-check-output" then
+      {
+        input with
+        check_output = BackendMap.add_each backends false input.check_output;
+      }
     else if Option.is_some charon_args then
       let args = Option.get charon_args in
       let args = String.split_on_char ' ' args in
@@ -197,8 +226,18 @@ module Input = struct
     let aeneas_options =
       BackendMap.make (fun backend -> aeneas_options_for_test backend name)
     in
+    let check_output = BackendMap.make (fun _ -> true) in
     let input =
-      { path; name; kind; actions; charon_options; subdirs; aeneas_options }
+      {
+        path;
+        name;
+        kind;
+        actions;
+        charon_options;
+        subdirs;
+        aeneas_options;
+        check_output;
+      }
     in
     match kind with
     | SingleFile ->
@@ -219,27 +258,57 @@ 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
+  let check_output = BackendMap.find backend case.check_output in
+
+  (* Build the command *)
   let args =
-    [|
-      env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str;
-    |]
+    [ env.aeneas_path; input_file; "-dest"; dest_dir; "-backend"; backend_str ]
   in
-  let args = Array.append args (Array.of_list 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 *)
+  if
+    Sys.file_exists output_file
+    &&
+    match action with
+    | Skip | Normal -> true
+    | KnownFailure when not check_output -> true
+    | _ -> false
+  then Sys.remove output_file;
   (* Run Aeneas *)
-  run_command args
-
+  match action with
+  | Skip -> ()
+  | Normal -> Command.run_command_expecting_success cmd
+  | KnownFailure ->
+      let out =
+        if check_output then
+          Core_unix.openfile ~mode:[ O_CREAT; O_TRUNC; O_WRONLY ] output_file
+        else Core_unix.openfile ~mode:[ O_WRONLY ] "/dev/null"
+      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) =
   match case.kind with
   | SingleFile ->
       let args =
-        [|
+        [
           env.charon_path;
           "--no-cargo";
           "--input";
@@ -248,20 +317,22 @@ let run_charon (env : runner_env) (case : Input.t) =
           case.name;
           "--dest";
           env.llbc_dir;
-        |]
+        ]
       in
-      let args = Array.append args (Array.of_list case.charon_options) in
+      let args = List.append args case.charon_options in
       (* Run Charon on the rust file *)
-      run_command args
+      Command.run_command_expecting_success (Command.make 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
+          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
           Unix.chdir case.path;
-          run_command args;
+          Command.run_command_expecting_success (Command.make args);
           Unix.chdir old_pwd
       | Some _ ->
           (* Crates with dependencies must be generated separately in CI. We skip
@@ -276,7 +347,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 =
         {
@@ -296,11 +369,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"