cmd/compile: add cases for StringLen to prove

Tricky index-offset logic had been added for slices,
but not for strings.  This fixes that, and also adds
tests for same behavior in string/slice cases, and adds
a new test for code in prove that had been added but not
explicitly tested.

Fixes #76270.

Change-Id: Ibd92b89e944d86b7f30b4486a9008e6f1ac6af7d
Reviewed-on: https://go-review.googlesource.com/c/go/+/723980
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Keith Randall <khr@golang.org>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 5581da445d8fb85ab9191f66bcb688abe65808fe..536965a0a0ac7a794489730b811750deb638b83b 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2040,14 +2040,14 @@ func (ft *factsTable) flowLimit(v *Value) {
 //
 // slicecap - index >= slicelen - index >= K
 //
-// Note that "index" is not useed for indexing in this pattern, but
+// Note that "index" is not used for indexing in this pattern, but
 // in the motivating example (chunked slice iteration) it is.
 func (ft *factsTable) detectSliceLenRelation(v *Value) {
        if v.Op != OpSub64 {
                return
        }
 
-       if !(v.Args[0].Op == OpSliceLen || v.Args[0].Op == OpSliceCap) {
+       if !(v.Args[0].Op == OpSliceLen || v.Args[0].Op == OpStringLen || v.Args[0].Op == OpSliceCap) {
                return
        }
 
@@ -2070,9 +2070,9 @@ func (ft *factsTable) detectSliceLenRelation(v *Value) {
                        continue
                }
                var lenOffset *Value
-               if bound := ow.Args[0]; bound.Op == OpSliceLen && bound.Args[0] == slice {
+               if bound := ow.Args[0]; (bound.Op == OpSliceLen || bound.Op == OpStringLen) && bound.Args[0] == slice {
                        lenOffset = ow.Args[1]
-               } else if bound := ow.Args[1]; bound.Op == OpSliceLen && bound.Args[0] == slice {
+               } else if bound := ow.Args[1]; (bound.Op == OpSliceLen || bound.Op == OpStringLen) && bound.Args[0] == slice {
                        lenOffset = ow.Args[0]
                }
                if lenOffset == nil || lenOffset.Op != OpConst64 {
@@ -2332,7 +2332,7 @@ func unsignedSubUnderflows(a, b uint64) bool {
 // iteration where the index is not directly compared to the length.
 // if isReslice, then delta can be equal to K.
 func checkForChunkedIndexBounds(ft *factsTable, b *Block, index, bound *Value, isReslice bool) bool {
-       if bound.Op != OpSliceLen && bound.Op != OpSliceCap {
+       if bound.Op != OpSliceLen && bound.Op != OpStringLen && bound.Op != OpSliceCap {
                return false
        }
 
@@ -2367,9 +2367,9 @@ func checkForChunkedIndexBounds(ft *factsTable, b *Block, index, bound *Value, i
                }
                if ow := o.w; ow.Op == OpAdd64 {
                        var lenOffset *Value
-                       if bound := ow.Args[0]; bound.Op == OpSliceLen && bound.Args[0] == slice {
+                       if bound := ow.Args[0]; (bound.Op == OpSliceLen || bound.Op == OpStringLen) && bound.Args[0] == slice {
                                lenOffset = ow.Args[1]
-                       } else if bound := ow.Args[1]; bound.Op == OpSliceLen && bound.Args[0] == slice {
+                       } else if bound := ow.Args[1]; (bound.Op == OpSliceLen || bound.Op == OpStringLen) && bound.Args[0] == slice {
                                lenOffset = ow.Args[0]
                        }
                        if lenOffset == nil || lenOffset.Op != OpConst64 {

diff --git a/test/loopbce.go b/test/loopbce.go
index 8a58d942361221738b4bca9e03614ade8eddda10..aabd56c682b878de9b1edfd414a6c2b4b539ae7d 100644 (file)
--- a/test/loopbce.go
+++ b/test/loopbce.go
@@ -420,7 +420,7 @@ func nobce2(a string) {
                useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
        }
        for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
-               useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
+               useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed"
        }
        for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Disproved Less64$" "Induction variable: limits \[0,\?\), increment 1$"
                useString(a[i:])

diff --git a/test/prove.go b/test/prove.go
index e440634813ee07491d18f3af0a8ad57ce5d06c80..1b50317fe3ea4e5abb4ad09f22e67518de1a123b 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -2659,14 +2659,63 @@ func subLengths2(b []byte, i int) {
 }
 
 func issue76355(s []int, i int) int {
-    var a [10]int
-    if i <= len(s)-1 {
-        v := len(s) - i
-        if v < 10 {
-            return a[v]
-        }
-    }
-    return 0
+       var a [10]int
+       if i <= len(s)-1 {
+               v := len(s) - i
+               if v < 10 {
+                       return a[v]
+               }
+       }
+       return 0
+}
+
+func stringDotDotDot(s string) bool {
+       for i := 0; i < len(s)-2; i++ { // ERROR "Induction variable: limits \[0,[?][)], increment 1"
+               if s[i] == '.' && // ERROR "Proved IsInBounds"
+                       s[i+1] == '.' && // ERROR "Proved IsInBounds"
+                       s[i+2] == '.' { // ERROR "Proved IsInBounds"
+                       return true
+               }
+       }
+       return false
+}
+
+func bytesDotDotDot(s []byte) bool {
+       for i := 0; i < len(s)-2; i++ { // ERROR "Induction variable"
+               if s[i] == '.' && // ERROR "Proved IsInBounds"
+                       s[i+1] == '.' && // ERROR "Proved IsInBounds"
+                       s[i+2] == '.' { // ERROR "Proved IsInBounds"
+                       return true
+               }
+       }
+       return false
+}
+
+// detectSliceLenRelation matches the pattern where
+//  1. v := slicelen - index, OR v := slicecap - index
+//     AND
+//  2. index <= slicelen - K
+//     THEN
+//
+// slicecap - index >= slicelen - index >= K
+func detectSliceLenRelation(s []byte) bool {
+       for i := 0; i <= len(s)-3; i++ { // ERROR "Induction variable"
+               v := len(s) - i
+               if v >= 3 { // ERROR "Proved Leq"
+                       return true
+               }
+       }
+       return false
+}
+
+func detectStringLenRelation(s string) bool {
+       for i := 0; i <= len(s)-3; i++ { // ERROR "Induction variable"
+               v := len(s) - i
+               if v >= 3 { // ERROR "Proved Leq"
+                       return true
+               }
+       }
+       return false
 }
 
 //go:noinline