vbpf / prevail / 34455346578

87%

push

github

Clamp the uvalue read in shl and lshr to 64 bits

Two more crash sites of the kind #1230 reports, found while reducing it. Adding
one shift to that program aborts the analysis before it ever reaches
assume_signed_32bit_eq:

    r0 <<= 1  ->  CRAB ERROR: Number 18446744075848581120 does not fit into m;
                  function narrow, line 208
    r0 >>= 1  ->  CRAB ERROR: Number 18446744075848581120 does not fit into m;
                  function cast_to, line 258

Same cause: the zone domain's closure derives r0.uvalue <= 2^64 + 0x7f7f0000
from the difference constraint it carries across the outer loop, and both shift
transfer functions take the endpoints of the stored interval as uint64_t without
checking. shl() goes through Interval::pair<uint64_t>(), which uses
Number::narrow and throws outright; lshr() goes through Number::cast_to, which
also accepts the int64_t range but not this.

Read the 64-bit unsigned view of the endpoints instead. The finite_size() test
still runs on the raw interval, so an unbounded uvalue keeps taking the
shl_overflow / full-range paths and nothing else changes: truncate_to<uint64_t>()
is zero_extend(64), the identity on any interval already inside [0, UINT64_MAX].

It also covers a case that was quietly wrong rather than loud: a uvalue whose
lower bound is still negative after a relational join -- the situation
Interval::bitwise_and() already compensates for -- made shl() throw and made
lshr() build an interval with lb > ub, i.e. bottom, from a state that is not
bottom. Zero-extending first turns both into the full unsigned range.

Both new shift.yaml cases fail with the CRAB ERROR above when the source fix is
reverted.

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

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

9026 of 10497 relevant lines covered (85.99%)

3165070.61 hits per line