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>

diff --git a/src/cmd/compile/internal/ssa/loopbce.go b/src/cmd/compile/internal/ssa/loopbce.go
index 403aed6b20295fe83e520299c6176a07948c1a17..d484d12a7888d5b5d0a1ad26227d08a8a9262bf2 100644 (file)
--- a/src/cmd/compile/internal/ssa/loopbce.go
+++ b/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)
        }

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 536cfcebf0c76f69e711e5f36fec8893ae18a104..0767be7d57479086b78ff180bd1f64038c857417 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/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

diff --git a/test/loopbce.go b/test/loopbce.go
index 95dd6ff58f6cccab77d11024d399fb2b5200e371..6ef183dea8319e60e39febc68668bed3b29168f2 100644 (file)
--- 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$"