vbpf / prevail / 34455208272

87%

push

github

Clamp the svalue read in assume_signed_32bit_eq to 64 bits (#1230)

The reported program aborted the analysis with

    CRAB ERROR: Number 18446744075848581120 does not fit into l

18446744075848581120 is 2^64 + 0x7f7f0000. It is not a value any register can
hold; it is what the zone domain's closure derives for r0.svalue at the head of
the outer loop, from the two facts it does hold there:

    r0.svalue - r1.uvalue <= 18446744073701163008   (2^64 - 8388608)
    r1.uvalue <= 2147418112

Zone weights are unbounded `Number`s, so that sum is a legitimate, sound bound.
It is simply weaker than INT64_MAX and therefore not representable.

Every other consumer of a register interval gets a 64-bit view: both
get_signed_intervals() and get_unsigned_intervals() end with a
truncate_to<int64_t>() / truncate_to<uint64_t>(). assume_signed_32bit_eq() is
the one helper that re-reads the raw interval, because it needs the 64-bit
svalue (it matches high 32 bits against the compared low 32 bits) rather than
the 32-bit view its caller computed. It then took both endpoints as int64_t
without checking, and threw.

Take the same 64-bit view before reading the endpoints. truncate_to<int64_t>()
is sign_extend(64), which is the identity on any in-range interval and returns
[INT64_MIN, INT64_MAX] for one this wide, so the fix is inert except where the
old code aborted.

The new jump.yaml case is the reporter's instruction sequence with the entry
invariant its ELF produces; it fails with the CRAB ERROR above when the source
fix is reverted. The reporter's object file now passes verification.

Reported-by: fuzzing, https://github.com/vbpf/prevail/issues/1230

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>

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

9026 of 10497 relevant lines covered (85.99%)

3164774.71 hits per line