Alan-Jowett / ebpf-verifier / 37071205739

87%

Build Type

push

github

Committed by web-flow

Commit Message

Stop descending iteration when narrowing is stationary (#1243)

* Stop descending iteration when narrowing is stationary

Descending fixpoint iteration currently stops only when the loop-body
transfer result subsumes the current invariant. If narrowing returns an
abstract state that is lattice-equivalent to the current invariant while
the transfer result remains strictly more precise, the next iteration
starts from the same abstract state and repeats until the descending
iteration limit.

Compute the narrowed candidate before assigning it and stop when it
mutually subsumes the current invariant. Retain the candidate so any
canonicalized representation or auxiliary stack-cell metadata is
preserved. Strict refinements continue as before, and the existing
iteration limit is unchanged.

Add a deterministic Extrapolator unit test covering strict meet and type
refinements followed by stationary numeric narrowing. Add the 32-bit
countdown reproducer from #783 as an end-to-end YAML regression.

Part of #783.

Signed-off-by: Michael Agun <danielagun@microsoft.com>
Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

* Address stationary narrowing review feedback

Rely on the narrowing contract that the refined state is below the
current invariant, so only the reverse ordering is needed to detect a
stationary result.

Replace the finite countdown YAML case, which PREVAIL rejected as a
false positive, with a true-positive regression. The same countdown SCC
still reaches stationary narrowing, then the program enters an
unconditional self-loop and is genuinely nonterminating.

Part of #783.

Signed-off-by: Michael Agun <danielagun@microsoft.com>

Coverage Stats

6 of 6 new or added lines in 1 file covered. (100.0%)

42 existing lines in 2 files now uncovered.

9121 of 10505 relevant lines covered (86.83%)

3202971.97 hits per line