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
