cmd/compile: enhance induction variable detection for unrolled loops

Would suggest extending capabilities (32-bit, unsigned, etc)
in separate CLs because prove bugs are so mystifying.

This implements the suggestion in this comment
https://go-review.googlesource.com/c/go/+/104041/10/src/cmd/compile/internal/ssa/loopbce.go#164
for inferring properly bounded iteration for loops of the form

for i := K0; i < KNN-(K-1); i += K
for i := K0; i <= KNN-K;    i += K

Where KNN is "known non negative" (i.e., len or cap) and K
is also not negative.  Because i <= KNN-K, i+K <= KNN and
no overflow occurs.

Also handles decreasing case (K1 > 0)
for i := KNN; i >= K0; i -= K1
which works when MININT+K1 < K0
(i.e. MININT < K0-K1, no overflow)

Signed only, also only 64 bit for now.

Change-Id: I5da6015aba2f781ec76c4ad59c9c48d952325fdc
Reviewed-on: https://go-review.googlesource.com/c/go/+/136375
Run-TryBot: David Chase <drchase@google.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Alexandru Moșoi <alexandru@mosoi.ro>

1 files changed, 117 insertions, 0 deletions

diff --git a/test/prove.go b/test/prove.go
index 275528dde7..39b23c5e0a 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -726,6 +726,123 @@ func signHint2(b []byte, n int) {
 	}
 }
 
+// Induction variable in unrolled loop.
+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]
+	}
+	if i == len(a)-1 {
+		x += a[i]
+	}
+	return x
+}
+
+// Induction variable in unrolled loop.
+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]
+		x += a[i+1]
+	}
+	if i == len(a)-1 {
+		x += a[i]
+	}
+	return x
+}
+
+// Induction variable in unrolled loop.
+func unrollDownExcl0(a []int) int {
+	var i, x int
+	for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
+		x += a[i]   // ERROR "Proved IsInBounds$"
+		x += a[i-1] // ERROR "Proved IsInBounds$"
+	}
+	if i == 0 {
+		x += a[i]
+	}
+	return x
+}
+
+// Induction variable in unrolled loop.
+func unrollDownExcl1(a []int) int {
+	var i, x int
+	for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \[1,\?\], increment 2$"
+		x += a[i]   // ERROR "Proved IsInBounds$"
+		x += a[i-1] // ERROR "Proved IsInBounds$"
+	}
+	if i == 0 {
+		x += a[i]
+	}
+	return x
+}
+
+// Induction variable in unrolled loop.
+func unrollDownInclStep(a []int) int {
+	var i, x int
+	for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
+		x += a[i-1] // ERROR "Proved IsInBounds$"
+		x += a[i-2]
+	}
+	if i == 1 {
+		x += a[i-1]
+	}
+	return x
+}
+
+// Not an induction variable (step too large)
+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]
+	}
+	if i == len(a)-1 {
+		x += a[i]
+	}
+	return x
+}
+
+// Not an induction variable (step too large)
+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]
+	}
+	if i == len(a)-1 {
+		x += a[i]
+	}
+	return x
+}
+
+// Not an induction variable (min too small, iterating down)
+func unrollDecMin(a []int) int {
+	var i, x int
+	for i = len(a); i >= math.MinInt64; i -= 2 {
+		x += a[i-1]
+		x += a[i-2]
+	}
+	if i == 1 { // ERROR "Disproved Eq64$"
+		x += a[i-1]
+	}
+	return x
+}
+
+// Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
+func unrollIncMin(a []int) int {
+	var i, x int
+	for i = len(a); i >= math.MinInt64; i += 2 {
+		x += a[i-1]
+		x += a[i-2]
+	}
+	if i == 1 { // ERROR "Disproved Eq64$"
+		x += a[i-1]
+	}
+	return x
+}
+
 //go:noinline
 func useInt(a int) {
 }