cmd/compile: in prove, detect loops with negative increments

To be effective, this also requires being able to relax constraints
on min/max bound inclusiveness; they are now exposed through a flags,
and prove has been updated to handle it correctly.

Change-Id: I3490e54461b7b9de8bc4ae40d3b5e2fa2d9f0556
Reviewed-on: https://go-review.googlesource.com/104041
Run-TryBot: Giovanni Bajo <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: David Chase <drchase@google.com>

1 files changed, 34 insertions, 0 deletions

diff --git a/test/loopbce.go b/test/loopbce.go
index 95dd6ff58f..6ef183dea8 100644
--- a/test/loopbce.go
+++ b/test/loopbce.go
@@ -84,6 +84,22 @@ func g0b(a string) int {
 	return x
 }
 
+func g0c(a string) int {
+	x := 0
+	for i := len(a); i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment -1$"
+		x += int(a[i-1]) // ERROR "Proved IsInBounds$"
+	}
+	return x
+}
+
+func g0d(a string) int {
+	x := 0
+	for i := len(a); 0 < i; i-- { // ERROR "Induction variable: limits \(0,\?\], increment -1$"
+		x += int(a[i-1]) // ERROR "Proved IsInBounds$"
+	}
+	return x
+}
+
 func g1() int {
 	a := "evenlength"
 	x := 0
@@ -190,6 +206,24 @@ func k3(a [100]int) [100]int {
 	return a
 }
 
+func k3neg(a [100]int) [100]int {
+	for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment -1$"
+		a[i+9] = i
+		a[i+10] = i // ERROR "Proved IsInBounds$"
+		a[i+11] = i
+	}
+	return a
+}
+
+func k3neg2(a [100]int) [100]int {
+	for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment -1$"
+		a[i+9] = i
+		a[i+10] = i // ERROR "Proved IsInBounds$"
+		a[i+11] = i
+	}
+	return a
+}
+
 func k4(a [100]int) [100]int {
 	min := (-1) << 63
 	for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"