[PATCH v2 0/2] bpf, verifier: Improve precision of BPF_ADD and BPF_SUB

[PATCH v2 0/2] bpf, verifier: Improve precision of BPF_ADD and BPF_SUB

[Harishankar Vishwanathan]

This patchset improves the precision of BPF_ADD and BPF_SUB range
tracking, and also adds selftests that exercise the precision
improvement.

Changelog:

v2:
* Add clearer example of precision improvement in the commit message for
  verifier.c changes.
* Add selftests that exercise the precision improvement to
  verifier_bounds.c (suggested by Eduard Zingerman).

v1:
  https://lore.kernel.org/bpf/20250610221356.2663491-1-harishankar.vishwanathan@gmail.com/

Harishankar Vishwanathan (2):
  bpf, verifier: Improve precision for BPF_ADD and BPF_SUB
  selftests/bpf: Add testcases for BPF_ADD and BPF_SUB

 kernel/bpf/verifier.c                         | 76 ++++++++++++-----
 .../selftests/bpf/progs/verifier_bounds.c     | 85 +++++++++++++++++++
 2 files changed, 141 insertions(+), 20 deletions(-)

-- 
2.45.2

[PATCH v2 1/2] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB

[Harishankar Vishwanathan]

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. At instruction 7: (0f) r5 += r3, due to conservative overflow
handling, the current implementation of scalar_min_max_add() sets r5's
bounds to [0, U64_MAX], which is then updated by reg_bounds_sync() to
[0x3d67e960f7d, U64_MAX].

0: R1=ctx() R10=fp0
0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
1: (bf) r3 = r0                       ; R0_w=scalar(id=1) R3_w=scalar(id=1)
2: (18) r4 = 0x950a43d67e960f7d       ; R4_w=0x950a43d67e960f7d
4: (4f) r3 |= r4                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R4_w=0x950a43d67e960f7d
5: (18) r5 = 0xc014a00000000000       ; R5_w=0xc014a00000000000
7: (0f) r5 += r3                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R5_w=scalar(smin=0x800003d67e960f7d,umin=0x3d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))
8: (b7) r0 = 0                        ; R0_w=0
9: (95) exit

With our patch, r5's bounds after instruction 7 are set to a much more
precise [0x551ee3d67e960f7d, 0xc0149fffffffffff] by
scalar_min_max_add().

