On Tue, May 28, 2024 at 7:18 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> On Tue, 2024-05-28 at 18:08 -0700, Eduard Zingerman wrote:
>
> [...]
>
> > > 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.
> >
> > I'm reading through verifier log, will get back shortly.
>
> Ok, so it is a bit more subtle than I thought.
> Comparing verification log for master and v3 here is the state in
> which they diverge and v3 rejects the program:
>
> from 14 to 15: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5) R7=2
> R10=fp0 fp-8=iter_num(ref_id=1,state=active,depth=3) refs=1
> 15: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5)
> R7=2 R10=fp0 fp-8=iter_num(ref_id=1,state=active,depth=3) refs=1
> 15: (55) if r0 != 0x0 goto pc+5 ; R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) refs=1
> ; if (i < 5) @ verifier_loops1.c:298
> 0-> 21: (65) if r7 s> 0x4 goto pc-10 ; R7=2 refs=1
> 21: refs=1
> ; sum += arr[i++]; @ verifier_loops1.c:299
> 1-> 22: (bf) r1 = r7 ; R1_w=scalar(id=7,smax=4) R7=scalar(id=7,smax=4) refs=1
> 2-> 23: (67) r1 <<= 3 ; R1_w=scalar(smax=0x7ffffffffffffff8,
> umax=0xfffffffffffffff8,
> smax32=0x7ffffff8,
> umax32=0xfffffff8,
> var_off=(0x0; 0xfffffffffffffff8)) refs=1
> 24: (18) r2 = 0xffffc900000f6000 ; R2_w=map_value(map=verifier.bss,ks=4,vs=80) refs=1
> 26: (0f) r2 += r1
> mark_precise: frame0: last_idx 26 first_idx 21 subseq_idx -1
> ...
> math between map_value pointer and register with unbounded min value is not allowed
>
> At point (0) the r7 is tracked as 2, at point (1) it is widened by the
> following code in the falltrhough branch processing:
>
> + if (ignore_pred) {
> + if (opcode != BPF_JEQ && opcode != BPF_JNE) {
> + widen_reg(dst_reg);
> + if (has_src_reg)
> + widen_reg(src_reg);
> + }
> + widen_reg(other_dst_reg);
> + if (has_src_reg)
> + widen_reg(other_src_reg);
> + } else {
>
> Here src_reg is a fake register set to 4,
> because comparison instruction is BPF_K it does not get widened.
> So, reg_set_min_max() produces range [-SMIN,+4] for R7.
> And at (2) all goes south because of the "<<" logic.
> Switch to unsigned values helps because umax range is computed
> instead of smax at point (1).
Exactly. Unsigned is the answer (as I mentioned in the previous email).
The heuristic of _not_ doing bounded loop inside open iter
is that step back that may cause pain.
But really, doing bpf_for() { for(i; i < ..;i++) ..}
is asking for trouble, since it's mixing two concepts.
And in this case the compiler is confused too,
since it cannot normalize i < 5 into i != 5 as it would
do for a canonical loop.
>
> However, below is an example where if comparison is BPF_X.
> Note that I obfuscated constant 5 as a volatile variable.
> And here is what happens when verifier rejects the program:
Sounds pretty much like: doctor it hurts when I do that.
> + volatile unsigned long five = 5;
> + unsigned long sum = 0, i = 0;
> + struct bpf_iter_num it;
> + int *v;
> +
> + bpf_iter_num_new(&it, 0, 10);
> + while ((v = bpf_iter_num_next(&it))) {
> + if (i < five)
> + sum += arr[i++];
If you're saying that the verifier should accept that
no matter what then I have to disagree.
Not interested in avoiding issues in programs that
are actively looking to explore a verifier implementation detail.
I'll add this test with __u64 i = 0;
to demo how such mixed loop constructs can be used.
-no_alu32, default and -cpuv4 all pass.
