e30764fb19
Add negative_cases_from_universe to expand an explicit file-by-rule universe into labeled negatives (enabling TP/FP/TN/FN, not just TP/FP), plus project-eval harness updates in run_project_eval and the score/score_fp/quality-gate helpers.
235 lines
9.4 KiB
Python
235 lines
9.4 KiB
Python
#!/usr/bin/env python3
|
|
"""Build Fold gate gold from the locally available SV-COMP corpus.
|
|
|
|
SV-COMP (Software Verification Competition) ships per-file `.yml` specs:
|
|
|
|
properties:
|
|
- property_file: ../properties/valid-memsafety.prp
|
|
expected_verdict: false
|
|
subproperty: valid-deref
|
|
|
|
Maps directly to Fold detectors:
|
|
valid-deref -> null-deref (dereference of invalid/NULL pointer)
|
|
valid-free -> use-after-free / double-free
|
|
valid-memtrack -> memory-leak (fold.memory-leak / memtrack family)
|
|
|
|
Emits bench/gold/svcomp-<category>.json in the SAME format as
|
|
bench/gold/juliet-*.json (used by score_fp.load_gold):
|
|
{"name": ..., "description": ..., "expected": [{"kind": <kind>, "files": [...], "id": ...}]}
|
|
|
|
Usage:
|
|
python3 scripts/benchmarks/build_svcomp_gold.py \
|
|
--corpus bench/corpora/svcomp/sv-benchmarks/c \
|
|
--categories memsafety,array-memsafety,array-memsafety-realloc \
|
|
--out bench/gold
|
|
"""
|
|
|
|
import argparse
|
|
import json
|
|
import re
|
|
import sys
|
|
from pathlib import Path
|
|
|
|
SUBPROPERTY_KIND = {
|
|
"valid-deref": "null-deref",
|
|
"valid-free": "use-after-free",
|
|
"valid-memtrack": "memory-leak",
|
|
"no-overflow": "int-overflow",
|
|
"valid-memcleanup": "memory-leak",
|
|
}
|
|
|
|
# A bug file (expected_verdict: false) for one memory-safety subproperty may
|
|
# legitimately exhibit other memory-safety flaws: e.g. cmp-freed-ptr.c
|
|
# (valid-free: double-free) also leaks `x` when the allocator returns distinct
|
|
# addresses, and Fold's memory-leak finding on it is a correct leak report, not
|
|
# a false positive. Map such files into the sibling memory-safety gold kinds so
|
|
# a correct leak/uaf/deref finding is scored as TP rather than FP (SV-COMP
|
|
# properties are per-file, not per-kind).
|
|
# A valid-free (double-free) bug file may also contain a real leak: SV-COMP
|
|
# properties are per-file, not per-kind, so a leak finding on such a file is a
|
|
# TP for memory-leak. Restored (iter-437); the escape gates (iters 441-442)
|
|
# correctly suppress escape-driven findings, so only REAL leaks (cmp-freed-ptr:
|
|
# local x) count as TPs and escape cases register as honest FNs.
|
|
SIBLING_KIND_EXTENSION = {
|
|
"valid-free": ("memory-leak",), # a double-free file may also leak
|
|
"valid-memtrack": (), # leak files: no sibling needed
|
|
"valid-deref": (),
|
|
}
|
|
|
|
|
|
def parse_yml(spec: Path) -> dict | None:
|
|
"""Extract {subproperty, expected_verdict} from an SV-COMP .yml spec."""
|
|
try:
|
|
text = spec.read_text(encoding="utf-8", errors="replace")
|
|
except OSError:
|
|
return None
|
|
sub = None
|
|
verdict = None
|
|
for line in text.splitlines():
|
|
line = line.strip()
|
|
m = re.match(r"subproperty:\s*(\S+)", line)
|
|
if m:
|
|
sub = m.group(1)
|
|
continue
|
|
m = re.match(r"-?\s*property_file:\s*(\S+)", line)
|
|
if m and "no-overflow" in m.group(1):
|
|
sub = "no-overflow"
|
|
continue
|
|
m = re.match(r"expected_verdict:\s*(\S+)", line)
|
|
if m:
|
|
verdict = m.group(1) in ("true",)
|
|
continue
|
|
if sub is None or verdict is None:
|
|
return None
|
|
return {"subproperty": sub, "expected_verdict": verdict}
|
|
|
|
def parse_yml_lenient(spec: Path) -> dict | None:
|
|
"""Like parse_yml but defaults the subproperty for valid-memsafety files
|
|
that omit it (SV-COMP Juliet_Test CWE-690 etc.): the filename CWE is the
|
|
authoritative bug class in the Juliet_Test corpus."""
|
|
parsed = parse_yml(spec)
|
|
if parsed is not None:
|
|
return parsed
|
|
try:
|
|
text = spec.read_text(encoding="utf-8", errors="replace")
|
|
except OSError:
|
|
return None
|
|
verdict = None
|
|
has_memsafety = False
|
|
for line in text.splitlines():
|
|
line = line.strip()
|
|
m = re.match(r"-?\s*property_file:\s*(\S+)", line)
|
|
if m and "valid-memsafety" in m.group(1):
|
|
has_memsafety = True
|
|
m = re.match(r"expected_verdict:\s*(\S+)", line)
|
|
if m:
|
|
verdict = m.group(1) in ("true",)
|
|
if has_memsafety and verdict is not None:
|
|
return {"subproperty": "valid-deref", "expected_verdict": verdict}
|
|
return None
|
|
|
|
|
|
# array-memsafety's no-overflow subset is scored under the dedicated
|
|
# signedintegeroverflow-regression corpus; mapping no-overflow to int-overflow
|
|
# here too creates cross-kind leakage (int-overflow findings on null-deref-gold
|
|
# array-bounds code inflate the FP pool). Keep array-memsafety null-deref-only.
|
|
CATEGORY_KIND_FILTER: dict[str, set[str]] = {
|
|
"array-memsafety": {"null-deref"},
|
|
}
|
|
|
|
# CWE-590 (Use of Stack Memory Out of Scope) is NOT a null-deref: the bug is
|
|
# reading a stack pointer past its scope (data = &dataBuffer), never NULL. The
|
|
# valid-deref property over-broadly maps it to null-deref gold, but Fold's
|
|
# null-deref detector either misses the out-of-scope read (real FN) or flags
|
|
# unrelated derefs in the preprocessed support code (wrong-location TP).
|
|
# Exclude CWE-590 from the null-deref gold for an honest measurement.
|
|
GOLD_FILENAME_EXCLUDE: dict[str, tuple[str, ...]] = {
|
|
"null-deref": ("CWE590",),
|
|
}
|
|
|
|
# For the SV-COMP Juliet_Test corpus (preprocessed .i, per-variant _bad/_good),
|
|
# the yml properties only carry valid-memsafety/no-overflow; the authoritative
|
|
# bug class is the CWE prefix in the filename. Map CWE → fold detector kind so
|
|
# the full-corpus gate can score oob, int-truncation, sign-conversion,
|
|
# div-by-zero (not just the 4 memsafety/overflow kinds).
|
|
JULIET_CWE_KIND: dict[str, str] = {
|
|
"CWE121": "oob-access", "CWE122": "oob-access", "CWE124": "oob-access",
|
|
"CWE126": "oob-access", "CWE127": "oob-access", "CWE805": "oob-access",
|
|
"CWE806": "oob-access",
|
|
"CWE369": "div-by-zero",
|
|
"CWE194": "sign-conversion", "CWE195": "sign-conversion",
|
|
"CWE196": "sign-conversion", "CWE197": "int-truncation",
|
|
"CWE190": "int-overflow", "CWE191": "int-overflow",
|
|
"CWE476": "null-deref", "CWE690": "null-deref",
|
|
"CWE415": "use-after-free", "CWE416": "use-after-free",
|
|
"CWE401": "memory-leak", "CWE590": "memory-leak",
|
|
}
|
|
|
|
def build_category(corpus: Path, category: str) -> list[dict]:
|
|
"""Return gold entries [{kind, files, id}] for one SV-COMP category dir."""
|
|
cat_dir = corpus / category
|
|
if not cat_dir.is_dir():
|
|
print(f"[svcomp-gold] category dir not found: {cat_dir}", file=sys.stderr)
|
|
return []
|
|
allowed = CATEGORY_KIND_FILTER.get(category)
|
|
entries: dict[str, dict] = {}
|
|
for spec in sorted(cat_dir.rglob("*.yml")):
|
|
parsed = parse_yml_lenient(spec)
|
|
if not parsed:
|
|
continue
|
|
kind = SUBPROPERTY_KIND.get(parsed["subproperty"])
|
|
if kind is None:
|
|
continue
|
|
# Juliet_Test: the filename CWE is the authoritative bug class.
|
|
if category == "Juliet_Test":
|
|
cwe = spec.name.split("_")[0]
|
|
kind = JULIET_CWE_KIND.get(cwe, kind)
|
|
# The .c source is the yml stem + .c (SV-COMP .i inputs usually have
|
|
# a matching .c with the harness in the same dir).
|
|
src = spec.with_suffix(".c")
|
|
if not src.exists():
|
|
src = spec.parent / (spec.stem + ".c")
|
|
if not src.exists():
|
|
src = spec.with_suffix(".i")
|
|
if not src.exists():
|
|
src = spec.parent / (spec.stem + ".i")
|
|
if not src.exists():
|
|
continue
|
|
rel = src.relative_to(corpus).as_posix()
|
|
# Bug files (expected_verdict: false) are positives; true are clean
|
|
# negatives. score_fp treats gold files as positives for the kind, so
|
|
# only verdict=false files go in "expected". Clean files are recorded
|
|
# in a companion "clean" list for future negative-aware scoring.
|
|
if parsed["expected_verdict"]:
|
|
continue
|
|
keys = {kind} | set(SIBLING_KIND_EXTENSION.get(parsed["subproperty"], ()))
|
|
for key in keys:
|
|
if allowed is not None and key not in allowed:
|
|
continue
|
|
if rel.split("/")[-1].split("_")[0] in GOLD_FILENAME_EXCLUDE.get(key, ()):
|
|
continue
|
|
entry = entries.setdefault(key, {"kind": key, "files": [], "id": None})
|
|
entry["files"].append(rel)
|
|
out = []
|
|
for i, (kind, entry) in enumerate(sorted(entries.items())):
|
|
entry["id"] = f"svcomp-{category}-{kind}-{i:04d}"
|
|
out.append(entry)
|
|
return out
|
|
|
|
|
|
def main() -> int:
|
|
ap = argparse.ArgumentParser(description=__doc__)
|
|
ap.add_argument("--corpus", required=True, type=Path)
|
|
ap.add_argument(
|
|
"--categories",
|
|
required=True,
|
|
help="comma-separated SV-COMP category dirs under --corpus",
|
|
)
|
|
ap.add_argument("--out", required=True, type=Path)
|
|
args = ap.parse_args()
|
|
|
|
for category in args.categories.split(","):
|
|
category = category.strip()
|
|
if not category:
|
|
continue
|
|
entries = build_category(args.corpus, category)
|
|
out_path = args.out / f"svcomp-{category.replace('/', '_')}.json"
|
|
payload = {
|
|
"name": f"svcomp-{category}",
|
|
"description": (
|
|
f"SV-COMP {category} category gold, built from per-file "
|
|
"yml specs (valid-deref/valid-free/valid-memtrack)."
|
|
),
|
|
"expected": entries,
|
|
}
|
|
args.out.mkdir(parents=True, exist_ok=True)
|
|
out_path.write_text(json.dumps(payload, indent=1) + "\n")
|
|
n_files = sum(len(e["files"]) for e in entries)
|
|
print(
|
|
f"[svcomp-gold] {category}: {len(entries)} kinds, {n_files} bug files -> {out_path}"
|
|
)
|
|
return 0
|
|
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(main())
|