Make prime conformance test pass

[dthaler]

Fixes #416

prime.data now returns either true or false, passing verification.
The best answer would be to know it always returns true, but it is at least not unsafe now.

Signed-off-by: Dave Thaler dthaler@microsoft.com

[coveralls]

Coverage increased (+0.08%) to 84.49% when pulling 5c03762 on dthaler:prime-test into 012f13f on vbpf:main.

[caballa]

The fix looks good to me. You probably need to do the same for the narrowing phase (https://github.com/vbpf/ebpf-verifier/blob/main/src/crab/fwd_analyzer.cpp#L206) but I would try to debug first. Probably in this case the analyzer won't be unsound but it might not be effective.

The reason why took me longer to reply was to see why the analyzer cannot prove the program. See next message

[caballa]

This is the essence of the program:

    x = 2;
L:  x++;
    if (x u< 67) goto L else exit

After widening we infer that x=[2,oo]. Then, since we try to model machine arithmetic after the increment we assume that x can overflow so we lose the lower bound. What it's surprising to me is that the transfer function for x u< 67 doesn't take any effect. We would cover the case for x u<= 67 (see https://github.com/vbpf/ebpf-verifier/blob/main/src/crab/ebpf_domain.cpp#L197) but not the strict inequality.

In any case, 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.

[dthaler]

@elazarg any idea why the analyze pass failed? The error looks unrelated to this PR.

[dthaler]

@elazarg any idea why the analyze pass failed? The error looks unrelated to this PR.

Looks to be due to this change in Linux: https://stackoverflow.com/questions/71454588/minsigstksz-error-after-update-in-my-manjaro-linux and covered by catch2 here: catchorg/Catch2#2421

[dthaler]

@elazarg Ok I fixed the analyze problem with catch2 by updating to use the latest header which fixed both this issue and the one you previously had to work around by editing catch.hpp. Anything else needed before merging?