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

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

On Tue, Mar 10, 2026 at 12:45:39PM -0700, Eduard Zingerman wrote:
> On Tue, 2026-03-10 at 15:56 +0800, Shung-Hsi Yu wrote:
> 
> [...]
> 
> > Agree that perhaps we still need to keep 3 rounds of deduction after
> > poking at this further.
> > 
> > I tried to run an updated cbmc script[a], manually editing the file to
> > change the number of __reg_deduce_bounds calls made, and check whether
> > an extra call would further change reg_state. For
> > __reg_deduce_bounds_old, it needs 3 calls to pass verification, and for
> > __reg_deduce_bounds_new, it still needs 3.
> 
> Using the same logic I played with orderings a bit:
> - For new ordering 3 and 4 deduction rounds are proven to be identical.
> - For ordering in [1] 2 and 3 deduction rounds are proven to be identical,

Nice!

>   1 round is not enough.
> 
> So, I think [2] is the way to go:
> 
> static void __reg_deduce_bounds(struct bpf_reg_state *reg)
> {
>         deduce_bounds_64_from_64(reg);
>         deduce_bounds_32_from_64(reg);
>         deduce_bounds_32_from_32(reg);
>         deduce_bounds_64_from_32(reg);
> }
> 
> With __reg_deduce_bounds() done 2 times.

Thanks Eduard and Shung-Hsi for the amazing reviews and contributions!
I'll send a v3 with:
1. The renaming commit from Eduard.
2. The initial reshuffle + additional reshuffle from [1].
3. The removal of one __reg_deduce_bounds.
4. The selftest and I'll see if I can craft a second selftest from the
   new inputs you shared Shung-Hsi.

> 
> [1] https://github.com/eddyz87/deduce-bounds-verif/blob/76755f763f9282b74ca4e2251f83767502a98e5e/deduce_bounds_new.c#L321
> [2] https://github.com/eddyz87/bpf/tree/deduce-bounds-reshuffle
> 
> [...]