diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 2ed7e68d..6809e862 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -24,59 +24,44 @@ class DictAction(argparse.Action): def __call__(self, parser, namespace, values, option_string=None): - assert isinstance(getattr(namespace, self.dest), dict), "Use ArgumentParser.set_defaults() to initialize {} to dict()".format(self.dest) + assert isinstance(getattr(namespace, self.dest), + dict), "Use ArgumentParser.set_defaults() to initialize {} to dict()".format(self.dest) name = option_string.lstrip(parser.prefix_chars).replace("-", "_") getattr(namespace, self.dest)[name] = values -parser = argparse.ArgumentParser(prog="sby", - usage="%(prog)s [options] [.sby [tasknames] | ]") +parser = argparse.ArgumentParser(prog="sby", usage="%(prog)s [options] [.sby [tasknames] | ]") parser.set_defaults(exe_paths=dict()) parser.add_argument("-d", metavar="", dest="workdir", - help="set workdir name. default: or _") -parser.add_argument("-f", action="store_true", dest="force", - help="remove workdir if it already exists") -parser.add_argument("-b", action="store_true", dest="backup", - help="backup workdir if it already exists") -parser.add_argument("-t", action="store_true", dest="tmpdir", - help="run in a temporary workdir (remove when finished)") + help="set workdir name. default: or _") +parser.add_argument("-f", action="store_true", dest="force", help="remove workdir if it already exists") +parser.add_argument("-b", action="store_true", dest="backup", help="backup workdir if it already exists") +parser.add_argument("-t", action="store_true", dest="tmpdir", help="run in a temporary workdir (remove when finished)") parser.add_argument("-T", metavar="", action="append", dest="tasknames", default=list(), - help="add taskname (useful when sby file is read from stdin)") + help="add taskname (useful when sby file is read from stdin)") parser.add_argument("-E", action="store_true", dest="throw_err", - help="throw an exception (incl stack trace) for most errors") - -parser.add_argument("--yosys", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--abc", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--smtbmc", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--suprove", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--aigbmc", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--avy", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--btormc", metavar="", - action=DictAction, dest="exe_paths") -parser.add_argument("--pono", metavar="", - action=DictAction, dest="exe_paths", - help="configure which executable to use for the respective tool") + help="throw an exception (incl stack trace) for most errors") + +parser.add_argument("--yosys", metavar="", action=DictAction, dest="exe_paths") +parser.add_argument("--abc", metavar="", action=DictAction, dest="exe_paths") +parser.add_argument("--smtbmc", metavar="", action=DictAction, dest="exe_paths") +parser.add_argument("--suprove", metavar="", action=DictAction, dest="exe_paths") +parser.add_argument("--aigbmc", metavar="", action=DictAction, dest="exe_paths") +parser.add_argument("--avy", metavar="", action=DictAction, dest="exe_paths") +parser.add_argument("--btormc", metavar="", action=DictAction, dest="exe_paths") +parser.add_argument("--pono", 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", - help="print the pre-processed configuration file") -parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks", - help="print the list of tasks") -parser.add_argument("--dumpfiles", action="store_true", dest="dump_files", - help="print the list of source files") -parser.add_argument("--setup", action="store_true", dest="setupmode", - help="set up the working directory and exit") - -parser.add_argument("--init-config-file", dest="init_config_file", - help="create a default .sby config file") + help="print the pre-processed configuration file") +parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks", help="print the list of tasks") +parser.add_argument("--dumpfiles", action="store_true", dest="dump_files", help="print the list of source files") +parser.add_argument("--setup", action="store_true", dest="setupmode", help="set up the working directory and exit") + +parser.add_argument("--init-config-file", dest="init_config_file", help="create a default .sby config file") parser.add_argument("sbyfile", metavar=".sby | ", nargs="?", - help=".sby file OR directory containing config.sby file") + help=".sby file OR directory containing config.sby file") parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*", - help="tasks to run (only valid when .sby is used)") + help="tasks to run (only valid when .sby is used)") args = parser.parse_args() @@ -198,11 +183,11 @@ def handle_line(line): task_skip_line = False for t in task_tags_all: - if line.startswith(t+":"): - line = line[len(t)+1:].lstrip() + if line.startswith(t + ":"): + line = line[len(t) + 1:].lstrip() match = t in task_tags_active - elif line.startswith("~"+t+":"): - line = line[len(t)+2:].lstrip() + elif line.startswith("~" + t + ":"): + line = line[len(t) + 2:].lstrip() match = t not in task_tags_active else: continue @@ -268,7 +253,6 @@ def handle_line(line): return cfgdata, tasklist - sbydata = list() with (open(sbyfile, "r") if sbyfile is not None else sys.stdin) as f: for line in f: @@ -295,7 +279,7 @@ def find_files(taskname): if start_index == -1: return - for line in sbyconfig[start_index+1:]: + for line in sbyconfig[start_index + 1:]: line = line.strip() if line.startswith("["): break @@ -341,7 +325,9 @@ def run_job(taskname): backup_idx = 0 while os.path.exists("{}.bak{:03d}".format(my_workdir, backup_idx)): backup_idx += 1 - early_log(my_workdir, "Moving directory '{}' to '{}'.".format(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx))) + early_log( + my_workdir, "Moving directory '{}' to '{}'.".format(my_workdir, + "{}.bak{:03d}".format(my_workdir, backup_idx))) shutil.move(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx)) if opt_force and not reusedir: @@ -361,7 +347,8 @@ def run_job(taskname): my_opt_tmpdir = True my_workdir = tempfile.mkdtemp() - junit_ts_name = os.path.basename(sbyfile[:-4]) if sbyfile is not None else workdir if workdir is not None else "stdin" + junit_ts_name = os.path.basename( + sbyfile[:-4]) if sbyfile is not None else workdir if workdir is not None else "stdin" junit_tc_name = taskname if taskname is not None else "default" if reusedir: @@ -404,12 +391,18 @@ def run_job(taskname): junit_errors = 1 if job.retcode == 16 else 0 junit_failures = 1 if job.retcode != 0 and junit_errors == 0 else 0 print('', file=f) - print(''.format(junit_errors, junit_failures, job.total_time), file=f) - print(''.format(junit_errors, junit_failures, junit_ts_name, job.total_time), file=f) + print( + ''.format( + junit_errors, junit_failures, job.total_time), file=f) + print( + ''.format( + junit_errors, junit_failures, junit_ts_name, job.total_time), file=f) print('', file=f) print(''.format(os.name), file=f) print('', file=f) - print(''.format(junit_ts_name, junit_tc_name, job.status, job.total_time), file=f) + print( + ''.format(junit_ts_name, junit_tc_name, + job.status, job.total_time), file=f) if junit_errors: print(''.format(job.status, job.status), file=f) if junit_failures: @@ -417,20 +410,22 @@ def run_job(taskname): print('', end="", file=f) with open("{}/logfile.txt".format(job.workdir), "r") as logf: for line in logf: - print(line.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """), end="", file=f) + print( + line.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """), + end="", file=f) print('', file=f) with open("{}/status".format(job.workdir), "w") as f: print("{} {} {}".format(job.status, job.retcode, job.total_time), file=f) return job.retcode - retcode = 0 for t in tasknames: retcode |= run_job(t) if retcode and (len(tasknames) > 1 or tasknames[0] is not None): tm = localtime() - print("SBY {:2d}:{:02d}:{:02d} One or more tasks produced a non-zero return code.".format(tm.tm_hour, tm.tm_min, tm.tm_sec)) + print("SBY {:2d}:{:02d}:{:02d} One or more tasks produced a non-zero return code.".format( + tm.tm_hour, tm.tm_min, tm.tm_sec)) sys.exit(retcode) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index a23ebf09..98cc7e68 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -60,9 +60,9 @@ def __init__(self, job, info, deps, cmdline, logfile=None, logstderr=True, silen # Windows command interpreter equivalents for sequential # commands (; => &) command grouping ({} => ()). replacements = { - ";" : "&", - "{" : "(", - "}" : ")", + ";": "&", + "{": "(", + "}": ")", } cmdline_copy = cmdline @@ -140,19 +140,21 @@ def poll(self): self.job.log("{}: starting process \"{}\"".format(self.info, self.cmdline)) if os.name == "posix": + def preexec_fn(): signal.signal(signal.SIGINT, signal.SIG_IGN) os.setpgrp() - self.p = subprocess.Popen(["/usr/bin/env", "bash", "-c", self.cmdline], stdin=subprocess.DEVNULL, stdout=subprocess.PIPE, - stderr=(subprocess.STDOUT if self.logstderr else None), preexec_fn=preexec_fn) + self.p = subprocess.Popen(["/usr/bin/env", "bash", "-c", self.cmdline], stdin=subprocess.DEVNULL, + stdout=subprocess.PIPE, + stderr=(subprocess.STDOUT if self.logstderr else None), preexec_fn=preexec_fn) fl = fcntl.fcntl(self.p.stdout, fcntl.F_GETFL) fcntl.fcntl(self.p.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK) else: self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE, - stderr=(subprocess.STDOUT if self.logstderr else None)) + stderr=(subprocess.STDOUT if self.logstderr else None)) self.job.tasks_pending.remove(self) self.job.tasks_running.append(self) @@ -200,11 +202,9 @@ def preexec_fn(): next_task.poll() return - class SbyAbort(BaseException): pass - class SbyJob: def __init__(self, sbyconfig, workdir, early_logs, reusedir): self.options = dict() @@ -285,13 +285,19 @@ def taskloop(self): def log(self, logmessage): tm = localtime() - print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True) - print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True) + print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), + flush=True) + print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), + file=self.logfile, flush=True) def error(self, logmessage): tm = localtime() - print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True) - print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True) + print( + "SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), + flush=True) + print( + "SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), + file=self.logfile, flush=True) self.status = "ERROR" if "ERROR" not in self.expect: self.retcode = 16 @@ -385,9 +391,9 @@ def make_model(self, model_name): print("hierarchy -simcheck", file=f) print("write_ilang ../model/design{}.il".format("" if model_name == "base" else "_nomem"), file=f) - task = SbyTask(self, model_name, [], - "cd {}/src; {} -ql ../model/design{s}.log ../model/design{s}.ys".format(self.workdir, self.exe_paths["yosys"], - s="" if model_name == "base" else "_nomem")) + task = SbyTask( + self, model_name, [], "cd {}/src; {} -ql ../model/design{s}.log ../model/design{s}.ys".format( + self.workdir, self.exe_paths["yosys"], s="" if model_name == "base" else "_nomem")) task.checkretcode = True return [task] @@ -410,8 +416,10 @@ def make_model(self, model_name): else: print("write_smt2 -wires design_{}.smt2".format(model_name), file=f) - task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"), - "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)) + task = SbyTask( + self, model_name, self.model("nomem" if "_nomem" in model_name else "base"), + "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], + s=model_name)) task.checkretcode = True return [task] @@ -433,10 +441,14 @@ def make_model(self, model_name): print("delete -output", file=f) print("dffunmap", file=f) print("stat", file=f) - print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) - - task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"), - "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)) + print( + "write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", + m=model_name), file=f) + + task = SbyTask( + self, model_name, self.model("nomem" if "_nomem" in model_name else "base"), + "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], + s=model_name)) task.checkretcode = True return [task] @@ -458,8 +470,9 @@ def make_model(self, model_name): print("stat", file=f) print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f) - task = SbyTask(self, "aig", self.model("nomem"), - "cd {}/model; {} -ql design_aiger.log design_aiger.ys".format(self.workdir, self.exe_paths["yosys"])) + task = SbyTask( + self, "aig", self.model("nomem"), + "cd {}/model; {} -ql design_aiger.log design_aiger.ys".format(self.workdir, self.exe_paths["yosys"])) task.checkretcode = True return [task] @@ -668,16 +681,18 @@ def run(self, setupmode): self.total_time = total_process_time self.summary = [ - "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format - (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time), - "Elapsed process time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format - (total_process_time // (60*60), (total_process_time // 60) % 60, total_process_time % 60, total_process_time), + "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format( + total_clock_time // (60 * 60), + (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time), + "Elapsed process time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format( + total_process_time // (60 * 60), + (total_process_time // 60) % 60, total_process_time % 60, total_process_time), ] + self.summary else: self.summary = [ - "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format - (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time), - "Elapsed process time unvailable on Windows" + "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format( + total_clock_time // (60 * 60), (total_clock_time // 60) % 60, total_clock_time % 60, + total_clock_time), "Elapsed process time unvailable on Windows" ] + self.summary for line in self.summary: diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 49d044d0..9f41d8a2 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -45,10 +45,11 @@ def run(mode, job, engine_idx, engine): else: job.error("Invalid ABC command {}.".format(abc_command[0])) - task = SbyTask(job, "engine_{}".format(engine_idx), job.model("aig"), - ("cd {}; {} -c 'read_aiger model/design_aiger.aig; fold; strash; {}; write_cex -a engine_{}/trace.aiw'").format - (job.workdir, job.exe_paths["abc"], " ".join(abc_command), engine_idx), - logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) + task = SbyTask( + job, "engine_{}".format(engine_idx), job.model("aig"), + ("cd {}; {} -c 'read_aiger model/design_aiger.aig; fold; strash; {}; write_cex -a engine_{}/trace.aiw'").format( + job.workdir, job.exe_paths["abc"], " ".join(abc_command), + engine_idx), logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) task.noprintregex = re.compile(r"^\.+$") task_status = None @@ -59,7 +60,8 @@ def output_callback(line): match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) if match: task_status = "FAIL" - match = re.match(r"^Simulation of [0-9]+ frames for [0-9]+ rounds with [0-9]+ restarts did not assert POs.", line) + match = re.match(r"^Simulation of [0-9]+ frames for [0-9]+ rounds with [0-9]+ restarts did not assert POs.", + line) if match: task_status = "UNKNOWN" match = re.match(r"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line) @@ -84,13 +86,13 @@ def exit_callback(retcode): job.terminate() if task_status == "FAIL" and job.opt_aigsmt != "none": - task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), - ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + - "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format - (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), - job.opt_append, i=engine_idx), - logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), ( + "cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + + + "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2" + ).format(job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, + "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), job.opt_append, + i=engine_idx), logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) task2_status = None diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index dbe05c50..42687025 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -43,8 +43,8 @@ def run(mode, job, engine_idx, engine): job.error("Invalid solver command {}.".format(solver_args[0])) task = SbyTask(job, "engine_{}".format(engine_idx), job.model("aig"), - "cd {}; {} model/design_aiger.aig".format(job.workdir, solver_cmd), - logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) + "cd {}; {} model/design_aiger.aig".format(job.workdir, solver_cmd), + logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) task_status = None produced_cex = False @@ -66,7 +66,7 @@ def output_callback(line): return None if line.startswith("u"): - return "No CEX up to depth {}.".format(int(line[1:])-1) + return "No CEX up to depth {}.".format(int(line[1:]) - 1) if line in ["0", "1", "2"]: print(line, file=aiw_file) @@ -92,21 +92,22 @@ def exit_callback(retcode): if task_status == "FAIL" and job.opt_aigsmt != "none": if produced_cex: if mode == "live": - task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), - ("cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + - "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format - (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), - i=engine_idx), - logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), ( + "cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + + + "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2" + ).format(job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, + "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), i=engine_idx), + logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) else: - task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), - ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + - "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format - (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), - job.opt_append, i=engine_idx), - logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), ( + "cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + + + "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2" + ).format(job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, + "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), job.opt_append, + i=engine_idx), logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), + "w")) task2_status = None @@ -129,7 +130,8 @@ def exit_callback2(line): assert task2_status == "FAIL" if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): - job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) + job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format( + job.workdir, engine_idx)) task2.output_callback = output_callback2 task2.exit_callback = exit_callback2 diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index fb80797d..b450ccb8 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -38,7 +38,8 @@ def run(mode, job, engine_idx, engine): solver_cmd = "" if random_seed: solver_cmd += "BTORSEED={} ".format(random_seed) - solver_cmd += job.exe_paths["btormc"] + " --stop-first {} -v 1 -kmax {}".format(0 if mode == "cover" else 1, job.opt_depth - 1) + solver_cmd += job.exe_paths["btormc"] + " --stop-first {} -v 1 -kmax {}".format( + 0 if mode == "cover" else 1, job.opt_depth - 1) if job.opt_skip is not None: solver_cmd += " -kmin {}".format(job.opt_skip) solver_cmd += " ".join([""] + solver_args[1:]) @@ -88,7 +89,8 @@ def print_traces_and_terminate(): job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status)) if len(common_state.produced_traces) == 0: - job.log("engine_{}: Engine did not produce a{}example.".format(engine_idx, " counter" if mode != "cover" else "n ")) + job.log("engine_{}: Engine did not produce a{}example.".format(engine_idx, + " counter" if mode != "cover" else "n ")) elif len(common_state.produced_traces) <= common_state.print_traces_max: job.summary.extend(common_state.produced_traces) else: @@ -99,12 +101,14 @@ def print_traces_and_terminate(): job.terminate() if mode == "cover": + def output_callback2(line): match = re.search(r"Assert failed in test", line) if match: common_state.assert_fail = True return line else: + def output_callback2(line): return line @@ -114,7 +118,8 @@ def exit_callback2(retcode): vcdpath = "{}/engine_{}/trace{}.vcd".format(job.workdir, engine_idx, suffix) if os.path.exists(vcdpath): - common_state.produced_traces.append("{}trace: {}".format("" if mode == "cover" else "counterexample ", vcdpath)) + common_state.produced_traces.append("{}trace: {}".format("" if mode == "cover" else "counterexample ", + vcdpath)) common_state.running_tasks -= 1 if (common_state.running_tasks == 0): @@ -131,14 +136,16 @@ def output_callback(line): assert common_state.produced_cex == 0 else: - job.error("engine_{}: BTOR solver '{}' is currently not supported in cover mode.".format(engine_idx, solver_args[0])) + job.error("engine_{}: BTOR solver '{}' is currently not supported in cover mode.".format( + engine_idx, solver_args[0])) if (common_state.produced_cex < common_state.expected_cex) and line == "sat": assert common_state.wit_file == None if common_state.expected_cex == 1: 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") + 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.") @@ -149,9 +156,11 @@ def output_callback(line): suffix = "" else: suffix = common_state.produced_cex - 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 = 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 task2.exit_callback = make_exit_callback(suffix) task2.checkretcode = True @@ -190,7 +199,7 @@ def output_callback(line): def exit_callback(retcode): if solver_args[0] == "pono": - assert retcode in [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2 + assert retcode in [0, 1, 255] # UNKNOWN = -1, FALSE = 0, TRUE = 1, ERROR = 2 else: assert retcode == 0 if common_state.expected_cex != 0: @@ -210,8 +219,8 @@ def exit_callback(retcode): print_traces_and_terminate() task = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"), - "cd {}; {} model/design_btor.btor".format(job.workdir, solver_cmd), - logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) + "cd {}; {} model/design_btor.btor".format(job.workdir, solver_cmd), + logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) task.output_callback = output_callback task.exit_callback = exit_callback diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 6d2ffc47..237a4e4d 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -33,8 +33,10 @@ def run(mode, job, engine_idx, engine): induction_only = False random_seed = None - opts, args = getopt.getopt(engine[1:], "", ["nomem", "syn", "stbv", "stdt", "presat", - "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", "induction", "seed="]) + opts, args = getopt.getopt(engine[1:], "", [ + "nomem", "syn", "stbv", "stdt", "presat", "nopresat", "unroll", "nounroll", "dumpsmt2", "progress", "basecase", + "induction", "seed=" + ]) for o, a in opts: if o == "--nomem": @@ -73,7 +75,7 @@ def run(mode, job, engine_idx, engine): xtra_opts = False for i, a in enumerate(args): if i == 0 and a == "z3" and unroll_opt is None: - unroll_opt = False + unroll_opt = False if a == "--": xtra_opts = True continue @@ -92,7 +94,7 @@ def run(mode, job, engine_idx, engine): smtbmc_opts += ["--smtc", "src/{}".format(job.opt_smtc)] if job.opt_tbtop is not None: - smtbmc_opts += ["--vlogtb-top", job.opt_tbtop] + smtbmc_opts += ["--vlogtb-top", job.opt_tbtop] model_name = "smt2" if syn_opt: model_name += "_syn" @@ -131,16 +133,17 @@ def run(mode, job, engine_idx, engine): if not progress: smtbmc_opts.append("--noprogress") - if job.opt_skip is not None: t_opt = "{}:{}".format(job.opt_skip, job.opt_depth) else: t_opt = "{}".format(job.opt_depth) - task = SbyTask(job, taskname, job.model(model_name), - "cd {}; {} {} -t {} {} --append {} --dump-vcd {p}.vcd --dump-vlogtb {p}_tb.v --dump-smtc {p}.smtc model/design_{}.smt2".format - (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, "--info \"(set-option :random-seed {})\"".format(random_seed) if random_seed else "", job.opt_append, model_name, p=trace_prefix), - logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress)) + task = SbyTask( + job, taskname, job.model(model_name), + "cd {}; {} {} -t {} {} --append {} --dump-vcd {p}.vcd --dump-vlogtb {p}_tb.v --dump-smtc {p}.smtc model/design_{}.smt2" + .format(job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, + "--info \"(set-option :random-seed {})\"".format(random_seed) if random_seed else "", job.opt_append, + model_name, p=trace_prefix), logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress)) if mode == "prove_basecase": job.basecase_tasks.append(task) @@ -197,17 +200,22 @@ def exit_callback(retcode): break else: excess_traces = 0 - while os.path.exists("{}/engine_{}/trace{}.vcd".format(job.workdir, engine_idx, print_traces_max + excess_traces)): + while os.path.exists("{}/engine_{}/trace{}.vcd".format(job.workdir, engine_idx, + print_traces_max + excess_traces)): excess_traces += 1 if excess_traces > 0: - job.summary.append("and {} further trace{}".format(excess_traces, "s" if excess_traces > 1 else "")) + job.summary.append("and {} further trace{}".format(excess_traces, + "s" if excess_traces > 1 else "")) job.terminate() elif mode in ["prove_basecase", "prove_induction"]: task_status_lower = task_status.lower() if task_status == "PASS" else task_status - job.log("engine_{}: Status returned by engine for {}: {}".format(engine_idx, mode.split("_")[1], task_status_lower)) - job.summary.append("engine_{} ({}) returned {} for {}".format(engine_idx, " ".join(engine), task_status_lower, mode.split("_")[1])) + job.log("engine_{}: Status returned by engine for {}: {}".format(engine_idx, + mode.split("_")[1], task_status_lower)) + job.summary.append("engine_{} ({}) returned {} for {}".format(engine_idx, " ".join(engine), + task_status_lower, + mode.split("_")[1])) if mode == "prove_basecase": for task in job.basecase_tasks: @@ -219,7 +227,8 @@ def exit_callback(retcode): else: job.update_status(task_status) if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): - job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) + job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format( + job.workdir, engine_idx)) job.terminate() elif mode == "prove_induction":