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@xxxxxxxxxxxxxx/ >
