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

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2026-03-05 at 14:54 +0800, Shung-Hsi Yu wrote:
> On Wed, Mar 04, 2026 at 04:48:43PM -0800, Ihor Solodrai wrote:
> > On 3/3/26 11:27 AM, 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}
> > >         /* __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}
> [...]
> > Hi Paul,
> > 
> > (trying to do my part with the code reviews and learn in the process)
> 
> +1, still
> 
> > Side note: you might be interested to know that Eduard is working on
> > consolidating signed and unsigned domains [1].
> 
> \o/
> 
> When I last look into this[1] there's was the "Interval Analysis and
> Machine Arithmetic: Why Signedness Ignorance Is Bliss" paper[2] that
> looks rather promising. And lately there was also "Program Analysis
> Combining Generalized Bit-Level and Word-Level Abstractions"[3] (haven't
> read) that seems more specific to BPF verifier.

Thank you for the links, I've only seen [1].
I was about to send [a], feeling really smug about cbmc tests.
But then a much simpler solution [b] occurred when figuring out why
64-bit test can't be written.

I'll probably continue playing with cnums at leisure pace.

[a] https://github.com/eddyz87/bpf/tree/cnum-sync-bounds
[b] https://github.com/eddyz87/bpf/tree/32-bit-range-overflow