cmd/compile: teach prove to handle expressions like len(s)-delta

When a loop has bound len(s)-delta, findIndVar detected it and
returned len(s) as (conservative) upper bound. This little lie
allowed loopbce to drop bound checks.

It is obviously more generic to teach prove about relations like
x+d<w for non-constant "w"; we already handled the case for
constant "w", so we just want to learn that if d<0, then x+d<w
proves that x<w.

To be able to remove the code from findIndVar, we also need
to teach prove that len() and cap() are always non-negative.

This CL allows to prove 633 more checks in cmd+std. Most
of them are cases where the code was already testing before
accessing a slice but the compiler didn't know it. For instance,
take strings.HasSuffix:

    func HasSuffix(s, suffix string) bool {
        return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
    }

When suffix is a literal string, the compiler now understands
that the explicit check is enough to not emit a slice check.

I also found a loopbce test that was incorrectly
written to detect an overflow but had a off-by-one (on the
conservative side), so it unexpectly passed with this CL; I
changed it to really trigger the overflow as intended.

Change-Id: Ib5abade337db46b8811425afebad4719b6e46c4a
Reviewed-on: https://go-review.googlesource.com/105635
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 d484d12a7888d5b5d0a1ad26227d08a8a9262bf2..692e55e17a8ef23a27d840a47debdd5d89fca05b 100644 (file)
--- a/src/cmd/compile/internal/ssa/loopbce.go
+++ b/src/cmd/compile/internal/ssa/loopbce.go
@@ -150,13 +150,6 @@ nextb:
                        continue
                }
 
-               // If max is c + SliceLen with c <= 0 then we drop c.
-               // Makes sure c + SliceLen doesn't overflow when SliceLen == 0.
-               // TODO: save c as an offset from max.
-               if w, c := dropAdd64(max); (w.Op == OpStringLen || w.Op == OpSliceLen) && 0 >= c && -c >= 0 {
-                       max = w
-               }
-
                // 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 && inc.AuxInt != -1 {

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 0767be7d57479086b78ff180bd1f64038c857417..9f2a38252e834b648d549301082585acc6cfe0cc 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -389,70 +389,78 @@ 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.
+       // Process: x+delta > w (with delta constant)
+       // Only signed domain for now (useful for accesses to slices in loops).
        if r == gt || r == gt|eq {
-               if x, delta := isConstDelta(v); x != nil && w.isGenericIntConst() && d == signed {
+               if x, delta := isConstDelta(v); x != nil && 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)
+                       if !w.isGenericIntConst() {
+                               // If we know that x+delta > w but w is not constant, we can derive:
+                               //    if delta < 0 and x > MinInt - delta, then x > w (because x+delta cannot underflow)
+                               // This is useful for loops with bounds "len(slice)-K" (delta = -K)
+                               if l, has := ft.limits[x.ID]; has && delta < 0 {
+                                       if (x.Type.Size() == 8 && l.min >= math.MinInt64-delta) ||
+                                               (x.Type.Size() == 4 && l.min >= math.MinInt32-delta) {
+                                               ft.update(parent, x, w, signed, r)
+                                       }
+                               }
                        } 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)
+                               // With w,delta constants, we want to derive: x+delta > w  ⇒  x > w-delta
+                               //
+                               // 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.
+                               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)
+                                               }
                                        }
                                }
                        }
@@ -661,24 +669,43 @@ func prove(f *Func) {
        ft := newFactsTable()
 
        // Find length and capacity ops.
+       var zero *Value
        for _, b := range f.Blocks {
                for _, v := range b.Values {
+                       // If we found a zero constant, save it (so we don't have
+                       // to build one later).
+                       if zero == nil && v.Op == OpConst64 && v.AuxInt == 0 {
+                               zero = v
+                       }
                        if v.Uses == 0 {
                                // We don't care about dead values.
                                // (There can be some that are CSEd but not removed yet.)
                                continue
                        }
                        switch v.Op {
+                       case OpStringLen:
+                               if zero == nil {
+                                       zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
+                               }
+                               ft.update(b, v, zero, signed, gt|eq)
                        case OpSliceLen:
                                if ft.lens == nil {
                                        ft.lens = map[ID]*Value{}
                                }
                                ft.lens[v.Args[0].ID] = v
+                               if zero == nil {
+                                       zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
+                               }
+                               ft.update(b, v, zero, signed, gt|eq)
                        case OpSliceCap:
                                if ft.caps == nil {
                                        ft.caps = map[ID]*Value{}
                                }
                                ft.caps[v.Args[0].ID] = v
+                               if zero == nil {
+                                       zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
+                               }
+                               ft.update(b, v, zero, signed, gt|eq)
                        }
                }
        }

diff --git a/test/loopbce.go b/test/loopbce.go
index 6ef183dea8319e60e39febc68668bed3b29168f2..c93bfc8f000fb69c5bb260f2f3f32cc4b5dcce0a 100644 (file)
--- a/test/loopbce.go
+++ b/test/loopbce.go
@@ -100,6 +100,22 @@ func g0d(a string) int {
        return x
 }
 
+func g0e(a string) int {
+       x := 0
+       for i := len(a) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment -1$"
+               x += int(a[i]) // ERROR "Proved IsInBounds$"
+       }
+       return x
+}
+
+func g0f(a string) int {
+       x := 0
+       for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment -1$"
+               x += int(a[i]) // ERROR "Proved IsInBounds$"
+       }
+       return x
+}
+
 func g1() int {
        a := "evenlength"
        x := 0
@@ -265,7 +281,14 @@ func nobce2(a string) {
                useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
        }
        for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
-               // tests an overflow of StringLen-MinInt64
+               useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
+       }
+       j := int64(len(a)) - 123
+       for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
+               useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
+       }
+       for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
+               // len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
                useString(a[i:])
        }
 }

diff --git a/test/prove.go b/test/prove.go
index b5b3f20082fe49f98e87d2c23b6adb06fed4f168..424ab5c0d70620cb42e4d459fdca2977e387b3d8 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -42,8 +42,8 @@ func f1b(a []int, i int, j uint) int {
        if i >= 10 && i < len(a) {
                return a[i] // ERROR "Proved IsInBounds$"
        }
-       if i >= 10 && i < len(a) { // todo: handle this case
-               return a[i-10]
+       if i >= 10 && i < len(a) {
+               return a[i-10] // ERROR "Proved IsInBounds$"
        }
        if j < uint(len(a)) {
                return a[j] // ERROR "Proved IsInBounds$"
@@ -613,6 +613,41 @@ func trans3(a, b []int, i int) {
        _ = b[i] // ERROR "Proved IsInBounds$"
 }
 
+// Derived from nat.cmp
+func natcmp(x, y []uint) (r int) {
+       m := len(x)
+       n := len(y)
+       if m != n || m == 0 {
+               return
+       }
+
+       i := m - 1
+       for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment -1"
+               x[i] == // ERROR "Proved IsInBounds$"
+                       y[i] { // ERROR "Proved IsInBounds$"
+               i--
+       }
+
+       switch {
+       case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
+               y[i]: // ERROR "Proved IsInBounds$"
+               r = -1
+       case x[i] > // ERROR "Proved IsInBounds$"
+               y[i]: // ERROR "Proved IsInBounds$"
+               r = 1
+       }
+       return
+}
+
+func suffix(s, suffix string) bool {
+       // todo, we're still not able to drop the bound check here in the general case
+       return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
+}
+
+func constsuffix(s string) bool {
+       return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
+}
+
 //go:noinline
 func useInt(a int) {
 }