From: N. Engelhardt Date: Tue, 11 Jan 2022 15:12:23 +0000 (+0100) Subject: Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file... X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7c9e5b026b0784d0f749dc63321602dae3470322;p=SymbiYosys.git Rename SbyJob to SbyTask and SbyTask to SbyProc to reduce confusion. Config file tasks now correspond to SbyTasks. --- diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 737297e..58f02d8 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -19,7 +19,7 @@ import argparse, os, sys, shutil, tempfile, re ##yosys-sys-path## -from sby_core import SbyJob, SbyAbort, process_filename +from sby_core import SbyTask, SbyAbort, process_filename from time import localtime class DictAction(argparse.Action): @@ -376,7 +376,7 @@ if (workdir is not None) and (len(tasknames) != 1): print("ERROR: Exactly one task is required when workdir is specified. Specify the task or use --prefix instead of -d.", file=sys.stderr) sys.exit(1) -def run_job(taskname): +def run_task(taskname): my_opt_tmpdir = opt_tmpdir my_workdir = None @@ -430,59 +430,59 @@ def run_job(taskname): junit_filename = "junit" sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname) - job = SbyJob(sbyconfig, my_workdir, early_logmsgs, reusedir) + task = SbyTask(sbyconfig, my_workdir, early_logmsgs, reusedir) for k, v in exe_paths.items(): - job.exe_paths[k] = v + task.exe_paths[k] = v if throw_err: - job.run(setupmode) + task.run(setupmode) else: try: - job.run(setupmode) + task.run(setupmode) except SbyAbort: pass if my_opt_tmpdir: - job.log(f"Removing directory '{my_workdir}'.") + task.log(f"Removing directory '{my_workdir}'.") shutil.rmtree(my_workdir, ignore_errors=True) if setupmode: - job.log(f"SETUP COMPLETE (rc={job.retcode})") + task.log(f"SETUP COMPLETE (rc={task.retcode})") else: - job.log(f"DONE ({job.status}, rc={job.retcode})") - job.logfile.close() + task.log(f"DONE ({task.status}, rc={task.retcode})") + task.logfile.close() if not my_opt_tmpdir and not setupmode: - with open("{}/{}.xml".format(job.workdir, junit_filename), "w") as f: - junit_errors = 1 if job.retcode == 16 else 0 - junit_failures = 1 if job.retcode != 0 and junit_errors == 0 else 0 + with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f: + junit_errors = 1 if task.retcode == 16 else 0 + junit_failures = 1 if task.retcode != 0 and junit_errors == 0 else 0 print('', file=f) - print(f'', file=f) - print(f'', file=f) + print(f'', file=f) + print(f'', file=f) print('', file=f) print(f'', file=f) print('', file=f) - print(f'', file=f) + print(f'', file=f) if junit_errors: - print(f'', file=f) + print(f'', file=f) if junit_failures: - print(f'', file=f) + print(f'', file=f) print('', end="", file=f) - with open(f"{job.workdir}/logfile.txt", "r") as logf: + with open(f"{task.workdir}/logfile.txt", "r") as logf: for line in logf: print(line.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """), end="", file=f) print('', file=f) - with open(f"{job.workdir}/status", "w") as f: - print(f"{job.status} {job.retcode} {job.total_time}", file=f) + with open(f"{task.workdir}/status", "w") as f: + print(f"{task.status} {task.retcode} {task.total_time}", file=f) - return job.retcode + return task.retcode failed = [] retcode = 0 for task in tasknames: - task_retcode = run_job(task) + task_retcode = run_task(task) retcode |= task_retcode if task_retcode: failed.append(task) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 78220e5..372cc9b 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -24,12 +24,12 @@ from shutil import copyfile, copytree, rmtree from select import select from time import time, localtime, sleep -all_tasks_running = [] +all_procs_running = [] def force_shutdown(signum, frame): print("SBY ---- Keyboard interrupt or external termination signal ----", flush=True) - for task in list(all_tasks_running): - task.terminate() + for proc in list(all_procs_running): + proc.terminate() sys.exit(1) if os.name == "posix": @@ -45,13 +45,13 @@ def process_filename(filename): return filename -class SbyTask: - def __init__(self, job, info, deps, cmdline, logfile=None, logstderr=True, silent=False): +class SbyProc: + def __init__(self, task, info, deps, cmdline, logfile=None, logstderr=True, silent=False): self.running = False self.finished = False self.terminated = False self.checkretcode = False - self.job = job + self.task = task self.info = info self.deps = deps if os.name == "posix": @@ -79,7 +79,7 @@ class SbyTask: self.logstderr = logstderr self.silent = silent - self.job.tasks_pending.append(self) + self.task.procs_pending.append(self) for dep in self.deps: dep.register_dep(self) @@ -87,17 +87,17 @@ class SbyTask: self.output_callback = None self.exit_callback = None - def register_dep(self, next_task): + def register_dep(self, next_proc): if self.finished: - next_task.poll() + next_proc.poll() else: - self.notify.append(next_task) + self.notify.append(next_proc) 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(f"{self.info}: {line}") + self.task.log(f"{self.info}: {line}") def handle_output(self, line): if self.terminated or len(line) == 0: @@ -115,19 +115,19 @@ class SbyTask: self.exit_callback(retcode) def terminate(self, timeout=False): - if self.job.opt_wait and not timeout: + if self.task.opt_wait and not timeout: return if self.running: if not self.silent: - self.job.log(f"{self.info}: terminating process") + self.task.log(f"{self.info}: terminating process") if os.name == "posix": try: os.killpg(self.p.pid, signal.SIGTERM) except PermissionError: pass self.p.terminate() - self.job.tasks_running.remove(self) - all_tasks_running.remove(self) + self.task.procs_running.remove(self) + all_procs_running.remove(self) self.terminated = True def poll(self): @@ -140,7 +140,7 @@ class SbyTask: return if not self.silent: - self.job.log(f"{self.info}: starting process \"{self.cmdline}\"") + self.task.log(f"{self.info}: starting process \"{self.cmdline}\"") if os.name == "posix": def preexec_fn(): @@ -157,9 +157,9 @@ class SbyTask: self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE, stderr=(subprocess.STDOUT if self.logstderr else None)) - self.job.tasks_pending.remove(self) - self.job.tasks_running.append(self) - all_tasks_running.append(self) + self.task.procs_pending.remove(self) + self.task.procs_running.append(self) + all_procs_running.append(self) self.running = True return @@ -175,32 +175,32 @@ class SbyTask: if self.p.poll() is not None: if not self.silent: - self.job.log(f"{self.info}: finished (returncode={self.p.returncode})") - self.job.tasks_running.remove(self) - all_tasks_running.remove(self) + self.task.log(f"{self.info}: finished (returncode={self.p.returncode})") + self.task.procs_running.remove(self) + all_procs_running.remove(self) self.running = False if self.p.returncode == 127: - self.job.status = "ERROR" + self.task.status = "ERROR" if not self.silent: - self.job.log(f"{self.info}: COMMAND NOT FOUND. ERROR.") + self.task.log(f"{self.info}: COMMAND NOT FOUND. ERROR.") self.terminated = True - self.job.terminate() + self.task.terminate() return self.handle_exit(self.p.returncode) if self.checkretcode and self.p.returncode != 0: - self.job.status = "ERROR" + self.task.status = "ERROR" if not self.silent: - self.job.log(f"{self.info}: job failed. ERROR.") + self.task.log(f"{self.info}: task failed. ERROR.") self.terminated = True - self.job.terminate() + self.task.terminate() return self.finished = True - for next_task in self.notify: - next_task.poll() + for next_proc in self.notify: + next_proc.poll() return @@ -208,7 +208,7 @@ class SbyAbort(BaseException): pass -class SbyJob: +class SbyTask: def __init__(self, sbyconfig, workdir, early_logs, reusedir): self.options = dict() self.used_options = set() @@ -235,8 +235,8 @@ class SbyJob: "pono": os.getenv("PONO", "pono"), } - self.tasks_running = [] - self.tasks_pending = [] + self.procs_running = [] + self.procs_pending = [] self.start_clock_time = time() @@ -257,14 +257,14 @@ class SbyJob: print(line, file=f) def taskloop(self): - for task in self.tasks_pending: - task.poll() + for proc in self.procs_pending: + proc.poll() - while len(self.tasks_running): + while len(self.procs_running): fds = [] - for task in self.tasks_running: - if task.running: - fds.append(task.p.stdout) + for proc in self.procs_running: + if proc.running: + fds.append(proc.p.stdout) if os.name == "posix": try: @@ -274,16 +274,16 @@ class SbyJob: else: sleep(0.1) - for task in self.tasks_running: - task.poll() + for proc in self.procs_running: + proc.poll() - for task in self.tasks_pending: - task.poll() + for proc in self.procs_pending: + proc.poll() if self.opt_timeout is not None: total_clock_time = int(time() - self.start_clock_time) if total_clock_time > self.opt_timeout: - self.log(f"Reached TIMEOUT ({self.opt_timeout} seconds). Terminating all tasks.") + self.log(f"Reached TIMEOUT ({self.opt_timeout} seconds). Terminating all subprocesses.") self.status = "TIMEOUT" self.terminate(timeout=True) @@ -392,16 +392,16 @@ class SbyJob: print("hierarchy -simcheck", file=f) print(f"""write_ilang ../model/design{"" if model_name == "base" else "_nomem"}.il""", file=f) - task = SbyTask( + proc = SbyProc( 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 + proc.checkretcode = True - return [task] + return [proc] if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name): with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f: @@ -421,15 +421,15 @@ class SbyJob: else: print(f"write_smt2 -wires design_{model_name}.smt2", file=f) - task = SbyTask( + proc = SbyProc( 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 + proc.checkretcode = True - return [task] + return [proc] if re.match(r"^btor(_syn)?(_nomem)?$", model_name): with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f: @@ -450,15 +450,15 @@ class SbyJob: 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( + proc = SbyProc( self, - model_name, + 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 + proc.checkretcode = True - return [task] + return [proc] if model_name == "aig": with open(f"{self.workdir}/model/design_aiger.ys", "w") as f: @@ -477,15 +477,15 @@ class SbyJob: print("stat", file=f) print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f) - task = SbyTask( + proc = SbyProc( self, "aig", self.model("nomem"), f"""cd {self.workdir}/model; {self.exe_paths["yosys"]} -ql design_aiger.log design_aiger.ys""" ) - task.checkretcode = True + proc.checkretcode = True - return [task] + return [proc] assert False @@ -495,8 +495,8 @@ class SbyJob: return self.models[model_name] def terminate(self, timeout=False): - for task in list(self.tasks_running): - task.terminate(timeout=timeout) + for proc in list(self.procs_running): + proc.terminate(timeout=timeout) def update_status(self, new_status): assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"] diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index e024a43..10e1268 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -17,110 +17,110 @@ # import re, os, getopt -from sby_core import SbyTask +from sby_core import SbyProc -def run(mode, job, engine_idx, engine): +def run(mode, task, engine_idx, engine): abc_opts, abc_command = getopt.getopt(engine[1:], "", []) if len(abc_command) == 0: - job.error("Missing ABC command.") + task.error("Missing ABC command.") for o, a in abc_opts: - job.error("Unexpected ABC engine options.") + task.error("Unexpected ABC engine options.") if abc_command[0] == "bmc3": if mode != "bmc": - job.error("ABC command 'bmc3' is only valid in bmc mode.") - abc_command[0] += f" -F {job.opt_depth} -v" + task.error("ABC command 'bmc3' is only valid in bmc mode.") + abc_command[0] += f" -F {task.opt_depth} -v" elif abc_command[0] == "sim3": if mode != "bmc": - job.error("ABC command 'sim3' is only valid in bmc mode.") - abc_command[0] += f" -F {job.opt_depth} -v" + task.error("ABC command 'sim3' is only valid in bmc mode.") + abc_command[0] += f" -F {task.opt_depth} -v" elif abc_command[0] == "pdr": if mode != "prove": - job.error("ABC command 'pdr' is only valid in prove mode.") + task.error("ABC command 'pdr' is only valid in prove mode.") else: - job.error(f"Invalid ABC command {abc_command[0]}.") + task.error(f"Invalid ABC command {abc_command[0]}.") - task = SbyTask( - job, + proc = SbyProc( + task, f"engine_{engine_idx}", - job.model("aig"), - f"""cd {job.workdir}; {job.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"{job.workdir}/engine_{engine_idx}/logfile.txt", "w") + task.model("aig"), + 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") ) - task.noprintregex = re.compile(r"^\.+$") - task_status = None + proc.noprintregex = re.compile(r"^\.+$") + proc_status = None def output_callback(line): - nonlocal task_status + nonlocal proc_status match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) - if match: task_status = "FAIL" + if match: proc_status = "FAIL" 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" + if match: proc_status = "UNKNOWN" match = re.match(r"^Stopping BMC because all 2\^[0-9]+ reachable states are visited.", line) - if match: task_status = "PASS" + if match: proc_status = "PASS" match = re.match(r"^No output asserted in [0-9]+ frames.", line) - if match: task_status = "PASS" + if match: proc_status = "PASS" match = re.match(r"^Property proved.", line) - if match: task_status = "PASS" + if match: proc_status = "PASS" return line def exit_callback(retcode): assert retcode == 0 - assert task_status is not None + assert proc_status is not None - job.update_status(task_status) - job.log(f"engine_{engine_idx}: Status returned by engine: {task_status}") - job.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status}""") + task.update_status(proc_status) + task.log(f"engine_{engine_idx}: Status returned by engine: {proc_status}") + task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""") - job.terminate() + task.terminate() - if task_status == "FAIL" and job.opt_aigsmt != "none": - task2 = SbyTask( - job, + if proc_status == "FAIL" and task.opt_aigsmt != "none": + proc2 = SbyProc( + task, f"engine_{engine_idx}", - job.model("smt2"), + task.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 f" --vlogtb-top {job.opt_tbtop}", - job.opt_append, i=engine_idx), - logfile=open(f"{job.workdir}/engine_{engine_idx}/logfile2.txt", "w") + (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt, + "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}", + task.opt_append, i=engine_idx), + logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") ) - task2_status = None + proc2_status = None def output_callback2(line): - nonlocal task2_status + nonlocal proc2_status match = re.match(r"^## [0-9: ]+ Status: FAILED", line) - if match: task2_status = "FAIL" + if match: proc2_status = "FAIL" match = re.match(r"^## [0-9: ]+ Status: PASSED", line) - if match: task2_status = "PASS" + if match: proc2_status = "PASS" return line def exit_callback2(line): - assert task2_status is not None - assert task2_status == "FAIL" + assert proc2_status is not None + assert proc2_status == "FAIL" - if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"): - job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd") + 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") - task2.output_callback = output_callback2 - task2.exit_callback = exit_callback2 + proc2.output_callback = output_callback2 + proc2.exit_callback = exit_callback2 - task.output_callback = output_callback - task.exit_callback = exit_callback + proc.output_callback = output_callback + proc.exit_callback = exit_callback diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index ffb8f52..4665691 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -17,50 +17,50 @@ # import re, os, getopt -from sby_core import SbyTask +from sby_core import SbyProc -def run(mode, job, engine_idx, engine): +def run(mode, task, engine_idx, engine): opts, solver_args = getopt.getopt(engine[1:], "", []) if len(solver_args) == 0: - job.error("Missing solver command.") + task.error("Missing solver command.") for o, a in opts: - job.error("Unexpected AIGER engine options.") + task.error("Unexpected AIGER engine options.") if solver_args[0] == "suprove": if mode == "live" and (len(solver_args) == 1 or solver_args[1][0] != "+"): solver_args.insert(1, "+simple_liveness") - solver_cmd = " ".join([job.exe_paths["suprove"]] + solver_args[1:]) + solver_cmd = " ".join([task.exe_paths["suprove"]] + solver_args[1:]) elif solver_args[0] == "avy": - solver_cmd = " ".join([job.exe_paths["avy"], "--cex", "-"] + solver_args[1:]) + solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:]) elif solver_args[0] == "aigbmc": - solver_cmd = " ".join([job.exe_paths["aigbmc"]] + solver_args[1:]) + solver_cmd = " ".join([task.exe_paths["aigbmc"]] + solver_args[1:]) else: - job.error(f"Invalid solver command {solver_args[0]}.") + task.error(f"Invalid solver command {solver_args[0]}.") - task = SbyTask( - job, + proc = SbyProc( + task, f"engine_{engine_idx}", - job.model("aig"), - f"cd {job.workdir}; {solver_cmd} model/design_aiger.aig", - logfile=open(f"{job.workdir}/engine_{engine_idx}/logfile.txt", "w") + task.model("aig"), + f"cd {task.workdir}; {solver_cmd} model/design_aiger.aig", + logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w") ) - task_status = None + proc_status = None produced_cex = False end_of_cex = False - aiw_file = open(f"{job.workdir}/engine_{engine_idx}/trace.aiw", "w") + aiw_file = open(f"{task.workdir}/engine_{engine_idx}/trace.aiw", "w") def output_callback(line): - nonlocal task_status + nonlocal proc_status nonlocal produced_cex nonlocal end_of_cex - if task_status is not None: + if proc_status is not None: if not end_of_cex and not produced_cex and line.isdigit(): produced_cex = True if not end_of_cex: @@ -74,80 +74,80 @@ def run(mode, job, engine_idx, engine): if line in ["0", "1", "2"]: print(line, file=aiw_file) - if line == "0": task_status = "PASS" - if line == "1": task_status = "FAIL" - if line == "2": task_status = "UNKNOWN" + if line == "0": proc_status = "PASS" + if line == "1": proc_status = "FAIL" + if line == "2": proc_status = "UNKNOWN" return None def exit_callback(retcode): if solver_args[0] not in ["avy"]: assert retcode == 0 - assert task_status is not None + assert proc_status is not None aiw_file.close() - job.update_status(task_status) - job.log(f"engine_{engine_idx}: Status returned by engine: {task_status}") - job.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status}""") + task.update_status(proc_status) + task.log(f"engine_{engine_idx}: Status returned by engine: {proc_status}") + task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""") - job.terminate() + task.terminate() - if task_status == "FAIL" and job.opt_aigsmt != "none": + if proc_status == "FAIL" and task.opt_aigsmt != "none": if produced_cex: if mode == "live": - task2 = SbyTask( - job, + proc2 = SbyProc( + task, f"engine_{engine_idx}", - job.model("smt2"), + task.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 f" --vlogtb-top {job.opt_tbtop}", + (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt, + "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}", i=engine_idx), - logfile=open(f"{job.workdir}/engine_{engine_idx}/logfile2.txt", "w") + logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") ) else: - task2 = SbyTask( - job, + proc2 = SbyProc( + task, f"engine_{engine_idx}", - job.model("smt2"), + task.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 f" --vlogtb-top {job.opt_tbtop}", - job.opt_append, i=engine_idx), - logfile=open(f"{job.workdir}/engine_{engine_idx}/logfile2.txt", "w") + (task.workdir, task.exe_paths["smtbmc"], task.opt_aigsmt, + "" if task.opt_tbtop is None else f" --vlogtb-top {task.opt_tbtop}", + task.opt_append, i=engine_idx), + logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") ) - task2_status = None + proc2_status = None def output_callback2(line): - nonlocal task2_status + nonlocal proc2_status match = re.match(r"^## [0-9: ]+ Status: FAILED", line) - if match: task2_status = "FAIL" + if match: proc2_status = "FAIL" match = re.match(r"^## [0-9: ]+ Status: PASSED", line) - if match: task2_status = "PASS" + if match: proc2_status = "PASS" return line def exit_callback2(line): - assert task2_status is not None + assert proc2_status is not None if mode == "live": - assert task2_status == "PASS" + assert proc2_status == "PASS" else: - assert task2_status == "FAIL" + assert proc2_status == "FAIL" - if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"): - job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd") + 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") - task2.output_callback = output_callback2 - task2.exit_callback = exit_callback2 + proc2.output_callback = output_callback2 + proc2.exit_callback = exit_callback2 else: - job.log(f"engine_{engine_idx}: Engine did not produce a counter example.") + task.log(f"engine_{engine_idx}: Engine did not produce a counter example.") - task.output_callback = output_callback - task.exit_callback = exit_callback + proc.output_callback = output_callback + proc.exit_callback = exit_callback diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 5763410..15344d8 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -18,38 +18,38 @@ import re, os, getopt from types import SimpleNamespace -from sby_core import SbyTask +from sby_core import SbyProc -def run(mode, job, engine_idx, engine): +def run(mode, task, engine_idx, engine): random_seed = None opts, solver_args = getopt.getopt(engine[1:], "", ["seed="]) if len(solver_args) == 0: - job.error("Missing solver command.") + task.error("Missing solver command.") for o, a in opts: if o == "--seed": random_seed = a else: - job.error("Unexpected BTOR engine options.") + task.error("Unexpected BTOR engine options.") if solver_args[0] == "btormc": solver_cmd = "" if random_seed: solver_cmd += f"BTORSEED={random_seed} " - solver_cmd += job.exe_paths["btormc"] + f""" --stop-first {0 if mode == "cover" else 1} -v 1 -kmax {job.opt_depth - 1}""" - if job.opt_skip is not None: - solver_cmd += f" -kmin {job.opt_skip}" + solver_cmd += task.exe_paths["btormc"] + f""" --stop-first {0 if mode == "cover" else 1} -v 1 -kmax {task.opt_depth - 1}""" + if task.opt_skip is not None: + solver_cmd += f" -kmin {task.opt_skip}" solver_cmd += " ".join([""] + solver_args[1:]) elif solver_args[0] == "pono": if random_seed: - job.error("Setting the random seed is not available for the pono solver.") - solver_cmd = job.exe_paths["pono"] + f" -v 1 -e bmc -k {job.opt_depth - 1}" + task.error("Setting the random seed is not available for the pono solver.") + solver_cmd = task.exe_paths["pono"] + f" -v 1 -e bmc -k {task.opt_depth - 1}" else: - job.error(f"Invalid solver command {solver_args[0]}.") + task.error(f"Invalid solver command {solver_args[0]}.") common_state = SimpleNamespace() common_state.solver_status = None @@ -59,44 +59,44 @@ def run(mode, job, engine_idx, engine): common_state.assert_fail = False common_state.produced_traces = [] common_state.print_traces_max = 5 - common_state.running_tasks = 0 + common_state.running_procs = 0 def print_traces_and_terminate(): if mode == "cover": if common_state.assert_fail: - task_status = "FAIL" + proc_status = "FAIL" elif common_state.expected_cex == 0: - task_status = "pass" + proc_status = "pass" elif common_state.solver_status == "sat": - task_status = "pass" + proc_status = "pass" elif common_state.solver_status == "unsat": - task_status = "FAIL" + proc_status = "FAIL" else: - job.error(f"engine_{engine_idx}: Engine terminated without status.") + task.error(f"engine_{engine_idx}: Engine terminated without status.") else: if common_state.expected_cex == 0: - task_status = "pass" + proc_status = "pass" elif common_state.solver_status == "sat": - task_status = "FAIL" + proc_status = "FAIL" elif common_state.solver_status == "unsat": - task_status = "pass" + proc_status = "pass" else: - job.error(f"engine_{engine_idx}: Engine terminated without status.") + task.error(f"engine_{engine_idx}: Engine terminated without status.") - job.update_status(task_status.upper()) - job.log(f"engine_{engine_idx}: Status returned by engine: {task_status}") - job.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status}""") + task.update_status(proc_status.upper()) + task.log(f"engine_{engine_idx}: Status returned by engine: {proc_status}") + task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status}""") if len(common_state.produced_traces) == 0: - job.log(f"""engine_{engine_idx}: Engine did not produce a{" counter" if mode != "cover" else "n "}example.""") + task.log(f"""engine_{engine_idx}: Engine did not produce a{" counter" if mode != "cover" else "n "}example.""") elif len(common_state.produced_traces) <= common_state.print_traces_max: - job.summary.extend(common_state.produced_traces) + task.summary.extend(common_state.produced_traces) else: - job.summary.extend(common_state.produced_traces[:common_state.print_traces_max]) + task.summary.extend(common_state.produced_traces[:common_state.print_traces_max]) excess_traces = len(common_state.produced_traces) - common_state.print_traces_max - job.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""") + task.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""") - job.terminate() + task.terminate() if mode == "cover": def output_callback2(line): @@ -112,12 +112,12 @@ def run(mode, job, engine_idx, engine): def exit_callback2(retcode): assert retcode == 0 - vcdpath = f"{job.workdir}/engine_{engine_idx}/trace{suffix}.vcd" + 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}""") - common_state.running_tasks -= 1 - if (common_state.running_tasks == 0): + common_state.running_procs -= 1 + if (common_state.running_procs == 0): print_traces_and_terminate() return exit_callback2 @@ -131,16 +131,16 @@ def run(mode, job, engine_idx, engine): assert common_state.produced_cex == 0 else: - job.error(f"engine_{engine_idx}: BTOR solver '{solver_args[0]}' is currently not supported in cover mode.") + 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.expected_cex == 1: - common_state.wit_file = open(f"{job.workdir}/engine_{engine_idx}/trace.wit", "w") + common_state.wit_file = open(f"{task.workdir}/engine_{engine_idx}/trace.wit", "w") else: - common_state.wit_file = open(f"""{job.workdir}/engine_{engine_idx}/trace{common_state.produced_cex}.wit""", "w") + common_state.wit_file = open(f"""{task.workdir}/engine_{engine_idx}/trace{common_state.produced_cex}.wit""", "w") if solver_args[0] != "btormc": - task.log("Found satisfiability witness.") + proc.log("Found satisfiability witness.") if common_state.wit_file: print(line, file=common_state.wit_file) @@ -149,17 +149,17 @@ def run(mode, job, engine_idx, engine): suffix = "" else: suffix = common_state.produced_cex - task2 = SbyTask( - job, + proc2 = SbyProc( + task, f"engine_{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(f"{job.workdir}/engine_{engine_idx}/logfile2.txt", "w") + task.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=task.workdir, idx=engine_idx, i=suffix), + logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") ) - task2.output_callback = output_callback2 - task2.exit_callback = make_exit_callback(suffix) - task2.checkretcode = True - common_state.running_tasks += 1 + proc2.output_callback = output_callback2 + proc2.exit_callback = make_exit_callback(suffix) + proc2.checkretcode = True + common_state.running_procs += 1 common_state.produced_cex += 1 common_state.wit_file.close() @@ -188,7 +188,7 @@ def run(mode, job, engine_idx, engine): if line not in ["b0"]: return line - print(line, file=task.logfile) + print(line, file=proc.logfile) return None @@ -202,24 +202,24 @@ def run(mode, job, engine_idx, engine): if common_state.solver_status == "unsat": if common_state.expected_cex == 1: - with open(f"""{job.workdir}/engine_{engine_idx}/trace.wit""", "w") as wit_file: + with open(f"""{task.workdir}/engine_{engine_idx}/trace.wit""", "w") as wit_file: print("unsat", file=wit_file) else: for i in range(common_state.produced_cex, common_state.expected_cex): - with open(f"{job.workdir}/engine_{engine_idx}/trace{i}.wit", "w") as wit_file: + with open(f"{task.workdir}/engine_{engine_idx}/trace{i}.wit", "w") as wit_file: print("unsat", file=wit_file) - common_state.running_tasks -= 1 - if (common_state.running_tasks == 0): + common_state.running_procs -= 1 + if (common_state.running_procs == 0): print_traces_and_terminate() - task = SbyTask( - job, - f"engine_{engine_idx}", job.model("btor"), - f"cd {job.workdir}; {solver_cmd} model/design_btor.btor", - logfile=open(f"{job.workdir}/engine_{engine_idx}/logfile.txt", "w") + proc = SbyProc( + task, + f"engine_{engine_idx}", task.model("btor"), + f"cd {task.workdir}; {solver_cmd} model/design_btor.btor", + logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w") ) - task.output_callback = output_callback - task.exit_callback = exit_callback - common_state.running_tasks += 1 + proc.output_callback = output_callback + proc.exit_callback = exit_callback + common_state.running_procs += 1 diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 2ad853f..da2e31c 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -17,9 +17,9 @@ # import re, os, getopt -from sby_core import SbyTask +from sby_core import SbyProc -def run(mode, job, engine_idx, engine): +def run(mode, task, engine_idx, engine): smtbmc_opts = [] nomem_opt = False presat_opt = True @@ -59,16 +59,16 @@ def run(mode, job, engine_idx, engine): progress = True elif o == "--basecase": if induction_only: - job.error("smtbmc options --basecase and --induction are exclusive.") + task.error("smtbmc options --basecase and --induction are exclusive.") basecase_only = True elif o == "--induction": if basecase_only: - job.error("smtbmc options --basecase and --induction are exclusive.") + task.error("smtbmc options --basecase and --induction are exclusive.") induction_only = True elif o == "--seed": random_seed = a else: - job.error(f"Invalid smtbmc options {o}.") + task.error(f"Invalid smtbmc options {o}.") xtra_opts = False for i, a in enumerate(args): @@ -88,11 +88,11 @@ def run(mode, job, engine_idx, engine): if unroll_opt is None or unroll_opt: smtbmc_opts += ["--unroll"] - if job.opt_smtc is not None: - smtbmc_opts += ["--smtc", f"src/{job.opt_smtc}"] + if task.opt_smtc is not None: + smtbmc_opts += ["--smtc", f"src/{task.opt_smtc}"] - if job.opt_tbtop is not None: - smtbmc_opts += ["--vlogtb-top", job.opt_tbtop] + if task.opt_tbtop is not None: + smtbmc_opts += ["--vlogtb-top", task.opt_tbtop] model_name = "smt2" if syn_opt: model_name += "_syn" @@ -102,21 +102,21 @@ def run(mode, job, engine_idx, engine): if mode == "prove": if not induction_only: - run("prove_basecase", job, engine_idx, engine) + run("prove_basecase", task, engine_idx, engine) if not basecase_only: - run("prove_induction", job, engine_idx, engine) + run("prove_induction", task, engine_idx, engine) return - taskname = f"engine_{engine_idx}" + procname = f"engine_{engine_idx}" trace_prefix = f"engine_{engine_idx}/trace" - logfile_prefix = f"{job.workdir}/engine_{engine_idx}/logfile" + logfile_prefix = f"{task.workdir}/engine_{engine_idx}/logfile" if mode == "prove_basecase": - taskname += ".basecase" + procname += ".basecase" logfile_prefix += "_basecase" if mode == "prove_induction": - taskname += ".induction" + procname += ".induction" trace_prefix += "_induct" logfile_prefix += "_induction" smtbmc_opts.append("-i") @@ -132,118 +132,118 @@ def run(mode, job, engine_idx, engine): smtbmc_opts.append("--noprogress") - if job.opt_skip is not None: - t_opt = "{}:{}".format(job.opt_skip, job.opt_depth) + if task.opt_skip is not None: + t_opt = "{}:{}".format(task.opt_skip, task.opt_depth) else: - t_opt = "{}".format(job.opt_depth) + t_opt = "{}".format(task.opt_depth) random_seed = f"--info \"(set-option :random-seed {random_seed})\"" if random_seed else "" - task = SbyTask( - job, - taskname, - job.model(model_name), - f"""cd {job.workdir}; {job.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {job.opt_append} --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""", + proc = SbyProc( + task, + procname, + task.model(model_name), + f"""cd {task.workdir}; {task.exe_paths["smtbmc"]} {" ".join(smtbmc_opts)} -t {t_opt} {random_seed} --append {task.opt_append} --dump-vcd {trace_prefix}.vcd --dump-vlogtb {trace_prefix}_tb.v --dump-smtc {trace_prefix}.smtc model/design_{model_name}.smt2""", logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress) ) if mode == "prove_basecase": - job.basecase_tasks.append(task) + task.basecase_procs.append(proc) if mode == "prove_induction": - job.induction_tasks.append(task) + task.induction_procs.append(proc) - task_status = None + proc_status = None def output_callback(line): - nonlocal task_status + nonlocal proc_status match = re.match(r"^## [0-9: ]+ Status: FAILED", line) if match: - task_status = "FAIL" + proc_status = "FAIL" return line.replace("FAILED", "failed") match = re.match(r"^## [0-9: ]+ Status: PASSED", line) if match: - task_status = "PASS" + proc_status = "PASS" return line.replace("PASSED", "passed") match = re.match(r"^## [0-9: ]+ Status: PREUNSAT", line) if match: - task_status = "ERROR" + proc_status = "ERROR" return line match = re.match(r"^## [0-9: ]+ Unexpected response from solver:", line) if match: - task_status = "ERROR" + proc_status = "ERROR" return line return line def exit_callback(retcode): - if task_status is None: - job.error(f"engine_{engine_idx}: Engine terminated without status.") + if proc_status is None: + task.error(f"engine_{engine_idx}: Engine terminated without status.") if mode == "bmc" or mode == "cover": - job.update_status(task_status) - task_status_lower = task_status.lower() if task_status == "PASS" else task_status - job.log(f"engine_{engine_idx}: Status returned by engine: {task_status_lower}") - job.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status_lower}""") - - if task_status == "FAIL" and mode != "cover": - if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"): - job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd") - elif task_status == "PASS" and mode == "cover": + task.update_status(proc_status) + proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status + task.log(f"engine_{engine_idx}: Status returned by engine: {proc_status_lower}") + task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status_lower}""") + + if proc_status == "FAIL" and mode != "cover": + 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") + elif proc_status == "PASS" and mode == "cover": print_traces_max = 5 for i in range(print_traces_max): - if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace{i}.vcd"): - job.summary.append(f"trace: {job.workdir}/engine_{engine_idx}/trace{i}.vcd") + if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace{i}.vcd"): + task.summary.append(f"trace: {task.workdir}/engine_{engine_idx}/trace{i}.vcd") else: break else: excess_traces = 0 - while os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace{print_traces_max + excess_traces}.vcd"): + while os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace{print_traces_max + excess_traces}.vcd"): excess_traces += 1 if excess_traces > 0: - job.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""") + task.summary.append(f"""and {excess_traces} further trace{"s" if excess_traces > 1 else ""}""") - job.terminate() + task.terminate() elif mode in ["prove_basecase", "prove_induction"]: - task_status_lower = task_status.lower() if task_status == "PASS" else task_status - job.log(f"""engine_{engine_idx}: Status returned by engine for {mode.split("_")[1]}: {task_status_lower}""") - job.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {task_status_lower} for {mode.split("_")[1]}""") + proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status + task.log(f"""engine_{engine_idx}: Status returned by engine for {mode.split("_")[1]}: {proc_status_lower}""") + task.summary.append(f"""engine_{engine_idx} ({" ".join(engine)}) returned {proc_status_lower} for {mode.split("_")[1]}""") if mode == "prove_basecase": - for task in job.basecase_tasks: - task.terminate() + for proc in task.basecase_procs: + proc.terminate() - if task_status == "PASS": - job.basecase_pass = True + if proc_status == "PASS": + task.basecase_pass = True else: - job.update_status(task_status) - if os.path.exists(f"{job.workdir}/engine_{engine_idx}/trace.vcd"): - job.summary.append(f"counterexample trace: {job.workdir}/engine_{engine_idx}/trace.vcd") - job.terminate() + task.update_status(proc_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") + task.terminate() elif mode == "prove_induction": - for task in job.induction_tasks: - task.terminate() + for proc in task.induction_procs: + proc.terminate() - if task_status == "PASS": - job.induction_pass = True + if proc_status == "PASS": + task.induction_pass = True else: assert False - if job.basecase_pass and job.induction_pass: - job.update_status("PASS") - job.summary.append("successful proof by k-induction.") - job.terminate() + if task.basecase_pass and task.induction_pass: + task.update_status("PASS") + task.summary.append("successful proof by k-induction.") + task.terminate() else: assert False - task.output_callback = output_callback - task.exit_callback = exit_callback + proc.output_callback = output_callback + proc.exit_callback = exit_callback diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index eff0a5c..fd128ed 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -17,31 +17,31 @@ # import re, os, getopt -from sby_core import SbyTask +from sby_core import SbyProc -def run(job): - job.handle_int_option("depth", 20) - job.handle_int_option("append", 0) - job.handle_str_option("aigsmt", "yices") +def run(task): + task.handle_int_option("depth", 20) + task.handle_int_option("append", 0) + task.handle_str_option("aigsmt", "yices") - for engine_idx in range(len(job.engines)): - engine = job.engines[engine_idx] + for engine_idx in range(len(task.engines)): + engine = task.engines[engine_idx] assert len(engine) > 0 - job.log(f"""engine_{engine_idx}: {" ".join(engine)}""") - job.makedirs(f"{job.workdir}/engine_{engine_idx}") + task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") + task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc": import sby_engine_smtbmc - sby_engine_smtbmc.run("bmc", job, engine_idx, engine) + sby_engine_smtbmc.run("bmc", task, engine_idx, engine) elif engine[0] == "abc": import sby_engine_abc - sby_engine_abc.run("bmc", job, engine_idx, engine) + sby_engine_abc.run("bmc", task, engine_idx, engine) elif engine[0] == "btor": import sby_engine_btor - sby_engine_btor.run("bmc", job, engine_idx, engine) + sby_engine_btor.run("bmc", task, engine_idx, engine) else: - job.error(f"Invalid engine '{engine[0]}' for bmc mode.") + task.error(f"Invalid engine '{engine[0]}' for bmc mode.") diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index da3c1ad..858ab9a 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -17,26 +17,26 @@ # import re, os, getopt -from sby_core import SbyTask +from sby_core import SbyProc -def run(job): - job.handle_int_option("depth", 20) - job.handle_int_option("append", 0) +def run(task): + task.handle_int_option("depth", 20) + task.handle_int_option("append", 0) - for engine_idx in range(len(job.engines)): - engine = job.engines[engine_idx] + for engine_idx in range(len(task.engines)): + engine = task.engines[engine_idx] assert len(engine) > 0 - job.log(f"""engine_{engine_idx}: {" ".join(engine)}""") - job.makedirs(f"{job.workdir}/engine_{engine_idx}") + task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") + task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc": import sby_engine_smtbmc - sby_engine_smtbmc.run("cover", job, engine_idx, engine) + sby_engine_smtbmc.run("cover", task, engine_idx, engine) elif engine[0] == "btor": import sby_engine_btor - sby_engine_btor.run("cover", job, engine_idx, engine) + sby_engine_btor.run("cover", task, engine_idx, engine) else: - job.error(f"Invalid engine '{engine[0]}' for cover mode.") + task.error(f"Invalid engine '{engine[0]}' for cover mode.") diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index 26cca22..a633053 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -17,23 +17,23 @@ # import re, os, getopt -from sby_core import SbyTask +from sby_core import SbyProc -def run(job): - job.handle_str_option("aigsmt", "yices") +def run(task): + task.handle_str_option("aigsmt", "yices") - job.status = "UNKNOWN" + task.status = "UNKNOWN" - for engine_idx in range(len(job.engines)): - engine = job.engines[engine_idx] + for engine_idx in range(len(task.engines)): + engine = task.engines[engine_idx] assert len(engine) > 0 - job.log(f"""engine_{engine_idx}: {" ".join(engine)}""") - job.makedirs(f"{job.workdir}/engine_{engine_idx}") + task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") + task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "aiger": import sby_engine_aiger - sby_engine_aiger.run("live", job, engine_idx, engine) + sby_engine_aiger.run("live", task, engine_idx, engine) else: - job.error(f"Invalid engine '{engine[0]}' for live mode.") + task.error(f"Invalid engine '{engine[0]}' for live mode.") diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index e8fbd20..6b446a8 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -17,38 +17,38 @@ # import re, os, getopt -from sby_core import SbyTask +from sby_core import SbyProc -def run(job): - job.handle_int_option("depth", 20) - job.handle_int_option("append", 0) - job.handle_str_option("aigsmt", "yices") +def run(task): + task.handle_int_option("depth", 20) + task.handle_int_option("append", 0) + task.handle_str_option("aigsmt", "yices") - job.status = "UNKNOWN" + task.status = "UNKNOWN" - job.basecase_pass = False - job.induction_pass = False - job.basecase_tasks = list() - job.induction_tasks = list() + task.basecase_pass = False + task.induction_pass = False + task.basecase_procs = list() + task.induction_procs = list() - for engine_idx in range(len(job.engines)): - engine = job.engines[engine_idx] + for engine_idx in range(len(task.engines)): + engine = task.engines[engine_idx] assert len(engine) > 0 - job.log(f"""engine_{engine_idx}: {" ".join(engine)}""") - job.makedirs(f"{job.workdir}/engine_{engine_idx}") + task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") + task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc": import sby_engine_smtbmc - sby_engine_smtbmc.run("prove", job, engine_idx, engine) + sby_engine_smtbmc.run("prove", task, engine_idx, engine) elif engine[0] == "aiger": import sby_engine_aiger - sby_engine_aiger.run("prove", job, engine_idx, engine) + sby_engine_aiger.run("prove", task, engine_idx, engine) elif engine[0] == "abc": import sby_engine_abc - sby_engine_abc.run("prove", job, engine_idx, engine) + sby_engine_abc.run("prove", task, engine_idx, engine) else: - job.error(f"Invalid engine '{engine[0]}' for prove mode.") + task.error(f"Invalid engine '{engine[0]}' for prove mode.")