From bd4094f216083c9c1cc9b65aeda3cbfb30114a16 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 9 Mar 2019 12:42:54 -0800 Subject: [PATCH] Add support for (re-)running in existing workdir Signed-off-by: Clifford Wolf --- sbysrc/sby.py | 49 ++++++++++++++++++++++++++++++++-------- sbysrc/sby_core.py | 25 +++++++++++++++----- sbysrc/sby_mode_bmc.py | 2 +- sbysrc/sby_mode_cover.py | 2 +- sbysrc/sby_mode_live.py | 2 +- sbysrc/sby_mode_prove.py | 2 +- 6 files changed, 62 insertions(+), 20 deletions(-) diff --git a/sbysrc/sby.py b/sbysrc/sby.py index f08f072..20a200f 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -32,10 +32,12 @@ exe_paths = dict() throw_err = False dump_cfg = False dump_tasks = False +reusedir = False +setupmode = False def usage(): print(""" -sby [options] [.sby [tasknames]] +sby [options] [.sby [tasknames] | ] -d set workdir name. default: (without .sby) @@ -69,13 +71,16 @@ sby [options] [.sby [tasknames]] --dumptasks print the list of tasks + + --setup + set up the working directory and exit """) sys.exit(1) try: opts, args = getopt.getopt(sys.argv[1:], "d:btfT:E", ["yosys=", "abc=", "smtbmc=", "suprove=", "aigbmc=", "avy=", "btormc=", - "dumpcfg", "dumptasks"]) + "dumpcfg", "dumptasks", "setup"]) except: usage() @@ -110,12 +115,27 @@ for o, a in opts: dump_cfg = True elif o == "--dumptasks": dump_tasks = True + elif o == "--setup": + setupmode = True else: usage() if len(args) > 0: sbyfile = args[0] - if not sbyfile.endswith(".sby"): + if os.path.isdir(sbyfile): + workdir = sbyfile + sbyfile += "/config.sby" + reusedir = True + if not opt_force and os.path.exists(workdir + "/model"): + print("ERROR: Use -f to re-run in existing directory.", file=sys.stderr) + sys.exit(1) + if len(args) > 1: + print("ERROR: Can't use tasks when running in existing directory.", file=sys.stderr) + sys.exit(1) + if setupmode: + print("ERROR: Can't use --setup with existing directory.", file=sys.stderr) + sys.exit(1) + elif not sbyfile.endswith(".sby"): print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr) sys.exit(1) @@ -278,12 +298,18 @@ def run_job(taskname): early_log(my_workdir, "Moving direcory '%s' to '%s'." % (my_workdir, "%s.bak%03d" % (my_workdir, backup_idx))) shutil.move(my_workdir, "%s.bak%03d" % (my_workdir, backup_idx)) - if opt_force: + if opt_force and not reusedir: early_log(my_workdir, "Removing direcory '%s'." % (my_workdir)) if sbyfile: shutil.rmtree(my_workdir, ignore_errors=True) - os.makedirs(my_workdir) + if reusedir: + pass + elif os.path.isdir(my_workdir): + print("ERROR: Direcory '%s' already exists." % (my_workdir)) + sys.exit(1) + else: + os.makedirs(my_workdir) else: my_opt_tmpdir = True @@ -302,16 +328,16 @@ def run_job(taskname): junit_filename = "junit" sbyconfig, _ = read_sbyconfig(sbydata, taskname) - job = SbyJob(sbyconfig, my_workdir, early_logmsgs) + job = SbyJob(sbyconfig, my_workdir, early_logmsgs, reusedir) for k, v in exe_paths.items(): job.exe_paths[k] = v if throw_err: - job.run() + job.run(setupmode) else: try: - job.run() + job.run(setupmode) except SbyAbort: pass @@ -319,10 +345,13 @@ def run_job(taskname): job.log("Removing direcory '%s'." % (my_workdir)) shutil.rmtree(my_workdir, ignore_errors=True) - job.log("DONE (%s, rc=%d)" % (job.status, job.retcode)) + if setupmode: + job.log("SETUP COMPLETE (rc=%d)" % (job.retcode)) + else: + job.log("DONE (%s, rc=%d)" % (job.status, job.retcode)) job.logfile.close() - if not my_opt_tmpdir: + if not my_opt_tmpdir and not setupmode: with open("%s/%s.xml" % (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 diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index e572f5c..e41fb54 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -18,7 +18,7 @@ import os, re, resource, sys import subprocess, fcntl -from shutil import copyfile +from shutil import copyfile, rmtree from select import select from time import time, localtime @@ -133,7 +133,7 @@ class SbyAbort(BaseException): class SbyJob: - def __init__(self, sbyconfig, workdir, early_logs): + def __init__(self, sbyconfig, workdir, early_logs, reusedir): self.options = dict() self.used_options = set() self.engines = list() @@ -142,6 +142,7 @@ class SbyJob: self.verbatim_files = dict() self.models = dict() self.workdir = workdir + self.reusedir = reusedir self.status = "UNKNOWN" self.total_time = 0 self.expect = [] @@ -166,7 +167,7 @@ class SbyJob: self.summary = list() - self.logfile = open("%s/logfile.txt" % workdir, "w") + self.logfile = open("%s/logfile.txt" % workdir, "a") for line in early_logs: print(line, file=self.logfile) @@ -223,6 +224,11 @@ class SbyJob: print("ERROR: %s" % logmessage, file=f) raise SbyAbort(logmessage) + def makedirs(self, path): + if self.reusedir and os.path.isdir(path): + rmtree(path, ignore_errors=True) + os.makedirs(path) + def copy_src(self): os.makedirs(self.workdir + "/src") @@ -273,7 +279,7 @@ class SbyJob: self.__dict__["opt_" + option_name] = default_value def make_model(self, model_name): - if not os.path.exists("%s/model" % self.workdir): + if not os.path.isdir("%s/model" % self.workdir): os.makedirs("%s/model" % self.workdir) if model_name in ["base", "nomem"]: @@ -411,7 +417,7 @@ class SbyJob: else: assert 0 - def run(self): + def run(self, setupmode): mode = None key = None @@ -536,7 +542,14 @@ class SbyJob: if engine[0] not in ["smtbmc", "btor"]: self.error("Option skip is only valid for smtbmc and btor engines.") - self.copy_src() + if self.reusedir: + rmtree("%s/model" % self.workdir, ignore_errors=True) + else: + self.copy_src() + + if setupmode: + self.retcode = 0 + return if self.opt_mode == "bmc": import sby_mode_bmc diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index c3c55ea..edb9b99 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -29,7 +29,7 @@ def run(job): assert len(engine) > 0 job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - os.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + job.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) if engine[0] == "smtbmc": import sby_engine_smtbmc diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index a4f3597..28c2f4d 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -28,7 +28,7 @@ def run(job): assert len(engine) > 0 job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - os.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + job.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) if engine[0] == "smtbmc": import sby_engine_smtbmc diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index bee065c..3a64ff0 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -29,7 +29,7 @@ def run(job): assert len(engine) > 0 job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - os.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + job.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) if engine[0] == "aiger": import sby_engine_aiger diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index d7742e7..daabe8f 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -36,7 +36,7 @@ def run(job): assert len(engine) > 0 job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - os.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + job.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) if engine[0] == "smtbmc": import sby_engine_smtbmc -- 2.30.2