Widening is too aggressive

[dthaler]

As @caballa wrote in PR #423:

the problem is that the widening is too aggressive because it jumps directly to -oo or +oo. In ebpf programs we expect that loops are bounded to relatively small numbers so during widening we could jump to smaller numbers (e.g., 1000, 5000, etc) and of course jumping to +oo if convergence is not achieved after few iterations. In this way, we wouldn't give up so early by assuming that arithmetic operations can overflow. In Crab, we call it widening with thresholds and in fact Prevail borrrowed the code (https://github.com/vbpf/ebpf-verifier/blob/main/src/crab/thresholds.hpp) but AFIK the code is unused. That code actually tries to learn some good integers to jump in during widening by looking at the code. But it might be enough something much simpler. It might be enough to change slightly the interval and zones domains to jump to a small (predefined) number of integers before jump to +oo. With that I think we should handle this example.

Before the fix in PR #423, valid programs passed verification, but now fail because of this issue so it is perceived as a regression.

https://github.com/vbpf/ebpf-samples/pull/32 has a sample program that illustrates this (slightly more complex than Jorge's "essense" in PR #423 so that cmake won't unroll the loop).

[dthaler]

This appears to be related to the TODO comment in https://github.com/vbpf/ebpf-verifier/blob/main/src/crab/split_dbm.hpp#L337

[dthaler]

SplitDBM::widen() gives the crab log:

Before widening:
DBM 1
[
    meta_offset=[-4098, 0],
    packet_size=[0, 65534],
    r1.type=number,
    r10.stack_offset=512, r10.type=stack, r10.value=[512, 2147418112],
    r2.type=number, r2.value=[0, 1],
    r3.type=number,
    r4.type=number, r4.value=1,
    s[480...487].value=0, s[488...495].value=0, s[496...503].value=0, s[504...511].value=0]
DBM 2
[
    meta_offset=[-4098, 0],
    packet_size=[0, 65534],
    r1.type=number,
    r10.stack_offset=512, r10.type=stack, r10.value=[512, 2147418112],
    r2.type=number, r2.value=[0, 2],
    r3.type=number,
    r4.type=number, r4.value=1,
    s[480...487].value=0, s[488...495].value=0, s[496...503].value=0, s[504...511].value=0]
Result widening:
[
    meta_offset=[-4098, 0],
    packet_size=[0, 65534],
    r1.type=number,
    r10.stack_offset=512, r10.type=stack, r10.value=[512, 2147418112],
    r2.type=number, r2.value=[0, +oo],
    r3.type=number,
    r4.type=number, r4.value=1,
    s[480...487].value=0, s[488...495].value=0, s[496...503].value=0, s[504...511].value=0]

so [0,1] to {0,2] widens to [0, +oo].