cmd/compile: implement loop BCE in prove

Reuse findIndVar to discover induction variables, and then
register the facts we know about them into the facts table
when entering the loop block.

Moreover, handle "x+delta > w" while updating the facts table,
to be able to prove accesses to slices with constant offsets
such as slice[i-10].

Change-Id: I2a63d050ed58258136d54712ac7015b25c893d71
Reviewed-on: https://go-review.googlesource.com/104038
Run-TryBot: Giovanni Bajo <rasky@develer.com>
Reviewed-by: David Chase <drchase@google.com>

1 files changed, 42 insertions, 38 deletions

diff --git a/test/loopbce.go b/test/loopbce.go
index 857cf2442b..c742df7e60 100644
--- a/test/loopbce.go
+++ b/test/loopbce.go
@@ -1,12 +1,12 @@
 // +build amd64
-// errorcheck -0 -d=ssa/loopbce/debug=3
+// errorcheck -0 -d=ssa/prove/debug=1
 
 package main
 
 func f0a(a []int) int {
 	x := 0
 	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
-		x += a[i] // ERROR "Found redundant IsInBounds$"
+		x += a[i] // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -14,7 +14,7 @@ func f0a(a []int) int {
 func f0b(a []int) int {
 	x := 0
 	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
-		b := a[i:] // ERROR "Found redundant IsSliceInBounds$"
+		b := a[i:] // ERROR "Proved IsSliceInBounds$"
 		x += b[0]
 	}
 	return x
@@ -23,7 +23,7 @@ func f0b(a []int) int {
 func f0c(a []int) int {
 	x := 0
 	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
-		b := a[:i+1] // ERROR "Found redundant IsSliceInBounds \(len promoted to cap\)$"
+		b := a[:i+1] // ERROR "Proved IsSliceInBounds$"
 		x += b[0]
 	}
 	return x
@@ -40,7 +40,7 @@ func f1(a []int) int {
 func f2(a []int) int {
 	x := 0
 	for i := 1; i < len(a); i++ { // ERROR "Induction variable with minimum 1 and increment 1$"
-		x += a[i] // ERROR "Found redundant IsInBounds$"
+		x += a[i] // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -48,7 +48,7 @@ func f2(a []int) int {
 func f4(a [10]int) int {
 	x := 0
 	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
-		x += a[i] // ERROR "Found redundant IsInBounds$"
+		x += a[i] // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -63,7 +63,7 @@ func f5(a [10]int) int {
 
 func f6(a []int) {
 	for i := range a { // ERROR "Induction variable with minimum 0 and increment 1$"
-		b := a[0:i] // ERROR "Found redundant IsSliceInBounds \(len promoted to cap\)$"
+		b := a[0:i] // ERROR "Proved IsSliceInBounds$"
 		f6(b)
 	}
 }
@@ -71,7 +71,7 @@ func f6(a []int) {
 func g0a(a string) int {
 	x := 0
 	for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		x += int(a[i]) // ERROR "Found redundant IsInBounds$"
+		x += int(a[i]) // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -79,7 +79,7 @@ func g0a(a string) int {
 func g0b(a string) int {
 	x := 0
 	for i := 0; len(a) > i; i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		x += int(a[i]) // ERROR "Found redundant IsInBounds$"
+		x += int(a[i]) // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -88,7 +88,7 @@ func g1() int {
 	a := "evenlength"
 	x := 0
 	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
-		x += int(a[i]) // ERROR "Found redundant IsInBounds$"
+		x += int(a[i]) // ERROR "Proved IsInBounds$"
 	}
 	return x
 }
@@ -98,7 +98,7 @@ func g2() int {
 	x := 0
 	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable with minimum 0 and increment 2$"
 		j := i
-		if a[i] == 'e' { // ERROR "Found redundant IsInBounds$"
+		if a[i] == 'e' { // ERROR "Proved IsInBounds$"
 			j = j + 1
 		}
 		x += int(a[j])
@@ -109,27 +109,27 @@ func g2() int {
 func g3a() {
 	a := "this string has length 25"
 	for i := 0; i < len(a); i += 5 { // ERROR "Induction variable with minimum 0 and increment 5$"
-		useString(a[i:]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 		useString(a[:i+3])
 	}
 }
 
 func g3b(a string) {
 	for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		useString(a[i+1:]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[i+1:]) // ERROR "Proved IsSliceInBounds$"
 	}
 }
 
 func g3c(a string) {
 	for i := 0; i < len(a); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		useString(a[:i+1]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[:i+1]) // ERROR "Proved IsSliceInBounds$"
 	}
 }
 
 func h1(a []byte) {
 	c := a[:128]
 	for i := range c { // ERROR "Induction variable with minimum 0 and increment 1$"
-		c[i] = byte(i) // ERROR "Found redundant IsInBounds$"
+		c[i] = byte(i) // ERROR "Proved IsInBounds$"
 	}
 }
 
@@ -142,11 +142,11 @@ func h2(a []byte) {
 func k0(a [100]int) [100]int {
 	for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 		a[i-11] = i
-		a[i-10] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 80$"
-		a[i-5] = i  // ERROR "Found redundant \(IsInBounds ind 100\), ind < 85$"
-		a[i] = i    // ERROR "Found redundant \(IsInBounds ind 100\), ind < 90$"
-		a[i+5] = i  // ERROR "Found redundant \(IsInBounds ind 100\), ind < 95$"
-		a[i+10] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 100$"
+		a[i-10] = i // ERROR "Proved IsInBounds$"
+		a[i-5] = i  // ERROR "Proved IsInBounds$"
+		a[i] = i    // ERROR "Proved IsInBounds$"
+		a[i+5] = i  // ERROR "Proved IsInBounds$"
+		a[i+10] = i // ERROR "Proved IsInBounds$"
 		a[i+11] = i
 	}
 	return a
@@ -155,12 +155,13 @@ func k0(a [100]int) [100]int {
 func k1(a [100]int) [100]int {
 	for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 		useSlice(a[:i-11])
-		useSlice(a[:i-10]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 80$"
-		useSlice(a[:i-5])  // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 85$"
-		useSlice(a[:i])    // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 90$"
-		useSlice(a[:i+5])  // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 95$"
-		useSlice(a[:i+10]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 100$"
-		useSlice(a[:i+11]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 101$"
+		useSlice(a[:i-10]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i-5])  // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i])    // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i+5])  // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i+10]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i+11]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[:i+12])
 
 	}
 	return a
@@ -169,19 +170,22 @@ func k1(a [100]int) [100]int {
 func k2(a [100]int) [100]int {
 	for i := 10; i < 90; i++ { // ERROR "Induction variable with minimum 10 and increment 1$"
 		useSlice(a[i-11:])
-		useSlice(a[i-10:]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 80$"
-		useSlice(a[i-5:])  // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 85$"
-		useSlice(a[i:])    // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 90$"
-		useSlice(a[i+5:])  // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 95$"
-		useSlice(a[i+10:]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 100$"
-		useSlice(a[i+11:]) // ERROR "Found redundant \(IsSliceInBounds ind 100\), ind < 101$"
+		useSlice(a[i-10:]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i-5:])  // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i:])    // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i+5:])  // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i+10:]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i+11:]) // ERROR "Proved IsSliceInBounds$"
+		useSlice(a[i+12:])
 	}
 	return a
 }
 
 func k3(a [100]int) [100]int {
 	for i := -10; i < 90; i++ { // ERROR "Induction variable with minimum -10 and increment 1$"
-		a[i+10] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 100$"
+		a[i+9] = i
+		a[i+10] = i // ERROR "Proved IsInBounds$"
+		a[i+11] = i
 	}
 	return a
 }
@@ -189,7 +193,7 @@ func k3(a [100]int) [100]int {
 func k4(a [100]int) [100]int {
 	min := (-1) << 63
 	for i := min; i < min+50; i++ { // ERROR "Induction variable with minimum -9223372036854775808 and increment 1$"
-		a[i-min] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 50$"
+		a[i-min] = i // ERROR "Proved IsInBounds$"
 	}
 	return a
 }
@@ -197,8 +201,8 @@ func k4(a [100]int) [100]int {
 func k5(a [100]int) [100]int {
 	max := (1 << 63) - 1
 	for i := max - 50; i < max; i++ { // ERROR "Induction variable with minimum 9223372036854775757 and increment 1$"
-		a[i-max+50] = i   // ERROR "Found redundant \(IsInBounds ind 100\), ind < 50$"
-		a[i-(max-70)] = i // ERROR "Found redundant \(IsInBounds ind 100\), ind < 70$"
+		a[i-max+50] = i   // ERROR "Proved IsInBounds$"
+		a[i-(max-70)] = i // ERROR "Proved IsInBounds$"
 	}
 	return a
 }
@@ -221,10 +225,10 @@ func nobce1() {
 
 func nobce2(a string) {
 	for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		useString(a[i:]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 	}
 	for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
-		useString(a[i:]) // ERROR "Found redundant IsSliceInBounds$"
+		useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
 	}
 	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable with minimum 0 and increment 1$"
 		// tests an overflow of StringLen-MinInt64