#!/usr/bin/env python3
"""#7 每目标符号变量数 + Z3 超时占比:跑各 -symcc 目标,解析运行时 stderr 的
'[SymCC] Solver stats: fast_solve=.. z3_solve=.. z3_timeout=.. total_generated=.. relevant_bytes=A/B'。"""
import os, sys, glob, subprocess, tempfile, re, shutil

ROOT = "/home/ubuntu/code/symcc"
BIN = os.path.join(ROOT, "benchmark/public/bin")
SEED = os.path.join(ROOT, "benchmark/public/seeds")
# (名字, 二进制, 种子目录, 模式, 额外args)
TARGETS = [
    ("gfts-xml",    "google-fts/xml_read_fuzzer", "google-fts/xml_read_fuzzer", "file", []),
    ("gfts-png",    "google-fts/png_read_fuzzer", "google-fts/png_read_fuzzer", "file", []),
    ("libarchive",  "libarchive/archive_fuzzer",  "libarchive",                 "file", []),
    ("sqlite",      "sqlite/sqlite_fuzzer",       "sqlite",                     "file", []),
    ("pcre2",       "pcre2/pcre2_fuzzer",         "pcre2",                      "file", []),
    ("freetype2",   "freetype2/freetype2_fuzzer", "freetype2",                  "file", []),
    ("lava-base64", "lava-m/base64",              "lava-m/base64",              "stdin", ["-d"]),
]
PAT = re.compile(r"Solver stats: fast_solve=(\d+) z3_solve=(\d+) z3_timeout=(\d+) "
                 r"total_generated=(-?\d+)(?: relevant_bytes=(\d+)/(\d+))?")

def run_one(b, args, mode, seed):
    """跑一个种子,返回 (fast_solve, z3_solve, z3_timeout, rel_bytes, tot_bytes) 或 None。"""
    od = tempfile.mkdtemp(prefix="ss_")
    env = dict(os.environ, SYMCC_OUTPUT_DIR=od, SYMCC_ENABLE_LINEARIZATION="1",
               SYMCC_TAINT_OUT=os.path.join(od, "taint"))
    try:
        if mode == "file":
            env["SYMCC_INPUT_FILE"] = seed
            r = subprocess.run([b] + args + [seed], stdin=subprocess.DEVNULL,
                               stdout=subprocess.DEVNULL, stderr=subprocess.PIPE, env=env, timeout=40)
        else:
            with open(seed, "rb") as inf:
                r = subprocess.run([b] + args, stdin=inf, stdout=subprocess.DEVNULL,
                                   stderr=subprocess.PIPE, env=env, timeout=40)
        m = PAT.search(r.stderr.decode("utf-8", "replace"))
        if not m:
            return None
        return (int(m.group(1)), int(m.group(2)), int(m.group(3)),
                int(m.group(5)) if m.group(5) else 0, int(m.group(6)) if m.group(6) else 0)
    except (subprocess.TimeoutExpired, OSError):
        return None
    finally:
        shutil.rmtree(od, ignore_errors=True)

print(f"{'target':13}{'seeds':>6}{'z3_solve':>9}{'z3_timeout':>11}{'超时%':>8}"
      f"{'fast_solve':>11}{'符号字节(relevant/总,均值)':>26}")
for name, binp, seedp, mode, args in TARGETS:
    b = os.path.join(BIN, binp); sd = os.path.join(SEED, seedp)
    if not os.path.exists(b) or not os.path.isdir(sd):
        print(f"{name:13} (缺二进制或种子)"); continue
    seeds = [s for s in sorted(glob.glob(os.path.join(sd, "*")))[:6] if os.path.isfile(s)]
    fss = z3s = z3t = 0; rels = []; tots = []
    for s in seeds:
        v = run_one(b, args, mode, s)
        if v:
            fss += v[0]; z3s += v[1]; z3t += v[2]
            if v[4]:
                rels.append(v[3]); tots.append(v[4])
    ratio = f"{100*z3t/z3s:.1f}%" if z3s else "n/a"
    rb = f"{sum(rels)//len(rels)}/{sum(tots)//len(tots)}" if tots else "n/a"
    print(f"{name:13}{len(seeds):>6}{z3s:>9}{z3t:>11}{ratio:>8}{fss:>11}{rb:>26}")