Assertion failed: !intv.is_bottom(), file E:\ebpf-verifier\src\crab\split_dbm.cpp, line 953

[Alan-Jowett]

Test case:

test-case: repro

pre: [r0.type=number]

code:
  <start>: |
    if r0 s< 0x8000 goto <exit>
    r0 %= 0x808
  <exit>: |
    exit

post:
  - r0.type=number

This was found while fuzzing using uBPF libfuzzer. Issue appears to be in the mod operation.

[Alan-Jowett]

Some more debugging info:
Range for r0 at start of "r0 %= 0x808" = [32768, 9223372036854775807]
Lower bound: dividend=32768, divisor=2056
Upper bound: dividend=9223372036854775807, divisor=2056

Resulting range:
[1928,1927]

Which turns into bottom.

[Alan-Jowett]

A more complete test case:

---
test-case: Inverted range after modulo

pre: [r0.type=number]

code:
  <start>: |
    if r0 s< 0x8000 goto <reset>
    r0 %= 0x808 
    goto <exit>
  <reset>: |
    r0 = 0
  <exit>: |
    exit

post:
  - r0.type=number
  - r0.svalue=[0, 2055]
  - r0.uvalue=[0, 2055]
  - r0.svalue=r0.uvalue

The issues are:

1. This asserts.
2. It ends up with the wrong range afterwards. It claims that r0=2055 is not possible, when it clearly is.