|
| 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 | +TraceXsdSpec = 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 | + # this one doesn't work for me locally at all |
| 31 | + 'integer-assignments1/test.desc', |
| 32 | + # these test for invalid command line handling |
| 33 | + 'bad_option/test_multiple.desc', |
| 34 | + 'bad_option/test.desc', |
| 35 | + # this one produces XML intermingled with main XML output when used with --xml-ui |
| 36 | + 'graphml_witness2/test.desc', |
| 37 | + # this one uses program-only again |
| 38 | + 'Quantifiers-simplify/simplify_not_forall.desc', |
| 39 | + # produces intermingled XML on the command line |
| 40 | + 'coverage_report1/test.desc', |
| 41 | + 'coverage_report1/paths.desc', |
| 42 | + # this uses json-ui (fails for a different reason actually, but should also |
| 43 | + # fail because of command line incompatibility) |
| 44 | + 'json1/test.desc', |
| 45 | + # uses show-goto-functions |
| 46 | + 'reachability-slice/test.desc', |
| 47 | + 'reachability-slice/test2.desc', |
| 48 | + 'reachability-slice/test3.desc', |
| 49 | + 'reachability-slice-interproc/test.desc', |
| 50 | + # again, intermingles several XML documents |
| 51 | + 'graphml_witness1/test.desc', |
| 52 | + 'switch8/program-only.desc', |
| 53 | + # show-goto-functions |
| 54 | + 'unsigned1/test.desc', |
| 55 | + # show-goto-functions |
| 56 | + 'reachability-slice-interproc3/test.desc', |
| 57 | + 'sync_lock_release-1/symbol_per_type.desc' |
| 58 | +])) |
| 59 | + |
| 60 | +if len(sys.argv) != 2: |
| 61 | + sys.stderr.write('Usage: check.py <path-to-cbmc>') |
| 62 | +CbmcPath = sys.argv[1] |
| 63 | +XsdValidateJar = os.path.join(this_script_dir, 'validate-xsd/build/libs/validate-xsd-1.0-SNAPSHOT-uber.jar') |
| 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_specs): |
| 88 | + self.failed_tests = [] |
| 89 | + self.total_specs = total_specs |
| 90 | + self.total_test_count = 0 |
| 91 | + |
| 92 | + def check_spec(self, spec_path): |
| 93 | + self.total_test_count += 1 |
| 94 | + sys.stdout.write('*** Checking [{}/{}] {}... '.format(self.total_test_count, self.total_specs, spec_path)) |
| 95 | + sys.stdout.flush() |
| 96 | + spec_dir = os.path.dirname(spec_path) |
| 97 | + spec = self.read_spec(spec_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 | + with ChangeDir(spec_dir): |
| 108 | + with tempfile.TemporaryFile() as trace_file: |
| 109 | + self.read_trace_into(trace_file, spec.args) |
| 110 | + trace_file.seek(0) |
| 111 | + self.check_trace(spec_path, trace_file) |
| 112 | + |
| 113 | + def read_trace_into(self, trace_file, args): |
| 114 | + subprocess.run([CbmcPath, '--trace', '--xml-ui', *args], |
| 115 | + stdout=trace_file) |
| 116 | + |
| 117 | + def check_trace(self, spec_path, trace_file): |
| 118 | + validate_result = subprocess.run(['java', '-jar', XsdValidateJar, TraceXsdSpec], |
| 119 | + stdin=trace_file, |
| 120 | + stdout=subprocess.PIPE, |
| 121 | + stderr=subprocess.PIPE) |
| 122 | + if validate_result.returncode == 0: |
| 123 | + print('[SUCCESS]') |
| 124 | + else: |
| 125 | + print('[FAILURE]') |
| 126 | + self.failed_tests.append(spec_path) |
| 127 | + sys.stdout.buffer.write(validate_result.stdout) |
| 128 | + sys.stdout.buffer.write(validate_result.stderr) |
| 129 | + |
| 130 | + def read_spec(self, spec_path): |
| 131 | + with open(spec_path) as spec_file: |
| 132 | + spec = spec_file.readline().split() |
| 133 | + source_file = spec_file.readline().strip() |
| 134 | + extra_args = spec_file.readline().split() |
| 135 | + is_future = 'FUTURE' in spec |
| 136 | + is_thorough = 'THOROUGH' in spec |
| 137 | + is_knownbug = 'KNOWNBUG' in spec |
| 138 | + return TestSpec(args=[source_file, *extra_args], |
| 139 | + is_thorough=is_thorough, |
| 140 | + is_future=is_future, |
| 141 | + is_knownbug=is_knownbug) |
| 142 | + |
| 143 | + def has_failed_tests(self): |
| 144 | + return len(self.failed_tests) > 0 |
| 145 | + |
| 146 | + def report(self): |
| 147 | + print('{}/{} tests succeed'.format(self.total_test_count - len(self.failed_tests), self.total_test_count)) |
| 148 | + if self.has_failed_tests(): |
| 149 | + print('Failed tests:') |
| 150 | + for spec in self.failed_tests: |
| 151 | + print(spec) |
| 152 | + |
| 153 | + |
| 154 | +def run_gradle(args): |
| 155 | + with ChangeDir('validate-xsd'): |
| 156 | + if os.name == 'nt': |
| 157 | + subprocess.check_call(['cmd', '/c', 'gradlew.bat' * args]) |
| 158 | + else: |
| 159 | + subprocess.check_call(['./gradlew', *args]) |
| 160 | + |
| 161 | + |
| 162 | +# ensure that the uberjar exists and is up to date |
| 163 | +run_gradle(['uberjar']) |
| 164 | + |
| 165 | +test_desc_files = list( |
| 166 | + filter(lambda s: s not in ExcludedTests, glob.glob(os.path.join(test_base_dir, '**/*.desc'), recursive=True))) |
| 167 | +validator = Validator(total_specs=len(test_desc_files)) |
| 168 | +for spec in test_desc_files: |
| 169 | + validator.check_spec(spec) |
| 170 | +validator.report() |
| 171 | +if validator.has_failed_tests(): |
| 172 | + sys.exit(1) |
0 commit comments