Re: [PATCH bpf-next v2 3/4] selftests/bpf: Test cross-sign 64bits range refinement

[Paul Chaignon <paul.chaignon@gmail.com>]

On Fri, Jul 25, 2025 at 12:15:18AM -0700, Eduard Zingerman wrote:

[...]

> 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.

Thanks a lot for the full analysis! I've added a patch in the v3 to call
__reg_deduce_bounds a third time. I reused your analysis and trace from
above in the patch description. Note I added you as a co-author; give
me a shout if I shouldn't have.

> 
> 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