92 lines
4.6 KiB
Python
92 lines
4.6 KiB
Python
#!/usr/bin/env python3
|
|
"""attack-f2: turn the search states into the record's tables, and verify every k >= 2 trail post hoc on the real
|
|
code (per application by sampling, the multiply-layer words exactly over 2^32).
|
|
|
|
summarise.py --state-dir DIR --binary attack-f2 --out DIR/summary.md [--verify-log2 26]
|
|
"""
|
|
import argparse
|
|
import glob
|
|
import json
|
|
import os
|
|
import subprocess
|
|
|
|
|
|
def run(cmd):
|
|
return subprocess.run(cmd, capture_output=True, text=True, check=True).stdout
|
|
|
|
|
|
def verify(binary, kind, st, path, log2):
|
|
"""Per-application measured weights and the exact multiply-word weights of a trail (written beside the state)."""
|
|
trail = path + ".trail"
|
|
mults = path + ".mults"
|
|
out = {}
|
|
if os.path.exists(trail):
|
|
txt = run([binary, "verify-" + kind, "--day", st["day"], "--variant", st["variant"], "--trail", trail, "--log2", str(log2)])
|
|
per, chain = [], None
|
|
for line in txt.splitlines():
|
|
f = line.split()
|
|
if f and f[0] == "app":
|
|
per.append(f[f.index("weight") + 1] if kind == "diff" else f[f.index("abs_log2") + 1])
|
|
elif f and f[0] == "chain":
|
|
chain = f[f.index("weight") + 1] if kind == "diff" else f[f.index("abs_log2") + 1]
|
|
out["per_app"] = per
|
|
out["chain"] = chain
|
|
open(path + ".verify.log", "w").write(txt)
|
|
if os.path.exists(mults) and os.path.getsize(mults) > 0:
|
|
txt = run([binary, "verify-mults", "--kind", kind, "--day", st["day"], "--variant", st["variant"], "--file", mults])
|
|
open(path + ".mults.log", "w").write(txt)
|
|
last = [l for l in txt.splitlines() if l.startswith("words")]
|
|
out["mults_exact"] = last[0] if last else ""
|
|
return out
|
|
|
|
|
|
def main():
|
|
ap = argparse.ArgumentParser()
|
|
ap.add_argument("--state-dir", required=True)
|
|
ap.add_argument("--binary", required=True)
|
|
ap.add_argument("--out", required=True)
|
|
ap.add_argument("--verify-log2", type=int, default=26)
|
|
ap.add_argument("--no-verify", action="store_true")
|
|
a = ap.parse_args()
|
|
rows = []
|
|
for path in sorted(glob.glob(os.path.join(a.state_dir, "*.json"))):
|
|
try:
|
|
st = json.load(open(path))
|
|
except json.JSONDecodeError:
|
|
import time
|
|
time.sleep(2)
|
|
try:
|
|
st = json.load(open(path))
|
|
except json.JSONDecodeError:
|
|
print("skipping half-written", path)
|
|
continue
|
|
name = os.path.basename(path)[:-5]
|
|
best = st.get("trail_weight") if st.get("trail") else None
|
|
v = {}
|
|
if not a.no_verify and st.get("trail") and st["apps"] >= 2 and st.get("verified_chain_weight") is None:
|
|
v = verify(a.binary, st["kind"], st, path, a.verify_log2)
|
|
rows.append({
|
|
"name": name, "kind": st["kind"], "family": st.get("family", "general"), "day": st["day"], "variant": st["variant"],
|
|
"apps": st["apps"], "best": best, "unsat_upto": st["unsat_upto"], "done": st.get("done", False),
|
|
"pending": st.get("pending"), "cap": st.get("cap_reached", False), "per_app_min": st.get("per_app_min", 0),
|
|
"by_tag": st.get("weight_by_tag"), "verified_chain": st.get("verified_chain_weight"),
|
|
"verified_per_app": st.get("verified_per_app"), "refuted": st.get("refuted", 0), "cancelled": st.get("cancelled", 0),
|
|
"solver_s": round(st.get("solver_seconds", 0)), "post": v, "log": st.get("log", [])[-1:],
|
|
})
|
|
with open(a.out, "w") as f:
|
|
f.write("| model | day | variant | k | best trail weight found | no trail at or below (model) | closed | per-app floor | verified on real code (chain; per app) | exact mult words | refuted / cancelled | solver s |\n")
|
|
f.write("|---|---|---|---|---|---|---|---|---|---|---|---|\n")
|
|
for r in rows:
|
|
ver = ""
|
|
if r["verified_chain"] is not None:
|
|
ver = f"{r['verified_chain']}; {r['verified_per_app']}"
|
|
elif r["post"].get("chain") is not None or r["post"].get("per_app"):
|
|
ver = f"{r['post'].get('chain')}; {r['post'].get('per_app')} (2^{a.verify_log2})"
|
|
closed = "yes" if r["done"] and (r["best"] is None or r["best"] == r["unsat_upto"] + 1) else ("cap" if r["cap"] else "no")
|
|
f.write(f"| {r['kind']}/{r['family']} | {r['day']} | {r['variant']} | {r['apps']} | {r['best']} | {r['unsat_upto']} | {closed} | {r['per_app_min']} | {ver} | {r['post'].get('mults_exact', '')} | {r['refuted']} / {r['cancelled']} | {r['solver_s']} |\n")
|
|
json.dump(rows, open(a.out + ".json", "w"), indent=1)
|
|
print(open(a.out).read())
|
|
|
|
|
|
if __name__ == "__main__":
|
|
main()
|