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.

sbysrc/sby.py

@@ -22,6 +22,7 @@ import json, os, sys, shutil, tempfile, re
 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 @@ autotune_config = args.autotune_config
 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 @@ class SbyAutotune:
 
     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 shutil import copyfile, copytree, rmtree
 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 @@ class SbySummary:
             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 @@ class SbyTask(SbyConfig):
                 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 @@ class SbyTask(SbyConfig):
         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 @@ class SbyTask(SbyConfig):
             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 @@ class SbyTask(SbyConfig):
 
         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 @@ class SbyTask(SbyConfig):
             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 @@ class SbyProperty:
                 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 run(mode, task, engine_idx, engine):
             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 run(mode, task, engine_idx, engine):
             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 run(mode, task, engine_idx, engine):
             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 run(mode, task, engine_idx, engine):
     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)
 

sbysrc/sby_status.py

@@ -0,0 +1,344 @@
+from __future__ import annotations
+
+import sqlite3
+import os
+import time
+import json
+from collections import defaultdict
+from functools import wraps
+from pathlib import Path
+from typing import Any, Callable, TypeVar, Optional, Iterable
+from sby_design import SbyProperty, pretty_path
+
+
+Fn = TypeVar("Fn", bound=Callable[..., Any])
+
+
+def transaction(method: Fn) -> Fn:
+    @wraps(method)
+    def wrapper(self: SbyStatusDb, *args: Any, **kwargs: Any) -> Any:
+        if self._transaction_active:
+            return method(self, *args, **kwargs)
+
+        try:
+            self.log_debug(f"begin {method.__name__!r} transaction")
+            self.db.execute("begin")
+            self._transaction_active = True
+            result = method(self, *args, **kwargs)
+            self.db.execute("commit")
+            self._transaction_active = False
+            self.log_debug(f"comitted {method.__name__!r} transaction")
+            return result
+        except sqlite3.OperationalError as err:
+            self.log_debug(f"failed {method.__name__!r} transaction {err}")
+            self.db.rollback()
+            self._transaction_active = False
+        except Exception as err:
+            self.log_debug(f"failed {method.__name__!r} transaction {err}")
+            self.db.rollback()
+            self._transaction_active = False
+            raise
+        try:
+            self.log_debug(
+                f"retrying {method.__name__!r} transaction once in immediate mode"
+            )
+            self.db.execute("begin immediate")
+            self._transaction_active = True
+            result = method(self, *args, **kwargs)
+            self.db.execute("commit")
+            self._transaction_active = False
+            self.log_debug(f"comitted {method.__name__!r} transaction")
+            return result
+        except Exception as err:
+            self.log_debug(f"failed {method.__name__!r} transaction {err}")
+            self.db.rollback()
+            self._transaction_active = False
+            raise
+
+    return wrapper  # type: ignore
+
+
+class SbyStatusDb:
+    def __init__(self, path: Path, task, timeout: float = 5.0):
+        self.debug = False
+        self.task = task
+        self._transaction_active = False
+
+        setup = not os.path.exists(path)
+
+        self.db = sqlite3.connect(path, isolation_level=None, timeout=timeout)
+        self.db.row_factory = sqlite3.Row
+        self.db.execute("PRAGMA journal_mode=WAL")
+        self.db.execute("PRAGMA synchronous=0")
+
+        if setup:
+            self._setup()
+
+        if task is not None:
+            self.task_id = self.create_task(workdir=task.workdir, mode=task.opt_mode)
+
+    def log_debug(self, *args):
+        if self.debug:
+            if self.task:
+                self.task.log(" ".join(str(arg) for arg in args))
+            else:
+                print(*args)
+
+    @transaction
+    def _setup(self):
+        script = """
+                CREATE TABLE task (
+                    id INTEGER PRIMARY KEY,
+                    workdir TEXT,
+                    mode TEXT,
+                    created REAL
+                );
+                CREATE TABLE task_status (
+                    id INTEGER PRIMARY KEY,
+                    task INTEGER,
+                    status TEXT,
+                    data TEXT,
+                    created REAL,
+                    FOREIGN KEY(task) REFERENCES task(id)
+                );
+                CREATE TABLE task_property (
+                    id INTEGER PRIMARY KEY,
+                    task INTEGER,
+                    src TEXT,
+                    name TEXT,
+                    created REAL,
+                    FOREIGN KEY(task) REFERENCES task(id)
+                );
+                CREATE TABLE task_property_status (
+                    id INTEGER PRIMARY KEY,
+                    task_property INTEGER,
+                    status TEXT,
+                    data TEXT,
+                    created REAL,
+                    FOREIGN KEY(task_property) REFERENCES task_property(id)
+                );
+                CREATE TABLE task_property_data (
+                    id INTEGER PRIMARY KEY,
+                    task_property INTEGER,
+                    kind TEXT,
+                    data TEXT,
+                    created REAL,
+                    FOREIGN KEY(task_property) REFERENCES task_property(id)
+                );
+            """
+        for statement in script.split(";\n"):
+            statement = statement.strip()
+            if statement:
+                self.db.execute(statement)
+
+    @transaction
+    def create_task(self, workdir: str, mode: str) -> int:
+        return self.db.execute(
+            """
+                INSERT INTO task (workdir, mode, created)
+                VALUES (:workdir, :mode, :now)
+            """,
+            dict(workdir=workdir, mode=mode, now=time.time()),
+        ).lastrowid
+
+    @transaction
+    def create_task_properties(
+        self, properties: Iterable[SbyProperty], *, task_id: Optional[int] = None
+    ):
+        if task_id is None:
+            task_id = self.task_id
+        now = time.time()
+        self.db.executemany(
+            """
+                INSERT INTO task_property (name, src, task, created)
+                VALUES (:name, :src, :task, :now)
+            """,
+            [
+                dict(
+                    name=json.dumps(prop.path),
+                    src=prop.location or "",
+                    task=task_id,
+                    now=now,
+                )
+                for prop in properties
+            ],
+        )
+
+    @transaction
+    def set_task_status(
+        self,
+        status: Optional[str] = None,
+        data: Any = None,
+    ):
+        if status is None:
+            status = property.status
+
+        now = time.time()
+        self.db.execute(
+            """
+                INSERT INTO task_status (
+                    task, status, data, created
+                )
+                VALUES (
+                    :task, :status, :data, :now
+                )
+            """,
+            dict(
+                task=self.task_id,
+                status=status,
+                data=json.dumps(data),
+                now=now,
+            ),
+        )
+
+    @transaction
+    def set_task_property_status(
+        self,
+        property: SbyProperty,
+        status: Optional[str] = None,
+        data: Any = None,
+    ):
+        if status is None:
+            status = property.status
+
+        now = time.time()
+        self.db.execute(
+            """
+                INSERT INTO task_property_status (
+                    task_property, status, data, created
+                )
+                VALUES (
+                    (SELECT id FROM task_property WHERE task = :task AND name = :name),
+                    :status, :data, :now
+                )
+            """,
+            dict(
+                task=self.task_id,
+                name=json.dumps(property.path),
+                status=status,
+                data=json.dumps(data),
+                now=now,
+            ),
+        )
+
+    @transaction
+    def add_task_property_data(self, property: SbyProperty, kind: str, data: Any):
+        now = time.time()
+        self.db.execute(
+            """
+                INSERT INTO task_property_data (
+                    task_property, kind, data, created
+                )
+                VALUES (
+                    (SELECT id FROM task_property WHERE task = :task AND name = :name),
+                    :kind, :data, :now
+                )
+            """,
+            dict(
+                task=self.task_id,
+                name=json.dumps(property.path),
+                kind=kind,
+                data=json.dumps(data),
+                now=now,
+            ),
+        )
+
+    @transaction
+    def all_tasks(self):
+        rows = self.db.execute(
+            """
+                SELECT id, workdir, created FROM task
+            """
+        ).fetchall()
+
+        return {row["id"]: dict(row) for row in rows}
+
+    @transaction
+    def all_task_properties(self):
+        rows = self.db.execute(
+            """
+                SELECT id, task, src, name, created FROM task_property
+            """
+        ).fetchall()
+
+        def get_result(row):
+            row = dict(row)
+            row["name"] = tuple(json.loads(row.get("name", "[]")))
+            row["data"] = json.loads(row.get("data", "null"))
+            return row
+
+        return {row["id"]: get_result(row) for row in rows}
+
+    @transaction
+    def all_task_property_statuses(self):
+        rows = self.db.execute(
+            """
+                SELECT id, task_property, status, data, created
+                FROM task_property_status
+            """
+        ).fetchall()
+
+        def get_result(row):
+            row = dict(row)
+            row["data"] = json.loads(row.get("data", "null"))
+            return row
+
+        return {row["id"]: get_result(row) for row in rows}
+
+    @transaction
+    def all_status_data(self):
+        return (
+            self.all_tasks(),
+            self.all_task_properties(),
+            self.all_task_property_statuses(),
+        )
+
+    @transaction
+    def reset(self):
+        self.db.execute("""DELETE FROM task_property_status""")
+        self.db.execute("""DELETE FROM task_property_data""")
+        self.db.execute("""DELETE FROM task_property""")
+        self.db.execute("""DELETE FROM task_status""")
+        self.db.execute("""DELETE FROM task""")
+
+    def print_status_summary(self):
+        tasks, task_properties, task_property_statuses = self.all_status_data()
+        properties = defaultdict(set)
+
+        uniquify_paths = defaultdict(dict)
+
+        def add_status(task_property, status):
+
+            display_name = task_property["name"]
+            if display_name[-1].startswith("$"):
+                counters = uniquify_paths[task_property["src"]]
+                counter = counters.setdefault(display_name[-1], len(counters) + 1)
+                if task_property["src"]:
+                    if counter < 2:
+                        path_based = f"<unnamed at {task_property['src']}>"
+                    else:
+                        path_based = f"<unnamed #{counter} at {task_property['src']}>"
+                else:
+                    path_based = f"<unnamed #{counter}>"
+                display_name = (*display_name[:-1], path_based)
+
+            properties[display_name].add(status)
+
+        for task_property in task_properties.values():
+            add_status(task_property, "UNKNOWN")
+
+        for status in task_property_statuses.values():
+            task_property = task_properties[status["task_property"]]
+            add_status(task_property, status["status"])
+
+        for display_name, statuses in sorted(properties.items()):
+            print(pretty_path(display_name), combine_statuses(statuses))
+
+
+def combine_statuses(statuses):
+    statuses = set(statuses)
+
+    if len(statuses) > 1:
+        statuses.discard("UNKNOWN")
+
+    return ",".join(sorted(statuses))

tests/make/collect_tests.py

@@ -9,7 +9,11 @@ SAFE_PATH = re.compile(r"^[a-zA-Z0-9_./\\]*$")
 
 def collect(path):
     # don't pick up any paths that need escaping nor any sby workdirs
-    if not SAFE_PATH.match(str(path)) or (path / "config.sby").exists():
+    if (
+        not SAFE_PATH.match(str(path))
+        or (path / "config.sby").exists()
+        or (path / "status.sqlite").exists()
+    ):
         return
 
     checked_dirs.append(path)