cmd/compile: enhance prove to deal with double-offset IsInBounds checks

For chunked iterations (useful for, but not exclusive to,
SIMD calculations) it is common to see the combination of
```
for ; i <= len(m)-4; i += 4 {
```
and
```
r0, r1, r2, r3 := m[i], m[i+1], m[i+2], m[i+3]
``

Prove did not handle the case of len-offset1 vs index+offset2
checking, but this change fixes this.  There may be other
similar cases yet to handle -- this worked for the chunked
loops for simd, as well as a handful in std.

Cherry-picked from the dev.simd branch. This CL is not
necessarily SIMD specific. Apply early to reduce risk.

Change-Id: I3785df83028d517e5e5763206653b34b2befd3d0
Reviewed-on: https://go-review.googlesource.com/c/go/+/700696
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-on: https://go-review.googlesource.com/c/go/+/708859
Reviewed-by: David Chase <drchase@google.com>

1 files changed, 6 insertions, 6 deletions

diff --git a/test/prove.go b/test/prove.go
index 6d2bb0962b..bcc023dfec 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -773,8 +773,8 @@ func indexGT0(b []byte, n int) {
 func unrollUpExcl(a []int) int {
 	var i, x int
 	for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
-		x += a[i] // ERROR "Proved IsInBounds$"
-		x += a[i+1]
+		x += a[i]   // ERROR "Proved IsInBounds$"
+		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
 	}
 	if i == len(a)-1 {
 		x += a[i]
@@ -786,8 +786,8 @@ func unrollUpExcl(a []int) int {
 func unrollUpIncl(a []int) int {
 	var i, x int
 	for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
-		x += a[i] // ERROR "Proved IsInBounds$"
-		x += a[i+1]
+		x += a[i]   // ERROR "Proved IsInBounds$"
+		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
 	}
 	if i == len(a)-1 {
 		x += a[i]
@@ -839,7 +839,7 @@ func unrollExclStepTooLarge(a []int) int {
 	var i, x int
 	for i = 0; i < len(a)-1; i += 3 {
 		x += a[i]
-		x += a[i+1]
+		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
 	}
 	if i == len(a)-1 {
 		x += a[i]
@@ -852,7 +852,7 @@ func unrollInclStepTooLarge(a []int) int {
 	var i, x int
 	for i = 0; i <= len(a)-2; i += 3 {
 		x += a[i]
-		x += a[i+1]
+		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
 	}
 	if i == len(a)-1 {
 		x += a[i]