[PATCH bpf-next v2 5/9] bpf, verifier: improve signed ranges inference for BPF_AND

[Shung-Hsi Yu]

On Mon, Jul 22, 2024 at 12:13:20AM GMT, Eduard Zingerman wrote:
> On Fri, 2024-07-19 at 19:00 +0800, Xu Kuohai wrote:
> > From: Shung-Hsi Yu <shung-hsi.yu at suse.com>
> 
> [...]
> 
> > 
> >                         |                         src_reg
> >        smin' = ?        +----------------------------+---------------------------
> >   smin'(r) <= smin(r)   |        negative            |       non-negative
> > ---------+--------------+----------------------------+---------------------------
> >          |   negative   |negative_bit_floor(         |negative_bit_floor(
> >          |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
> > dst_reg  +--------------+----------------------------+---------------------------
> >          | non-negative |negative_bit_floor(         |negative_bit_floor(
> >          |              |  min(dst->smin, src->smin))|  min(dst->smin, src->smin))
> > 
> > Meaning that simply using
> > 
> >     negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value))
> > 
> > to calculate the resulting smin_value would work across all sign combinations.
> > 
> > Together these allows the BPF verifier to infer the signed range of the
> > result of BPF_AND operation using the signed range from its operands,
> > and use that information

I accidentally left the above paragraph unfinished, it should end with

... and using that information, it can be sure that that the result of
[-1, 0] & -13 will be within that expected range of [-4095, 0].

> >     r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0)
> >     r0 &= -13 ; R0_w=scalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3))
> > 
> > [0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@gmail.com/
> > 
> > Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/
> > Cc: Eduard Zingerman <eddyz87 at gmail.com>
> > Signed-off-by: Shung-Hsi Yu <shung-hsi.yu at suse.com>
> > Acked-by: Xu Kuohai <xukuohai at huawei.com>
> > ---
> 
> I find derivation of these new rules logical.
> Also tried a simple brute force testing of this algorithm for 6-bit
> signed integers, and have not found any constraint violations:
> https://github.com/eddyz87/bpf-and-brute-force-check

Thanks!

> As a nitpick, I think that it would be good to have some shortened
> version of the derivation in the comments alongside the code.

Agree it would. Will try to add a 2-4 sentence explanation.

> (Maybe with a link to the mailing list).

Adding a link to the mailing list seems out of the usual for comment in
verifier.c though, and it would be quite long. That said, it would be
nice to hint that there exists a more verbose version of the
explanation.

Maybe an explicit "see commit for the full detail" at the end of
the added comment?

> Acked-by: Eduard Zingerman <eddyz87 at gmail.com>
> 
> [...]

Will send an update for this tomorrow.