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)