On 1/8/24 11:06 AM, Eduard Zingerman wrote:
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.
Ack. We do not need to introduce this yet as the variable index range
should be much much less common.
Andrii has similar comments in
https://lore.kernel.org/bpf/CAEf4Bzb0LdSPnFZ-kPRftofA6LsaOkxXLN4_fr9BLR3iG-te-g@xxxxxxxxxxxxxx/
