From fb16d0af4caacd2c9a3463f6d2b455209b755697 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 27 May 2024 14:34:12 +0200
Subject: runner: Add `no-check-output` option for unstable outputs

---
 tests/src/string-chars.lean.out | 21 ---------------------
 tests/src/string-chars.rs       |  1 +
 tests/test_runner/run_test.ml   | 36 ++++++++++++++++++++++++++++++------
 3 files changed, 31 insertions(+), 27 deletions(-)
 delete mode 100644 tests/src/string-chars.lean.out

(limited to 'tests')

diff --git a/tests/src/string-chars.lean.out b/tests/src/string-chars.lean.out
deleted file mode 100644
index 0d28744f..00000000
--- a/tests/src/string-chars.lean.out
+++ /dev/null
@@ -1,21 +0,0 @@
-[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
index 5ba9a2d6..f8490e76 100644
--- a/tests/src/string-chars.rs
+++ b/tests/src/string-chars.rs
@@ -1,5 +1,6 @@
 //@ [lean] known-failure
 //@ [coq,fstar] skip
+//@ no-check-output
 fn main() {
     let s = "hello";
     let _chs: Vec<char> = s.chars().collect();
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 7a52b6f3..1c885d4b 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -139,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. *)
@@ -182,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
@@ -219,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 ->
@@ -251,6 +268,7 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   let dest_dir = concat_path [ env.dest_dir; backend_str; subdir ] in
   let aeneas_options = BackendMap.find backend case.aeneas_options in
   let action = BackendMap.find backend case.actions in
+  let check_output = BackendMap.find backend case.check_output in
 
   (* Build the command *)
   let args =
@@ -264,21 +282,27 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
   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
-  | _ -> ());
+  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 *)
   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
+        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
-- 
cgit v1.2.3