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
|
#!/usr/bin/python3
import sys
import subprocess
class smtio:
def __init__(self, solver="yices", debug_print=False, debug_file=None):
if solver == "yices":
popen_vargs = ['yices-smt2', '--incremental']
if solver == "z3":
popen_vargs = ['z3', '-smt2', '-in']
if solver == "cvc4":
popen_vargs = ['cvc4', '--incremental']
if solver == "mathsat":
popen_vargs = ['mathsat']
self.debug_print = debug_print
self.debug_file = debug_file
self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
def write(self, stmt):
stmt = stmt.strip()
if self.debug_print:
print("> %s" % stmt)
if self.debug_file:
print(stmt, file=self.debug_file)
self.debug_file.flush()
self.p.stdin.write(bytes(stmt + "\n", "ascii"))
self.p.stdin.flush()
def read(self):
stmt = []
count_brackets = 0
while True:
line = self.p.stdout.readline().decode("ascii").strip()
count_brackets += line.count("(")
count_brackets -= line.count(")")
stmt.append(line)
if self.debug_print:
print("< %s" % line)
if count_brackets == 0:
break
if not self.p.poll():
print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
sys.exit(1)
stmt = "".join(stmt)
if stmt.startswith("(error"):
print("SMT Solver Error: %s" % stmt, file=sys.stderr)
sys.exit(1)
return stmt
def parse(self, stmt):
def worker(stmt):
if stmt[0] == '(':
expr = []
cursor = 1
while stmt[cursor] != ')':
el, le = worker(stmt[cursor:])
expr.append(el)
cursor += le
return expr, cursor+1
if stmt[0] == '|':
expr = "|"
cursor = 1
while stmt[cursor] != '|':
expr += stmt[cursor]
cursor += 1
expr += "|"
return expr, cursor+1
if stmt[0] in [" ", "\t", "\r", "\n"]:
el, le = worker(stmt[1:])
return el, le+1
expr = ""
cursor = 0
while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
expr += stmt[cursor]
cursor += 1
return expr, cursor
return worker(stmt)[0]
def bv2hex(self, v):
if v == "true": return "1"
if v == "false": return "0"
h = ""
while len(v) > 2:
d = 0
if len(v) > 0 and v[-1] == "1": d += 1
if len(v) > 1 and v[-2] == "1": d += 2
if len(v) > 2 and v[-3] == "1": d += 4
if len(v) > 3 and v[-4] == "1": d += 8
h = hex(d)[2:] + h
if len(v) < 4: break
v = v[:-4]
return h
def bv2bin(self, v):
if v == "true": return "1"
if v == "false": return "0"
return v[2:]
def get(self, expr):
self.write("(get-value (%s))" % (expr))
return self.parse(self.read())[0][1]
def get_net(self, mod_name, net_name, state_name):
return self.get("(|%s_n %s| %s)" % (mod_name, net_name, state_name))
def get_net_bool(self, mod_name, net_name, state_name):
v = self.get_net(mod_name, net_name, state_name)
assert v in ["true", "false"]
return 1 if v == "true" else 0
def get_net_hex(self, mod_name, net_name, state_name):
return self.bv2hex(self.get_net(mod_name, net_name, state_name))
def get_net_bin(self, mod_name, net_name, state_name):
return self.bv2bin(self.get_net(mod_name, net_name, state_name))
def wait(self):
self.p.wait()
|
