Initial support for a multi-task property status database

This adds initial support for an sqlite database that is shared across
multiple tasks of a single SBY file and that can track the status of
individual properties.

The amount of information tracked in the database is currently quite
minimal and depends on the engine and options used. This can be
incrementally extended in the future.

The ways in which the information in the database can be queries is even
more limited for this initial version, consisting of a single '--status'
option which lists all properties and their status.

Author: jix

sbysrc/sby.py

@@ -22,6 +22,7 @@
 from sby_cmdline import parser_func
 from sby_core import SbyConfig, SbyTask, SbyAbort, SbyTaskloop, process_filename, dress_message
 from sby_jobserver import SbyJobClient, process_jobserver_environment
+from sby_status import SbyStatusDb
 import time, platform, click
 
 process_jobserver_environment()  # needs to be called early
@@ -55,6 +56,39 @@
 sequential = args.sequential
 jobcount = args.jobcount
 init_config_file = args.init_config_file
+status_show = args.status
+status_reset = args.status_reset
+
+if status_show or status_reset:
+    target = workdir_prefix or workdir or sbyfile
+    if not os.path.isdir(target) and target.endswith('.sby'):
+        target = target[:-4]
+    if not os.path.isdir(target):
+        print(f"ERROR: No directory found at {target!r}.", file=sys.stderr)
+        sys.exit(1)
+
+    try:
+        with open(f"{target}/status.path", "r") as status_path_file:
+            status_path = f"{target}/{status_path_file.read().rstrip()}"
+    except FileNotFoundError:
+        status_path = f"{target}/status.sqlite"
+
+    if not os.path.exists(status_path):
+        print(f"ERROR: No status database found at {status_path!r}.", file=sys.stderr)
+        sys.exit(1)
+
+    status_db = SbyStatusDb(status_path, task=None)
+
+    if status_show:
+        status_db.print_status_summary()
+        sys.exit(0)
+
+    if status_reset:
+        status_db.reset()
+
+    status_db.db.close()
+    sys.exit(0)
+
 
 if sbyfile is not None:
     if os.path.isdir(sbyfile):
@@ -356,6 +390,7 @@ def start_task(taskloop, taskname):
 
     my_opt_tmpdir = opt_tmpdir
     my_workdir = None
+    my_status_db = None
 
     if workdir is not None:
         my_workdir = workdir
@@ -364,10 +399,12 @@ def start_task(taskloop, taskname):
             my_workdir = workdir_prefix
         else:
             my_workdir = workdir_prefix + "_" + taskname
+            my_status_db = f"../{os.path.basename(workdir_prefix)}/status.sqlite"
 
     if my_workdir is None and sbyfile is not None and not my_opt_tmpdir:
         my_workdir = sbyfile[:-4]
         if taskname is not None:
+            my_status_db = f"../{os.path.basename(my_workdir)}/status.sqlite"
             my_workdir += "_" + taskname
 
     if my_workdir is not None:
@@ -399,6 +436,14 @@ def start_task(taskloop, taskname):
         with open(f"{my_workdir}/.gitignore", "w") as gitignore:
             print("*", file=gitignore)
 
+    if my_status_db is not None:
+        os.makedirs(f"{my_workdir}/{os.path.dirname(my_status_db)}", exist_ok=True)
+        if os.getenv("SBY_WORKDIR_GITIGNORE"):
+            with open(f"{my_workdir}/{os.path.dirname(my_status_db)}/.gitignore", "w") as gitignore:
+                print("*", file=gitignore)
+        with open(f"{my_workdir}/status.path", "w") as status_path:
+            print(my_status_db, file=status_path)
+
     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"
 

sbysrc/sby_autotune.py

@@ -378,6 +378,7 @@ def log(self, message):
 
     def run(self):
         self.task.handle_non_engine_options()
+        self.task.setup_status_db(':memory:')
         self.config = self.task.autotune_config or SbyAutotuneConfig()
 
         if "expect" not in self.task.options:

sbysrc/sby_cmdline.py

@@ -69,6 +69,11 @@ def parser_func():
     parser.add_argument("--setup", action="store_true", dest="setupmode",
             help="set up the working directory and exit")
 
