From c483eeb3505a61aa1b4f8432e07555176dd7598c Mon Sep 17 00:00:00 2001 From: yoni206 Date: Wed, 28 Oct 2020 14:52:18 -0700 Subject: [PATCH] run_regression.py to fail on invalid requirements (#5264) Currently, the following test is skipped when running ctest: ; REQUIRES: symfpuuuu ; EXPECT: sat (set-logic ALL) (assert true) (check-sat) I think it is better for such a test to fail, because otherwise it might never run without anyone noticing (this almost happened to me here: c7e277b). This PR makes such tests to fail by checking whether the REQUIRES value is valid. No regressions fail as a result. Co-authored-by: Mathias Preiner mathias.preiner@gmail.com --- test/regress/run_regression.py | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 8047a0ca8..17aa9e0c6 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -114,14 +114,17 @@ def get_cvc4_features(cvc4_binary): output = output.decode() features = [] + disabled_features = [] for line in output.split('\n'): tokens = [t.strip() for t in line.split(':')] if len(tokens) == 2: key, value = tokens if value == 'yes': features.append(key) + elif value == 'no': + disabled_features.append(key) - return features + return features, disabled_features def logic_supported_with_proofs(logic): @@ -213,7 +216,7 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, if not os.path.isfile(benchmark_path): sys.exit('"{}" does not exist or is not a file'.format(benchmark_path)) - cvc4_features = get_cvc4_features(cvc4_binary) + cvc4_features, cvc4_disabled_features = get_cvc4_features(cvc4_binary) basic_command_line_args = [] @@ -315,11 +318,20 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, return (EXIT_SKIP if use_skip_return_code else EXIT_OK) for req_feature in requires: + is_negative = False if req_feature.startswith("no-"): - inv_feature = req_feature[len("no-"):] - if inv_feature in cvc4_features: + req_feature = req_feature[len("no-"):] + is_negative = True + if req_feature not in (cvc4_features + cvc4_disabled_features): + print( + 'Illegal requirement in regression: {}\nAllowed requirements: {}' + .format(req_feature, + ' '.join(cvc4_features + cvc4_disabled_features))) + return EXIT_FAILURE + if is_negative: + if req_feature in cvc4_features: print('1..0 # Skipped regression: not valid with {}'.format( - inv_feature)) + req_feature)) return (EXIT_SKIP if use_skip_return_code else EXIT_OK) elif req_feature not in cvc4_features: print('1..0 # Skipped regression: {} not supported'.format( -- 2.30.2