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>

diff --git a/src/cmd/compile/fmt_test.go b/src/cmd/compile/fmt_test.go
index 8af7cced6a7d4bb024dcbd071c8e0062cafd70e3..5dd2fa50be8bcbcd7b2cca20d55f436cb83b82af 100644 (file)
--- a/src/cmd/compile/fmt_test.go
+++ b/src/cmd/compile/fmt_test.go
@@ -646,6 +646,7 @@ var knownFormats = map[string]string{
        "cmd/compile/internal/ssa.Op %s":                  "",
        "cmd/compile/internal/ssa.Op %v":                  "",
        "cmd/compile/internal/ssa.ValAndOff %s":           "",
+       "cmd/compile/internal/ssa.domain %v":              "",
        "cmd/compile/internal/ssa.posetNode %v":           "",
        "cmd/compile/internal/ssa.posetTestOp %v":         "",
        "cmd/compile/internal/ssa.rbrank %d":              "",

diff --git a/src/cmd/compile/internal/ssa/loopbce.go b/src/cmd/compile/internal/ssa/loopbce.go
index a96d98717dabe31e56ad11d09b710ef9db13e2d3..7f2da4870e46e4daba1fbd18132a3962153ae7a9 100644 (file)
--- a/src/cmd/compile/internal/ssa/loopbce.go
+++ b/src/cmd/compile/internal/ssa/loopbce.go
@@ -137,7 +137,7 @@ nextb:
                        }
                }
 
-               if f.pass.debug > 1 {
+               if f.pass.debug >= 1 {
                        if min.Op == OpConst64 {
                                b.Func.Warnl(b.Pos, "Induction variable with minimum %d and increment %d", min.AuxInt, inc.AuxInt)
                        } else {

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 371009a57d480376a375f77d14104bdb7a253358..536cfcebf0c76f69e711e5f36fec8893ae18a104 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -388,6 +388,77 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
                        }
                }
        }
+
+       // Process: x+delta > w    (with delta,w constants)
+       //
+       // We want to derive: x+delta > w  ⇒  x > w-delta
+       //
+       // We do this for signed numbers for now, as that allows to prove many
+       // accesses to slices in loops.
+       //
+       // From x+delta > w, we compute (using integers of the correct size):
+       //    min = w - delta
+       //    max = MaxInt - delta
+       //
+       // And we prove that:
+       //    if min<max: min < x AND x <= max
+       //    if min>max: min < x OR  x <= max
+       //
+       // This is always correct, even in case of overflow.
+       //
+       // If the initial fact is x+delta >= w instead, the derived conditions are:
+       //    if min<max: min <= x AND x <= max
+       //    if min>max: min <= x OR  x <= max
+       //
+       // Notice the conditions for max are still <=, as they handle overflows.
+       if r == gt || r == gt|eq {
+               if x, delta := isConstDelta(v); x != nil && w.isGenericIntConst() && d == signed {
+                       if parent.Func.pass.debug > 1 {
+                               parent.Func.Warnl(parent.Pos, "x+d >= w; x:%v %v delta:%v w:%v d:%v", x, parent.String(), delta, w.AuxInt, d)
+                       }
+
+                       var min, max int64
+                       var vmin, vmax *Value
+                       switch x.Type.Size() {
+                       case 8:
+                               min = w.AuxInt - delta
+                               max = int64(^uint64(0)>>1) - delta
+
+                               vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min)
+                               vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max)
+
+                       case 4:
+                               min = int64(int32(w.AuxInt) - int32(delta))
+                               max = int64(int32(^uint32(0)>>1) - int32(delta))
+
+                               vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min)
+                               vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max)
+
+                       default:
+                               panic("unimplemented")
+                       }
+
+                       if min < max {
+                               // Record that x > min and max >= x
+                               ft.update(parent, x, vmin, d, r)
+                               ft.update(parent, vmax, x, d, r|eq)
+                       } else {
+                               // We know that either x>min OR x<=max. factsTable cannot record OR conditions,
+                               // so let's see if we can already prove that one of them is false, in which case
+                               // the other must be true
+                               if l, has := ft.limits[x.ID]; has {
+                                       if l.max <= min {
+                                               // x>min is impossible, so it must be x<=max
+                                               ft.update(parent, vmax, x, d, r|eq)
+                                       } else if l.min > max {
+                                               // x<=max is impossible, so it must be x>min
+                                               ft.update(parent, x, vmin, d, r)
+                                       }
+                               }
+                       }
+               }
+       }
+
 }
 
 var opMin = map[Op]int64{
@@ -405,8 +476,25 @@ func (ft *factsTable) isNonNegative(v *Value) bool {
        if isNonNegative(v) {
                return true
        }
-       l, has := ft.limits[v.ID]
-       return has && (l.min >= 0 || l.umax <= math.MaxInt64)
+
+       // Check if the recorded limits can prove that the value is positive
+       if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= math.MaxInt64) {
+               return true
+       }
+
+       // Check if v = x+delta, and we can use x's limits to prove that it's positive
+       if x, delta := isConstDelta(v); x != nil {
+               if l, has := ft.limits[x.ID]; has {
+                       if delta > 0 && l.min >= -delta && l.max <= math.MaxInt64-delta {
+                               return true
+                       }
+                       if delta < 0 && l.min >= -delta {
+                               return true
+                       }
+               }
+       }
+
+       return false
 }
 
 // checkpoint saves the current state of known relations.
