Add support for (re-)running in existing workdir

Signed-off-by: Clifford Wolf <clifford@clifford.at>

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] [<jobname>.sby [tasknames]]
+sby [options] [<jobname>.sby [tasknames] | <dirname>]
 
     -d <dirname>
         set workdir name. default: <jobname> (without .sby)
@@ -69,13 +71,16 @@ sby [options] [<jobname>.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,11 +298,17 @@ 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)
 
+        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:
@@ -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)
 
+    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

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,8 +542,15 @@ class SbyJob:
                     if engine[0] not in ["smtbmc", "btor"]:
                         self.error("Option skip is only valid for smtbmc and btor engines.")
 
+        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
             sby_mode_bmc.run(self)

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

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

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

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