From 52184e5bf0e02b879d39e5f891bd6c45810abefb Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 19 Feb 2024 21:06:26 +0100 Subject: [PATCH] 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 | 45 +++++ sbysrc/sby_autotune.py | 1 + sbysrc/sby_cmdline.py | 5 + sbysrc/sby_core.py | 54 +++++- sbysrc/sby_design.py | 7 + sbysrc/sby_engine_smtbmc.py | 5 + sbysrc/sby_status.py | 344 ++++++++++++++++++++++++++++++++++++ tests/make/collect_tests.py | 6 +- 8 files changed, 462 insertions(+), 5 deletions(-) create mode 100644 sbysrc/sby_status.py diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 986fb9d..99dcc6c 100644 --- a/sbysrc/sby.py +++ b/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" diff --git a/sbysrc/sby_autotune.py b/sbysrc/sby_autotune.py index 1d6f102..b861890 100644 --- a/sbysrc/sby_autotune.py +++ b/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: diff --git a/sbysrc/sby_cmdline.py b/sbysrc/sby_cmdline.py index a75c273..bc45b4a 100644 --- a/sbysrc/sby_cmdline.py +++ b/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=".sby | ", nargs="?", diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index d59ffa1..ecbd081 100644 --- a/sbysrc/sby_core.py +++ b/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()) diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index df2977f..d93d17d 100644 --- a/sbysrc/sby_design.py +++ b/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): diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 7e15589..3b43113 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/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) diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py new file mode 100644 index 0000000..e4722c3 --- /dev/null +++ b/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"" + else: + path_based = f"" + else: + path_based = f"" + 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)) diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py index 2aeccee..636ecb6 100644 --- a/tests/make/collect_tests.py +++ b/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)