182 lines
7.2 KiB
Python
182 lines
7.2 KiB
Python
#!/usr/bin/env python3
|
|
"""Mutation sensitivity check for proveit.py (the judge's real teeth).
|
|
|
|
The judge (_judge.py) checks observable behaviour. This file asks the harder
|
|
question: does the judge actually notice when the artifact is broken? It plants
|
|
N real, plausible regressions, runs the judge against each, and requires that
|
|
the judge exits NONZERO for every one of them.
|
|
|
|
A judge that always exits 0 -- or that only fails on the one hardcoded mutation
|
|
in _probe_teeth.py -- is decoration. This script measures the judge's
|
|
sensitivity across a whole defect family, so "judge exit 0" on a clean tree is
|
|
a statement about N defects, not one.
|
|
|
|
Exit 0 == every planted defect was caught (judge is sensitive).
|
|
Exit 1 == at least one defect slipped past the judge (a real coverage hole).
|
|
"""
|
|
import os
|
|
import shutil
|
|
import subprocess
|
|
import sys
|
|
import tempfile
|
|
|
|
HERE = os.path.dirname(os.path.abspath(__file__))
|
|
ART = os.path.join(HERE, "proveit.py")
|
|
JUDGE = os.path.join(HERE, "_judge.py")
|
|
|
|
# Each mutation: (name, old, new, probe_args)
|
|
# `probe_args` is what we run on the mutated artifact: the judge runs the full
|
|
# contract set, but a mutation that breaks e.g. the selfcheck should be caught
|
|
# by that selfcheck specifically -- so we assert both "judge nonzero" and
|
|
# "the named probe also fails", which localises the hole if one exists.
|
|
MUTATIONS = [
|
|
("swap PASS/FAIL derivation",
|
|
'status="PASS" if (ok and measured) else "FAIL"',
|
|
'status="FAIL" if (ok and measured) else "PASS"'),
|
|
("make every predicate read as true",
|
|
"ok = isinstance(value, bool) and value is True",
|
|
"ok = True"),
|
|
("never actually invoke the predicate",
|
|
"value = predicate()",
|
|
"value = None"),
|
|
("control never counts as a real raise",
|
|
"ran += 1\n last_error = \"\".join(",
|
|
"pass # mutation: swallow the raise, ran never increments\n last_error = \"\".join("),
|
|
("predicate invocation never counted",
|
|
"ran += 1\n except",
|
|
"pass # mutation: exception never counted\n except"),
|
|
("status domain widened to UNVERIFIED",
|
|
'status="PASS" if (ok and measured) else "FAIL"',
|
|
'status="PASS" if (ok and measured) else "UNVERIFIED"'),
|
|
("summary pass count lies",
|
|
'"pass": sum(1 for c in suite.claims if c.status == "PASS"),',
|
|
'"pass": len(suite.claims),'),
|
|
("exit code always success",
|
|
"return 0 if all(c.status == \"PASS\" for c in suite.claims) else 1",
|
|
"return 0"),
|
|
("skip claims that would fail",
|
|
"self.claims.append(claim)",
|
|
"self.claims.append(claim)\n self.claims.pop() if claim.status == \"FAIL\" else None"),
|
|
("run loop neutered (zero iterations)",
|
|
"for _ in range(max(1, repeat)):",
|
|
"for _ in range(0):"),
|
|
("predicate return value discarded",
|
|
"value = predicate()",
|
|
"predicate(); value = None"),
|
|
("expected-exception check removed",
|
|
"ok = isinstance(exc, expect_exception) if expect_exception else False",
|
|
"ok = False"),
|
|
("measured flag hardcoded true",
|
|
"measured = ran >= max(1, repeat)",
|
|
"measured = True"),
|
|
("repeat is silently capped at 1",
|
|
"for _ in range(max(1, repeat)):",
|
|
"for _ in range(min(1, max(1, repeat))):"),
|
|
("drop the traceback from the claim",
|
|
"error=last_error,",
|
|
"error=\"\","),
|
|
# --- the four defects found by _hunt_blindspots.py -----------------------
|
|
# Each was measured to slip past the judge BEFORE the matching contract
|
|
# (12-15) existed: judge exit 0 on the mutated tree. They are now pinned
|
|
# here so a regression re-introducing any of them fails the battery.
|
|
("truthy non-bool accepted as PASS",
|
|
"ok = isinstance(value, bool) and value is True",
|
|
"ok = bool(value)"),
|
|
("unrelated raise counts as controlled",
|
|
"ok = isinstance(exc, expect_exception) if expect_exception else False",
|
|
"ok = True if expect_exception else False"),
|
|
("controlled-exception check uses type() not isinstance()",
|
|
"ok = isinstance(exc, expect_exception) if expect_exception else False",
|
|
"ok = type(exc) is expect_exception if expect_exception else False"),
|
|
("harness fault counter never incremented",
|
|
" FAILURES += 1",
|
|
" pass # mutation: harness fault silently uncounted"),
|
|
]
|
|
|
|
|
|
def run(cmd, cwd=None):
|
|
p = subprocess.run(cmd, capture_output=True, text=True, cwd=cwd)
|
|
return p.returncode, p.stdout, p.stderr
|
|
|
|
|
|
def run_judge(adir):
|
|
"""Run the judge located in `adir` (where the artifact also lives)."""
|
|
return run([sys.executable, os.path.join(adir, "_judge.py")], cwd=adir)
|
|
|
|
|
|
def write_probe(dirpath, filename, artifact_dir, body):
|
|
"""Write a probe file next to `artifact_dir` so its sys.path trick lands."""
|
|
path = os.path.join(dirpath, filename)
|
|
with open(path, "w", encoding="utf-8") as fh:
|
|
fh.write(body % artifact_dir)
|
|
return path
|
|
|
|
|
|
def run_probe(path):
|
|
return run([sys.executable, path], cwd="/")
|
|
|
|
|
|
def main():
|
|
# sanity: every anchor must exist exactly once in the artifact, otherwise
|
|
# the sensitivity measurement below is silently vacuous.
|
|
if not os.path.exists(ART):
|
|
print("MUTATION: artifact missing: %s" % ART)
|
|
return 1
|
|
with open(ART, "r", encoding="utf-8") as fh:
|
|
src = fh.read()
|
|
bad = [name for name, old, _ in MUTATIONS if src.count(old) != 1]
|
|
if bad:
|
|
print("MUTATION: anchors not unique in %s: %s" % (ART, ", ".join(bad)))
|
|
return 1
|
|
|
|
# ---- baseline: clean tree must pass the judge --------------------------
|
|
rc, out, err = run_judge(HERE)
|
|
print("baseline judge exit: %d" % rc)
|
|
if rc != 0:
|
|
print("MUTATION: judge does not pass on the clean artifact; "
|
|
"sensitivity test is meaningless")
|
|
print(err[-2000:])
|
|
return 1
|
|
if "all contract checks hold" not in out:
|
|
print("MUTATION: baseline judge output lacks its success line")
|
|
return 1
|
|
|
|
tmpdir = tempfile.mkdtemp(prefix="proveit-mut-")
|
|
caught, missed = 0, []
|
|
try:
|
|
for name, old, new in MUTATIONS:
|
|
if src.count(old) != 1:
|
|
print(" SKIP %-38s (anchor not unique: %d)"
|
|
% (name, src.count(old)))
|
|
missed.append(name + " (anchor not found)")
|
|
continue
|
|
mdir = tempfile.mkdtemp(prefix="mut-", dir=tmpdir)
|
|
mpath = os.path.join(mdir, "proveit.py")
|
|
with open(mpath, "w", encoding="utf-8") as fh:
|
|
fh.write(src.replace(old, new, 1))
|
|
# copy the judge alongside so relative artifact discovery works
|
|
shutil.copy2(JUDGE, os.path.join(mdir, "_judge.py"))
|
|
jrc, jout, jerr = run_judge(mdir)
|
|
if jrc != 0:
|
|
caught += 1
|
|
print(" CAUGHT %-37s judge exit=%d" % (name, jrc))
|
|
else:
|
|
print(" MISSED %-37s judge exit=0 <-- coverage hole" % name)
|
|
missed.append(name)
|
|
finally:
|
|
shutil.rmtree(tmpdir, ignore_errors=True)
|
|
|
|
print()
|
|
total = len(MUTATIONS)
|
|
print("MUTATION SENSITIVITY: %d/%d planted defects caught by the judge"
|
|
% (caught, total))
|
|
if missed:
|
|
print("MUTATION: uncovered defect(s): %s" % ", ".join(missed))
|
|
return 1
|
|
print("MUTATION SENSITIVITY OK")
|
|
return 0
|
|
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(main())
|