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

[Eduard Zingerman <eddyz87@gmail.com>]

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,
  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.

[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

[...]