On Tue, Jul 14, 2026 at 12:31:38PM +0800, Shung-Hsi Yu wrote:
...
> > > var_off = (s64)reg->var_off.value;
> > > if (var_off >= BPF_MAX_VAR_OFF || var_off <= -BPF_MAX_VAR_OFF)
> >
> > This should hold already.
>
> FWIW, I had thought so, but after checking I realize that the verifier
> only ensure that
>
> -BPF_MAX_VAR_OFF < smin < BPF_MAX_VAR_OFF
>
> holds true in check_reg_sane_offset_{scalar,ptr}(), and does not check
> smax, so technically var_off.value can be greater than BPF_MAX_VAR_OFF
> when we reach here...
Scratch that, it cannot. Below just shows that (var_off.value |
var_off.mask) can be greater than BPF_MAX_VAR_OFF, not var_off.value.
So what Eduard said is correct, and
-BPF_MAX_VAR_OFF < var_off.value < BPF_MAX_VAR_OFF
does always hold.
> ..., just that it doesn't really matter much as it is
> rejected anyway. And if it is a constant then smin=smax, so for a
> constant value it does always falls between +-BPF_MAX_VAR_OFF.
>
> 0: (79) r6 = *(u64 *)(r1 +0) ; R1=ctx() R6=tp_buffer()
> 1: (85) call bpf_get_prandom_u32#7 ; R0=scalar()
> 2: (bf) r2 = r0 ; R0=scalar(id=1) R2=scalar(id=1)
> 3: (67) r2 <<= 32 ;
> R2=scalar(smax=0x7fffffff00000000,smin32=0,smax32=umax32=0,var_off=(0x0;
> 0xffffffff00000000))
> 4: (77) r2 >>= 32 ;
> R2=scalar(smin=0,smax=umax=0xffffffff,var_off=(0x0; 0xffffffff))
> 5: (07) r2 += 536870911 ;
> R2=scalar(smin=umin=0x1fffffff,smax=umax=0x11ffffffe,var_off=(0x0;
> 0x1ffffffff))
> /* r2 is now [2^29 - 1, 2^32 + 2^29 - 2] */
> 6: (0f) r6 += r2
> 7: R2=scalar(smin=umin=0x1fffffff,smax=umax=0x11ffffffe,var_off=(0x0;
> 0x1ffffffff))
> R6=tp_buffer(smin=umin=0x1fffffff,smax=umax=0x11ffffffe,var_off=(0x0;
> 0x1ffffffff))
> 7: (79) r0 = *(u64 *)(r6 +0)
> R6 invalid variable buffer offset: off=0, var_off=(0x0; 0x1ffffffff)
>
[...]
