BPF verifier series adds scalar evolution for bounded loops

Eduard Zingerman has posted a large patch series to the BPF development list that adds scalar evolution analysis to the kernel verifier, aiming to verify bounded loops by widening induction variables into ranges rather than walking every possible value.

Scalar evolution infers algebraic expressions for how registers and spilled counters change across loop iterations, then estimates how many times the body can run. A simple counter from 0 to 9, for example, would be checked inside the body as the closed range [0, 9] instead of ten separate states. The work also relaxes some rules on memory access through pointers whose offsets vary within known bounds, including stack and BTF-typed object pointers, and adds interval tracking for values that advance in fixed steps.

Supported shapes include pre- and post-condition loops with the usual signed and unsigned compares, nested and sibling loops, multiple induction variables used for map-value access, and conservative handling when a nest contains irreducible control flow. The series deliberately refuses to widen registers that must stay exact for stack spills, fills, and dynptr construction, so precise stack-slot tracking is preserved.

The approach draws on classical chains-of-recurrences literature. It is a substantial change to how the verifier reasons about looping programs and is intended to accept more realistic bounded-loop patterns without exploding verifier state.

BPF maintainer Alexei Starovoitov has already pushed back on parts of the preparatory liveness work. He notes that the new may-write masks omit stores performed by helpers and kfuncs, which matters for what scalar evolution assumes about stack slots that appear unmodified inside a loop, and he flags the per-instruction memory cost of the extra bitmaps on every program, not only those that contain loops.

The series is under active review on bpf-next.