Extend ir::Loop classification: a monotone single-induction-variable for-loop
with a symbolic bound (e.g. `for (i=0; i<n; ++i)`) is now Affine (was General).
The walker summarizes Affine loops like Counted ones — bind the induction
variable to a fresh symbolic, assert its start bound plus the loop condition
(encoded to a Z3 bool) as path constraints, walk the body once — exposing
high-index OOB that bounded unroll misses. Findings are over-approximations
(LoopHavoc/heuristic), never proved.
Net effect on the gate: oob recall 0.531 -> 0.559, F1 0.637 -> 0.652 (precision
dips 0.796 -> 0.782) — a contract-sanctioned over-approximation tradeoff.
Also regenerate bench/fp-baseline.json deterministically from a clean run: the
prior committed oob numbers (0.574) were not reproducible (transient warm-state
artifact); fresh runs are now bit-identical, so the gate is reliable.
Tests: test_ir_loop (affine classification), test_loop_summary (symbolic-bound
OOB exposed, not proved). Suite green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Foundation for core loop summarization (Workstream B). Adds a clang-free
ir::Loop / InductionVar / LoopKind (Counted | Affine | General) mirroring the
M30 ir::Expr pattern (Symbol-keyed, opaque frontend handle, lowering in
src/symbolic/ir_loop_clang.cpp).
buildLoopFromClang classifies counted `for` loops (constant init/stride/bound,
ascending or descending) into a Counted loop with a known trip count; affine
and unrecognized shapes (while(1) scanners, data-dependent bounds) stay
General and will use the bounded-unroll fallback. The symbolic core will
consume ir::Loop instead of clang::ForStmt so summarization is written once
and reused by the rust/binary frontends.
Tests: test_ir_loop (counted asc/strided/desc trip counts; while(1) and
data-dependent bound -> General). Suite 67/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
