|
| 1 | +import os |
| 2 | +import subprocess |
| 3 | +import sys |
| 4 | +import tempfile |
| 5 | +import glob |
| 6 | + |
| 7 | +this_script_dir = os.path.abspath(os.path.dirname(__file__)) |
| 8 | + |
| 9 | +TraceXsd = os.path.abspath(os.path.join(this_script_dir, '..', '..', 'doc/assets/xml_spec.xsd')) |
| 10 | + |
| 11 | +test_base_dir = os.path.abspath(os.path.join(this_script_dir, '..', 'cbmc')) |
| 12 | + |
| 13 | +# some tests in the cbmc suite don't work for the trace checks for one reason or another |
| 14 | +ExcludedTests = list(map(lambda s: os.path.join(test_base_dir, s), [ |
| 15 | + # these tests except input from stdin |
| 16 | + 'json-interface1/test_wrong_option.desc', |
| 17 | + 'json-interface1/test.desc', |
| 18 | + 'json-interface1/test_wrong_flag.desc', |
| 19 | + 'xml-interface1/test_wrong_option.desc', |
| 20 | + 'xml-interface1/test.desc', |
| 21 | + 'xml-interface1/test_wrong_flag.desc', |
| 22 | + # these want --show-goto-functions instead of producing a trace |
| 23 | + 'destructors/compound_literal.desc', |
| 24 | + 'destructors/enter_lexical_block.desc', |
| 25 | + 'reachability-slice-interproc2/test.desc', |
| 26 | + # this one wants show-properties instead producing a trace |
| 27 | + 'show_properties1/test.desc', |
| 28 | + # program-only instead of trace |
| 29 | + 'vla1/program-only.desc', |
| 30 | + 'Quantifiers-simplify/simplify_not_forall.desc', |
| 31 | + # this one doesn't work for me locally at all |
| 32 | + # 'integer-assignments1/test.desc', |
| 33 | + # these test for invalid command line handling |
| 34 | + 'bad_option/test_multiple.desc', |
| 35 | + 'bad_option/test.desc', |
| 36 | + # this one produces XML intermingled with main XML output when used with --xml-ui |
| 37 | + 'graphml_witness2/test.desc', |
| 38 | + # produces intermingled XML on the command line |
| 39 | + 'coverage_report1/test.desc', |
| 40 | + 'coverage_report1/paths.desc', |
| 41 | + 'graphml_witness1/test.desc', |
| 42 | + 'switch8/program-only.desc', |
| 43 | + # this uses json-ui (fails for a different reason actually, but should also |
| 44 | + # fail because of command line incompatibility) |
| 45 | + 'json1/test.desc', |
| 46 | + # uses show-goto-functions |
| 47 | + 'reachability-slice/test.desc', |
| 48 | + 'reachability-slice/test2.desc', |
| 49 | + 'reachability-slice/test3.desc', |
| 50 | + 'reachability-slice-interproc/test.desc', |
| 51 | + 'unsigned1/test.desc', |
| 52 | + 'reachability-slice-interproc3/test.desc', |
| 53 | + 'sync_lock_release-1/symbol_per_type.desc', |
| 54 | + # this test is marked broken-smt-backend and doesn't work for me locally |
| 55 | + 'integer-assignments1/test.desc' |
| 56 | +])) |
| 57 | + |
| 58 | +# TODO maybe consider looking them up on PATH, but direct paths are |
| 59 | +# harder to get wrong |
| 60 | +if len(sys.argv) != 3: |
| 61 | + sys.stderr.write('Usage: check.py <path-to-cbmc> <path-to-xmllint>') |
| 62 | +CbmcPath = os.path.abspath(sys.argv[1]) |
| 63 | +XmlLintPath = os.path.abspath(sys.argv[2]) |
| 64 | + |
| 65 | + |
| 66 | +class ChangeDir: |
| 67 | + def __init__(self, change_to_wd): |
| 68 | + self.current_wd = os.getcwd() |
| 69 | + self.change_to_wd = change_to_wd |
| 70 | + |
| 71 | + def __enter__(self): |
| 72 | + os.chdir(self.change_to_wd) |
| 73 | + |
| 74 | + def __exit__(self, _type, _value, _tb): |
| 75 | + os.chdir(self.current_wd) |
| 76 | + |
| 77 | + |
| 78 | +class TestSpec: |
| 79 | + def __init__(self, args, is_knownbug, is_future, is_thorough): |
| 80 | + self.args = args |
| 81 | + self.is_knownbug = is_knownbug |
| 82 | + self.is_future = is_future |
| 83 | + self.is_thorough = is_thorough |
| 84 | + |
| 85 | + |
| 86 | +class Validator: |
| 87 | + def __init__(self, total_desc_count): |
| 88 | + self.failed_tests = [] |
| 89 | + self.total_desc_count = total_desc_count |
| 90 | + self.checked_desc_count = 0 |
| 91 | + |
| 92 | + def check_test_desc(self, test_desc_path): |
| 93 | + self.checked_desc_count += 1 |
| 94 | + sys.stdout.write('*** Checking [{}/{}] {}... '.format( |
| 95 | + self.checked_desc_count, self.total_desc_count, test_desc_path)) |
| 96 | + sys.stdout.flush() |
| 97 | + spec = self.read_spec(test_desc_path) |
| 98 | + if spec.is_knownbug: |
| 99 | + print('[Skipping KNOWNBUG]') |
| 100 | + return |
| 101 | + elif spec.is_future: |
| 102 | + print('[Skipping FUTURE]') |
| 103 | + return |
| 104 | + elif spec.is_thorough: |
| 105 | + print('[Skipping THOROUGH]') |
| 106 | + return |
| 107 | + test_desc_dir = os.path.dirname(test_desc_path) |
| 108 | + with ChangeDir(test_desc_dir): |
| 109 | + with tempfile.TemporaryFile() as trace_file: |
| 110 | + self.read_trace_into(trace_file, spec.args) |
| 111 | + trace_file.seek(0) |
| 112 | + self.check_trace(test_desc_path, trace_file) |
| 113 | + |
| 114 | + def read_trace_into(self, trace_file, args): |
| 115 | + subprocess.run([CbmcPath, '--trace', '--xml-ui'] + args, |
| 116 | + stdout=trace_file) |
| 117 | + |
| 118 | + def check_trace(self, test_desc_path, trace_file): |
| 119 | + validate_result = subprocess.run([XmlLintPath, |
| 120 | + '--noout', # we don't want it to print the XML we pipe in |
| 121 | + '--schema', TraceXsd, |
| 122 | + '-' # read from STDIN |
| 123 | + ], |
| 124 | + stdin=trace_file, |
| 125 | + stdout=subprocess.PIPE, |
| 126 | + stderr=subprocess.PIPE) |
| 127 | + if validate_result.returncode == 0: |
| 128 | + sys.stdout.buffer.write(b'[SUCCESS]\n') |
| 129 | + else: |
| 130 | + sys.stdout.buffer.write(b'[FAILURE]\n') |
| 131 | + self.failed_tests.append(test_desc_path) |
| 132 | + sys.stdout.buffer.write(validate_result.stdout) |
| 133 | + sys.stdout.buffer.write(validate_result.stderr) |
| 134 | + |
| 135 | + def read_spec(self, test_desc_path): |
| 136 | + with open(test_desc_path) as test_desc_file: |
| 137 | + test_tags = test_desc_file.readline().split() |
| 138 | + source_file = test_desc_file.readline().strip() |
| 139 | + extra_args = test_desc_file.readline().split() |
| 140 | + is_future = 'FUTURE' in test_tags |
| 141 | + is_thorough = 'THOROUGH' in test_tags |
| 142 | + is_knownbug = 'KNOWNBUG' in test_tags |
| 143 | + return TestSpec(args=[source_file] + extra_args, |
| 144 | + is_thorough=is_thorough, |
| 145 | + is_future=is_future, |
| 146 | + is_knownbug=is_knownbug) |
| 147 | + |
| 148 | + def has_failed_tests(self): |
| 149 | + return len(self.failed_tests) > 0 |
| 150 | + |
| 151 | + def report(self): |
| 152 | + print('{}/{} tests succeed'.format(self.checked_desc_count - len(self.failed_tests), self.checked_desc_count)) |
| 153 | + if self.has_failed_tests(): |
| 154 | + print('Failed tests:') |
| 155 | + for spec in self.failed_tests: |
| 156 | + print(spec) |
| 157 | + |
| 158 | + |
| 159 | +test_desc_files = list( |
| 160 | + filter(lambda s: s not in ExcludedTests, glob.glob(os.path.join(test_base_dir, '*/*.desc')))) |
| 161 | +validator = Validator(total_desc_count=len(test_desc_files)) |
| 162 | +for test_desc in test_desc_files: |
| 163 | + validator.check_test_desc(test_desc) |
| 164 | +validator.report() |
| 165 | +if validator.has_failed_tests(): |
| 166 | + sys.exit(1) |
0 commit comments