cmd/compile: teach prove about incrementing, len, and overflow

[josharian]

I have some hot code that looks approximately like this:

func f(a []int, i int) int {
	for i < len(a) && a[i] != 0 {
		i++
	}
	return i
}

The generated code has a bounds check on every iteration. This is because i might be negative. We can rule that out up front:

func f(a []int, i int) int {
	if i < 0 {
		panic("bad")
	}
	for i < len(a) && a[i] != 0 {
		i++
	}
	return i
}

This could should be able to go without a bounds check. i cannot be negative at the beginning. In order to become negative, it must overflow. However, it cannot overflow: It is being incremented, so it must reach len(a) before overflowing, in which case we exit the loop before evaluating a[i].

(I actually know a priori in my code that i is not negative; I'd be tempted to use #30582 here. I could also switch to i being a uint, which does remove the bounds check, but it makes other things in the real code a bit awkward.)

I don't know how hard it is to teach prove about this case.

cc @zdjones @rasky @randall77

[rasky]

It should be fixed by the patch serie finishing at CL 196680. I can't test it right now though.