3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00

simplify skill scripts: expose find_repo_root, fix split string, simplify label

- z3db.py: rename _find_repo_root to find_repo_root (make public) and
  add require_repo_root helper that exits on failure; update docstring
  and internal caller; fix unnecessary string literal split in log()
- memory_safety.py: remove 13-line duplicate find_repo_root function;
  import and use require_repo_root from z3db instead
- static_analysis.py: simplify two-line label assignment in
  print_findings to a single expression using 'or'

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
github-actions[bot] 2026-06-08 05:59:22 +00:00 committed by GitHub
parent 59bb444694
commit 4dec7b1324
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 17 additions and 22 deletions

View file

@ -18,7 +18,7 @@ import time
from pathlib import Path
sys.path.insert(0, str(Path(__file__).resolve().parent.parent.parent / "shared"))
from z3db import Z3DB, setup_logging
from z3db import Z3DB, require_repo_root, setup_logging
logger = logging.getLogger("z3agent")
@ -52,19 +52,6 @@ def check_dependencies():
sys.exit(1)
def find_repo_root() -> Path:
d = Path.cwd()
for _ in range(10):
if (d / "CMakeLists.txt").exists() and (d / "src").is_dir():
return d
parent = d.parent
if parent == d:
break
d = parent
logger.error("could not locate Z3 repository root")
sys.exit(1)
def build_is_configured(build_dir: Path, sanitizer: str) -> bool:
"""Check whether the build directory already has a matching cmake config."""
cache = build_dir / "CMakeCache.txt"
@ -220,7 +207,7 @@ def main():
setup_logging(args.debug)
check_dependencies()
repo_root = find_repo_root()
repo_root = require_repo_root()
sanitizers = ["asan", "ubsan"] if args.sanitizer == "both" else [args.sanitizer]
all_findings = []

View file

@ -3,7 +3,7 @@
z3db: shared library and CLI for Z3 skill scripts.
Library usage:
from z3db import Z3DB, find_z3, run_z3
from z3db import Z3DB, find_z3, run_z3, find_repo_root, require_repo_root
CLI usage:
python z3db.py init
@ -131,7 +131,7 @@ class Z3DB:
"""Write to stderr and to the interaction_log table."""
getattr(logger, level, logger.info)(message)
self.conn.execute(
"INSERT INTO interaction_log (run_id, level, message) " "VALUES (?, ?, ?)",
"INSERT INTO interaction_log (run_id, level, message) VALUES (?, ?, ?)",
(run_id, level, message),
)
self.conn.commit()
@ -182,7 +182,7 @@ def find_z3(hint: str = None) -> str:
if hint:
candidates.append(hint)
repo_root = _find_repo_root()
repo_root = find_repo_root()
if repo_root:
for build_dir in ["build", "build/release", "build/debug"]:
candidates.append(str(repo_root / build_dir / "z3"))
@ -201,7 +201,8 @@ def find_z3(hint: str = None) -> str:
sys.exit(1)
def _find_repo_root() -> Optional[Path]:
def find_repo_root() -> Optional[Path]:
"""Walk up from cwd looking for the Z3 repository root."""
d = Path.cwd()
for _ in range(10):
if (d / "CMakeLists.txt").exists() and (d / "src").is_dir():
@ -213,6 +214,15 @@ def _find_repo_root() -> Optional[Path]:
return None
def require_repo_root() -> Path:
"""Return the Z3 repo root, or exit with an error message if not found."""
root = find_repo_root()
if root is None:
logger.error("could not locate Z3 repository root")
sys.exit(1)
return root
def run_z3(
formula: str,
z3_bin: str = None,

View file

@ -176,9 +176,7 @@ def print_findings(findings: list):
return
for f in findings:
label = f["category"]
if f["type"]:
label = f["type"]
label = f["type"] or f["category"]
print(f"[{label}] {f['file']}:{f['line']}: {f['description']}")
print()