On Mon, May 27, 2024 at 9:10 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Fri, 2024-05-24 at 20:11 -0700, Alexei Starovoitov wrote:
> > From: Alexei Starovoitov <ast@xxxxxxxxxx>
>
> [...]
>
> > With that the get_loop_entry() can be used to gate is_branch_taken() logic.
> > When the verifier sees 'r1 > 1000' inside the loop and it can predict it
> > instead of marking r1 as precise it widens both branches, so r1 becomes
> > [0, 1000] in fallthrough and [1001, UMAX] in other_branch.
> >
> > Consider the loop:
> > bpf_for_each(...) {
> > if (r1 > 1000)
> > break;
> >
> > arr[r1] = ..;
> > }
> > At arr[r1] access the r1 is bounded and the loop can quickly converge.
> >
> > Unfortunately compilers (both GCC and LLVM) often optimize loop exit
> > condition to equality, so
> > for (i = 0; i < 100; i++) arr[i] = 1
> > becomes
> > for (i = 0; i != 100; i++) arr[1] = 1
> >
> > Hence treat != and == conditions specially in the verifier.
> > Widen only not-predicted branch and keep predict branch as is. Example:
> > r1 = 0
> > goto L1
> > L2:
> > arr[r1] = 1
> > r1++
> > L1:
> > if r1 != 100 goto L2
> > fallthrough: r1=100 after widening
> > other_branch: r1 stays as-is (0, 1, 2, ..)
>
> [...]
>
> I'm not sure how much of a deal-breaker this is, but proposed
> heuristics precludes verification for the following program:
not quite.
> char arr[10];
>
> SEC("socket")
> __success __flag(BPF_F_TEST_STATE_FREQ)
> int simple_loop(const void *ctx)
> {
> struct bpf_iter_num it;
> int *v, sum = 0, i = 0;
>
> bpf_iter_num_new(&it, 0, 10);
> while ((v = bpf_iter_num_next(&it))) {
> if (i < 5)
> sum += arr[i++];
> }
> bpf_iter_num_destroy(&it);
> return sum;
> }
>
> The presence of the loop with bpf_iter_num creates a set of states
> with non-null loop_header, which in turn switches-off predictions for
> comparison operations inside the loop.
Is this a pseudo code ?
Because your guess at the reason for the verifier reject is not correct.
It's signed stuff that is causing issues.
s/int i/__u32 i/
and this test is passing the verifier with just 143 insn processed.
> This looks like a bad a compose-ability of verifier features to me.
As with any heuristic there are two steps forward and one step back.
The heuristic is trying to minimize the size of that step back.
If you noticed in v1 and v2 I had to add 'if (!v) break;'
to iter_pragma_unroll_loop().
And it would have been ok this way.
It is a step back for a corner case like iter_pragma_unroll_loop().
Luckily this new algorithm in v3 doesn't need this if (!v) workaround
anymore. So the step back is minimized.
Is it still there? Absolutely. There is a chance that some working prog
will stop working. (as with any verifier change).
> --
>
> Instead of heuristics, maybe rely on hints from the programmer?
> E.g. add a kfunc `u64 bpf_widen(u64)` which will be compiled as an
> identity function, but would instruct verifier to drop precision for a
> specific value. When work on no_caller_saved_registers finishes this
> even could be available w/o runtime cost.
> (And at the moment could be emulated by something like `rX /= 1`).
No way. i = zero is an unpleasant enough workaround.
The verifier precision tracking is not something users understand.
Using i=zero is not pretty, but asking them doing i = bpf_widen(0)
or i = 0; asm("i /= 1") is definitely no go.
The main issue is that users don't know when to do that.
bpf_widen(0) is magic. People will be just guessing.
Just like i=zero is magical.
All such magic has to go. The users should write normal C.