+    parser.add_argument("--status", action="store_true", dest="status",
+            help="summarize the contents of the status database")
+    parser.add_argument("--statusreset", action="store_true", dest="status_reset",
+            help="reset the contents of the status database")
+
     parser.add_argument("--init-config-file", dest="init_config_file",
             help="create a default .sby config file")
     parser.add_argument("sbyfile", metavar="<jobname>.sby | <dirname>", nargs="?",

sbysrc/sby_core.py

@@ -27,6 +27,7 @@
 from select import select
 from time import monotonic, localtime, sleep, strftime
 from sby_design import SbyProperty, SbyModule, design_hierarchy
+from sby_status import SbyStatusDb
 
 all_procs_running = []
 
@@ -674,20 +675,41 @@ def engine_summary(self, engine_idx):
             self.engine_summaries[engine_idx] = SbyEngineSummary(engine_idx)
         return self.engine_summaries[engine_idx]
 
-    def add_event(self, *args, **kwargs):
+    def add_event(self, *args, update_status=True, **kwargs):
         event = SbySummaryEvent(*args, **kwargs)
+
+        engine = self.engine_summary(event.engine_idx)
+
+        if update_status:
+            status_metadata = dict(source="summary_event", engine=engine.engine)
+
         if event.prop:
             if event.type == "$assert":
                 event.prop.status = "FAIL"
                 if event.path:
                     event.prop.tracefiles.append(event.path)
+                    if update_status:
+                        self.task.status_db.add_task_property_data(
+                            event.prop,
+                            "trace",
+                            data=dict(path=event.path, step=event.step, **status_metadata),
+                        )
         if event.prop:
             if event.type == "$cover":
                 event.prop.status = "PASS"
                 if event.path:
                     event.prop.tracefiles.append(event.path)
-
-        engine = self.engine_summary(event.engine_idx)
+                    if update_status:
+                        self.task.status_db.add_task_property_data(
+                            event.prop,
+                            "trace",
+                            data=dict(path=event.path, step=event.step, **status_metadata),
+                        )
+        if event.prop and update_status:
+            self.task.status_db.set_task_property_status(
+                event.prop,
+                data=status_metadata
+            )
 
         if event.trace not in engine.traces:
             engine.traces[event.trace] = SbyTraceSummary(event.trace, path=event.path, engine_case=event.engine_case)
@@ -1041,6 +1063,10 @@ def instance_hierarchy_callback(retcode):
                 if self.design == None:
                     with open(f"{self.workdir}/model/design.json") as f:
                         self.design = design_hierarchy(f)
+                        self.status_db.create_task_properties([
+                            prop for prop in self.design.properties_by_path.values()
+                            if not prop.type.assume_like
+                        ])
 
             def instance_hierarchy_error_callback(retcode):
                 self.precise_prop_status = False
@@ -1186,8 +1212,13 @@ def proc_failed(self, proc):
         self.status = "ERROR"
         self.terminate()
 
+    def pass_unknown_asserts(self, data):
+        for prop in self.design.pass_unknown_asserts():
+            self.status_db.set_task_property_status(prop, data=data)
+
     def update_status(self, new_status):
         assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
+        self.status_db.set_task_status(new_status)
 
         if new_status == "UNKNOWN":
             return
@@ -1199,7 +1230,7 @@ def update_status(self, new_status):
             assert self.status != "FAIL"
             self.status = "PASS"
             if self.opt_mode in ("bmc", "prove") and self.design:
-                self.design.pass_unknown_asserts()
+                self.pass_unknown_asserts(dict(source="task_status"))
 
         elif new_status == "FAIL":
             assert self.status != "PASS"
@@ -1258,6 +1289,19 @@ def handle_non_engine_options(self):
 
         self.handle_bool_option("assume_early", True)
 
+    def setup_status_db(self, status_path=None):
+        if hasattr(self, 'status_db'):
+            return
+
+        if status_path is None:
+            try:
+                with open(f"{self.workdir}/status.path", "r") as status_path_file:
+                    status_path = f"{self.workdir}/{status_path_file.read().rstrip()}"
+            except FileNotFoundError:
+                status_path = f"{self.workdir}/status.sqlite"
+
+        self.status_db = SbyStatusDb(status_path, self)
+
     def setup_procs(self, setupmode):
         self.handle_non_engine_options()
         if self.opt_smtc is not None:
@@ -1285,6 +1329,8 @@ def setup_procs(self, setupmode):
             self.retcode = 0
             return
 
+        self.setup_status_db()
+
         if self.opt_make_model is not None:
             for name in self.opt_make_model.split(","):
                 self.model(name.strip())

sbysrc/sby_design.py

@@ -88,6 +88,10 @@ def from_flavor(c, name):
                 return c.FAIR
             raise ValueError("Unknown property type: " + name)
 
+        @property
+        def assume_like(self):
+            return self in [self.ASSUME, self.FAIR]
+
     name: str
     path: Tuple[str, ...]
     type: Type
@@ -171,9 +175,12 @@ class SbyDesign:
     properties_by_path: dict = field(default_factory=dict)
 
     def pass_unknown_asserts(self):
+        updated = []
         for prop in self.hierarchy:
             if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
                 prop.status = "PASS"
+                updated.append(prop)
+        return updated
 
 
 def cell_path(cell):

sbysrc/sby_engine_smtbmc.py

@@ -233,6 +233,7 @@ def output_callback(line):
             cell_name = match[3] or match[2]
             prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
+            task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))
             last_prop.append(prop)
             return line
 
@@ -241,6 +242,7 @@ def output_callback(line):
             cell_name = match[2] or match[1]
             prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "PASS"
+            task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))
             last_prop.append(prop)
             return line
 
@@ -271,6 +273,7 @@ def output_callback(line):
             cell_name = match[2]
             prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
             prop.status = "FAIL"
+            task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))
 
         return line
 
@@ -288,6 +291,8 @@ def exit_callback(retcode):
     def last_exit_callback():
         if mode == "bmc" or mode == "cover":
             task.update_status(proc_status)
+            if proc_status == "FAIL" and mode == "bmc" and keep_going:
+                task.pass_unknown_asserts(dict(source="smtbmc", keep_going=True, engine=f"engine_{engine_idx}"))
             proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status
             task.summary.set_engine_status(engine_idx, proc_status_lower)