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>

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

@@ -2,13 +2,21 @@ package ssa
 
 import "fmt"
 
+type indVarFlags uint8
+
+const (
+	indVarMinExc indVarFlags = 1 << iota // minimum value is exclusive (default: inclusive)
+	indVarMaxInc                         // maximum value is inclusive (default: exclusive)
+)
+
 type indVar struct {
 	ind   *Value // induction variable
 	inc   *Value // increment, a constant
 	nxt   *Value // ind+inc variable
-	min   *Value // minimum value. inclusive,
-	max   *Value // maximum value. exclusive.
+	min   *Value // minimum value, inclusive/exclusive depends on flags
+	max   *Value // maximum value, inclusive/exclusive depends on flags
 	entry *Block // entry block in the loop.
+	flags indVarFlags
 	// Invariants: for all blocks dominated by entry:
 	//	min <= ind < max
 	//	min <= nxt <= max
@@ -43,15 +51,22 @@ nextb:
 			continue
 		}
 
+		var flags indVarFlags
 		var ind, max *Value // induction, and maximum
 		entry := -1         // which successor of b enters the loop
 
-		// Check thet the control if it either ind < max or max > ind.
-		// TODO: Handle Leq64, Geq64.
+		// Check thet the control if it either ind </<= max or max >/>= ind.
+		// TODO: Handle 32-bit comparisons.
 		switch b.Control.Op {
+		case OpLeq64:
+			flags |= indVarMaxInc
+			fallthrough
 		case OpLess64:
 			entry = 0
 			ind, max = b.Control.Args[0], b.Control.Args[1]
+		case OpGeq64:
+			flags |= indVarMaxInc
+			fallthrough
 		case OpGreater64:
 			entry = 0
 			ind, max = b.Control.Args[1], b.Control.Args[0]
@@ -59,6 +74,11 @@ nextb:
 			continue nextb
 		}
 
+		// See if the arguments are reversed (i < len() <=> len() > i)
+		if max.Op == OpPhi {
+			ind, max = max, ind
+		}
+
 		// Check that the induction variable is a phi that depends on itself.
 		if ind.Op != OpPhi {
 			continue
@@ -84,12 +104,24 @@ nextb:
 			panic("unreachable") // one of the cases must be true from the above.
 		}
 
-		// Expect the increment to be a positive constant.
-		// TODO: handle negative increment.
-		if inc.Op != OpConst64 || inc.AuxInt <= 0 {
+		// Expect the increment to be a constant.
+		if inc.Op != OpConst64 {
 			continue
 		}
 
+		// If the increment is negative, swap min/max and their flags
+		if inc.AuxInt <= 0 {
+			min, max = max, min
+			oldf := flags
+			flags = 0
+			if oldf&indVarMaxInc == 0 {
+				flags |= indVarMinExc
+			}
+			if oldf&indVarMinExc == 0 {
+				flags |= indVarMaxInc
+			}
+		}
+
 		// Up to now we extracted the induction variable (ind),
 		// the increment delta (inc), the temporary sum (nxt),
 		// the mininum value (min) and the maximum value (max).
@@ -126,8 +158,8 @@ nextb:
 		}
 
 		// We can only guarantee that the loops runs within limits of induction variable
-		// if the increment is 1 or when the limits are constants.
-		if inc.AuxInt != 1 {
+		// if the increment is ±1 or when the limits are constants.
+		if inc.AuxInt != 1 && inc.AuxInt != -1 {
 			ok := false
 			if min.Op == OpConst64 && max.Op == OpConst64 {
 				if max.AuxInt > min.AuxInt && max.AuxInt%inc.AuxInt == min.AuxInt%inc.AuxInt { // handle overflow
@@ -140,6 +172,14 @@ nextb:
 		}
 
 		if f.pass.debug >= 1 {
+			mb1, mb2 := "[", "]"
+			if flags&indVarMinExc != 0 {
+				mb1 = "("
+			}
+			if flags&indVarMaxInc == 0 {
+				mb2 = ")"
+			}
+
 			mlim1, mlim2 := fmt.Sprint(min.AuxInt), fmt.Sprint(max.AuxInt)
 			if !min.isGenericIntConst() {
 				if f.pass.debug >= 2 {
@@ -155,7 +195,7 @@ nextb:
 					mlim2 = "?"
 				}
 			}
-			b.Func.Warnl(b.Pos, "Induction variable: limits [%v,%v), increment %d", mlim1, mlim2, inc.AuxInt)
+			b.Func.Warnl(b.Pos, "Induction variable: limits %v%v,%v%v, increment %d", mb1, mlim1, mlim2, mb2, inc.AuxInt)
 		}
 
 		iv = append(iv, indVar{
@@ -165,6 +205,7 @@ nextb:
 			min:   min,
 			max:   max,
 			entry: b.Succs[entry].b,
+			flags: flags,
 		})
 		b.Logf("found induction variable %v (inc = %v, min = %v, max = %v)\n", ind, inc, min, max)
 	}

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

@@ -799,8 +799,17 @@ func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
 		d |= unsigned
 	}
 
-	addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
-	addRestrictions(b, ft, d, iv.ind, iv.max, lt)
+	if iv.flags&indVarMinExc == 0 {
+		addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
+	} else {
+		addRestrictions(b, ft, d, iv.min, iv.ind, lt)
+	}
+
+	if iv.flags&indVarMaxInc == 0 {
+		addRestrictions(b, ft, d, iv.ind, iv.max, lt)
+	} else {
+		addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq)
+	}
 }
 
 // addBranchRestrictions updates the factsTables ft with the facts learned when

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$"