- checkAdaptive: cap escalation at 4 min (8x base) instead of 1 hour. The
1-hour ceiling let a genuinely-hard query pin a worker for an hour with
zero file completion, stalling the whole scan (observed: 5 workers at 100%
CPU, log stopped advancing). 4 min still resolves "just barely over budget"
queries while bounding pathological ones.
- score_fp.py: guard the last bare .read_text(), drop an unused `elapsed`,
log the fold --version failure instead of bare pass, and suppress the
runtime sys.path import (reportMissingImports/E402).
Replace bare json.loads/int/float calls with small guarded helpers so a
missing or malformed gold/SARIF/compile-DB file exits with a clear message
instead of a raw traceback, and numeric fields degrade to defaults.
Add negative_cases_from_universe to expand an explicit file-by-rule universe
into labeled negatives (enabling TP/FP/TN/FN, not just TP/FP), plus project-eval
harness updates in run_project_eval and the score/score_fp/quality-gate helpers.
For a counted loop whose trip count exceeds the unroll bound, bind the
induction variable to its full closed-form range (asserted as a Z3 path
constraint, not just interval metadata) and walk the body once, instead of
unrolling loop_unroll times. This fires each in-body sink against all
iterations at once: it exposes high-index OOB that bounded unroll misses
(oob recall 0.531 -> 0.574, F1 0.637 -> 0.658 on the gate) and collapses
per-iteration queries to one. Findings from the summarized walk are
over-approximations and are tagged LoopHavoc (heuristic) confidence, never
proved. General/while(1) loops keep the bounded-unroll fallback.
Per the precision contract (loop-summarization-research.md), this is a
recall-improving over-approximation that may add bounded, tagged FPs. The
drift gate is updated to match: it now fails on recall- or F1-drop beyond
tolerance (the regressions it was built for) and allows precision dips that
come with recall gains; the committed baseline is regenerated to the B2
numbers.
Tests: test_loop_summary (high-index OOB found + not proved; in-bounds loop
clean). Suite 68/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Enumeration: replace the hand-rolled top-level `tu->decls()` walks (TU
security prefilter + every interprocedural pre-pass/cross-TU primer in
div-by-zero/int-overflow/null-deref/oob) with a shared RAV-based
`fold::detect::forEachFunctionWithBody`, so functions nested in namespaces
and classes are analyzed. Fixes 0-findings on namespaced C++ (dbench CTF).
TU prefilter: extracted to fold/cli/tu_security_prefilter; flags unsigned
-/* wraps so int-overflow candidates in size arithmetic are not skipped.
Timeout robustness: cooperative per-TU walk deadline (WalkOptions) checked
in the walk/unrollLoop/CFG-block checkpoints and the BatchSafetyObserver
flush loop, plus a non-progress unroll fixpoint — slow TUs degrade with
partial findings instead of being SIGALRM-quarantined.
OOB precheck: treat `*(p+i)` and indirect callees as candidates.
null-deref drift fix: remove the unsound `priorFunctionTextProvesNonNull`
source-text heuristic (added in 331a68467) that treated a textual `p!=0`
before a deref as proof of non-null, silently suppressing real null-derefs
(CWE-476 F1 0.485 -> 0.583, recall 0.379 -> 0.517).
Tests: test_function_enumeration, test_tu_security_prefilter, namespaced
cross-TU int-overflow regression. Full suite green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
