Merge pull request #180 from jix/sby-fewer-asserts

Don't use python asserts to handle unexpected solver output

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index ab10614fc6906f0594dfc2b748d0dbbc91c76f8e..eec0fe6611acd1f507c0cba0aec520254bc8d024 100644 (file)
--- 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
@@ -87,6 +88,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 +117,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 +195,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:
+            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.")
+                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 +515,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]
 

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index 10e12687c6b86f4f66e4e821ca4277185253916b..4635ee17143c78db29a2fbd394e2375fb18974bd 100644 (file)
--- 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 2850d4615b94512705becb53084d11544075a8ea..e392932e0dd04bea89982f25f3020781e3af7466 100644 (file)
--- 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 0fe577b48f93beb5171af48072fb8e3d6e00cb8b..9670a1bd7b4ae36ada98f66e2ef1ccd41b7d70b2 100644 (file)
--- 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