From d0c59a3155abf9a1adf6564303da6fa909aca0cd Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 14 Jun 2022 17:59:08 +0200 Subject: [PATCH] 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 -- 2.30.2