vbpf / prevail / 26711049670

86%

push

github

Havoc offsets on non-singleton-typeset pointer add/sub

When the destination register of an `add`/`sub` carries a non-singleton
typeset (two or more simultaneously possible pointer types, e.g. at a join
where the same register may be a context or shared pointer),
`primary_kind_variable_for_type` returns `nullopt` because there is no single
offset variable to update. Previously the offset update was silently skipped
while `svalue`/`uvalue` were still advanced, leaving the offset variables
stale. Subsequent `valid_access` checks then used the pre-arithmetic offset
and accepted out-of-bounds memory accesses, so a crafted program could pass
verification despite performing an OOB read/write.

Conservatively invalidate all offset variables (`havoc_offsets`) in this case,
mirroring the existing pattern in `shl()`/`lshr()`/`ashr()`. The same gap
existed on the register-register subtract path; both are fixed.

A `{number, pointer}` union has the same defect on a different path: it takes
the numeric `may_have_type(T_NUM)` fast-path, which advances `svalue`/`uvalue`
but never updates the pointer offset, again leaving it stale. Invalidate the
pointer offsets there too when the destination is not purely numeric.

Adds regression tests for the add, subtract, and {number, pointer} paths, plus
a companion showing a non-singleton register accessed in bounds still passes.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

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

8997 of 10417 relevant lines covered (86.37%)

6413903.77 hits per line