Re: [PATCH bpf-next] bpf: Simplify bounds refinement from s32

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

On Fri, Jul 25, 2025 at 05:21:38PM +0800, Shung-Hsi Yu wrote:
> On Thu, Jul 24, 2025 at 02:49:47PM -0700, Eduard Zingerman wrote:
> > On Thu, 2025-07-24 at 19:42 +0200, Paul Chaignon wrote:
> > > During the bounds refinement, we improve the precision of various ranges
> > > by looking at other ranges. Among others, we improve the following in
> > > this order (other things happen between 1 and 2):
> > > 
> > >   1. Improve u32 from s32 in __reg32_deduce_bounds.
> > >   2. Improve s/u64 from u32 in __reg_deduce_mixed_bounds.
> > >   3. Improve s/u64 from s32 in __reg_deduce_mixed_bounds.
> > > 
> > > In particular, if the s32 range forms a valid u32 range, we will use it
> > > to improve the u32 range in __reg32_deduce_bounds. In
> > > __reg_deduce_mixed_bounds, under the same condition, we will use the s32
> > > range to improve the s/u64 ranges.
> > > 
> > > If at (1) we were able to learn from s32 to improve u32, we'll then be
> > > able to use that in (2) to improve s/u64. Hence, as (3) happens under
> > > the same precondition as (1), it won't improve s/u64 ranges further than
> > > (1)+(2) did. Thus, we can get rid of (3).
> > > 
> > > In addition to the extensive suite of selftests for bounds refinement,
> > > this patch was also tested with the Agni formal verification tool [1].
> > > 
> > > Link: https://github.com/bpfverif/agni [1]
> > > Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
> > > ---
> > 
> > So, the argument appears to be as follows:
> > 
> > Under precondition `(u32)reg->s32_min <= (u32)reg->s32_max`
> > __reg32_deduce_bounds produces:
> > 
> >   reg->u32_min = max_t(u32, reg->s32_min, reg->u32_min);
> >   reg->u32_max = min_t(u32, reg->s32_max, reg->u32_max);
> > 
> > And then first part of __reg_deduce_mixed_bounds assigns:
> > 
> >   a. reg->umin umax= (reg->umin & ~0xffffffffULL) | max_t(u32, reg->s32_min, reg->u32_min);
> >   b. reg->umax umin= (reg->umax & ~0xffffffffULL) | min_t(u32, reg->s32_max, reg->u32_max);
> > 
> > And then second part of __reg_deduce_mixed_bounds assigns:
> > 
> >   c. reg->umin umax= (reg->umin & ~0xffffffffULL) | (u32)reg->s32_min;
> >   d. reg->umax umin= (reg->umax & ~0xffffffffULL) | (u32)reg->s32_max;
> > 
> > But assignment (c) is a noop because:
> > 
> >    max_t(u32, reg->s32_min, reg->u32_min) >= (u32)reg->s32_min
> > 
> > Hence RHS(a) >= RHS(c) and umin= does nothing.
> > 
> > Also assignment (d) is a noop because:
> > 
> >   min_t(u32, reg->s32_max, reg->u32_max) <= (u32)reg->s32_max
> > 
> > Hence RHS(b) <= RHS(d) and umin= does nothing.
> > 
> > Plus the same reasoning for the part dealing with reg->s{min,max}_value:
> > 
> >   e. reg->smin_value smax= (reg->smin_value & ~0xffffffffULL) | max_t(u32, reg->s32_min_value, reg->u32_min_value);
> >   f. reg->smax_value smin= (reg->smax_value & ~0xffffffffULL) | min_t(u32, reg->s32_max_value, reg->u32_max_value);
> > 
> >     vs
> > 
> >   g. reg->smin_value smax= (reg->smin_value & ~0xffffffffULL) | (u32)reg->s32_min_value;
> >   h. reg->smax_value smin= (reg->smax_value & ~0xffffffffULL) | (u32)reg->s32_max_value;
> > 
> >     RHS(e) >= RHS(g) and RHS(f) <= RHS(h), hence smax=,smin= do nothing.
> > 
> > This appears to be correct.
> > 
> > Shung-Hsi, wdyt?
> 
> Agree with the reasoning above, it looks solid.
> 
> Beside going through the reasoning, I also played with CBMC a bit to
> double check that as far as a single run of __reg_deduce_bounds() is
> concerned (and that the register state matches certain handwavy
> expectations), the change indeed still preserve the original behavior.

Ah, I didn't even think about checking input-output equivalence. Thanks
for testing this!

> 
> Reviewed-by: Shung-Hsi Yu <shung-hsi.yu@suse.com>
> 
> Simplification of bound deduction logic! \o/

Yeah, I'll admit it felt too good to be true :')
I feel more confident with both of your reviews. Thank you both for
reviewing this closely!

[...]