On 1/4/24 16:30, Barret Rhoden wrote:
[snip]
The LLVM bpf backend has made some improvement to handle the case like
r1 = ...
r2 = r1 + 1
if (r2 < num) ...
using r1
by preventing generating the above code pattern.
The implementation is a pattern matching style so surely it won't be
able to cover all cases.
Do you have specific examples which has verification failure due to
false array out of bound access?
[ snip ]
I'll play around and see if I can come up with a selftest that can run
into any of these "you did the check, but threw the check away" scenarios.
I got an example for this, and will include it in my next patch version,
which I'll CC you on.
If we can get the compiler to spill the register r1 to the stack (L11 in
the asm below), it might spill it before doing the bounds check. Then
it checks the register (L12), but the verifier doesn't know that applies
to the stack variable too. Later, we refill r1 from the stack (L21).
The reason for the spill was that I made another bpf_map_lookup_elem()
call (L19), which needed r1 as an argument.
11: (63) *(u32 *)(r10 -8) = r1 ;
R1=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff)) R10=fp0
fp-8=????scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
12: (35) if r1 >= 0x64 goto pc+13 ;
R1=scalar(smin=smin32=0,smax=umax=smax32=umax32=99,var_off=(0x0; 0x7f))
13: (b4) w1 = 0 ; R1_w=0
14: (63) *(u32 *)(r10 -4) = r1 ; R1_w=0 R10=fp0 fp-8=0000mmmm
15: (bf) r2 = r10 ; R2_w=fp0 R10=fp0
16: (07) r2 += -4 ; R2_w=fp-4
17: (18) r1 = 0xffffc9000011edf0 ;
R1_w=map_ptr(map=arraymap,ks=4,vs=400)
19: (85) call bpf_map_lookup_elem#1 ;
R0_w=map_value_or_null(id=2,map=arraymap,ks=4,vs=400)
20: (15) if r0 == 0x0 goto pc+5 ;
R0_w=map_value(map=arraymap,ks=4,vs=400)
21: (61) r1 = *(u32 *)(r10 -8) ;
R1_w=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
R10=fp0 fp-8=mmmmmmmm
Thanks,
Barret
