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.

[jub0bs]

@rasky Any update on this? CL 196680 was never merged, it seems.

Here is another example (adapted from internal/stringslite) which I believe would benefit from this fix:

func Cut(s, sep string) (before, after string, found bool) {
	if i := strings.Index(s, sep); i >= 0 {
		return s[:i], s[i+len(sep):], true // two bounds checks
	}
	return s, "", false
}

Two bounds checks occur on the highlighted line. The following version aims to eliminate one of the two bounds checks:

func Cut(s, sep string) (before, after string, found bool) {
	if i := strings.Index(s, sep); i >= 0 {
		after = s[i+len(sep):]    // one bounds check
		return s[:i], after, true // one (unnecessary) bounds check
	}
	return s, "", false
}

The if's condition guarantees that i is positive; and under the assumption that i + len(sep) does not overflow int, we have a guarantee that i <= i + len(sep). Therefore, I would expect no bounds check for s[:i].

[rasky]

I'm not currently working on this anymore, sorry.