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
|
#!/usr/bin/env python3
# Boolector: Satisfiablity Modulo Theories (SMT) solver.
#
# Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
#
# This file is part of Boolector.
# See COPYING for more information on using this software.
#
import argparse
import os
import subprocess
import sys
def check(expected, out, err, output_dir):
out = out.decode()
err = err.decode()
if err:
try:
pos = err.index('log/')
err = err[pos:]
except ValueError:
pass
cmp = '{}{}'.format(out, err)
if expected.strip() != cmp.strip():
print("Expected:\n{}".format(expected.encode()), file=sys.stderr)
print('-' * 80, file=sys.stderr)
outfile_name = os.path.join(output_dir, 'expected.log')
print("see {}".format(outfile_name), file=sys.stderr)
print('-' * 80, file=sys.stderr)
outfile = open(outfile_name, 'w')
outfile.write(expected)
outfile.close()
print('=' * 80, file=sys.stderr)
print("Got:\n{}".format(cmp.encode()), file=sys.stderr)
print('-' * 80, file=sys.stderr)
outfile_name = os.path.join(output_dir, 'got.log')
print("see {}".format(outfile_name), file=sys.stderr)
print('-' * 80, file=sys.stderr)
outfile = open(outfile_name, 'w')
outfile.write(cmp)
outfile.close()
sys.exit(1)
def main():
#print(sys.argv)
ap = argparse.ArgumentParser()
ap.add_argument('binary')
ap.add_argument('testcase')
ap.add_argument('output_dir')
ap.add_argument('--check-sat', action='store_true', default=False)
ap.add_argument('--check-unsat', action='store_true', default=False)
ap.add_argument('--check-output', action='store_true', default=False)
args = ap.parse_args()
btor_args = args.testcase.split()
cmd_args = [args.binary]
cmd_args.extend(btor_args)
testname, _ = os.path.splitext(btor_args[0])
outfilename = '{}.out'.format(testname)
#print(outfilename)
#print(btor_args)
print("Running test case '{}'".format(' '.join(cmd_args)))
proc = subprocess.Popen(cmd_args,
stdin=subprocess.PIPE,
stdout=subprocess.PIPE,
stderr=subprocess.PIPE)
out, err = proc.communicate()
expected = None
if args.check_sat:
expected = 'sat'
elif args.check_unsat:
expected = 'unsat'
else:
assert args.check_output
with open(outfilename, 'r') as outfile:
expected = outfile.read()
check(expected, out, err, args.output_dir)
if __name__ == '__main__':
main()
|
