File size: 4,241 Bytes
4951e76 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 | #!/usr/bin/env python3 -I
"""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) # libFuzzer sanitizer flags need a nightly
b = limited(["cargo", "fuzz", "build", p["id"]], out, 900, fenv) # build is reported, not charged to the budget
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()
|