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
|
#!/usr/bin/env python
import os
import re
import sys
import hashlib
import distutils.spawn
sail_dir = os.environ['SAIL_DIR']
os.chdir(os.path.dirname(__file__))
sys.path.insert(0, os.path.join(sail_dir, 'test'))
from sailtest import *
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('.', '_')
tests[filename] = os.fork()
if tests[filename] == 0:
step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
step('timeout 300s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
if re.match('.+\.sat\.sail$', filename):
step('grep -q ^sat$ {}.out'.format(basename))
else:
step('grep -q ^unsat$ {}.out'.format(basename))
print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END)
sys.exit()
results.collect(tests)
return results.finish()
return collect_results(name, tests)
xml = '<testsuites>\n'
if distutils.spawn.find_executable('cvc4'):
xml += test_smt('cvc4', 'cvc4 --lang=smt2.6', '')
else:
print '{}Cannot find SMT solver cvc4 skipping tests{}'.format(color.WARNING, color.END)
#if distutils.spawn.find_executable('z3'):
# xml += test_smt('z3', 'z3', '')
#else:
# print '{}Cannot find SMT solver cvc4 skipping tests{}'.format(color.WARNING, color.END)
xml += '</testsuites>\n'
output = open('tests.xml', 'w')
output.write(xml)
output.close()
|
