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

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

On Fri, Mar 13, 2026 at 10:17:52AM +0800, Shung-Hsi Yu wrote:
> On Thu, Mar 12, 2026 at 07:35:15PM +0100, Paul Chaignon wrote:
> > 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:

[...]

> > 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.
> 
> Perhaps I can try to see if I can come up with a better example, from
> the difference between initial reshuffle vs additional reshuffle.

If you have another example, that'd be great. I tried to convert the
inputs you gave into a selftest, but I'm starting to suspect it's not
possible to reach those inputs.

I initially tried manually. For the first example, the trick was to
write all (or most) jumps needed for the different bounds and then find
the ordering that puts us in the exact case generated with CBMC. After
failing to find that manually, I tried the brute force approach:
generating all ordering of those jumps with a selftest that fails if we
reach the state we're looking for. That also failed.

> 
> The problem is that I'm operating on a simplified assumption of "not
> being able to converage to a fix-point is bad because it could lead to
> bound invariant violation". So taking this chance to ask, does that all
> ties back to is_scalar_branch_taken and reg_set_min_max (or was it
> regs_refine_cond_op) difference?

As Eduard answered, not reaching a fixed point in the refinement doesn't
lead to invariant violations. It's just a missed opportunity to get more
precise bounds. In general, Agni tells us the refinement functions are
sound so if they output ill-formed bounds it's because they were given
ill-formed bounds as input.

> 
> Also, when we fail to reach a fix-point, it does not become a problem
> immediately, but only becomes a invariant violation some where down the
> line when we again do bound deduction?
> 
> I haven't actually look into an invariant violation myself, so details
> are rather hazy. 
> 
> > > [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
> > > 
> > > [...]