cmd/compile: make prove use non-equality in subtraction for a stronger bound

Given:
  s := /* slice */
  k := /* proved valid index in s (0 <= k < len(s)) */
  v := s[k:]

len(v) >= 1, so v[0] needs no bounds check. However, for
len(v) = len(s) - k, we only checked if len(s) >= k and so could only
prove len(v) >= 0, thus the bounds check wasn't removed.

As far as I can tell these checks were commented out for performance,
but after benchmarking prove I see no difference.

Fixes: #76429
Change-Id: I39ba2a18cbabc0559924d4d226dcb99dbe9a06ed
GitHub-Last-Rev: 53f3344d261986cd021c8d7b8435ab89b5438b8f
GitHub-Pull-Request: golang/go#76609
Reviewed-on: https://go-review.googlesource.com/c/go/+/725100
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
Auto-Submit: Keith Randall <khr@golang.org>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Dmitri Shuralyov <dmitshur@google.com>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index c9f75daa67207acb8cba641ba8c03a7024a224f3..108387410095a57b96a781aba84cb86a6361f7a0 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2187,24 +2187,22 @@ func (ft *factsTable) detectSubRelations(v *Value) {
                return // x-y might overflow
        }
 
-       // Subtracting a positive number only makes
-       // things smaller.
-       if yLim.min >= 0 {
+       // Subtracting a positive non-zero number only makes
+       // things smaller. If it's positive or zero, it might
+       // also do nothing (x-0 == v).
+       if yLim.min > 0 {
+               ft.update(v.Block, v, x, signed, lt)
+       } else if yLim.min == 0 {
                ft.update(v.Block, v, x, signed, lt|eq)
-               // TODO: is this worth it?
-               //if yLim.min > 0 {
-               //      ft.update(v.Block, v, x, signed, lt)
-               //}
        }
 
        // Subtracting a number from a bigger one
-       // can't go below 0.
-       if ft.orderS.OrderedOrEqual(y, x) {
+       // can't go below 1. If the numbers might be
+       // equal, then it can't go below 0.
+       if ft.orderS.Ordered(y, x) {
+               ft.signedMin(v, 1)
+       } else if ft.orderS.OrderedOrEqual(y, x) {
                ft.setNonNegative(v)
-               // TODO: is this worth it?
-               //if ft.orderS.Ordered(y, x) {
-               //      ft.signedMin(v, 1)
-               //}
        }
 }
 

diff --git a/test/loopbce.go b/test/loopbce.go
index aabd56c682b878de9b1edfd414a6c2b4b539ae7d..ca09e7e7f70e6b1e77acf4be1672c9fcf8389583 100644 (file)
--- a/test/loopbce.go
+++ b/test/loopbce.go
@@ -17,8 +17,8 @@ func f0a(a []int) int {
 func f0b(a []int) int {
        x := 0
        for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
-               b := a[i:] // ERROR "Proved IsSliceInBounds$"
-               x += b[0]
+               b := a[i:] // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\)$"
+               x += b[0]  // ERROR "Proved IsInBounds$"
        }
        return x
 }
@@ -417,7 +417,7 @@ func bce1() {
 
 func nobce2(a string) {
        for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
-               useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
+               useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\)$"
        }
        for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
                useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed"

diff --git a/test/prove.go b/test/prove.go
index e04b510e17001cc8d98f83bdbbdd7e865f6099c7..e12b6087d3f4b49f1c1dccc9064af903d2e597af 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -2552,7 +2552,7 @@ func swapbound(v []int) {
        for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable"
                v[i], // ERROR "Proved IsInBounds"
                        v[len(v)-1-i] = // ERROR "Proved IsInBounds"
-                       v[len(v)-1-i],
+                       v[len(v)-1-i],  // ERROR "Proved IsInBounds"
                        v[i] // ERROR "Proved IsInBounds"
        }
 }
@@ -2726,6 +2726,14 @@ func issue76688(x, y uint64) uint64 {
        return x * y
 }
 
+func issue76429(s []byte, k int) byte {
+       if k < 0 || k >= len(s) {
+               return 0
+       }
+       s = s[k:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
+       return s[0] // ERROR "Proved IsInBounds"
+}
+
 //go:noinline
 func prove(x int) {
 }