vbpf / prevail / 30096987245

Build # 30096987245

Build Type

push

github

Committed by web-flow

Commit Message

Handle out-of-bounds negative stack offset without crashing (fixes #1211) (#1212)

A stack access at a negative constant offset (a stack pointer walked below its
frame) crashed the verifier with an uncaught InternalError instead of rejecting
the out-of-bounds access:

    CRAB ERROR: Number -8 does not fit into m; function narrow, line 208

The strong-update path narrows the byte offset to the unsigned cell-offset type
Index (uint64_t): `n->narrow<Index>()` in both `kill_and_find_var` (used by
havoc/havoc_type/store/store_type) and `split_number_var`. A negative singleton
offset does not fit an unsigned type, so narrow throws and aborts the whole
analysis -- a robustness/DoS hole on adversarial input.

Guard the constant-offset path with `n->fits<Index>()`, exactly the condition
under which the narrow is safe. A negative offset has no corresponding stack
cell, so the cell bookkeeping is skipped and the out-of-bounds access is left
for the assertion checker to reject. Verified end-to-end that the crash becomes
a clean rejection ("Lower bound must be at least
r10.stack_offset - subprogram_stack_size") rather than a silent accept.

Regression test in test_array_domain.cpp drives store_type/havoc_type/havoc/
store with a negative singleton offset and asserts no throw and that the
in-bounds cell is untouched; it throws the InternalError without the fix.

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>

* Don't route negative constant stack offsets through symbolic kill (

Addresses review feedback. The guard only prevented the narrow
crash: a negative singleton offset left `res` empty and fell through to the
symbolic kill path, which builds the inclusive range `ii | (ii + elem_size)`
(e.g. [-8, 0]). That range overlaps the tracked cell [0, 8) at the shared
endpoint 0, so a havoc/store at a negative offset erased th... (continued)

Coverage Stats

9326 of 10749 relevant lines covered (86.76%)

6319078.39 hits per line

Source File

Press 'n' to go to next uncovered line, 'b' for previous

Source Not Available