Re: [PATCH bpf-next v2 1/2] bpf: Track aligned st store as imprecise spilled registers

[Eduard Zingerman <eddyz87@gmail.com>]

On Mon, 2024-01-08 at 10:59 -0800, Yonghong Song wrote:
[...]

> I guess one way could be doing backtracking with "... = arr[i]"
> is to have four ranges, [-32, -24), [-24, -16), [-16, -8), [-8, 0).
> Later, when we see arr[i] = r0 and i has range [-32, 0). Since it covers [-32, -24), etc.,
> precision marking can proceed with 'r0'. But I guess this can potentially
> increase verifier backtracking states a lot and is not scalable. Conservatively
> doing precision marking with 'r0' (in arr[i] = r0) is a better idea.

In theory it should be possible to collapse this range to min/max pair.
But it is a complication, and I'd say it shouldn't be implemented
unless we have evidence that it significantly improves verification
performance.

> 
> Andrii has similar comments in
>    https://lore.kernel.org/bpf/CAEf4Bzb0LdSPnFZ-kPRftofA6LsaOkxXLN4_fr9BLR3iG-te-g@mail.gmail.com/
>