...
7: (0f) r5 += r3                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R5_w=scalar(smin=0x800003d67e960f7d,umin=0x551ee3d67e960f7d,umax=0xc0149fffffffffff,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))
8: (b7) r0 = 0                        ; R0_w=0
9: (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>
---
 kernel/bpf/verifier.c | 76 +++++++++++++++++++++++++++++++------------
 1 file changed, 56 insertions(+), 20 deletions(-)

diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
index 279a64933262..f403524bd215 100644
--- a/kernel/bpf/verifier.c
+++ b/kernel/bpf/verifier.c
@@ -14605,14 +14605,25 @@ static void scalar32_min_max_add(struct bpf_reg_state *dst_reg,
 	s32 *dst_smax = &dst_reg->s32_max_value;
 	u32 *dst_umin = &dst_reg->u32_min_value;
 	u32 *dst_umax = &dst_reg->u32_max_value;
+	u32 umin_val = src_reg->u32_min_value;
+	u32 umax_val = src_reg->u32_max_value;
+	bool min_overflow, max_overflow;
 
 	if (check_add_overflow(*dst_smin, src_reg->s32_min_value, dst_smin) ||
 	    check_add_overflow(*dst_smax, src_reg->s32_max_value, dst_smax)) {
 		*dst_smin = S32_MIN;
 		*dst_smax = S32_MAX;
 	}
-	if (check_add_overflow(*dst_umin, src_reg->u32_min_value, dst_umin) ||
-	    check_add_overflow(*dst_umax, src_reg->u32_max_value, dst_umax)) {
+
+	/* If either all additions overflow or no additions overflow, then
+	 * it is okay to set: dst_umin = dst_umin + src_umin, dst_umax =
+	 * dst_umax + src_umax. Otherwise (some additions overflow), set
+	 * the output bounds to unbounded.
+	 */
+	min_overflow = check_add_overflow(*dst_umin, umin_val, dst_umin);
+	max_overflow = check_add_overflow(*dst_umax, umax_val, dst_umax);
+
+	if (!min_overflow && max_overflow) {
 		*dst_umin = 0;
 		*dst_umax = U32_MAX;
 	}
@@ -14625,14 +14636,25 @@ static void scalar_min_max_add(struct bpf_reg_state *dst_reg,
 	s64 *dst_smax = &dst_reg->smax_value;
 	u64 *dst_umin = &dst_reg->umin_value;
 	u64 *dst_umax = &dst_reg->umax_value;
+	u64 umin_val = src_reg->umin_value;
+	u64 umax_val = src_reg->umax_value;
+	bool min_overflow, max_overflow;
 
 	if (check_add_overflow(*dst_smin, src_reg->smin_value, dst_smin) ||
 	    check_add_overflow(*dst_smax, src_reg->smax_value, dst_smax)) {
 		*dst_smin = S64_MIN;
 		*dst_smax = S64_MAX;
 	}
-	if (check_add_overflow(*dst_umin, src_reg->umin_value, dst_umin) ||
-	    check_add_overflow(*dst_umax, src_reg->umax_value, dst_umax)) {
+
+	/* If either all additions overflow or no additions overflow, then
+	 * it is okay to set: dst_umin = dst_umin + src_umin, dst_umax =
+	 * dst_umax + src_umax. Otherwise (some additions overflow), set
+	 * the output bounds to unbounded.
+	 */
+	min_overflow = check_add_overflow(*dst_umin, umin_val, dst_umin);
+	max_overflow = check_add_overflow(*dst_umax, umax_val, dst_umax);
+
+	if (!min_overflow && max_overflow) {
 		*dst_umin = 0;
 		*dst_umax = U64_MAX;
 	}
@@ -14643,8 +14665,11 @@ static void scalar32_min_max_sub(struct bpf_reg_state *dst_reg,
 {
 	s32 *dst_smin = &dst_reg->s32_min_value;
 	s32 *dst_smax = &dst_reg->s32_max_value;
+	u32 *dst_umin = &dst_reg->u32_min_value;
+	u32 *dst_umax = &dst_reg->u32_max_value;
 	u32 umin_val = src_reg->u32_min_value;
 	u32 umax_val = src_reg->u32_max_value;
+	bool min_underflow, max_underflow;
 
 	if (check_sub_overflow(*dst_smin, src_reg->s32_max_value, dst_smin) ||
 	    check_sub_overflow(*dst_smax, src_reg->s32_min_value, dst_smax)) {
@@ -14652,14 +14677,18 @@ static void scalar32_min_max_sub(struct bpf_reg_state *dst_reg,
 		*dst_smin = S32_MIN;
 		*dst_smax = S32_MAX;
 	}
-	if (dst_reg->u32_min_value < umax_val) {
-		/* Overflow possible, we know nothing */
-		dst_reg->u32_min_value = 0;
-		dst_reg->u32_max_value = U32_MAX;
-	} else {
-		/* Cannot overflow (as long as bounds are consistent) */
-		dst_reg->u32_min_value -= umax_val;
-		dst_reg->u32_max_value -= umin_val;
+
+	/* If either all subtractions underflow or no subtractions
+	 * underflow, it is okay to set: dst_umin = dst_umin - src_umax,
+	 * dst_umax = dst_umax - src_umin. Otherwise (some subtractions
+	 * underflow), set the output bounds to unbounded.
+	 */
+	min_underflow = check_sub_overflow(*dst_umin, umax_val, dst_umin);
+	max_underflow = check_sub_overflow(*dst_umax, umin_val, dst_umax);
+
+	if (min_underflow && !max_underflow) {
+		*dst_umin = 0;
+		*dst_umax = U32_MAX;
 	}
 }
 
@@ -14668,8 +14697,11 @@ static void scalar_min_max_sub(struct bpf_reg_state *dst_reg,
 {
 	s64 *dst_smin = &dst_reg->smin_value;
 	s64 *dst_smax = &dst_reg->smax_value;
+	u64 *dst_umin = &dst_reg->umin_value;
+	u64 *dst_umax = &dst_reg->umax_value;
 	u64 umin_val = src_reg->umin_value;
 	u64 umax_val = src_reg->umax_value;
+	bool min_underflow, max_underflow;
 
 	if (check_sub_overflow(*dst_smin, src_reg->smax_value, dst_smin) ||
 	    check_sub_overflow(*dst_smax, src_reg->smin_value, dst_smax)) {
@@ -14677,14 +14709,18 @@ static void scalar_min_max_sub(struct bpf_reg_state *dst_reg,
 		*dst_smin = S64_MIN;
 		*dst_smax = S64_MAX;
 	}
-	if (dst_reg->umin_value < umax_val) {
-		/* Overflow possible, we know nothing */
-		dst_reg->umin_value = 0;
-		dst_reg->umax_value = U64_MAX;
-	} else {
-		/* Cannot overflow (as long as bounds are consistent) */
-		dst_reg->umin_value -= umax_val;
-		dst_reg->umax_value -= umin_val;
+
+	/* If either all subtractions underflow or no subtractions
+	 * underflow, it is okay to set: dst_umin = dst_umin - src_umax,
+	 * dst_umax = dst_umax - src_umin. Otherwise (some subtractions
+	 * underflow), set the output bounds to unbounded.
+	 */
+	min_underflow = check_sub_overflow(*dst_umin, umax_val, dst_umin);
+	max_underflow = check_sub_overflow(*dst_umax, umin_val, dst_umax);
+
+	if (min_underflow && !max_underflow) {
+		*dst_umin = 0;
+		*dst_umax = U64_MAX;
 	}
 }
 
-- 
2.45.2

[PATCH v2 2/2] selftests/bpf: Add testcases for BPF_ADD and BPF_SUB

[Harishankar Vishwanathan]

The previous commit improves the precision in scalar(32)_min_max_add,
and scalar(32)_min_max_sub. The improvement in precision occurs in
cases when all outcomes overflow or underflow, respectively. This
commit adds selftests that exercise those cases.

Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
---
 .../selftests/bpf/progs/verifier_bounds.c     | 85 +++++++++++++++++++
 1 file changed, 85 insertions(+)

diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c
index 30e16153fdf1..20fb0fef5719 100644
--- a/tools/testing/selftests/bpf/progs/verifier_bounds.c
+++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c
@@ -1371,4 +1371,89 @@ __naked void mult_sign_ovf(void)
 	  __imm(bpf_skb_store_bytes)
 	: __clobber_all);
 }
+
+SEC("socket")
+__description("64-bit addition overflow, all outcomes overflow")
+__success __log_level(2)
+__msg("7: (0f) r5 += r3 {{.*}} R5_w=scalar(smin=0x800003d67e960f7d,umin=0x551ee3d67e960f7d,umax=0xc0149fffffffffff,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))")
+__retval(0)
+__naked void add64_ovf(void)
+{
+	asm volatile (
+	"call %[bpf_get_prandom_u32];"
+	"r3 = r0;"
+	"r4 = 0x950a43d67e960f7d ll;"
+	"r3 |= r4;"
+	"r5 = 0xc014a00000000000 ll;"
+	"r5 += r3;"
+	"r0 = 0;"
+	"exit"
+	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("32-bit addition overflow, all outcomes overflow")
+__success __log_level(2)
+__msg("5: (0c) w5 += w3 {{.*}} R5_w=scalar(smin=umin=umin32=0x20130018,smax=umax=umax32=0x8000ffff,smin32=0x80000018,var_off=(0x18; 0xffffffe7))")
+__retval(0)
+__naked void add32_ovf(void)
+{
+	asm volatile (
+	"call %[bpf_get_prandom_u32];"
+	"r3 = r0;"
+	"w4 = 0xa0120018;"
+	"w3 |= w4;"
+	"w5 = 0x80010000;"
+	"w5 += w3;"
+	"r0 = 0;"
+	"exit"
+	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("64-bit subtraction overflow, all outcomes underflow")
+__success __log_level(2)
+__msg("6: (1f) r3 -= r1 {{.*}} R3_w=scalar(umin=1,umax=0x8000000000000000)")
+__retval(0)
+__naked void sub64_ovf(void)
+{
+	asm volatile (
+	"call %[bpf_get_prandom_u32];"
+	"r1 = r0;"
+	"r2 = 0x8000000000000000 ll;"
+	"r1 |= r2;"
+	"r3 = 0x0;"
+	"r3 -= r1;"
+	"r0 = 0;"
+	"exit"
+	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
+SEC("socket")
+__description("32-bit subtraction overflow, all outcomes underflow")
+__success __log_level(2)
+__msg("5: (1c) w3 -= w1 {{.*}} R3_w=scalar(smin=umin=umin32=1,smax=umax=umax32=0x80000000,var_off=(0x0; 0xffffffff))")
+__retval(0)
+__naked void sub32_ovf(void)
+{
+	asm volatile (
+	"call %[bpf_get_prandom_u32];"
+	"r1 = r0;"
+	"w2 = 0x80000000;"
+	"w1 |= w2;"
+	"r3 = 0x0;"
+	"w3 -= w1;"
+	"r0 = 0;"
+	"exit"
+	:
+	: __imm(bpf_get_prandom_u32)
+	: __clobber_all);
+}
+
 char _license[] SEC("license") = "GPL";
-- 
2.45.2

Re: [PATCH v2 1/2] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB

[Hao Sun]

On Tue, Jun 17, 2025 at 07:17:31PM -0400, Harishankar Vishwanathan wrote:
[...]
> 
> 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].
> 
 
In case anyone is interested, the above (case c) can also be proved by
the following SMT formula directly, which may ease the reasoning here:

```
; ================================================================
;  Unsigned 32- and 64-bit interval addition & subtraction
;  with wrap-around semantics and endpoint overflow / underflow.
; ================================================================
(set-logic ALL)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ----------  u32  (32-bit)  ----------
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const l0_32 (_ BitVec 32))
(declare-const h0_32 (_ BitVec 32))
(declare-const l1_32 (_ BitVec 32))
(declare-const h1_32 (_ BitVec 32))

; Well-formed input ranges
(assert (bvule l0_32 h0_32))
(assert (bvule l1_32 h1_32))

; ----- Addition -----
(define-fun lowSum32  () (_ BitVec 32) (bvadd l0_32 l1_32))
(define-fun highSum32 () (_ BitVec 32) (bvadd h0_32 h1_32))

; Both endpoint sums overflow (wrap) ⇒ result < first addend
(assert (bvult lowSum32  l0_32))
(assert (bvult highSum32 h0_32))

; Soundness of addition
(assert
  (forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
    (=> (and (bvule l0_32 x) (bvule x h0_32)
             (bvule l1_32 y) (bvule y h1_32))
        (and (bvule lowSum32  (bvadd x y))
             (bvule (bvadd x y) highSum32)))))

; ----- Subtraction -----
(define-fun lowDiff32  () (_ BitVec 32) (bvsub l0_32 h1_32))
(define-fun highDiff32 () (_ BitVec 32) (bvsub h0_32 l1_32))

; Both endpoint differences underflow ⇒ result > minuend
(assert (bvugt lowDiff32  l0_32))
(assert (bvugt highDiff32 h0_32))

; Soundness of subtraction
(assert
  (forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
    (=> (and (bvule l0_32 x) (bvule x h0_32)
             (bvule l1_32 y) (bvule y h1_32))
        (and (bvule lowDiff32  (bvsub x y))
             (bvule (bvsub x y) highDiff32)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ----------  u64  (64-bit)  ----------
;; Basically the same as above but for u64
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const l0_64 (_ BitVec 64))
(declare-const h0_64 (_ BitVec 64))
(declare-const l1_64 (_ BitVec 64))
(declare-const h1_64 (_ BitVec 64))

; Well-formed input ranges
(assert (bvule l0_64 h0_64))
(assert (bvule l1_64 h1_64))

; ----- Addition -----
(define-fun lowSum64  () (_ BitVec 64) (bvadd l0_64 l1_64))
(define-fun highSum64 () (_ BitVec 64) (bvadd h0_64 h1_64))

(assert (bvult lowSum64  l0_64))
(assert (bvult highSum64 h0_64))

(assert
  (forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
    (=> (and (bvule l0_64 x) (bvule x h0_64)
             (bvule l1_64 y) (bvule y h1_64))
        (and (bvule lowSum64  (bvadd x y))
             (bvule (bvadd x y) highSum64)))))

; ----- Subtraction -----
(define-fun lowDiff64  () (_ BitVec 64) (bvsub l0_64 h1_64))
(define-fun highDiff64 () (_ BitVec 64) (bvsub h0_64 l1_64))

(assert (bvugt lowDiff64  l0_64))
(assert (bvugt highDiff64 h0_64))

(assert
  (forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
    (=> (and (bvule l0_64 x) (bvule x h0_64)
             (bvule l1_64 y) (bvule y h1_64))
        (and (bvule lowDiff64  (bvsub x y))
             (bvule (bvsub x y) highDiff64)))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(check-sat)
(exit)
```

Both cvc5 and z3 can prove the above, and one can try this and expect
it producing SAT on:
https://cvc5.github.io/app/#temp_a95e25c4-88c5-4257-96c8-0bd74125b179

In addition, the unsoundness of partial case-b can also be proved by
the following formula, and the counter examples generated may be used
as test cases if needed:
https://pastebin.com/raw/qrT7rC1P

Regards
Hao

Re: [PATCH v2 1/2] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB

[Eduard Zingerman]

On Tue, 2025-06-17 at 19:17 -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. At instruction 7: (0f) r5 += r3, due to conservative overflow
> handling, the current implementation of scalar_min_max_add() sets r5's
> bounds to [0, U64_MAX], which is then updated by reg_bounds_sync() to
> [0x3d67e960f7d, U64_MAX].
> 
> 0: R1=ctx() R10=fp0
> 0: (85) call bpf_get_prandom_u32#7    ; R0_w=scalar()
> 1: (bf) r3 = r0                       ; R0_w=scalar(id=1) R3_w=scalar(id=1)
> 2: (18) r4 = 0x950a43d67e960f7d       ; R4_w=0x950a43d67e960f7d
> 4: (4f) r3 |= r4                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R4_w=0x950a43d67e960f7d
> 5: (18) r5 = 0xc014a00000000000       ; R5_w=0xc014a00000000000
> 7: (0f) r5 += r3                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R5_w=scalar(smin=0x800003d67e960f7d,umin=0x3d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))
> 8: (b7) r0 = 0                        ; R0_w=0
> 9: (95) exit
> 
> With our patch, r5's bounds after instruction 7 are set to a much more
> precise [0x551ee3d67e960f7d, 0xc0149fffffffffff] by
> scalar_min_max_add().
> 
> ...
> 7: (0f) r5 += r3                      ; R3_w=scalar(smin=0x950a43d67e960f7d,smax=-1,umin=0x950a43d67e960f7d,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x950a43d67e960f7d; 0x6af5bc298169f082)) R5_w=scalar(smin=0x800003d67e960f7d,umin=0x551ee3d67e960f7d,umax=0xc0149fffffffffff,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))
> 8: (b7) r0 = 0                        ; R0_w=0
> 9: (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>
> ---

Acked-by: Eduard Zingerman <eddyz87@gmail.com>

[...]

Re: [PATCH v2 2/2] selftests/bpf: Add testcases for BPF_ADD and BPF_SUB

[Eduard Zingerman]

On Tue, 2025-06-17 at 19:17 -0400, Harishankar Vishwanathan wrote:
> The previous commit improves the precision in scalar(32)_min_max_add,
> and scalar(32)_min_max_sub. The improvement in precision occurs in
> cases when all outcomes overflow or underflow, respectively. This
> commit adds selftests that exercise those cases.
> 
> Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> ---

Could you please also add test cases when one bound overflows while
another does not? Or these are covered by some other tests?

[...]

> +SEC("socket")
> +__description("64-bit addition overflow, all outcomes overflow")
> +__success __log_level(2)
> +__msg("7: (0f) r5 += r3 {{.*}} R5_w=scalar(smin=0x800003d67e960f7d,umin=0x551ee3d67e960f7d,umax=0xc0149fffffffffff,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))")

Would it be possible to pick some more "human readable" constants here?
As-is it is hard to make sense what verifier actually computes.

> +__retval(0)
> +__naked void add64_ovf(void)
> +{
> +	asm volatile (
> +	"call %[bpf_get_prandom_u32];"
> +	"r3 = r0;"
> +	"r4 = 0x950a43d67e960f7d ll;"
> +	"r3 |= r4;"
> +	"r5 = 0xc014a00000000000 ll;"
> +	"r5 += r3;"
> +	"r0 = 0;"
> +	"exit"
> +	:
> +	: __imm(bpf_get_prandom_u32)
> +	: __clobber_all);
> +}

[...]

Re: [PATCH v2 2/2] selftests/bpf: Add testcases for BPF_ADD and BPF_SUB

[Harishankar Vishwanathan]

On Wed, Jun 18, 2025 at 5:22 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Tue, 2025-06-17 at 19:17 -0400, Harishankar Vishwanathan wrote:
> > The previous commit improves the precision in scalar(32)_min_max_add,
> > and scalar(32)_min_max_sub. The improvement in precision occurs in
> > cases when all outcomes overflow or underflow, respectively. This
> > commit adds selftests that exercise those cases.
> >
> > Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
> > Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> > Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> > ---
>
> Could you please also add test cases when one bound overflows while
> another does not? Or these are covered by some other tests?

Yes this is possible and I can add such test cases. These are not covered by
other tests as far as I can see.

[...]

> > +SEC("socket")
> > +__description("64-bit addition overflow, all outcomes overflow")
> > +__success __log_level(2)
> > +__msg("7: (0f) r5 += r3 {{.*}} R5_w=scalar(smin=0x800003d67e960f7d,umin=0x551ee3d67e960f7d,umax=0xc0149fffffffffff,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))")
>
> Would it be possible to pick some more "human readable" constants here?
> As-is it is hard to make sense what verifier actually computes.
>
> > +__retval(0)
> > +__naked void add64_ovf(void)
> > +{
> > +     asm volatile (
> > +     "call %[bpf_get_prandom_u32];"
> > +     "r3 = r0;"
> > +     "r4 = 0x950a43d67e960f7d ll;"
> > +     "r3 |= r4;"
> > +     "r5 = 0xc014a00000000000 ll;"
> > +     "r5 += r3;"
> > +     "r0 = 0;"
> > +     "exit"
> > +     :
> > +     : __imm(bpf_get_prandom_u32)
> > +     : __clobber_all);
> > +}

It is possible to pick more human readable constants, but the precision gains
might not be as apparent. For instance, with the above (current) test case,
the old scalar_min_max_add() produced
[umin_value=0x3d67e960f7d, umax_value=U64_MAX],
while the updated scalar_min_max_add() produces a much more
precise [0x551ee3d67e960f7d, 0xc0149fffffffffff], a bound that has close to
2**63 fewer inhabitants.

For the purposes of a test case, if human readability is more important
than the demonstration of a large precision gain, I can prefer one that is more
readable, similar to the one shown in the commit message of v1 of the
patch [1]:

With the old scalar_min_max_add(), we get r3's bounds set to unbounded, i.e.,
[0, U64_MAX] after instruction 6: (0f) r3 += r3

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 the new scalar_min_max_add(), we get r3's bounds set to
[0, 0xfffffffffffffffe], a bound that is more precise by having only 1 less
inhabitant.

...
6: (0f) r3 += r3                      ; R3_w=scalar(umax=0xfffffffffffffffe)
7: (b7) r0 = 1                        ; R0_w=1
8: (95) exit

Please advise which test cases to prefer. I will follow up with a v3.

[1]: https://lore.kernel.org/bpf/20250610221356.2663491-1-harishankar.vishwanathan@gmail.com/

[...]

Re: [PATCH v2 2/2] selftests/bpf: Add testcases for BPF_ADD and BPF_SUB

[Eduard Zingerman]

On Thu, 2025-06-19 at 17:13 -0400, Harishankar Vishwanathan wrote:
> On Wed, Jun 18, 2025 at 5:22 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > 
> > On Tue, 2025-06-17 at 19:17 -0400, Harishankar Vishwanathan wrote:
> > > The previous commit improves the precision in scalar(32)_min_max_add,
> > > and scalar(32)_min_max_sub. The improvement in precision occurs in
> > > cases when all outcomes overflow or underflow, respectively. This
> > > commit adds selftests that exercise those cases.
> > > 
> > > Co-developed-by: Matan Shachnai <m.shachnai@rutgers.edu>
> > > Signed-off-by: Matan Shachnai <m.shachnai@rutgers.edu>
> > > Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
> > > ---
> > 
> > Could you please also add test cases when one bound overflows while
> > another does not? Or these are covered by some other tests?
> 
> Yes this is possible and I can add such test cases. These are not covered by
> other tests as far as I can see.

Great, thank you.

> > > +SEC("socket")
> > > +__description("64-bit addition overflow, all outcomes overflow")
> > > +__success __log_level(2)
> > > +__msg("7: (0f) r5 += r3 {{.*}} R5_w=scalar(smin=0x800003d67e960f7d,umin=0x551ee3d67e960f7d,umax=0xc0149fffffffffff,smin32=0xfe960f7d,umin32=0x7e960f7d,var_off=(0x3d67e960f7d; 0xfffffc298169f082))")
> > 
> > Would it be possible to pick some more "human readable" constants here?
> > As-is it is hard to make sense what verifier actually computes.
> > 
> > > +__retval(0)
> > > +__naked void add64_ovf(void)
> > > +{
> > > +     asm volatile (
> > > +     "call %[bpf_get_prandom_u32];"
> > > +     "r3 = r0;"
> > > +     "r4 = 0x950a43d67e960f7d ll;"
> > > +     "r3 |= r4;"
> > > +     "r5 = 0xc014a00000000000 ll;"
> > > +     "r5 += r3;"
> > > +     "r0 = 0;"
> > > +     "exit"
> > > +     :
> > > +     : __imm(bpf_get_prandom_u32)
> > > +     : __clobber_all);
> > > +}
> 
> It is possible to pick more human readable constants, but the precision gains
> might not be as apparent. For instance, with the above (current) test case,
> the old scalar_min_max_add() produced
> [umin_value=0x3d67e960f7d, umax_value=U64_MAX],
> while the updated scalar_min_max_add() produces a much more
> precise [0x551ee3d67e960f7d, 0xc0149fffffffffff], a bound that has close to
> 2**63 fewer inhabitants.
> 
> For the purposes of a test case, if human readability is more important
> than the demonstration of a large precision gain, I can prefer one that is more
> readable, similar to the one shown in the commit message of v1 of the
> patch [1]:
> 
> With the old scalar_min_max_add(), we get r3's bounds set to unbounded, i.e.,
> [0, U64_MAX] after instruction 6: (0f) r3 += r3
> 
> 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 the new scalar_min_max_add(), we get r3's bounds set to
> [0, 0xfffffffffffffffe], a bound that is more precise by having only 1 less
> inhabitant.
> 
> ...
> 6: (0f) r3 += r3                      ; R3_w=scalar(umax=0xfffffffffffffffe)
> 7: (b7) r0 = 1                        ; R0_w=1
> 8: (95) exit
> 
> Please advise which test cases to prefer. I will follow up with a v3.

Hm, I see, that's an interesting angle.
The problem is, if I do something silly changing the code and this
test fails I'd have a hard time understanding the expected output.
Therefore, I'd prefer something more obvious.

Maybe let's go with this:

  SEC("tc")
  __success
  __naked void test1(void)
  {
	asm volatile (
	"r3 = 0xa000000000000000 ll;"
	"r4 = 0x0;"
	"r4 = -r4;"
	"r3 |= r4;"
	"r3 += r3;"
	"r0 = 1;"
	"exit;"
	:
	: __imm(bpf_get_prandom_u32)
	: __clobber_all);
  }

Here is verifier log comparison:

  master: 5: (0f) r3 += r3     ; R3_w=scalar()
  branch: 5: (0f) r3 += r3     ; R3_w=scalar(umin=0x4000000000000000,umax=0xfffffffffffffffe)

?

> [1]: https://lore.kernel.org/bpf/20250610221356.2663491-1-harishankar.vishwanathan@gmail.com/
> 
> [...]

Re: [PATCH v2 1/2] bpf, verifier: Improve precision for BPF_ADD and BPF_SUB

[Harishankar Vishwanathan]

On Wed, Jun 18, 2025 at 7:24 AM Hao Sun <sunhao.th@gmail.com> wrote:
>
> On Tue, Jun 17, 2025 at 07:17:31PM -0400, Harishankar Vishwanathan wrote:
[...]
>
> Both cvc5 and z3 can prove the above, and one can try this and expect
> it producing SAT on:
> https://cvc5.github.io/app/#temp_a95e25c4-88c5-4257-96c8-0bd74125b179

Thanks for verifying this! As mentioned, we tested the new operators
using Agni, which extracts SMT encodings automatically from the C
source code and
verifies them with Z3, and found the operators to be sound. It is nice
to see that your
testing also concluded that the new operators are sound.

If you’re comfortable, feel free to reply to the patch with a
Tested-by: tag. I’d be happy
to include it in v3 of the patch.

> In addition, the unsoundness of partial case-b can also be proved by
> the following formula, and the counter examples generated may be used
> as test cases if needed:
> https://pastebin.com/raw/qrT7rC1P

We have found that using counterexamples directly for writing test cases is not
straightforward. For instance, consider constructing a test case for the partial
overflow case B. A counterexample might return specific range inputs
([umin, umax]) to
scalar_min_max_add(), which should cause the output to be unbounded
([0, U64_MAX]) due
to the partial overflow. However, these specific range inputs suggested by the
counterexample might not be reachable at all during real verifier
execution. In other
cases, the *tnum* may later refine the result in reg_bounds_sync(),
making the final
output not actually unbounded (when seen in the verifier log).

As such, we adapted Agni's enumerative synthesis procedure with
additional constraints
to generate the test cases.

Re: [PATCH v2 2/2] selftests/bpf: Add testcases for BPF_ADD and BPF_SUB

[Harishankar Vishwanathan]

On Thu, Jun 19, 2025 at 5:55 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
>
> On Thu, 2025-06-19 at 17:13 -0400, Harishankar Vishwanathan wrote:
> > On Wed, Jun 18, 2025 at 5:22 PM Eduard Zingerman <eddyz87@gmail.com> wrote:
> > >
> > > On Tue, 2025-06-17 at 19:17 -0400, Harishankar Vishwanathan wrote:
[...]
> Hm, I see, that's an interesting angle.
> The problem is, if I do something silly changing the code and this
> test fails I'd have a hard time understanding the expected output.
> Therefore, I'd prefer something more obvious.
>
> Maybe let's go with this:
>
>   SEC("tc")
>   __success
>   __naked void test1(void)
>   {
>         asm volatile (
>         "r3 = 0xa000000000000000 ll;"
>         "r4 = 0x0;"
>         "r4 = -r4;"
>         "r3 |= r4;"
>         "r3 += r3;"
>         "r0 = 1;"
>         "exit;"
>         :
>         : __imm(bpf_get_prandom_u32)
>         : __clobber_all);
>   }
>
> Here is verifier log comparison:
>
>   master: 5: (0f) r3 += r3     ; R3_w=scalar()
>   branch: 5: (0f) r3 += r3     ; R3_w=scalar(umin=0x4000000000000000,umax=0xfffffffffffffffe)
>
> ?

Okay, this seems both readable and also demonstrates precision gains.
I'll follow up with a
v3 with similar updated test cases for full overflow and partial
overflow for all the four functions.

[...]