Revision 105b3645
Added by Guillaume Davy over 8 years ago
| tests/gen_contracts.py | ||
|---|---|---|
| 12 | 12 |
re_node = re.compile('.*node.*')
|
| 13 | 13 |
re_ensures = re.compile('.*ensures.*')
|
| 14 | 14 |
re_k = re.compile('--![ ]*k[ ]*:([^;]*);')
|
| 15 |
re_frama_res = re.compile('Proved goals:[ ]*([0-9]*)[ ]*/[ ]*([0-9]*)')
|
|
| 15 | 16 |
|
| 16 | 17 |
def findInLines(lines, regex): |
| 17 | 18 |
res = [] |
| ... | ... | |
| 59 | 60 |
properties = findInLines(lines, re_property) |
| 60 | 61 |
k = findInLines(lines, re_k) |
| 61 | 62 |
if k: |
| 62 |
return (None, "ALREADY", None)
|
|
| 63 |
return (None, "ALREADY", "KEEP")
|
|
| 63 | 64 |
if not properties: |
| 64 | 65 |
return (None, "NOPR", None) |
| 65 | 66 |
if len(properties) > 1: |
| ... | ... | |
| 68 | 69 |
f = open(top, 'w') |
| 69 | 70 |
f.write("".join(lines))
|
| 70 | 71 |
f.close() |
| 71 |
p = subprocess.Popen(["timeout", "40", "pkind", top, "-timeout", str(TIMEOUT), "-k_incremental", str(MAX)], stdout=subprocess.PIPE, stderr=subprocess.PIPE)
|
|
| 72 |
p = subprocess.Popen(["timeout", "10", "pkind", top, "-timeout", str(TIMEOUT), "-k_incremental", str(MAX)], stdout=subprocess.PIPE, stderr=subprocess.PIPE)
|
|
| 72 | 73 |
(stdout, stderr) = p.communicate() |
| 73 | 74 |
try: |
| 74 | 75 |
root = ET.fromstring(stdout) |
| 75 | 76 |
except ET.ParseError: |
| 76 | 77 |
return (None, "TIMEOUT", None) |
| 78 |
answer = root.find(".//Answer")
|
|
| 79 |
if answer is None: |
|
| 80 |
return (None, "NO_ANS", None) |
|
| 81 |
if answer.text != "valid": |
|
| 82 |
return (None, "INVALID", None) |
|
| 77 | 83 |
k = root.find(".//K")
|
| 78 | 84 |
if k is None: |
| 79 |
return (None, "ERR", None)
|
|
| 85 |
return (None, "NO_K", None)
|
|
| 80 | 86 |
try: |
| 81 | 87 |
k = int(k.text) |
| 82 | 88 |
except ValueError: |
| 83 | 89 |
return (None, "NOTPROVED", None) |
| 84 | 90 |
lines.insert(properties[0][0], "--!k:{};\n".format(k))
|
| 85 |
return (lines, "OK("+"k=" + str(k)+")", None)
|
|
| 91 |
return (lines, "OK("+"k=" + str(k)+")", "KEEP")
|
|
| 86 | 92 |
|
| 87 | 93 |
def compileLustre(lines, temp): |
| 88 | 94 |
top = temp + "/top.lus" |
| ... | ... | |
| 93 | 99 |
(stdout, stderr) = p.communicate() |
| 94 | 100 |
res = p.wait() |
| 95 | 101 |
if res != 0: |
| 96 |
return (None, "ERR_"+str(res), stdout+"\n-------\n"+stderr)
|
|
| 102 |
return (None, "ERR_"+str(res), None)
|
|
| 97 | 103 |
return (lines, "OK", None) |
| 98 | 104 |
|
| 99 |
|
|
| 100 |
|
|
| 101 | 105 |
def framac(lines, temp): |
| 102 |
FRAMAC=["frama-c", "-wp", "-wp-prover", "CVC4,alt-ergo,z3,coq", temp+"/top.c", "-wp-par", "2", "-wp-rte", "-wp-model", "ref", """-wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10""", "-wp-script", temp+"/top.coq" "-wp-no-let"]
|
|
| 106 |
FRAMAC=["frama-c", temp+"/top.c"]
|
|
| 103 | 107 |
p = subprocess.Popen(FRAMAC, stdout=subprocess.PIPE, stderr=subprocess.PIPE) |
| 104 | 108 |
(stdout, stderr) = p.communicate() |
| 105 | 109 |
res = p.wait() |
| 106 | 110 |
if res != 0: |
| 107 |
return (None, "ERR_"+str(res), temp+"\n"+stdout+"\n-------\n"+stderr) |
|
| 108 |
return (lines, "OK", stdout) |
|
| 111 |
return (None, "PARSE_"+str(res), None) |
|
| 112 |
FRAMAC=["frama-c", "-wp", "-wp-prover", "CVC4,alt-ergo,z3,coq", temp+"/top.c", "-wp-par", "2", "-wp-model", "ref", """-wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10" """, "-wp-script", temp+"/top.coq", "-wp-no-let"] |
|
| 113 |
#"-wp-rte", |
|
| 114 |
p = subprocess.Popen(FRAMAC, stdout=subprocess.PIPE, stderr=subprocess.PIPE) |
|
| 115 |
(stdout, stderr) = p.communicate() |
|
| 116 |
res = p.wait() |
|
| 117 |
if res != 0: |
|
| 118 |
return (None, "ERR_"+str(res), None) |
|
| 119 |
m = re_frama_res.search(stdout) |
|
| 120 |
if not m: |
|
| 121 |
return (None, "BAD_OUT", None) |
|
| 122 |
return (lines, str(m.group(1))+"/"+str(m.group(2)), None) |
|
| 109 | 123 |
|
| 110 | 124 |
|
| 111 |
def parseFile(inp, out, todo):
|
|
| 125 |
def parseFile(inp, todo): |
|
| 112 | 126 |
lines = inp.readlines() |
| 113 | 127 |
|
| 114 | 128 |
temp = tempfile.mkdtemp(prefix="contracts_") |
| 115 | 129 |
res = "" |
| 116 |
dats = [] |
|
| 130 |
data = None |
|
| 131 |
ok = False |
|
| 117 | 132 |
for f in todo: |
| 118 | 133 |
x = [[]] |
| 119 |
(newlines, r, data) = f(lines[:], temp)
|
|
| 120 |
res += "{:10} ".format(r[:10])
|
|
| 134 |
(newlines, r, cmd) = f(lines[:], temp)
|
|
| 135 |
res += "{:8} ".format(r[:8])
|
|
| 121 | 136 |
if newlines: |
| 122 | 137 |
lines = newlines |
| 123 |
if data: |
|
| 124 |
dats.append(data) |
|
| 125 |
out.write("".join(lines))
|
|
| 138 |
if cmd == "STOP": |
|
| 139 |
break |
|
| 140 |
if cmd == "KEEP": |
|
| 141 |
ok = True |
|
| 142 |
if ok: |
|
| 143 |
res += "WRITE" |
|
| 144 |
data = "".join(lines) |
|
| 126 | 145 |
shutil.rmtree(temp) |
| 127 | 146 |
|
| 128 |
return (res, dats)
|
|
| 147 |
return (res, data)
|
|
| 129 | 148 |
|
| 130 |
TODO=[modProperties, addEnsures, addK, compileLustre] |
|
| 149 |
TODO=[modProperties, addEnsures, addK, compileLustre, framac]
|
|
| 131 | 150 |
|
| 132 |
LENGTH=50
|
|
| 151 |
LENGTH=40
|
|
| 133 | 152 |
|
| 134 | 153 |
target="./generated/" |
| 135 | 154 |
|
| 136 |
#if os.path.exists(target):
|
|
| 137 |
# shutil.rmtree(target)
|
|
| 155 |
if os.path.exists(target): |
|
| 156 |
shutil.rmtree(target) |
|
| 138 | 157 |
|
| 139 |
orig = "/home/davyg/good"
|
|
| 158 |
orig = "tests_new"
|
|
| 140 | 159 |
for root, dirs, files in os.walk(orig): |
| 141 | 160 |
short = root[len(orig):] |
| 142 | 161 |
os.mkdir(target+"/"+short) |
| ... | ... | |
| 144 | 163 |
if not x.endswith(".lus"):
|
| 145 | 164 |
continue |
| 146 | 165 |
inp = open(root+"/"+x, "r") |
| 147 |
out = open(target+"/"+short+"/"+x, "w") |
|
| 148 |
(res, dats) = parseFile(inp, out, TODO) |
|
| 166 |
(res, data) = parseFile(inp, TODO) |
|
| 149 | 167 |
inp.close() |
| 150 |
out.close() |
|
| 168 |
if data: |
|
| 169 |
out = open(target+"/"+short+"/"+x, "w") |
|
| 170 |
out.write(data) |
|
| 171 |
out.close() |
|
| 151 | 172 |
print(("Process {0:"+str(LENGTH)+"} : {1}").format(("./"+short+"/"+x)[:LENGTH], res))
|
| 152 |
if dats: |
|
| 153 |
print("\n/////////////////////\n".join(dats))
|
|
| 154 | 173 |
sys.stdout.flush() |
Also available in: Unified diff
Delete tests files that have no k