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

[Eduard Zingerman <eddyz87@gmail.com>]

On Sat, 2026-03-07 at 01:01 +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}
>         /* __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. Without this refactoring, the test
> "verifier_bounds/bounds deduction cross sign boundary, negative
> overlap" fails when removing one call to __reg_deduce_bounds. This
> patch therefore implements that bit of refactoring and reverts commit
> 5dbb19b16ac49 ("bpf: Add third round of bounds deduction").
>
> In some cases, this change can even improve precision a little bit, as
> illustrated in the new selftest in the next patch.
>
> As expected, this change didn't have any impact on the number of
> instructions processed when running it through the Cilium complexity
> test suite [2].
>
> Link: https://lore.kernel.org/bpf/aIKtSK9LjQXB8FLY@mail.gmail.com/ [1]
> Link: https://pchaigno.github.io/test-verifier-complexity.html [2]
> Acked-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>

I wish we had better names for functions in question, e.g. like in [1].

Since sbmc is all the rage now, I tried to check if new and old
definitions for reg_bounds_sync() function are equivalent.
See [2], where I copied relevant definitions (except for tnum part)
and added a simple test to see if old and new functions compute the
same result. Running this test seem to show some differences, e.g.:

  Values extracted from log:
    s32: [-1741665249,  1482110531]  v_s32=-1202410177
    u32: [ 1358815199,  3092723295]  v_u32=3092557119
    s64: [  -509161414271901871,   9223372036728946880]  v_s64=9223372035652365631
    u64: [  9223372034449554622,  17937582659561010782]  v_u64=9223372035652365631

  Running C code directly:
  input:
    s32: [0x98304c1f, 0x58573643]
    u32: [0x50fddfdf, 0xb857365f]
    s64: [0xf8ef186430fcdf51, 0x7ffffffff88000c0]
    u64: [0x7fffffff70a33cbe, 0xf8ef18643857365e]

  old:
    s32: [0x98304c1f, 0xb857365f]
    u32: [0x98304c1f, 0xb857365f]
    s64: [0x7fffffff98304c1f, 0x7fffffffb857365f]
    u64: [0x7fffffff98304c1f, 0x7fffffffb857365f]

  new:
    s32: [0x98304c1f, 0x58573643]
    u32: [0x70a33cbe, 0xb857365f]
    s64: [0x7fffffff70a33cbe, 0x7fffffffb857365f]
    u64: [0x7fffffff70a33cbe, 0x7fffffffb857365f]

Of-course, I might have some bugs in the test definition, but in case
the definition is correct, I think I'm inclined to agree with Ihor
here. If we can't mathematically prove that the sequence converges in
a fixed number of steps, putting a loop on top of it seem to be a
reasonable thing to do.

[1] https://github.com/eddyz87/bpf/tree/deduce-bounds-reshuffle
[2] https://github.com/eddyz87/deduce-bounds-verif

[...]