| |
| """Run Kani / proptest / cargo-fuzz on one property bank under an EQUAL CPU budget. |
| Usage: run_baselines.py BANK --cpu-seconds 60 [--arms kani,proptest,fuzz] [--workdir /apps/...] |
| Emits one JSON line per (property, arm): {item_id, property, arm, flagged, cpu_seconds, status}. |
| Budget is per (property, arm). `flagged` = tool reported a violation / panic. Build time is reported |
| as build_seconds and not charged to the budget. |
| """ |
| import argparse, json, os, resource, subprocess, sys, time |
| HERE = os.path.dirname(os.path.abspath(__file__)) |
| sys.path.insert(0, HERE) |
| import property_bank as pb |
|
|
|
|
| def limited(cmd, cwd, cpu, env=None): |
| def pre(): |
| os.setsid(); resource.setrlimit(resource.RLIMIT_CPU, (cpu, cpu + 5)) |
| t0 = time.time(); r0 = resource.getrusage(resource.RUSAGE_CHILDREN) |
| try: |
| p = subprocess.run(cmd, cwd=cwd, capture_output=True, text=True, timeout=cpu * 3 + 10, preexec_fn=pre, env=env) |
| rc, out = p.returncode, p.stdout + p.stderr |
| except subprocess.TimeoutExpired as e: |
| rc, out = -9, "wall timeout" |
| r1 = resource.getrusage(resource.RUSAGE_CHILDREN) |
| return rc, out, (r1.ru_utime + r1.ru_stime) - (r0.ru_utime + r0.ru_stime), time.time() - t0 |
|
|
|
|
| def main(): |
| ap = argparse.ArgumentParser() |
| ap.add_argument("bank"); ap.add_argument("--cpu-seconds", type=int, default=60) |
| ap.add_argument("--arms", default="kani,proptest,fuzz"); ap.add_argument("--revision", default="pre", choices=["pre", "post"], help="post = negative control (the fixed revision)") |
| ap.add_argument("--fuzz-toolchain", default="nightly-2026-09-17"); ap.add_argument("--workdir", default="/apps/development/rlhf/bugfind_data/work/baselines") |
| a = ap.parse_args() |
| if not a.workdir.startswith("/apps/"): sys.exit("workdir must be under /apps") |
| bank = pb.load(a.bank) |
| for arm in a.arms.split(","): |
| out = os.path.join(a.workdir, bank["item_id"] + "." + a.revision, arm) |
| subprocess.run([sys.executable, "-I", os.path.join(HERE, "gen_harness.py"), a.bank, arm, out, a.revision], check=True, capture_output=True) |
| env = dict(os.environ, CARGO_TARGET_DIR=os.path.join(out, "target")) |
| for p in bank["properties"]: |
| res = dict(item_id=bank["item_id"], revision=a.revision, property=p["id"], arm=arm, cpu_budget=a.cpu_seconds) |
| if arm == "proptest": |
| b = limited(["cargo", "test", "--no-run", "--test", "pt_props", "-j4"], out, 900, env) |
| res["build_seconds"] = round(b[3], 1) |
| if b[0] != 0: res.update(status="build_fail", flagged=None, log=b[1][-400:]) |
| else: |
| rc, o, cpu, wall = limited(["cargo", "test", "--test", "pt_props", f"prop_{p['id']}"], out, a.cpu_seconds, env) |
| res.update(flagged=(rc != 0 and "test result: FAILED" in o), status="ok" if rc in (0, 101) else f"rc{rc}", cpu_seconds=round(cpu, 1)) |
| elif arm == "fuzz": |
| fdir = os.path.join(out, "fuzz") |
| fenv = dict(env, RUSTUP_TOOLCHAIN=a.fuzz_toolchain) |
| b = limited(["cargo", "fuzz", "build", p["id"]], out, 900, fenv) |
| res["build_seconds"] = round(b[3], 1) |
| if b[0] != 0: |
| res.update(status="build_fail", flagged=None, log=b[1][-400:]); print(json.dumps(res), flush=True); continue |
| rc, o, cpu, wall = limited(["cargo", "fuzz", "run", p["id"], "--", f"-max_total_time={a.cpu_seconds}", "-rss_limit_mb=2048"], out, a.cpu_seconds + 20, fenv) |
| res.update(flagged=("panicked" in o or "SUMMARY: libFuzzer" in o or "AddressSanitizer" in o), status="ok" if rc in (0, 77) else f"rc{rc}", cpu_seconds=round(cpu, 1)) |
| elif arm == "kani": |
| rc, o, cpu, wall = limited(["cargo", "kani", "--tests", "--harness", f"proof_{p['id']}"], out, a.cpu_seconds, env) |
| res.update(flagged=("VERIFICATION:- FAILED" in o or "VERIFICATION FAILED" in o), status="ok" if rc in (0, 1) else f"rc{rc}", cpu_seconds=round(cpu, 1)) |
| print(json.dumps(res), flush=True) |
|
|
| if __name__ == "__main__": |
| main() |
|
|
