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)
?
[...]