From b1fe934c551dd89f1001ca2c56a146231c1e49a0 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 2 Oct 2018 20:56:36 -0700 Subject: [PATCH] cmake: Display skipped tests as not run (#2567) Currently, the run_regression.py script just returns 0 when we skip a test due to a feature not supported by the current configuration. Returning 0 marks those tests as passed. To make it more clear which tests were skipped, this commit adds the `SKIP_RETURN_CODE` [0] property to the regression tests and changes the regression script to return 77 for skipped tests. The feature is supported since at least CMake 3.0 [0]. For backwards compatibility with autotools, returning 77 for skipped tests is only active when `--cmake` is passed to the run_regression.py script. [0] https://cmake.org/cmake/help/v3.0/prop_test/SKIP_RETURN_CODE.html --- test/regress/CMakeLists.txt | 5 +++- test/regress/run_regression.py | 44 +++++++++++++++++++--------------- 2 files changed, 29 insertions(+), 20 deletions(-) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fd4026dc0..c798af378 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2091,9 +2091,12 @@ add_custom_target(regress macro(cvc4_add_regression_test level file) add_test(${file} ${run_regress_script} + --cmake ${RUN_REGRESSION_ARGS} ${path_to_cvc4}/cvc4 ${CMAKE_CURRENT_LIST_DIR}/${file}) - set_tests_properties(${file} PROPERTIES LABELS "regress${level}") + set_tests_properties(${file} PROPERTIES + LABELS "regress${level}" + SKIP_RETURN_CODE 77) endmacro() foreach(file ${regress_0_tests}) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index fa23bd9bf..09ec8b7cf 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -2,8 +2,9 @@ """ Usage: - run_regression.py [ --proof | --dump ] [ wrapper ] cvc4-binary - [ benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p ] + run_regression.py [--enable-proof] [--with-lfsc] [--dump] [--cmake] + [wrapper] cvc4-binary + [benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p] Runs benchmark and checks for correct exit status and output. """ @@ -27,6 +28,8 @@ REQUIRES = 'REQUIRES: ' EXIT_OK = 0 EXIT_FAILURE = 1 +EXIT_SKIP = 77 + def run_process(args, cwd, timeout, s_input=None): """Runs a process with a timeout `timeout` in seconds. `args` are the @@ -124,13 +127,14 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary, return (output.strip(), error.strip(), exit_status) -def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, +def run_regression(unsat_cores, proofs, dump, cmake, wrapper, cvc4_binary, benchmark_path, timeout): """Determines the expected output for a benchmark, runs CVC4 on it and then checks whether the output corresponds to the expected output. Optionally uses a wrapper `wrapper`, tests unsat cores (if unsat_cores is true), checks proofs (if proofs is true), or dumps a benchmark and uses that as - the input (if dump is true).""" + the input (if dump is true). `cmake` enables/disables CMake-specific + behavior.""" if not os.access(cvc4_binary, os.X_OK): sys.exit( @@ -230,7 +234,7 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, print( '1..0 # Skipped regression: unsat cores not supported without proof support' ) - return + return (EXIT_SKIP if cmake else EXIT_OK) for req_feature in requires: if req_feature.startswith("no-"): @@ -238,11 +242,11 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, if inv_feature in cvc4_features: print('1..0 # Skipped regression: not valid with {}'.format( inv_feature)) - return + return (EXIT_SKIP if cmake else EXIT_OK) elif req_feature not in cvc4_features: print('1..0 # Skipped regression: {} not supported'.format( req_feature)) - return + return (EXIT_SKIP if cmake else EXIT_OK) if not command_lines: command_lines.append('') @@ -254,14 +258,14 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, if not unsat_cores and ('--check-unsat-cores' in all_args): print( - '# Skipped command line options ({}): unsat cores not supported without proof support'. - format(all_args)) + '# Skipped command line options ({}): unsat cores not supported without proof support' + .format(all_args)) continue if not proofs and ('--check-proofs' in all_args or '--dump-proofs' in all_args): print( - '# Skipped command line options ({}): checking proofs not supported without LFSC support'. - format(all_args)) + '# Skipped command line options ({}): checking proofs not supported without LFSC support' + .format(all_args)) continue command_line_args_configs.append(all_args) @@ -291,8 +295,8 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, not cvc4_binary.endswith('pcvc4'): extra_command_line_args += ['--check-unsat-cores'] if extra_command_line_args: - command_line_args_configs.append( - all_args + extra_command_line_args) + command_line_args_configs.append(all_args + + extra_command_line_args) # Run CVC4 on the benchmark with the different option sets and check # whether the exit status, stdout output, stderr output are as expected. @@ -306,8 +310,8 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, if output != expected_output: exit_code = EXIT_FAILURE print( - 'not ok - Differences between expected and actual output on stdout - Flags: {}'. - format(command_line_args)) + 'not ok - Differences between expected and actual output on stdout - Flags: {}' + .format(command_line_args)) for line in difflib.context_diff(output.splitlines(), expected_output.splitlines()): print(line) @@ -317,8 +321,8 @@ def run_regression(unsat_cores, proofs, dump, wrapper, cvc4_binary, elif error != expected_error: exit_code = EXIT_FAILURE print( - 'not ok - Differences between expected and actual output on stderr - Flags: {}'. - format(command_line_args)) + 'not ok - Differences between expected and actual output on stderr - Flags: {}' + .format(command_line_args)) for line in difflib.context_diff(error.splitlines(), expected_error.splitlines()): print(line) @@ -349,6 +353,7 @@ def main(): parser.add_argument('--enable-proof', action='store_true') parser.add_argument('--with-lfsc', action='store_true') parser.add_argument('--dump', action='store_true') + parser.add_argument('--cmake', action='store_true') parser.add_argument('wrapper', nargs='*') parser.add_argument('cvc4_binary') parser.add_argument('benchmark') @@ -361,8 +366,9 @@ def main(): timeout = float(os.getenv('TEST_TIMEOUT', 600.0)) - return run_regression(args.enable_proof, args.with_lfsc, args.dump, wrapper, - cvc4_binary, args.benchmark, timeout) + return run_regression(args.enable_proof, args.with_lfsc, args.dump, + args.cmake, wrapper, cvc4_binary, args.benchmark, + timeout) if __name__ == "__main__": -- 2.30.2