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? [...]