@@ -595,6 +683,16 @@ func prove(f *Func) {
                }
        }
 
+       // Find induction variables. Currently, findIndVars
+       // is limited to one induction variable per block.
+       var indVars map[*Block]indVar
+       for _, v := range findIndVar(f) {
+               if indVars == nil {
+                       indVars = make(map[*Block]indVar)
+               }
+               indVars[v.entry] = v
+       }
+
        // current node state
        type walkState int
        const (
@@ -634,6 +732,10 @@ func prove(f *Func) {
                switch node.state {
                case descend:
                        ft.checkpoint()
+                       if iv, ok := indVars[node.block]; ok {
+                               addIndVarRestrictions(ft, parent, iv)
+                       }
+
                        if branch != unknown {
                                addBranchRestrictions(ft, parent, branch)
                                if ft.unsat {
@@ -688,6 +790,19 @@ func getBranch(sdom SparseTree, p *Block, b *Block) branch {
        return unknown
 }
 
+// addIndVarRestrictions updates the factsTables ft with the facts
+// learned from the induction variable indVar which drives the loop
+// starting in Block b.
+func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
+       d := signed
+       if isNonNegative(iv.min) && isNonNegative(iv.max) {
+               d |= unsigned
+       }
+
+       addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
+       addRestrictions(b, ft, d, iv.ind, iv.max, lt)
+}
+
 // addBranchRestrictions updates the factsTables ft with the facts learned when
 // branching from Block b in direction br.
 func addBranchRestrictions(ft *factsTable, b *Block, br branch) {

diff --git a/test/loopbce.go b/test/loopbce.go
index 857cf2442b64ee026301b13b51178e95be4fe923..c742df7e60cd33a8e4498a09ec26ad13da510c91 100644 (file)
--- 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

diff --git a/test/prove.go b/test/prove.go
index f7b3ef0847b0748460e0663f35d350999befca22..a4eedbb717bb119be8d04037b39153a8b26c31f6 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -62,7 +62,7 @@ func f1c(a []int, i int64) int {
 }
 
 func f2(a []int) int {
-       for i := range a {
+       for i := range a { // ERROR "Induction variable with minimum 0 and increment 1"
                a[i+1] = i
                a[i+1] = i // ERROR "Proved IsInBounds$"
        }
@@ -464,8 +464,7 @@ func f16(s []int) []int {
 }
 
 func f17(b []int) {
-       for i := 0; i < len(b); i++ {
-               useSlice(b[i:]) // Learns i <= len
+       for i := 0; i < len(b); i++ { // ERROR "Induction variable with minimum 0 and increment 1"
                // This tests for i <= cap, which we can only prove
                // using the derived relation between len and cap.
                // This depends on finding the contradiction, since we