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
|
#!/usr/bin/env python3
import sys
import sexpdata
import math
import os
from subprocess import Popen, PIPE, DEVNULL
debug = os.environ.get("DEBUG") != None
loads_kwargs = dict(nil=None, true=None) # Don't convert nil or #t in s-exp
class CommandFailed(Exception):
def __init__(self, msg):
self.msg = msg
class NotEqual(Exception):
def __init__(self, path, sexp0, sexp1):
self.path = path
self.sexp0 = sexp0
self.sexp1 = sexp1
# Read a whyml file as a s-exp
def read(why3, filename):
p = Popen([why3, "pp", "--output=sexp", filename], stdout=PIPE, stderr=DEVNULL, encoding='utf8')
s, _ = p.communicate()
if p.returncode == 0:
return sexpdata.loads(s, **loads_kwargs) if s else None
else:
raise CommandFailed("cannot print s-expr for original file (returncode={})"
.format(p.returncode))
# Pretty-print a whyml file and read the result as a s-exp
def print_and_read(why3, filename):
p1 = Popen([why3, "pp", "--output=mlw", filename], stdout=PIPE, stderr=DEVNULL, encoding='utf8')
p2 = Popen([why3, "pp", "--output=sexp", "-"], stdin=p1.stdout, stdout=PIPE, stderr=DEVNULL, encoding='utf8')
s, _ = p2.communicate()
if p2.returncode == 0:
return sexpdata.loads(s, **loads_kwargs) if s else None
else:
raise CommandFailed("cannot print s-expr for pretty-printed output (returncode={})"
.format(p2.returncode))
def is_location(sexp):
try:
return [type(x) for x in sexp] == [str, int, int, int]
except:
return False
IGNORE_ID_ATTRS = [
"W:unused_variable:N", "extraction:array_make", "extraction:array",
"induction", "mlw:reference_var", "infer", "useraxiom", "W:non_conservative_extension:N",
"model_trace:flag", "model_trace:first_val", "model_trace:sec_val", "model_trace:TEMP_NAME",
"model", "W:unmodified_variable:N"
]
def keep_id_attr(at):
try:
# (ATstr ((attr_string "...") (attr_tag N)))
variant, fields = at
field0, field1 = fields
field, value = field0
if variant.value() == 'ATstr' and field.value() == 'attr_string':
return value not in IGNORE_ID_ATTRS
else:
return True
except:
return True
def ignore_id_attrs(sexp):
try:
# (id_ats (at ...))
field, value = sexp
if field.value() == 'id_ats':
ats = [at for at in value if keep_id_attr(at)]
return [sexp[0], ats]
else:
return sexp
except:
return sexp
# Test for sexp (<field_name> _)
def is_field(sexp, field_name):
try:
return len(sexp) == 2 and sexp[0].value() == field_name
except:
return False
def assert_equal(path, sexp0, sexp1):
if sexp0 == sexp1:
return
if is_location(sexp0) and is_location(sexp1):
return # Don't bother with locations
if is_field(sexp0, "attr_tag") and is_field(sexp1, "attr_tag"):
return # Don't bother with tags
if type(sexp0) == float and math.isnan(sexp0) and type(sexp1) == float and math.isnan(sexp1):
return # nan != nan
if type(sexp0) == list and type(sexp1) == list:
while True: # Ignore additional parentheses
try:
if sexp0[0].value() == "PTparen" and sexp1[0].value() != "PTparen":
path = path+[1]
sexp0 = sexp0[1]
elif sexp1[0].value() == "PTparen" and sexp0[0].value() != "PTparen":
sexp1 = sexp1[1]
elif sexp0[0].value() == "Pparen" and sexp1[0].value() != "Pparen":
path = path+[1]
sexp0 = sexp0[1][0][1]
elif sexp1[0].value() == "Pparen" and sexp0[0].value() != "Pparen":
sexp1 = sexp1[1][0][1]
elif sexp0[0].value() == "Ptuple" and len(sexp0[1]) == 1 and sexp1[0].value() != "Ptuple":
path = path+[1]
sexp0 = sexp0[1][0][1]
elif sexp1[0].value() == "Ptuple" and len(sexp1[1]) == 1 and sexp0[0].value() != "Ptuple":
sexp1 = sexp1[1][0][1]
elif ((sexp0[0].value() == "Tinfix" and sexp1[0].value() == "Tinnfix") or
(sexp0[0].value() == "Tinnfix" and sexp1[0].value() == "Tinfix") or
(sexp0[0].value() == "Tbinop" and sexp1[0].value() == "Tbinnop") or
(sexp0[0].value() == "Tbinnop" and sexp1[0].value() == "Tbinop") or
(sexp0[0].value() == "Einfix" and sexp1[0].value() == "Einnfix") or
(sexp0[0].value() == "Einnfix" and sexp1[0].value() == "Einfix")):
sexp0 = sexp0[1:]
sexp1 = sexp1[1:]
else:
break
except AttributeError:
break
sexp0 = ignore_id_attrs(sexp0)
sexp1 = ignore_id_attrs(sexp1)
if len(sexp0) > len(sexp1):
raise NotEqual(path, sexp0, sexp1)
if len(sexp0) < len(sexp1):
raise NotEqual(path, sexp0, sexp1)
for i, (s0, s1) in enumerate(zip(sexp0, sexp1)):
assert_equal(path+[i], s0, s1)
else:
raise NotEqual(path, sexp0, sexp1)
def trace(path, sexp, sexp1):
if path == []:
return [sexpdata.Symbol("ERROR"),
[sexpdata.Symbol("EXPECTED"), sexp],
[sexpdata.Symbol("FOUND"), sexp1]]
elif type(sexp) == list:
return [trace(path[1:], sexp[i], sexp1)
if i == path[0] else sexp[i]
for i, x in enumerate(sexp)]
def test(why3, filename):
print(" {}: ".format(filename), end='', flush=True)
try:
sexp0 = read(why3, filename)
sexp1 = print_and_read(why3, filename)
assert_equal([], sexp0, sexp1)
print("ok")
return True
except NotEqual as e:
print("FAILED")
if debug:
sexpdata.dump(trace(e.path, sexp0, e.sexp1) or "NO TRACE", sys.stdout)
return False
except CommandFailed as e:
print("COMMAND FAILED:", e.msg)
return False
def main():
why3 = sys.argv[1]
files = sys.argv[2:]
res = all(test(why3, f) for f in files)
exit(0 if res else 1)
if __name__ == "__main__":
main()
|
