Re: [RFC bpf-next] bpf, verifier: improve signed ranges inference for BPF_AND

[Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>]

On Tue, Jul 30, 2024 at 12:26 AM Shung-Hsi Yu <shung-hsi.yu@suse.com> wrote:
[...]
> That is great to hear and really boost the level of confidence. Though I
> did made an update[1] to the patch such that implementation of
> negative_bit_floor() is change from
>
>         v &= v >> 1;
>         v &= v >> 2;
>         v &= v >> 4;
>         v &= v >> 8;
>         v &= v >> 16;
>         v &= v >> 32;
>         return v;
>
> to one that closer resembles tnum_range()
>
>         u8 bits = fls64(~v); /* find most-significant unset bit */
>         u64 delta;
>
>         /* special case, needed because 1ULL << 64 is undefined */
>         if (bits > 63)
>                 return 0;
>
>         delta = (1ULL << bits) - 1;
>         return ~delta;
>

This [1] is indeed the version of the patch that we checked: the one that
uses fls and fls64 in negative_bit_floor and negative32_bit_floor .
I replied here because you had CCed us in this thread.

Note that for checking in Agni, the implementation of fls and fls64 were
borrowed from asm-generic [2,3,4].

Having said that, the patch [1] looks good to me.
Tested-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>

[1]: https://lore.kernel.org/bpf/20240719081702.137173-1-shung-hsi.yu@suse.com/
[2]: https://elixir.bootlin.com/linux/v6.10/source/include/asm-generic/bitops/fls.h#L43
[3]: https://elixir.bootlin.com/linux/v6.10/source/include/asm-generic/bitops/fls64.h#L19
[4]: https://elixir.bootlin.com/linux/v6.10/source/include/asm-generic/bitops/__fls.h#L45