From c7668de077fdcc12c5ee07043d5ae6d7f6106482 Mon Sep 17 00:00:00 2001 From: Claire Wolf Date: Mon, 18 May 2020 15:13:56 +0200 Subject: [PATCH] Add support for cosa2 BTOR solver Signed-off-by: Claire Wolf --- sbysrc/sby.py | 2 ++ sbysrc/sby_core.py | 12 +++++--- sbysrc/sby_engine_btor.py | 61 +++++++++++++++++++++++++-------------- 3 files changed, 49 insertions(+), 26 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 82f6eae..5c8c797 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -58,6 +58,8 @@ parser.add_argument("--aigbmc", metavar="", parser.add_argument("--avy", metavar="", action=DictAction, dest="exe_paths") parser.add_argument("--btormc", metavar="", + action=DictAction, dest="exe_paths") +parser.add_argument("--cosa2", metavar="", action=DictAction, dest="exe_paths", help="configure which executable to use for the respective tool") parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg", diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index b62d5f7..972e047 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -90,15 +90,18 @@ class SbyTask: else: self.notify.append(next_task) + def log(self, line): + if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)): + if self.logfile is not None: + print(line, file=self.logfile) + self.job.log("{}: {}".format(self.info, line)) + def handle_output(self, line): if self.terminated or len(line) == 0: return if self.output_callback is not None: line = self.output_callback(line) - if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)): - if self.logfile is not None: - print(line, file=self.logfile) - self.job.log("{}: {}".format(self.info, line)) + self.log(line) def handle_exit(self, retcode): if self.terminated: @@ -222,6 +225,7 @@ class SbyJob: "aigbmc": "aigbmc", "avy": "avy", "btormc": "btormc", + "cosa2": "cosa2", } self.tasks_running = [] diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 6dbec1b..caa999f 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -35,6 +35,9 @@ def run(mode, job, engine_idx, engine): solver_cmd += " -kmin {}".format(job.opt_skip) solver_cmd += " ".join([""] + solver_args[1:]) + elif solver_args[0] == "cosa2": + solver_cmd = job.exe_paths["cosa2"] + " -v 1 -e bmc -k {}".format(job.opt_depth - 1) + else: job.error("Invalid solver command {}.".format(solver_args[0])) @@ -111,10 +114,14 @@ def run(mode, job, engine_idx, engine): def output_callback(line): if mode == "cover": - 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 solver_args[0] == "btormc": + 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 + + else: + job.error("engine_{}: BTOR solver '{}' is currently not supported in cover mode.".format(solver_args[0])) if (common_state.produced_cex < common_state.expected_cex) and line == "sat": assert common_state.wit_file == None @@ -122,6 +129,8 @@ def run(mode, job, engine_idx, engine): common_state.wit_file = open("{}/engine_{}/trace.wit".format(job.workdir, engine_idx), "w") else: common_state.wit_file = open("{}/engine_{}/trace{}.wit".format(job.workdir, engine_idx, common_state.produced_cex), "w") + if solver_args[0] != "btormc": + task.log("Found satisfiability witness.") if common_state.wit_file: print(line, file=common_state.wit_file) @@ -130,7 +139,7 @@ def run(mode, job, engine_idx, engine): suffix = "" else: suffix = common_state.produced_cex - task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"), + task2 = SbyTask(job, "engine_{}_{}".format(engine_idx, common_state.produced_cex), job.model("btor"), "cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=job.workdir, idx=engine_idx, i=suffix), logfile=open("{dir}/engine_{idx}/logfile2.txt".format(dir=job.workdir, idx=engine_idx), "w")) task2.output_callback = output_callback2 @@ -144,28 +153,36 @@ def run(mode, job, engine_idx, engine): if common_state.produced_cex == common_state.expected_cex: common_state.solver_status = "sat" - if line.startswith("u"): - return "No CEX up to depth {}.".format(int(line[1:])-1) - - if solver_args[0] == "btormc": - if "calling BMC on" in line: - return line - if "SATISFIABLE" in line: - return line - if "bad state properties at bound" in line: - return line - if "deleting model checker:" in line: - if common_state.solver_status is None: - common_state.solver_status = "unsat" - return line - - if not common_state.wit_file: + else: + if solver_args[0] == "btormc": + if "calling BMC on" in line: + return line + if "SATISFIABLE" in line: + return line + if "bad state properties at bound" in line: + return line + if "deleting model checker:" in line: + if common_state.solver_status is None: + common_state.solver_status = "unsat" + return line + + elif solver_args[0] == "cosa2": + if line == "unknown": + if common_state.solver_status is None: + common_state.solver_status = "unsat" + return "No CEX found." + if line not in ["b0"]: + return line + print(line, file=task.logfile) return None def exit_callback(retcode): - assert retcode == 0 + if solver_args[0] == "cosa2": + assert retcode in [1, 2] + else: + assert retcode == 0 if common_state.expected_cex != 0: assert common_state.solver_status is not None -- 2.30.2