assert(!thread_local_options.assume_assertions || is_bottom()) hit when fuzzing with assume_assertions on

[Alan-Jowett]

ebpf-verifier/src/crab/ebpf_domain.cpp

Line 1437 in 01d26e5

assert(!thread_local_options.assume_assertions || is_bottom());

timeout-dfb7ccfe8977abf66ca5c27e6629a0c50d99601c.zip

0000000000000000 <read_write_packet_start>:
       0:       b7 00 00 00 01 00 00 00 r0 = 1
       1:       61 12 04 00 00 00 00 00 r2 = *(u32 *)(r1 + 4)
       2:       61 11 00 00 00 00 00 00 r1 = *(u32 *)(r1 + 0)
       3:       bf 13 00 00 00 00 00 00 r3 = r1
       4:       07 03 00 00 04 00 00 00 r3 += 4
       5:       2d 23 04 00 00 00 00 00 if r3 > r2 goto +4 <LBB0_2>
       6:       61 12 00 00 00 00 00 00 r2 = *(u32 *)(r1 + 0)
       7:       07 02 00 00 01 00 00 00 r2 += 1
       8:       63 21 00 00 00 00 00 00 *(u32 *)(r1 + 0) = r2
       9:       b7 00 00 00 00 00 00 00 r0 = 0

0000000000000050 <LBB0_2>:
      10:       95 00 00 00 00 00 00 00 exit

Assertion occurs on branch from 5 -> 10.

[elazarg]

I think the entire else branch there (the assertion and the set-to-top action) can be simply removed.

[elazarg]

I can't reproduce it. What flags do you pass?

[Alan-Jowett]

Let me see if I can get it to repro with the check program from this repo instead of verifier_fuzzer tool in our repo.