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

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

[...]