On Mon, 2025-06-23 at 00:03 -0400, Harishankar Vishwanathan wrote: > This patch improves the precison of the scalar(32)_min_max_add and > scalar(32)_min_max_sub functions, which update the u(32)min/u(32)_max > ranges for the BPF_ADD and BPF_SUB instructions. We discovered this more > precise operator using a technique we are developing for automatically > synthesizing functions for updating tnums and ranges. > > According to the BPF ISA [1], "Underflow and overflow are allowed during > arithmetic operations, meaning the 64-bit or 32-bit value will wrap". > Our patch leverages the wrap-around semantics of unsigned overflow and > underflow to improve precision. > > Below is an example of our patch for scalar_min_max_add; the idea is > analogous for all four functions. > > There are three cases to consider when adding two u64 ranges [dst_umin, > dst_umax] and [src_umin, src_umax]. Consider a value x in the range > [dst_umin, dst_umax] and another value y in the range [src_umin, > src_umax]. > > (a) No overflow: No addition x + y overflows. This occurs when even the > largest possible sum, i.e., dst_umax + src_umax <= U64_MAX. > > (b) Partial overflow: Some additions x + y overflow. This occurs when > the largest possible sum overflows (dst_umax + src_umax > U64_MAX), but > the smallest possible sum does not overflow (dst_umin + src_umin <= > U64_MAX). > > (c) Full overflow: All additions x + y overflow. This occurs when both > the smallest possible sum and the largest possible sum overflow, i.e., > both (dst_umin + src_umin) and (dst_umax + src_umax) are > U64_MAX. > [...] > Co-developed-by: Matan Shachnai <m.shachnai@xxxxxxxxxxx> > Signed-off-by: Matan Shachnai <m.shachnai@xxxxxxxxxxx> > Co-developed-by: Srinivas Narayana <srinivas.narayana@xxxxxxxxxxx> > Signed-off-by: Srinivas Narayana <srinivas.narayana@xxxxxxxxxxx> > Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@xxxxxxxxxxx> > Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@xxxxxxxxxxx> > Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx> > --- Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx> (Please don't drop acks).
