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).
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:
from 16 to 17: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5)
R7=2 R10=fp0 fp-8=5 fp-16=iter_num(ref_id=1,state=active,depth=3) refs=1
17: R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) R6=scalar(id=5)
R7=2 R10=fp0 fp-8=5 fp-16=iter_num(ref_id=1,state=active,depth=3) refs=1
17: (55) if r0 != 0x0 goto pc+5 ; R0=rdonly_mem(id=6,ref_obj_id=1,sz=4) refs=1
; if (i < five) @ verifier_loops1.c:299
23: (79) r1 = *(u64 *)(r10 -8) ; R1=5 R10=fp0 fp-8=5 refs=1
0-> 24: (3d) if r7 >= r1 goto pc-11 ; R1=5 R7=2 refs=1
24: refs=1
; sum += arr[i++]; @ verifier_loops1.c:300
1-> 25: (bf) r1 = r7 ; R1_w=scalar(id=7,umax=0xfffffffffffffffe)
R7=scalar(id=7,umax=0xfffffffffffffffe) refs=1
26: (67) r1 <<= 3 ; R1_w=scalar(smax=0x7ffffffffffffff8,umax=0xfffffffffffffff8,
smax32=0x7ffffff8,umax32=0xfffffff8,
var_off=(0x0; 0xfffffffffffffff8)) refs=1
27: (18) r2 = 0xffffc90000112000 ; R2_w=map_value(map=verifier.bss,ks=4,vs=80) refs=1
29: (0f) r2 += r1
Note R7 has exact value 2 at point (0) and is widened to
umax=0xfffffffffffffffe at point (1).
Widening happens at the same point as before, but this time src_reg is
widened as well, so there is no upper bound for r7 anymore.
---
diff --git a/tools/testing/selftests/bpf/progs/verifier_loops1.c b/tools/testing/selftests/bpf/progs/verifier_loops1.c
index e07b43b78fd2..0249fb63f18b 100644
--- a/tools/testing/selftests/bpf/progs/verifier_loops1.c
+++ b/tools/testing/selftests/bpf/progs/verifier_loops1.c
@@ -283,4 +283,24 @@ exit_%=: \
: __clobber_all);
}
+unsigned long arr[10];
+
+SEC("socket")
+__success __flag(BPF_F_TEST_STATE_FREQ)
+int simple_loop(const void *ctx)
+{
+ 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++];
+ }
+ bpf_iter_num_destroy(&it);
+ return sum;
+}
+
