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

[Eduard Zingerman]

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

As a nitpick, I think that it would be good to have some shortened
version of the derivation in the comments alongside the code.
(Maybe with a link to the mailing list).

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

[...]