Re: [PATCH bpf-next 1/1] bpf: Avoid one round of bounds deduction

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

On Fri, Mar 06, 2026 at 12:14:01PM +0800, Shung-Hsi Yu wrote:
> On Tue, Mar 03, 2026 at 08:27:20PM +0100, Paul Chaignon wrote:
> > In commit 5dbb19b16ac49 ("bpf: Add third round of bounds deduction"), I
> > added a new round of bounds deduction because two rounds were not enough
> > to converge to a fixed point. This commit slightly refactor the bounds
> > deduction logic such that two rounds are enough.
> > 
> > In [1], Eduard noticed that after we improved the refinement logic, a
> > third call to the bounds deduction (__reg_deduce_bounds) was needed to
> > converge to a fixed point. More specifically, we needed this third call
> > to improve the s64 range using the s32 range. We added the third call
> > and postponed a more detailed analysis of the refinement logic.
> > 
> > I've been looking into this more recently. To help, I wrote a high level
> > sequence of all the refinements carried out in reg_bounds_sync. u64 ->
> > s32 means we used the u64 ranges to improve the s32 ranges.
> > 
> >     /* __update_reg_bounds: */
> >     tnum -> {s32, u32, s64, u64}
> >     /* __reg_deduce_bounds: */
> >     for (3 times) {
> >         /* __reg32_deduce_bounds: */
> >         u64 -> {u32, s32}
> >         s64 -> {u32, s32}
> >         u64 -> s32
> >         s64 -> s32
> >         u32 -> s32
> >         s32 -> u32
> >         /* __reg64_deduce_bounds: */
> >         u64 -> s64
> >         s64 -> u64
> >         {u64, s64} -> {u64, s64}
> 
> Nit picking: my mind read the above with bashism and at first thought it
> expands to the following:
> 
>         /* __reg64_deduce_bounds: */
>         u64 -> s64
>         s64 -> u64
>         u64 -> u64
>         u64 -> s64
>         s64 -> u64
>         s64 -> s64
> 
> But on a second look I do get that we're {u64, s64} means we're
> combining knowledge in both u64 and s64.

Yeah, it's not a very formal write up. I just used it to have a
high-level of the sequence of refinements. I'll switch this to u64+s64
in the v2; hopefully it's a bit clearer.

> 
> >         /* __reg_deduce_mixed_bounds: */
> >         u32 -> u64
> >         u32 -> s64
> >         {s32, s64} -> {s64, u64, tnum}
> >     }
> >     /* __reg_bound_offset: */
> >     {u64, u32} -> tnum
> >     /* __update_reg_bounds: */
> >     tnum -> {s32, u32, s64, u64}
> > 
> > From this, we can observe that we first improve the 32bit ranges from
> > the 64bit ranges in __reg32_deduce_bounds, then improve the 64bit
> > ranges on their own in __reg64_deduce_bounds. Intuitively, if we were to
> > improve the 64bit ranges on their own *before* we use them to improve
> > the 32bit ranges, we may reach a fixed point earlier. Said otherwise, we
> > would need to move the *64 -> *32 refinements to the beginning of
> > __reg_deduce_mixed_bounds. (The logic would then also better match the
> > function names, but that's secondary.)
> > 
> > After testing, this small refactoring does allow us to lose one call to
> > __reg_deduce_bounds.
> [...]
> 
> I poked at this patch with CBMC[1] because I was curious how much worse
> off it might be compared to the old one, but the first counter-example
> CBMC give me actually shows that it is possible for the new version to
> perform better despite loosing one call to __reg_deduce_bounds.
> 
> Given that it is possible new version perform better (at least for one
> case, with caveat that such case may not be representative) with one
> less  __reg_deduce_bounds, and that we used to do just two rounds of
> __reg_deduce_bounds anyway, I believe this patch is good.
> 
> Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> 
> 
> The improvement seems to come from making sure *64 is the tightest
> possible first (with __reg64_deduce_bounds) before using the knowledge
> there to improve *32.
> 
> The counter-example that I got enters reg_bounds_sync with:
> (I have no idea if this represents an actual register state that is
> possible to encounter, and it is rather suspicious that that smin is a
> value that is not within tnum/var_off)
> 
>   reg.var_off.value=2
>   reg.var_off.mask=0x8000000000000001 (10000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)
>   reg.smin_value=0xfffffffd80000000 (11111111 11111111 11111111 11111101 10000000 00000000 00000000 00000000)
>   reg.smax_value=2
>   reg.umin_value=2
>   reg.umax_value=19
>   reg.s32_min_value=2
>   reg.s32_max_value=3
>   reg.u32_min_value=2
>   reg.u32_max_value=3

Thanks a lot for the review and the detailed analysis! I also initially
doubted that it could be reproduced in a program, but gave it a try
anyway. The v2 includes a selftest that reproduces this (with a
slightly different value on smin). I added you as a co-author; please
give me a shout if I shouldn't have.

The tnum does look suspicious but my intuition was that it doesn't
actually matter to the reproduction. So it's just a matter of reaching
those *32 and *64 values. The v2 selftest details how to get to that,
but the difficulty was mostly to find the right sequence of bounds
checks to not trigger refinement too early.

So this demonstrates that the patch not only avoids one round of bounds
deduction, but does so while improving precision in some cases! I wasn't
expecting that. Thanks!

[...]

> Haven't check whether Eduard's latest u32/s32 bounds refinement patch
> makes any difference. Likely not.

Eduard's patch shouldn't make any difference as the u32 and s32 ranges
are equal and therefore one can't be used to improve the other.

> 
> 
> We also likely want to retain *64 knowledge final block of
> __reg_deduce_mixed_bounds with min_t/max_t as precautionary measure, but
> that is orthogonal to your patch here.
> 
> 
> 1: https://github.com/shunghsiyu/reg_bounds_sync-review/