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> > --- Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx> [...]
