From e99884e319e7482c442e519cee4e059f6abd7a21 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 15 Jun 2022 12:10:52 +0200
Subject: [PATCH 1/2] SbyProc: New error_callback instead of exit_callback for
failing procs
---
sbysrc/sby_core.py | 22 +++++++++++++++++-----
1 file changed, 17 insertions(+), 5 deletions(-)
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index ab10614..55b582e 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -87,6 +87,7 @@ class SbyProc:
self.output_callback = None
self.exit_callback = None
+ self.error_callback = None
def register_dep(self, next_proc):
if self.finished:
@@ -115,6 +116,14 @@ class SbyProc:
if self.exit_callback is not None:
self.exit_callback(retcode)
+ def handle_error(self, retcode):
+ if self.terminated:
+ return
+ if self.logfile is not None:
+ self.logfile.close()
+ if self.error_callback is not None:
+ self.error_callback(retcode)
+
def terminate(self, timeout=False):
if self.task.opt_wait and not timeout:
return
@@ -185,20 +194,22 @@ class SbyProc:
self.task.status = "ERROR"
if not self.silent:
self.task.log(f"{self.info}: COMMAND NOT FOUND. ERROR.")
+ self.handle_error(self.p.returncode)
self.terminated = True
self.task.terminate()
return
- self.handle_exit(self.p.returncode)
-
if self.checkretcode and self.p.returncode != 0:
self.task.status = "ERROR"
if not self.silent:
self.task.log(f"{self.info}: task failed. ERROR.")
+ self.handle_error(self.p.returncode)
self.terminated = True
self.task.terminate()
return
+ self.handle_exit(self.p.returncode)
+
self.finished = True
for next_proc in self.notify:
next_proc.poll()
@@ -503,14 +514,15 @@ class SbyTask(SbyConfig):
proc.checkretcode = True
def instance_hierarchy_callback(retcode):
- if retcode != 0:
- self.precise_prop_status = False
- return
if self.design_hierarchy == None:
with open(f"{self.workdir}/model/design.json") as f:
self.design_hierarchy = design_hierarchy(f)
+ def instance_hierarchy_error_callback(retcode):
+ self.precise_prop_status = False
+
proc.exit_callback = instance_hierarchy_callback
+ proc.error_callback = instance_hierarchy_error_callback
return [proc]
From d0c59a3155abf9a1adf6564303da6fa909aca0cd Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Tue, 14 Jun 2022 17:59:08 +0200
Subject: [PATCH 2/2] Don't use python asserts to handle unexpected solver
output
---
sbysrc/sby_core.py | 3 ++-
sbysrc/sby_engine_abc.py | 13 ++++++++-----
sbysrc/sby_engine_aiger.py | 16 ++++++++--------
sbysrc/sby_engine_btor.py | 19 +++++++++----------
4 files changed, 27 insertions(+), 24 deletions(-)
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 55b582e..eec0fe6 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -52,6 +52,7 @@ class SbyProc:
self.finished = False
self.terminated = False
self.checkretcode = False
+ self.retcodes = [0]
self.task = task
self.info = info
self.deps = deps
@@ -199,7 +200,7 @@ class SbyProc:
self.task.terminate()
return
- if self.checkretcode and self.p.returncode != 0:
+ if self.checkretcode and self.p.returncode not in self.retcodes:
self.task.status = "ERROR"
if not self.silent:
self.task.log(f"{self.info}: task failed. ERROR.")
diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 10e1268..4635ee1 100644
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -52,6 +52,7 @@ def run(mode, task, engine_idx, engine):
f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
+ proc.checkretcode = True
proc.noprintregex = re.compile(r"^\.+$")
proc_status = None
@@ -77,8 +78,8 @@ def run(mode, task, engine_idx, engine):
return line
def exit_callback(retcode):
- assert retcode == 0
- assert proc_status is not None
+ if proc_status is None:
+ task.error(f"engine_{engine_idx}: Could not determine engine status.")
task.update_status(proc_status)
task.log(f"engine_{engine_idx}: Status returned by engine: {proc_status}")
@@ -112,9 +113,11 @@ def run(mode, task, engine_idx, engine):
return line
- def exit_callback2(line):
- assert proc2_status is not None
- assert proc2_status == "FAIL"
+ def exit_callback2(retcode):
+ if proc2_status is None:
+ task.error(f"engine_{engine_idx}: Could not determine aigsmt status.")
+ if proc2_status != "FAIL":
+ task.error(f"engine_{engine_idx}: Unexpected aigsmt status.")
if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"):
task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index 2850d46..e392932 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -58,6 +58,8 @@ def run(mode, task, engine_idx, engine):
f"cd {task.workdir}; {solver_cmd} model/design_aiger.aig",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
+ if solver_args[0] not in ["avy"]:
+ proc.checkretcode = True
proc_status = None
produced_cex = False
@@ -90,9 +92,8 @@ def run(mode, task, engine_idx, engine):
return None
def exit_callback(retcode):
- if solver_args[0] not in ["avy"]:
- assert retcode == 0
- assert proc_status is not None
+ if proc_status is None:
+ task.error(f"engine_{engine_idx}: Could not determine engine status.")
aiw_file.close()
@@ -143,11 +144,10 @@ def run(mode, task, engine_idx, engine):
return line
def exit_callback2(line):
- assert proc2_status is not None
- if mode == "live":
- assert proc2_status == "PASS"
- else:
- assert proc2_status == "FAIL"
+ if proc2_status is None:
+ task.error(f"engine_{engine_idx}: Could not determine aigsmt status.")
+ if proc2_status != ("PASS" if mode == "live" else "FAIL"):
+ task.error(f"engine_{engine_idx}: Unexpected aigsmt status.")
if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"):
task.summary.append(f"counterexample trace: {task.workdir}/engine_{engine_idx}/trace.vcd")
diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index 0fe577b..9670a1b 100644
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -113,8 +113,6 @@ def run(mode, task, engine_idx, engine):
def make_exit_callback(suffix):
def exit_callback2(retcode):
- assert retcode == 0
-
vcdpath = f"{task.workdir}/engine_{engine_idx}/trace{suffix}.vcd"
if os.path.exists(vcdpath):
common_state.produced_traces.append(f"""{"" if mode == "cover" else "counterexample "}trace: {vcdpath}""")
@@ -131,13 +129,15 @@ def run(mode, task, engine_idx, engine):
match = re.search(r"calling BMC on ([0-9]+) properties", line)
if match:
common_state.expected_cex = int(match[1])
- assert common_state.produced_cex == 0
+ if common_state.produced_cex != 0:
+ task.error(f"engine_{engine_idx}: Unexpected engine output (property count).")
else:
task.error(f"engine_{engine_idx}: BTOR solver '{solver_args[0]}' is currently not supported in cover mode.")
if (common_state.produced_cex < common_state.expected_cex) and line == "sat":
- assert common_state.wit_file == None
+ if common_state.wit_file != None:
+ task.error(f"engine_{engine_idx}: Unexpected engine output (sat).")
if common_state.expected_cex == 1:
common_state.wit_file = open(f"{task.workdir}/engine_{engine_idx}/trace.wit", "w")
else:
@@ -196,12 +196,9 @@ def run(mode, task, engine_idx, engine):
return None
def exit_callback(retcode):
- if solver_args[0] == "pono":
- assert retcode in [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2
- else:
- assert retcode == 0
if common_state.expected_cex != 0:
- assert common_state.solver_status is not None
+ if common_state.solver_status is None:
+ task.error(f"engine_{engine_idx}: Could not determine engine status.")
if common_state.solver_status == "unsat":
if common_state.expected_cex == 1:
@@ -222,7 +219,9 @@ def run(mode, task, engine_idx, engine):
f"cd {task.workdir}; {solver_cmd} model/design_btor{'_single' if solver_args[0]=='pono' else ''}.btor",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
-
+ proc.checkretcode = True
+ if solver_args[0] == "pono":
+ proc.retcodes = [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2
proc.output_callback = output_callback
proc.exit_callback = exit_callback
common_state.running_procs += 1