vbpf / prevail / 22275929647

89%

push

github

Fix soundness bugs in 32-bit comparison handling (#1038)

* Fix soundness bugs in 32-bit comparison handling (#874, #875)

Bug #875: is64 flag was set but never read. Hardcoded 64 replaced with
is64?64:32 in get_signed_intervals and get_unsigned_intervals.

Bug #874: In assume_signed_32bit_eq, lb was incremented but lb_match
(from original lb) was used. Fix: adjust lb_match/ub_match directly
instead of lb.

* Guard against signed overflow in assume_signed_32bit_eq

lb_match += 0x100000000 and ub_match -= 0x100000000 can overflow int64_t
when the 64-bit svalue interval bounds are near INT64_MAX or INT64_MIN.
Add overflow checks before each adjustment; if the adjustment would
overflow, return {} (no constraints = sound overapproximation).

---------

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

18 of 19 new or added lines in 1 file covered. (94.74%)

13149 of 14853 relevant lines covered (88.53%)

4639178.91 hits per line