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@xxxxxxxxx> > > > --- > > > > 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@xxxxxxxx> > > 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! [...]
