vbpf / prevail / 30096987245
87%

DEFAULT BRANCH: main
Ran
Jobs 2
Files 79
Run time 1min
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst
coverage: 86.762%. Remained the same
30096987245

push

github

web-flow 
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)

9326 of 10749 relevant lines covered (86.76%)

6319078.39 hits per line

Coverage Regressions

Lines Coverage ∆ File
30
85.16
 0.0% src/crab/array_domain.cpp
Jobs
ID Job ID Ran Files Coverage
1 run-Release - 30096987245.1 79
85.87
 GitHub Action Run
2 run-Debug - 30096987245.2 77
85.03
 GitHub Action Run
Source Files on build 30096987245