mirror of
https://github.com/Z3Prover/z3
synced 2026-06-10 19:07:18 +00:00
[code-simplifier] Consolidate repo-root helpers and simplify skill script logic (#9772)
This change simplifies recently touched skill scripts by removing
duplicated repo-root discovery code, promoting shared root lookup to a
public API, and tightening small readability issues without changing
behavior. It keeps script semantics intact while making cross-skill
reuse explicit.
- **Shared API cleanup (`.github/skills/shared/z3db.py`)**
- Promote `_find_repo_root` to public `find_repo_root`.
- Add `require_repo_root()` for scripts that should fail-fast when root
discovery fails.
- Update library usage docstring to expose both helpers.
- Replace adjacent SQL string literals in `log()` with a single literal.
- **Deduplicate memory-safety root lookup
(`.github/skills/memory-safety/scripts/memory_safety.py`)**
- Remove local `find_repo_root()` implementation.
- Import and use shared `require_repo_root()` from `z3db`.
- **Simplify static-analysis label selection
(`.github/skills/static-analysis/scripts/static_analysis.py`)**
- Replace two-step label assignment with a single expression:
- `label = f["type"] or f["category"]`
```python
# before
label = f["category"]
if f["type"]:
label = f["type"]
# after
label = f["type"] or f["category"]
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
parent
c174df4071
commit
0cc04b53eb
3 changed files with 17 additions and 22 deletions
|
|
@ -18,7 +18,7 @@ import time
|
||||||
from pathlib import Path
|
from pathlib import Path
|
||||||
|
|
||||||
sys.path.insert(0, str(Path(__file__).resolve().parent.parent.parent / "shared"))
|
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")
|
logger = logging.getLogger("z3agent")
|
||||||
|
|
||||||
|
|
@ -52,19 +52,6 @@ def check_dependencies():
|
||||||
sys.exit(1)
|
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:
|
def build_is_configured(build_dir: Path, sanitizer: str) -> bool:
|
||||||
"""Check whether the build directory already has a matching cmake config."""
|
"""Check whether the build directory already has a matching cmake config."""
|
||||||
cache = build_dir / "CMakeCache.txt"
|
cache = build_dir / "CMakeCache.txt"
|
||||||
|
|
@ -220,7 +207,7 @@ def main():
|
||||||
|
|
||||||
setup_logging(args.debug)
|
setup_logging(args.debug)
|
||||||
check_dependencies()
|
check_dependencies()
|
||||||
repo_root = find_repo_root()
|
repo_root = require_repo_root()
|
||||||
|
|
||||||
sanitizers = ["asan", "ubsan"] if args.sanitizer == "both" else [args.sanitizer]
|
sanitizers = ["asan", "ubsan"] if args.sanitizer == "both" else [args.sanitizer]
|
||||||
all_findings = []
|
all_findings = []
|
||||||
|
|
|
||||||
18
.github/skills/shared/z3db.py
vendored
18
.github/skills/shared/z3db.py
vendored
|
|
@ -3,7 +3,7 @@
|
||||||
z3db: shared library and CLI for Z3 skill scripts.
|
z3db: shared library and CLI for Z3 skill scripts.
|
||||||
|
|
||||||
Library usage:
|
Library usage:
|
||||||
from z3db import Z3DB, find_z3, run_z3
|
from z3db import Z3DB, find_z3, find_repo_root, require_repo_root, run_z3
|
||||||
|
|
||||||
CLI usage:
|
CLI usage:
|
||||||
python z3db.py init
|
python z3db.py init
|
||||||
|
|
@ -131,7 +131,7 @@ class Z3DB:
|
||||||
"""Write to stderr and to the interaction_log table."""
|
"""Write to stderr and to the interaction_log table."""
|
||||||
getattr(logger, level, logger.info)(message)
|
getattr(logger, level, logger.info)(message)
|
||||||
self.conn.execute(
|
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),
|
(run_id, level, message),
|
||||||
)
|
)
|
||||||
self.conn.commit()
|
self.conn.commit()
|
||||||
|
|
@ -182,7 +182,7 @@ def find_z3(hint: str = None) -> str:
|
||||||
if hint:
|
if hint:
|
||||||
candidates.append(hint)
|
candidates.append(hint)
|
||||||
|
|
||||||
repo_root = _find_repo_root()
|
repo_root = find_repo_root()
|
||||||
if repo_root:
|
if repo_root:
|
||||||
for build_dir in ["build", "build/release", "build/debug"]:
|
for build_dir in ["build", "build/release", "build/debug"]:
|
||||||
candidates.append(str(repo_root / build_dir / "z3"))
|
candidates.append(str(repo_root / build_dir / "z3"))
|
||||||
|
|
@ -201,7 +201,8 @@ def find_z3(hint: str = None) -> str:
|
||||||
sys.exit(1)
|
sys.exit(1)
|
||||||
|
|
||||||
|
|
||||||
def _find_repo_root() -> Optional[Path]:
|
def find_repo_root() -> Optional[Path]:
|
||||||
|
"""Best-effort search for the Z3 repository root from the current directory."""
|
||||||
d = Path.cwd()
|
d = Path.cwd()
|
||||||
for _ in range(10):
|
for _ in range(10):
|
||||||
if (d / "CMakeLists.txt").exists() and (d / "src").is_dir():
|
if (d / "CMakeLists.txt").exists() and (d / "src").is_dir():
|
||||||
|
|
@ -213,6 +214,15 @@ def _find_repo_root() -> Optional[Path]:
|
||||||
return None
|
return None
|
||||||
|
|
||||||
|
|
||||||
|
def require_repo_root() -> Path:
|
||||||
|
"""Return the Z3 repository root or exit the process if it is not found."""
|
||||||
|
repo_root = find_repo_root()
|
||||||
|
if repo_root is None:
|
||||||
|
logger.error("could not locate Z3 repository root")
|
||||||
|
sys.exit(1)
|
||||||
|
return repo_root
|
||||||
|
|
||||||
|
|
||||||
def run_z3(
|
def run_z3(
|
||||||
formula: str,
|
formula: str,
|
||||||
z3_bin: str = None,
|
z3_bin: str = None,
|
||||||
|
|
|
||||||
|
|
@ -176,9 +176,7 @@ def print_findings(findings: list):
|
||||||
return
|
return
|
||||||
|
|
||||||
for f in findings:
|
for f in findings:
|
||||||
label = f["category"]
|
label = f["type"] or f["category"]
|
||||||
if f["type"]:
|
|
||||||
label = f["type"]
|
|
||||||
print(f"[{label}] {f['file']}:{f['line']}: {f['description']}")
|
print(f"[{label}] {f['file']}:{f['line']}: {f['description']}")
|
||||||
|
|
||||||
print()
|
print()
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue