runner: Support negative tests

9 files changed, 123 insertions, 26 deletions

diff --git a/Makefile b/Makefile
index bda88c74..38da9f7e 100644
--- a/Makefile
+++ b/Makefile
@@ -25,7 +25,7 @@ CHARON_OPTIONS ?=
 # The directory thta contains the rust source files for tests.
 INPUTS_DIR ?= tests/src
 # The directory where to look for the .llbc files.
-LLBC_DIR ?= $(PWD)/tests/llbc
+LLBC_DIR ?= tests/llbc
 
 # In CI, we enforce formatting and activate the (expensive) sanity checks.
 IN_CI ?=
@@ -157,6 +157,8 @@ verify:
 
 # List the files and directories in `INPUTS_DIR`
 INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*)
+# Remove the committed output files
+INPUTS_LIST := $(filter-out %.out,$(INPUTS_LIST))
 # Remove the directory prefix, replace with `test-`
 INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST))
 
diff --git a/flake.nix b/flake.nix
index 68378954..f1a2258a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -118,17 +118,19 @@
             export CHARON_EXE=${charon.packages.${system}.charon}/bin/charon
             export TEST_RUNNER_EXE=${test_runner}/bin/test_runner
 
-            mkdir llbc
-            export LLBC_DIR=llbc
-            # Copy over the llbc file we can't generate ourselves.
-            cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR
-
             # Copy the tests
             cp -r tests tests-copy
             make clean-generated-aeneas
 
+            mkdir tests/llbc
+            export LLBC_DIR=tests/llbc
+            # Copy over the llbc file we can't generate ourselves.
+            cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR
+
             # Run the tests with extra sanity checks enabled
             IN_CI=1 make test-all -j $NIX_BUILD_CORES
+            # Clean generated llbc files so we don't compare them.
+            rm -r tests/llbc
 
             # Check that there are no differences between the generated tests
             # and the original tests
diff --git a/tests/lean/misc/MutuallyRecursiveTraits.lean b/tests/lean/misc/MutuallyRecursiveTraits.lean
new file mode 100644
index 00000000..b0fcb9e9
--- /dev/null
+++ b/tests/lean/misc/MutuallyRecursiveTraits.lean
@@ -0,0 +1,6 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [mutually_recursive_traits]
+import Base
+open Primitives
+
+namespace mutually_recursive_traits
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
new file mode 100644
index 00000000..33206fe5
--- /dev/null
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -0,0 +1,17 @@
+[Info ] Imported: tests/llbc/mutually_recursive_traits.llbc
+[Error] In file Translate.ml, line 813:
+Mutually recursive trait declarations are not supported
+
+Uncaught exception:
+  
+  (Failure
+    "In file Translate.ml, line 813:\
+   \nIn file Translate.ml, line 813:\
+   \nMutually recursive trait declarations are not supported")
+
+Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
+Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
+Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1502, characters 5-42
+Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
diff --git a/tests/src/mutually-recursive-traits.rs b/tests/src/mutually-recursive-traits.rs
new file mode 100644
index 00000000..351763b2
--- /dev/null
+++ b/tests/src/mutually-recursive-traits.rs
@@ -0,0 +1,11 @@
+//@ [lean] known-failure
+//@ [coq,fstar] skip
+//@ subdir=misc
+pub trait Trait1 {
+    type T: Trait2;
+}
+
+pub trait Trait2: Trait1 {}
+
+pub trait T1<T: T2<Self>>: Sized {}
+pub trait T2<T: T1<Self>>: Sized {}
diff --git a/tests/src/string-chars.lean.out b/tests/src/string-chars.lean.out
new file mode 100644
index 00000000..0d28744f
--- /dev/null
+++ b/tests/src/string-chars.lean.out
@@ -0,0 +1,21 @@
+[Info ] Imported: tests/llbc/string_chars.llbc
+[Error] In file SymbolicToPure.ml, line 588:
+ADTs containing borrows are not supported yet
+Source: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20
+
+Uncaught exception:
+  
+  (Failure
+    "In file SymbolicToPure.ml, line 588:\
+   \nIn file SymbolicToPure.ml, line 588:\
+   \nADTs containing borrows are not supported yet\
+   \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20\
+   \nSource: '/rustc/ad963232d9b987d66a6f8e6ec4141f672b8b9900/library/core/src/str/iter.rs', lines 32:0-32:20")
+
+Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
+Called from Aeneas__SymbolicToPure.translate_type_decl in file "SymbolicToPure.ml", line 588, characters 2-113
+Called from Aeneas__SymbolicToPure.translate_type_decls.(fun) in file "SymbolicToPure.ml", line 3923, characters 15-42
+Called from Stdlib__List.filter_map.aux in file "list.ml", line 258, characters 14-17
+Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 229, characters 19-64
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 981, characters 4-33
+Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61
diff --git a/tests/src/string-chars.rs b/tests/src/string-chars.rs
new file mode 100644
index 00000000..5ba9a2d6
--- /dev/null
+++ b/tests/src/string-chars.rs
@@ -0,0 +1,6 @@
+//@ [lean] known-failure
+//@ [coq,fstar] skip
+fn main() {
+    let s = "hello";
+    let _chs: Vec<char> = s.chars().collect();
+}
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"