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