#!/usr/bin/env python3
"""Diagnose why Juliet test cases are missed by fold.

Usage:
  # 1. Run fold with trace JSON output:
  fold scan --compile-db ... --detectors null-deref --trace --format sarif \
    --output results.sarif --processes 1 2>trace.log

  # 2. Parse trace and compare against gold:
  python3 bench/diagnose.py --trace trace.log --gold bench/gold/juliet-476.json \
    --results results.sarif --detector null-deref
"""

from __future__ import annotations

import argparse
import json
import os
import re
import sys
from collections import defaultdict
from pathlib import Path

TRACE_RE = re.compile(
    r'trace_json \{"detector":"(\S+)","file":"([^"]+)",'
    r'"line":(\d+),"col":(\d+),"result":"(\S+)","detail":"([^"]+)"\}'
)


def parse_trace(log_path: str, detector: str) -> dict[str, list[dict]]:
    """Parse trace JSON lines, return {basename: [trace_entry, ...]}."""
    by_file = defaultdict(list)
    with open(log_path) as f:
        for line in f:
            m = TRACE_RE.search(line)
            if not m:
                continue
            if m.group(1) != detector:
                continue
            by_file[Path(m.group(2)).name].append({
                "file": m.group(2),
                "line": int(m.group(3)),
                "col": int(m.group(4)),
                "result": m.group(5),
                "detail": m.group(6),
            })
    return dict(by_file)


def load_gold(gold_path: str) -> list[dict]:
    return json.loads(Path(gold_path).read_text())["expected"]


def load_findings(sarif_path: str) -> set[str]:
    """Return set of file paths that were found (had at least one finding)."""
    found = set()
    if not Path(sarif_path).exists():
        return found
    doc = json.loads(Path(sarif_path).read_text())
    for run in doc.get("runs", []):
        for result in run.get("results", []):
            for loc in result.get("locations", []):
                uri = loc.get("physicalLocation", {}).get(
                    "artifactLocation", {}).get("uri", "")
                if uri:
                    found.add(uri)
    return found


def diagnose(gold_path: str, log_path: str, sarif_path: str,
             detector: str) -> dict:
    gold_entries = load_gold(gold_path)
    traces = parse_trace(log_path, detector)
    found_files = load_findings(sarif_path)

    categories = defaultdict(list)
    for g in gold_entries:
        bn = Path(g["files"][0]).name
        has_trace = bn in traces
        found = any(bn in f for f in found_files)

        if found:
            continue  # already detected, no diagnosis needed

        file_traces = traces.get(bn, [])
        sat_traces = [t for t in file_traces if t["result"] == "sat"]
        unsat_traces = [t for t in file_traces if t["result"] == "unsat"]

        if not file_traces:
            categories["no-trace"].append({
                "file": bn,
                "id": g["id"],
                "diagnosis": "encoder never reached Z3 — walker/encoder gap",
            })
        elif sat_traces:
            categories["sat-but-missed"].append({
                "file": bn,
                "id": g["id"],
                "traces": len(sat_traces),
                "diagnosis": "Z3 found bug (SAT) but not in scoring — gold/file mismatch",
            })
        elif unsat_traces:
            categories["unsat-only"].append({
                "file": bn,
                "id": g["id"],
                "traces": len(unsat_traces),
                "diagnosis": "Z3 proved safe (UNSAT) — analysis precision gap",
            })

    # Also categorize FP files
    fp_files = set()
    for fn in traces:
        is_gold = any(Path(g["files"][0]).name == fn for g in gold_entries)
        if not is_gold:
            fp_files.add(fn)

    for fn in sorted(fp_files):
        file_traces = traces[fn]
        sat = [t for t in file_traces if t["result"] == "sat"]
        if sat:
            categories["fp-sat"].append({
                "file": fn,
                "traces": len(sat),
                "diagnosis": "Z3 flagged clean file (FP) — path too weak or operands over-approx",
            })

    return dict(categories)


def render(categories: dict, gold_total: int) -> str:
    lines = [
        f"# fold diagnosis — {gold_total} gold entries",
        "",
        "## Miss categories",
    ]

    cat_labels = {
        "no-trace": "No Z3 queries (encoder/walker gap)",
        "unsat-only": "Z3 proved safe (analysis precision)",
        "sat-but-missed": "Z3 found bug but scoring mismatch",
        "fp-sat": "False positive (Z3 flagged clean file)",
    }

    for cat, label in cat_labels.items():
        entries = categories.get(cat, [])
        if not entries:
            continue
        pct = len(entries) * 100.0 / max(1, gold_total)
        lines.append(f"\n### {label} — {len(entries)} ({pct:.1f}%)")
        for e in entries[:10]:
            lines.append(f"- `{e['file']}` — {e['diagnosis']}")
        if len(entries) > 10:
            lines.append(f"- ... and {len(entries)-10} more")

    return "\n".join(lines) + "\n"


def main() -> int:
    p = argparse.ArgumentParser(description=__doc__)
    p.add_argument("--trace", required=True, help="fold stderr with trace_json lines")
    p.add_argument("--gold", required=True, help="Juliet gold JSON")
    p.add_argument("--results", required=True, help="fold SARIF output")
    p.add_argument("--detector", required=True,
                   help="Detector name (null-deref, div-by-zero, int-overflow, oob-access)")
    args = p.parse_args()

    gold = load_gold(args.gold)
    categories = diagnose(args.gold, args.trace, args.results, args.detector)

    print(render(categories, len(gold)))
    return 0


if __name__ == "__main__":
    raise SystemExit(main())