On Mon, 2025-06-23 at 00:03 -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.
This commit also adds selftests for cases where the output register state bounds for u(32)_min/u(32)_max are conservatively set to unbounded (when there is partial overflow or underflow).
Signed-off-by: Harishankar Vishwanathan harishankar.vishwanathan@gmail.com Co-developed-by: Matan Shachnai m.shachnai@rutgers.edu Signed-off-by: Matan Shachnai m.shachnai@rutgers.edu Suggested-by: Eduard Zingerman eddyz87@gmail.com
Thank you for adding these tests. Even with "human readable" numbers took me 15-20 minutes to verify the numbers :)
Acked-by: Eduard Zingerman eddyz87@gmail.com
.../selftests/bpf/progs/verifier_bounds.c | 161 ++++++++++++++++++ 1 file changed, 161 insertions(+)
diff --git a/tools/testing/selftests/bpf/progs/verifier_bounds.c b/tools/testing/selftests/bpf/progs/verifier_bounds.c index 30e16153fdf1..31986f6c609e 100644 --- a/tools/testing/selftests/bpf/progs/verifier_bounds.c +++ b/tools/testing/selftests/bpf/progs/verifier_bounds.c @@ -1371,4 +1371,165 @@ __naked void mult_sign_ovf(void) __imm(bpf_skb_store_bytes) : __clobber_all); }
+SEC("socket") +__description("64-bit addition, all outcomes overflow") +__success __log_level(2) +__msg("5: (0f) r3 += r3 {{.*}} R3_w=scalar(umin=0x4000000000000000,umax=0xfffffffffffffffe)") +__retval(0) +__naked void add64_full_overflow(void) +{
- asm volatile (
- "r4 = 0;"
- "r4 = -r4;"
Nit: there is a change in the workings that would make range propagation in negation instruction, a better way to get unbound scalar here is e.g. call to bpf_get_prandom_u32() or read from a constant global map. Depending on order in which patches would be accepted this rework would be either on you or on the other patch-set author.
- "r3 = 0xa000000000000000 ll;"
- "r3 |= r4;"
- "r3 += r3;"
- "r0 = 0;"
- "exit"
- :
- :
- : __clobber_all);
+}
[...]