#!/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())