3f1234f7bb
Clang LibTooling + Z3 BV-64 encoding. 11 detectors: clone, equiv, class-dup, dead, null-deref, div-by-zero, int-overflow, oob, int-truncation, sign-conversion, taint-track. Interfaces: CLI, MCP (JSON-RPC 2.0), LSP. Output: SARIF 2.1.0, JSON, Markdown.
62 lines
1.6 KiB
Python
62 lines
1.6 KiB
Python
#!/usr/bin/env python3
|
|
|
|
import argparse
|
|
import json
|
|
import subprocess
|
|
import sys
|
|
from pathlib import Path
|
|
|
|
|
|
def run_fold(fold_bin: Path, compile_db: str, source: str) -> subprocess.CompletedProcess[str]:
|
|
return subprocess.run(
|
|
[
|
|
str(fold_bin),
|
|
"scan",
|
|
"--compile-db",
|
|
compile_db,
|
|
"--format",
|
|
"json",
|
|
source,
|
|
],
|
|
check=False,
|
|
capture_output=True,
|
|
text=True,
|
|
)
|
|
|
|
|
|
def main() -> int:
|
|
parser = argparse.ArgumentParser(
|
|
description="Prototype loop invariant demo for fold's fixedpoint API"
|
|
)
|
|
parser.add_argument("source", help="Source file containing the loop under test")
|
|
parser.add_argument("--compile-db", required=True, help="Path to compile_commands.json")
|
|
parser.add_argument(
|
|
"--fold-bin",
|
|
default="build/release/fold",
|
|
help="Path to the fold executable (default: build/release/fold)",
|
|
)
|
|
args = parser.parse_args()
|
|
|
|
fold_bin = Path(args.fold_bin)
|
|
result = run_fold(fold_bin, args.compile_db, args.source)
|
|
print(f"fold exit code: {result.returncode}")
|
|
|
|
findings = []
|
|
if result.stdout.strip():
|
|
try:
|
|
payload = json.loads(result.stdout)
|
|
findings = payload.get("runs", [{}])[0].get("results", [])
|
|
except json.JSONDecodeError:
|
|
pass
|
|
|
|
print(f"scan findings reported: {len(findings)}")
|
|
if result.stderr.strip():
|
|
print("fold stderr:")
|
|
print(result.stderr.strip())
|
|
|
|
print("loop invariant inference: prototype wired, no invariant extracted yet")
|
|
return 0
|
|
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(main())
|