vbpf / prevail / 29778242089

push

github

Havoc exact-match stack cell on kill (fixes #1202)

`get_overlap_cells` deliberately excludes the exact-match cell (o, size)
because loads handle it separately via `get_cell`. But `kill_and_find_var`
reuses `get_overlap_cells` for the havoc path, so overwriting an exact-match
stack cell with an uninitialized register (ebpf_transformer's pure-havoc
branch) never forgot the cell's value/type. A later aligned load then read
back the stale known value, so the verifier believed a register held a known
scalar while at runtime it was uninitialized garbage -- an accept-unsafe
soundness hole.

Include the exact-match cell in the kill set. Strong-update callers (store,
store_type) re-create and reassign the cell afterward, so they are unaffected;
pure-havoc callers (havoc, havoc_type) now correctly forget it.

Regression test in test-data/stack.yaml: store a known 8-byte value, overwrite
the same slot/width with an uninitialized register, reload, and assert the
value is gone. Confirmed to fail without the fix (stale svalue/uvalue=42
survive) and pass with it.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QRunjNUunuZjp6KiBSZXzt
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

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

9326 of 10749 relevant lines covered (86.76%)

6319021.66 hits per line