vbpf / prevail / 28621100060

push

github

Fix unsound signed-division interval abstraction (#1158)

* Fix unsound signed-division interval abstraction

Interval::sdiv and operator/ adjusted the dividend by +1-divisor (or
+divisor+1) before dividing corners, in the branch where neither operand
contains zero. Because Number::operator/ truncates toward zero (matching
eBPF SDIV), this adjustment produced a floored-division hull that could be
disjoint from the true quotient set for a negative dividend and a
non-singleton divisor. For example -8 s/ [5,6] was modeled as [-2,-2] while
the true result is -1, so a subsequent branch guarded by the real value was
judged infeasible and its (reachable) path went unverified.

Truncated division is monotone in each argument on a sign-consistent box, so
the extreme quotients occur at the corners. Divide the original corners
directly in sdiv and operator/; positive and negative/negative boxes were
already exact and are unchanged. udiv keeps the existing adjustment (its
operands are non-negative, so it is unaffected).

* test: cover positive-dividend / negative-divisor signed division

Rounds out sign-combination coverage for the corner-extrema logic, per
automated review feedback.

---------

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

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

9143 of 10573 relevant lines covered (86.47%)

6473387.76 hits per line