On Thu, 2025-07-24 at 16:52 -0700, Eduard Zingerman wrote:
> On Fri, 2025-07-25 at 00:01 +0200, Paul Chaignon wrote:
> > On Thu, Jul 24, 2025 at 12:15:53PM -0700, Eduard Zingerman wrote:
> > > On Thu, 2025-07-24 at 15:43 +0200, Paul Chaignon wrote:
> >
> > [...]
> >
> > > > +SEC("socket")
> > > > +__description("bounds deduction cross sign boundary, negative overlap")
> > > > +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
> > > > +__msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")
> > >
> > > Interesting, note the difference: smin=-655, smin32=-783.
> > > There is a code to infer s32 range from s46 range in this situation in
> > > __reg32_deduce_bounds(), but it looks like a third __reg_deduce_bounds
> > > call is needed to trigger it. E.g. the following patch removes the
> > > difference for me:
> >
> > Hm, I can add the third __reg_deduce_bounds to the first patch in the
> > series. That said, we may want to rethink and optimize reg_bounds_sync
> > in a followup patchset. It's probably worth listing all the inferences
> > we have and their dependencies and see if we can reorganize the
> > subfunctions.
>
> Let's not add third __reg_deduce_bounds yet. After inserting some
> prints and looking more closely at the log, something funny happens at
> instruction #2:
>
> 2: (bc) w6 = (s8)w0
> reg_bounds_sync entry: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
> reg_bounds_sync __update_reg_bounds #1: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
> reg_bounds_sync __reg_deduce_bounds #1: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
> reg_bounds_sync __reg_deduce_bounds #2: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
> reg_bounds_sync __reg_bound_offset: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
> reg_bounds_sync __update_reg_bounds #2: scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
> 3: R0_w=scalar() R6_w=scalar(smin=0,smax=umax=0xffffffff,smin32=-128,smax32=127,var_off=(0x0; 0xffffffff))
>
> It would be good to figure out what happens here.
> That being said, the issue is not related to the patch in question.
> I suggest rephrasing the test to avoid the sign extension above.
>
> [...]
Apologies, I'm being stupid above. The range after sign extension is
perfectly fine.
So, going back to the question of the test cases, here is a relevant
part with debug prints [1]:
7: (1f) r0 -= r6
reg_bounds_sync entry: scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146)
reg_bounds_sync __update_reg_bounds #1: scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146)
__reg32_deduce_bounds #8: scalar(smin=-655,smax=0xeffffeee,smin32=-783,smax32=-146,umin32=0xfffffcf1,umax32=0xffffff6e)
__reg_deduce_mixed_bounds #1: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e)
reg_bounds_sync __reg_deduce_bounds #1: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e)
__reg32_deduce_bounds #7: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e)
__reg32_deduce_bounds #8: scalar(smin=-655,smax=0xeffffeee,umin=umin32=0xfffffcf1, umax=0xffffffffffffff6e,smin32=-783,smax32=-146, umax32=0xffffff6e)
__reg64_deduce_bounds #4: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
__reg_deduce_mixed_bounds #1: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
reg_bounds_sync __reg_deduce_bounds #2: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e)
reg_bounds_sync __reg_bound_offset: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))
reg_bounds_sync __update_reg_bounds #2: scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))
8: R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))
R6=scalar(smin=umin=smin32=umin32=400,smax=umax=smax32=umax32=527,var_off=(0x0; 0x3ff))
Important parts are:
a. "__reg32_deduce_bounds #8" updates umin32 and umax32
b. "__reg_deduce_mixed_bounds #1" updates umin and umax (uses values from a)
c. "__reg64_deduce_bounds #4" updates smax and umin (enabled by b)
Only at this point there is an opportunity to refine smin32 from smin
using rule "__reg32_deduce_bounds #2", because of the conditions for
umin and umax (umin refinement by (c) is crucial).
Your new check is (c).
So, it looks like adding third call to __reg_deduce_bounds() in
reg_bounds_sync() is not wrong and the change is linked to this
patch-set.
As you say, whether there is a better way to organize all these rules
requires further analysis, and is a bit out of scope for this
patch-set.
[1] https://github.com/kernel-patches/bpf/commit/f68d4957204f21caac67d24de40fb66e4618f354
