On Thu, 2025-06-19 at 17:13 -0400, Harishankar Vishwanathan wrote:
> On Wed, Jun 18, 2025 at 5:22 PM Eduard Zingerman <eddyz87@xxxxxxxxx> 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@xxxxxxxxxxx>
> > > Signed-off-by: Matan Shachnai <m.shachnai@xxxxxxxxxxx>
> > > Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@xxxxxxxxx>
> > > ---
> >
> > 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@xxxxxxxxx/
>
> [...]
