[DTrace-devel] Possible (long standing) issue in the BPF verifier?

[Eugene Loh]

I'm confused what problem you're describing here.  Are you saying there 
is an opportunity for the verifier to do better?  Or are you saying that 
the actual computation is incorrect?

So far as I can tell, the actual computation is fine (at least with 
5.15.0).  Specifically, if r4 is assigned 253, 254, 255, 256, and 257, 
then after the +=7 and &=-8 I get 256, 256, 256, 256, and 264, 
respectively.  That looks right.

Now, [7:262] & -8 = [0:256].  So when the verifier bounds the result as 
[0:262], it isn't wrong -- it simply is not as aggressive as it could 
be.  It should be able to bound the result more tightly.  Is that the 
issue you're talking about?

On 4/27/24 21:35, Kris Van Hees wrote:
> So, I found the following in a BPF log on kernel 6.8.0:
>
> BPF: 799: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,smin=smin3
> 2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,smin=smin3
> 2=0,smax=umax=smax32=umax32=255,var_off=(0x0; 0xff))
> BPF: 800: (07) r4 += 7                     ; frame2: R4_w=scalar(smin=umin=smin32=umin32=7,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1ff))
> BPF: 801: (57) r4 &= -8                    ; frame2: R4_w=scalar(smin=smin32=0,smax=umax=smax32=umax32=262,var_off=(0x0; 0x1f8))
>
> And when checking kernel 6.5.0:
>
> BPF: 791: (bf) r4 = r6                     ; frame2: R4_w=scalar(id=8,umax=255,var_off=(0x0; 0xff)) R6_w=scalar(id=8,umax=255,var_off=(0x0; 0xff))
> BPF: 792: (07) r4 += 7                     ; frame2: R4_w=scalar(umin=7,umax=262,var_off=(0x0; 0x1ff))
> BPF: 793: (57) r4 &= -8                    ; frame2: R4_w=scalar(umax=262,var_off=(0x0; 0x1f8))
>
> And kernel 5.15.0:
>
> BPF: 799: (bf) r4 = r6
> BPF: 800: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
> BPF: 800: (07) r4 += 7
> BPF: 801: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umin_value=7,umax_value=262,var_off=(0x0; 0x1ff)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
> BPF: 801: (57) r4 &= -8
> BPF: 802: frame2: R0=inv(id=11,umin_value=1,umax_value=256,var_off=(0x0; 0x1ff)) R4_w=inv(id=0,umax_value=262,var_off=(0x0; 0x1f8)) R6_w=inv(id=12,umax_value=255,var_off=(0x0; 0xff)) R10=fp0 fp-8=map_value fp-16=inv4774451407313060418 fp-24=map_value fp-32=map_value
>
> This code is supposed to round the value in %r4 up to the nearest multiple of
> 8.  So, if %r4 is 255, one would expect this to yield 256.  Yet, it does not.
>