#!/usr/bin/env python3
"""迭代式 concolic：把上一轮产出喂回，直到解出全部嵌套魔数或达轮次上限。
统计每一轮:执行次数、总产出、Z3 查询、求解时间、当前最深已解层数。"""
import json, os, shutil, subprocess, sys, tempfile, time, hashlib

BIN, DEPTH, MAXGEN = sys.argv[1], int(sys.argv[2]), int(sys.argv[3])
W = tempfile.mkdtemp(prefix="nested_", dir=os.path.dirname(os.path.abspath(BIN)))
seed = os.path.join(W, "seed"); open(seed, "wb").write(b"\x00" * DEPTH)

def depth_of(path):                       # 已匹配的前缀长度
    d = open(path, "rb").read()
    n = 0
    while n < DEPTH and n < len(d) and d[n] == 0x41 + n:
        n += 1
    return n

corpus = {hashlib.sha256(open(seed,'rb').read()).hexdigest(): seed}
frontier = [seed]
best = depth_of(seed)
tot_q = tot_t = tot_exec = tot_out = 0
t0 = time.time()
print(f"  {'代':>3} {'执行':>5} {'产出':>6} {'Z3查询':>7} {'求解ms':>8} {'最深层':>6} {'累计秒':>7}")
for gen in range(1, MAXGEN + 1):
    nxt = []
    gq = gt = gout = 0
    for inp in frontier:
        out = tempfile.mkdtemp(dir=W); tel = out + ".json"
        subprocess.run([BIN, inp], env={**os.environ, "SYMCC_OUTPUT_DIR": out,
                        "SYMCC_INPUT_FILE": inp, "SYMCC_TELEMETRY_OUT": tel},
                       stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL, timeout=600)
        tot_exec += 1
        if os.path.exists(tel):
            d = json.load(open(tel)); gq += d["solver_queries"]; gt += d["solver_time_us"]
        for fn in sorted(os.listdir(out)):
            if fn.endswith(".hints"): continue
            p = os.path.join(out, fn); gout += 1
            h = hashlib.sha256(open(p, "rb").read()).hexdigest()
            if h in corpus: continue
            keep = os.path.join(W, h[:16]); shutil.copy(p, keep); corpus[h] = keep
            nxt.append(keep); best = max(best, depth_of(keep))
    tot_q += gq; tot_t += gt; tot_out += gout
    print(f"  {gen:>3} {len(frontier):>5} {gout:>6} {gq:>7} {gt/1000:>8.1f} {best:>6} {time.time()-t0:>7.1f}")
    if best >= DEPTH: 
        print(f"  ==> 深度 {DEPTH} 在第 {gen} 代解出;累计 执行={tot_exec} 产出={tot_out} Z3查询={tot_q} 求解={tot_t/1000:.0f}ms 墙钟={time.time()-t0:.1f}s")
        break
    frontier = nxt[:64]      # 前沿限流,避免指数爆炸
    if not frontier:
        print(f"  ==> 前沿枯竭,止步于深度 {best}/{DEPTH}"); break
else:
    print(f"  ==> {MAXGEN} 代未解出,止步于深度 {best}/{DEPTH};累计 执行={tot_exec} 产出={tot_out} Z3查询={tot_q} 求解={tot_t/1000:.0f}ms 墙钟={time.time()-t0:.1f}s")
shutil.rmtree(W, ignore_errors=True)