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>

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 {

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:])

test/prove.go

@@ -2659,14 +2659,63 @@ func subLengths2(b []byte, i int) {
 }
 
 func issue76355(s []int, i int) int {
-    var a [10]int
+	var a [10]int
-    if i <= len(s)-1 {
+	if i <= len(s)-1 {
-        v := len(s) - i
+		v := len(s) - i
-        if v < 10 {
+		if v < 10 {
-            return a[v]
+			return a[v]
-        }
+		}
-    }
+	}
-    return 0
+	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