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

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__":