Skip to content

measure_support over-reports "black" (soundness-bug) cells: ~96% are false positives #456

Description

@pschanely

Summary

A full regeneration of the support map on current main-lineage code produces 242 black ("gives a wrong answer / soundness bug") cells out of 2243. Auditing every one of them (re-running each cell's demo through crosshair and reconciling against its verdict) shows only ~8–10 are genuine soundness bugs; ~96% are false positives. The black category currently can't be trusted, and a regenerated SVG would visually claim ~240 bugs where there are ~10.

(The genuine ones are mostly the float/precision family tracked in #455float.__mod__/__divmod__, colorsys.hls_to_rgb/hsv_to_rgb/rgb_to_yiq — plus three real string-transform bugs: re.escape, fnmatch.translate, shlex.quote.)

Audited breakdown of the 242 black cells

Reconciled label Count Why it's not a real "wrong answer"
No demo (nondeterministic / mutator / opaque) 130 graded black with no reproducible witness
CrossHair raises an exception 48 TypeError/ValueError/AttributeError/OverflowError/ZeroDivisionError/CrossHairInternal — an unsupported/erroring op, not a wrong value; should be red
Confirmed-inversion, mostly nondeterministic 41 incl. a 28-cell re.RegexFlag (IntFlag) cluster; the holdout's UNSAT is expected here, not a bug
Flaky (invertible on re-run) 13 e.g. bytearray.find/startswith/index/…, operator.concat — holdout "confirms no input" but a re-run readily finds one
Real wrong-answer 10 genuine (and 2 of these are actually nondeterministic misclassifications)

Root causes (each independently reproducible)

1. Nondeterministic functions aren't filtered. uuid.uuid1/3/4/5, secrets.token_bytes/hex/urlsafe, secrets.randbelow, time.perf_counter/thread_time all land on black. The determinism guard in _sweep is deliberately skipped when there are no params (so time.time() can invert via its symbolic return), and _NOT_A_VALUE_FUNCTION only lists id/is_/is_not. Result — a zero-arg func CrossHair doesn't model symbolically gets a false "confirms no input yields an output" black; a func with args (randbelow) gets a false "forward differs" black.

# secrets.randbelow — flagged black "forward result differs"; it's just random.
def f(exclusive_upper_bound: int):
    """
    pre: exclusive_upper_bound == 13
    post: _ == 5
    """
    return secrets.randbelow(exclusive_upper_bound)

2. "CrossHair raised (unsupported)" is misread as "forward result differs." 48 cells. The differential treats a symbolic-side exception as a value divergence from concrete Python. Example — hmac.compare_digest just raises inside CrossHair:

error: TypeError: unsupported operand type(s) ... 'SymbolicBytes' and 'SymbolicBytes'

This should grade red/unsupported, not "gives a wrong answer."

3. No-demo cells are graded black anyway (130). _diff_demo/_pinned_demo return None (concrete raised, or values don't repr-round-trip, or it's a mutator), yet the cell is still colored black with no runnable witness. A black with no reproducible demo isn't defensible — it should downgrade to red/grey.

4. Holdout UNSAT ("confirms no input yields an output that one does") is flaky. For bytearray.find / startswith / operator.concat the measurement CONFIRMS no input exists, but re-running the demo, CrossHair immediately finds one (sub=b'' makes find()==0). So the UNSAT is being reached unreliably — likely the per-condition timeout hit and read as CONFIRMED, compounded by (5).

5. (Related, reproducibility) fuzz seeding is nondeterministic. _sweep uses seed = hash(seedkey) % 1000 + n with PYTHONHASHSEED unset, so string hashing is salted per process. Two runs pick different fuzzed inputs, so borderline cells flip color and demo inputs change run-to-run. Suggest a stable hash (e.g. zlib.crc32/hashlib) or pinning PYTHONHASHSEED.

Suggested direction

  • Detect nondeterminism even for zero-arg ops (run the op twice concretely; if outputs differ and CrossHair doesn't model it symbolically, grade ?), and/or broaden the not-a-value-function filter.
  • In the differential, distinguish "symbolic side raised an unsupported/CrossHair exception" (→ red) from "returned a different value" (→ black).
  • Require a reproducible demo before grading a cell black.
  • Harden the holdout UNSAT verdict (verify an inverting input truly doesn't exist, e.g. one concrete probe) before calling it unsound.
  • Make seeding deterministic.

Repro

python -m crosshair.tools.measure_support funcs  --modules secrets,uuid,time,hmac --json f.json --jobs 1
python -m crosshair.tools.measure_support surface --types bytearray                --json s.json --jobs 1

then inspect the black records. Found during the support-grid regeneration (lineage of #454); companion to #455.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions