Re: [PATCH] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB

[Eduard Zingerman <eddyz87@gmail.com>]

On Tue, 2025-06-10 at 18:13 -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.
> 
> The current implementation conservatively sets the output bounds to
> unbounded, i.e, [umin=0, umax=U64_MAX], whenever there is *any*
> possibility of overflow, i.e, in cases (b) and (c). Otherwise it
> computes tight bounds as [dst_umin + src_umin, dst_umax + src_umax]:
> 
> if (check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin) ||
>     check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax)) {
> 	*dst_umin = 0;
> 	*dst_umax = U64_MAX;
> }
> 
> Our synthesis-based technique discovered a more precise operator.
> Particularly, in case (c), all possible additions x + y overflow and
> wrap around according to eBPF semantics, and the computation of the
> output range as [dst_umin + src_umin, dst_umax + src_umax] continues to
> work. Only in case (b), do we need to set the output bounds to
> unbounded, i.e., [0, U64_MAX].
> 
> Case (b) can be checked by seeing if the minimum possible sum does *not*
> overflow and the maximum possible sum *does* overflow, and when that
> happens, we set the output to unbounded:
> 
> min_overflow = check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin);
> max_overflow = check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax);
> 
> if (!min_overflow && max_overflow) {
> 	*dst_umin = 0;
> 	*dst_umax = U64_MAX;
> }
> 
> Below is an example eBPF program and the corresponding log from the
> verifier. Before instruction 6, register r3 has bounds
> [0x8000000000000000, U64_MAX].
> 
> The current implementation sets r3's bounds to [0, U64_MAX] after
> instruction r3 += r3, due to conservative overflow handling.
> 
> 0: R1=ctx() R10=fp0
> 0: (18) r3 = 0x8000000000000000       ; R3_w=0x8000000000000000
> 2: (18) r4 = 0x0                      ; R4_w=0
> 4: (87) r4 = -r4                      ; R4_w=scalar()
> 5: (4f) r3 |= r4                      ; R3_w=scalar(smax=-1,umin=0x8000000000000000,var_off=(0x8000000000000000; 0x7fffffffffffffff)) R4_w=scalar()
> 6: (0f) r3 += r3                      ; R3_w=scalar()
> 7: (b7) r0 = 1                        ; R0_w=1
> 8: (95) exit
> 
> With our patch, r3's bounds after instruction 6 are set to a more precise
> [0, 0xfffffffffffffffe].
> 
> ...
> 6: (0f) r3 += r3                      ; R3_w=scalar(umax=0xfffffffffffffffe)
> 7: (b7) r0 = 1                        ; R0_w=1
> 8: (95) exit
> 
> The logic for scalar32_min_max_add is analogous. For the
> scalar(32)_min_max_sub functions, the reasoning is similar but applied
> to detecting underflow instead of overflow.
> 
> We verified the correctness of the new implementations using Agni [3,4].
> 
> We since also discovered that a similar technique has been used to
> calculate output ranges for unsigned interval addition and subtraction
> in Hacker's Delight [2].
> 
> [1] https://docs.kernel.org/bpf/standardization/instruction-set.html
> [2] Hacker's Delight Ch.4-2, Propagating Bounds through Add’s and Subtract’s
> [3] https://github.com/bpfverif/agni
> [4] https://people.cs.rutgers.edu/~sn349/papers/sas24-preprint.pdf
> 
> Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
> Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> ---

Is this patch dictated by mere possibility of improvement or you
observed some C programs that can benefit from the change?

Could you please add selftests covering each overflow / underflow
combination?
Please use same framework as tools/testing/selftests/bpf/progs/verifier_and.c.

[...]