vbpf / prevail / 29361137028

87%

push

github

Soundly narrow sign-extending memory loads, extend to ctx inline fields

On a signed memory load the narrow helper set uvalue to the
zero-extended range [0, 2^(8*width) - 1]. That is unsound: the unsigned
64-bit view of a sign-extended negative result sits up near 2^64,
disjoint from that range, so no concrete value satisfies the resulting
abstract state (e.g. an s8 of -1 has svalue=-1 but uvalue=2^64-1, not
uvalue<=255).

The fix is to havoc uvalue on signed loads, matching what FiniteDomain
already does for arithmetic: sign_extend routes through overflow_bounds,
which havocs uvalue when the value wraps. The narrow helper was the one
load path that bypassed this. Register MOVSX was already sound and is
unchanged.

The narrowing logic moves into a shared helper that is now also applied
to ctx inline-field loads, which previously got no width-based bound at
all (only packet/shared loads did). Reusing the helper also fixes the
same uvalue unsoundness on the packet/shared signed path.

Tests cover signed and unsigned loads across widths for ctx inline
fields, plus a signed packet load checking that svalue narrows while
uvalue is left unconstrained.

Signed-off-by: Alex Forster <alex@alexforster.com>
Co-Authored-By: Claude <noreply@anthropic.com>

13 of 14 new or added lines in 1 file covered. (92.86%)

9324 of 10747 relevant lines covered (86.76%)

6393562.81 hits per line