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 <[email protected]>
Reviewed-by: Keith Randall <[email protected]>
LUCI-TryBot-Result: Go LUCI <[email protected]>
Reviewed-on: https://go-review.googlesource.com/c/go/+/708859
Reviewed-by: David Chase <[email protected]>

Author: dr2chase

src/cmd/compile/internal/ssa/prove.go

@@ -2174,6 +2174,65 @@ func unsignedSubUnderflows(a, b uint64) bool {
 	return a < b
 }
 
+// checkForChunkedIndexBounds looks for index expressions of the form
+// A[i+delta] where delta < K and i <= len(A)-K.  That is, this is a chunked
+// iteration where the index is not directly compared to the length.
+func checkForChunkedIndexBounds(ft *factsTable, b *Block, index, bound *Value) bool {
+	if bound.Op != OpSliceLen {
+		return false
+	}
+	lim := ft.limits[index.ID]
+	if lim.min < 0 {
+		return false
+	}
+	i, delta := isConstDelta(index)
+	if i == nil {
+		return false
+	}
+	if delta < 0 {
+		return false
+	}
+	// special case for blocked iteration over a slice.
+	// slicelen > i + delta && <==== if clauses above
+	// && index >= 0           <==== if clause above
+	// delta >= 0 &&           <==== if clause above
+	// slicelen-K >/>= x       <==== checked below
+	// && K >=/> delta         <==== checked below
+	// then v > w
+	// example: i <=/< len - 4/3 means i+{0,1,2,3} are legal indices
+	for o := ft.orderings[i.ID]; o != nil; o = o.next {
+		if o.d != signed {
+			continue
+		}
+		if ow := o.w; ow.Op == OpAdd64 {
+			var lenOffset *Value
+			if ow.Args[0] == bound {
+				lenOffset = ow.Args[1]
+			} else if ow.Args[1] == bound {
+				lenOffset = ow.Args[0]
+			}
+			if lenOffset == nil || lenOffset.Op != OpConst64 {
+				continue
+			}
+			if K := -lenOffset.AuxInt; K >= 0 {
+				or := o.r
+				if or == lt {
+					or = lt | eq
+					K++
+					if K < 0 {
+						continue
+					}
+				}
+
+				if delta < K && or == lt|eq {
+					return true
+				}
+			}
+		}
+	}
+	return false
+}
+
 func addLocalFacts(ft *factsTable, b *Block) {
 	// Propagate constant ranges among values in this block.
 	// We do this before the second loop so that we have the
@@ -2285,6 +2344,13 @@ func addLocalFacts(ft *factsTable, b *Block) {
 			if v.Args[0].Op == OpSliceMake {
 				ft.update(b, v, v.Args[0].Args[2], signed, eq)
 			}
+		case OpIsInBounds:
+			if checkForChunkedIndexBounds(ft, b, v.Args[0], v.Args[1]) {
+				if b.Func.pass.debug > 0 {
+					b.Func.Warnl(v.Pos, "Proved %s for blocked indexing", v.Op)
+				}
+				ft.booleanTrue(v)
+			}
 		case OpPhi:
 			addLocalFactsPhi(ft, v)
 		}

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]