From aee6dc227c4ed041bbbae7cf38729a4b1a3a6869 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 10:48:07 +0200 Subject: runner: Correctly catch command exit status --- tests/test_runner/dune | 2 +- tests/test_runner/run_test.ml | 67 +++++++++++++++++++++++++------------------ 2 files changed, 40 insertions(+), 29 deletions(-) diff --git a/tests/test_runner/dune b/tests/test_runner/dune index 1c719532..c38e009c 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.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..a5a89317 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -60,24 +60,37 @@ 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 } + 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 } + 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 pid = + Unix.create_process cmd.args.(0) cmd.args Unix.stdin Unix.stdout + Unix.stderr + 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.") +end -(* File-specific options *) let aeneas_options_for_test backend test_name = if test_name = "betree" then let options = @@ -226,20 +239,18 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) = let backend_str = Backend.to_string backend in let dest_dir = concat_path [ "tests"; backend_str; subdir ] in 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 args = List.append args aeneas_options in (* Run Aeneas *) - run_command args + Command.run_command_expecting_success (Command.make args) (* 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 +259,20 @@ 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"; 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 -- cgit v1.2.3 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 --- Makefile | 4 +- flake.nix | 12 +++-- tests/lean/misc/MutuallyRecursiveTraits.lean | 6 +++ tests/src/mutually-recursive-traits.lean.out | 17 +++++++ tests/src/mutually-recursive-traits.rs | 11 +++++ tests/src/string-chars.lean.out | 21 +++++++++ tests/src/string-chars.rs | 6 +++ tests/test_runner/dune | 2 +- tests/test_runner/run_test.ml | 70 ++++++++++++++++++++-------- 9 files changed, 123 insertions(+), 26 deletions(-) create mode 100644 tests/lean/misc/MutuallyRecursiveTraits.lean create mode 100644 tests/src/mutually-recursive-traits.lean.out create mode 100644 tests/src/mutually-recursive-traits.rs create mode 100644 tests/src/string-chars.lean.out create mode 100644 tests/src/string-chars.rs 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>: Sized {} +pub trait T2>: 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 = 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" -- cgit v1.2.3 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 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 = 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