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

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

On Thu, Mar 05, 2026 at 02:54:07PM +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}

[...]

> > If I understand correctly from the pseudocode there is a dependency
> > loop between *64 -> *32 -> *64 -> *32 -> ... and so on.
> > 
> > This got me curious, why don't we actually try to compute a fixed
> > point here with a loop? If we were, we wouldn't have to guess how many
> > iterations need to be there, and the order of the narrowing steps.
> > 
> > So I implemented a dumb loop in reg_bounds_sync() with a limit, and
> > added global counters to collect stats. Pasting a (mostly vibe-coded,
> > sorry) patch at the bottom.
> [...]
> >   $ grep bounds_sync tools/testing/selftests/bpf/veristat.log | grep -o 'max_iters.*' | sort -u
> >   max_iters 2 avg_iters 0.09
> >   max_iters 2 avg_iters 0.10
> >   max_iters 2 avg_iters 0.11
> > 
> > This is across 400+ progs of various sizes. The vast majority of
> > reg_bounds_sync() calls don't change anything (0 iterations), and
> > those that do converge in max 2 iterations.
> > 
> > My interpretation of this (assuming I haven't messed up anything while
> > experimenting) is that the situation you hit in [2] is rare. And I think
> > it is safe to implement a loop in reg_bounds_sync() with a reasonable
> > iteration limit (10 maybe?).
> > 
> > Am I missing anything that makes it a bad idea?
> 
> My (limited) understand that this would make verification of BPF
> verifier with Agni[4] much harder, because it have to unrolls all
> loops & branch based on the result. Having known number of calls and
> no limited makes verification easy. Paul and Harishankar has a much
> better understand there.

That should be fine actually. Agni doesn't verify reg_bounds_sync as a
whole anymore. It follows a divide-and-conqueer approach and verifies
each subfunction independently [1]. So as long as the subfunctions are
individually sound, we should be fine and having a loop shouldn't even
impact Agni's runtime.

1 - https://lpc.events/event/18/contributions/1937/

> 
> From a conceptual view, we're trading always the understanding of
> fix-point convergence (or the potential to understand it); with a loop
> subtle difference will be hidden away. Might be reasonable as a
> security-hardening tactic, but seem to hurt the codebase on the long
> run. That's my 2 cent.

I think I agree with Shung-Hsi here. I'm not against using a loop to
ensure we always have the right number of iterations, but I wonder if
that would be over-engineering it a bit. And as Shung-Hsi pointed out,
once we have a loop, we lose the opportunity to identify optimizations
as I did here.

The one upside I see to the loop is avoiding unnecessary refinements
(the 0 iteration cases). But maybe there's an easier way to detect those
cases? And even then, do we care that much? I noticed the impact of one
more iteration is very small—I couldn't measure it on the runtime.

> 
> 1: https://lore.kernel.org/all/ZTZxoDJJbX9mrQ9w@u94a/
> 2: https://doi.org/10.1145/2651360
> 3: https://doi.org/10.1145/3728905
> 4: https://github.com/bpfverif/agni
> 
> [...]