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
|
#!/usr/bin/env python3
import os
import re
import sys
import hashlib
import shutil
mydir = os.path.dirname(__file__)
os.chdir(mydir)
sys.path.insert(0, os.path.join(mydir, '..'))
from sailtest import *
sail_dir = get_sail_dir()
sail = get_sail()
skip_tests = {
'assembly_mapping_sat': { 'z3', 'cvc4' }, # This test using unsupported CVC4 features
'arith_unsat': { 'z3', 'cvc4' },
'arith_LFL_unsat' : { 'z3', 'cvc4' },
'store_load_sat' : { 'z3', 'cvc4' },
'load_store_dep_sat' : { 'z3', 'cvc4' },
'store_load_scattered_sat' : { 'z3', 'cvc4' },
'mem_builtins_unsat' : { 'z3', 'cvc4' },
'arith_FFL_3_unsat' : { 'cvc4' },
'arith_LCBL_unsat' : { 'cvc4' },
'arith_LC32L_3_unsat' : { 'cvc4' },
'arith_FFL_5_unsat' : { 'cvc4' },
}
print("Sail is {}".format(sail))
print("Sail dir is {}".format(sail_dir))
def test_smt(name, solver, sail_opts):
banner('Testing SMT: {}'.format(name))
results = Results(name)
for filenames in chunks(os.listdir('.'), parallel()):
tests = {}
for filename in filenames:
basename = os.path.splitext(os.path.basename(filename))[0]
basename = basename.replace('.', '_')
if basename in skip_tests:
if name in skip_tests[basename]:
print_skip(filename)
continue
tests[filename] = os.fork()
if tests[filename] == 0:
step('\'{}\' {} -smt {} -o {}'.format(sail, sail_opts, filename, basename))
step('timeout 30s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
if re.match(r'.+\.sat\.sail$', filename):
step('grep -q ^sat$ {}.out'.format(basename))
else:
step('grep -q ^unsat$ {}.out'.format(basename))
print_ok(filename)
sys.exit()
results.collect(tests)
return results.finish()
return collect_results(name, tests)
xml = '<testsuites>\n'
if shutil.which('cvc4') is not None:
xml += test_smt('cvc4', 'cvc4 --lang=smt2.6', '')
else:
print('{}Cannot find SMT solver cvc4 skipping tests{}'.format(color.WARNING, color.END))
if shutil.which('z3') is not None:
xml += test_smt('z3', 'z3', '')
else:
print('{}Cannot find SMT solver z3 skipping tests{}'.format(color.WARNING, color.END))
xml += '</testsuites>\n'
output = open('tests.xml', 'w')
output.write(xml)
output.close()
|
