From: Keith Randall <khr@golang.org>
Date: Sun, 22 Jun 2025 23:50:16 +0000 (-0700)
Subject: cmd/compile: add missing StringLen rule in prove
X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=f703dc5befdad9390decc251e8b1f5e0f061c088;p=gostls13.git

cmd/compile: add missing StringLen rule in prove

(StringLen (StringMake _ x)) == x, just like the rules we
currently have for slices.

This helps propagate string length knowledge to places which need it.

Change-Id: Ifdcf6d1f2d430c1c4bbac32e0ea74c188eae998e
Reviewed-on: https://go-review.googlesource.com/c/go/+/682777
Reviewed-by: Daniel Morsing <daniel.morsing@gmail.com>
Reviewed-by: Michael Knyszek <mknyszek@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Auto-Submit: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Jorropo <jorropo.pgm@gmail.com>
---

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 0c0581690f..b8c952ef33 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2267,6 +2267,10 @@ func addLocalFacts(ft *factsTable, b *Block) {
 			// the mod instruction executes (and thus panics if the
 			// modulus is 0). See issue 67625.
 			ft.update(b, v, v.Args[1], unsigned, lt)
+		case OpStringLen:
+			if v.Args[0].Op == OpStringMake {
+				ft.update(b, v, v.Args[0].Args[1], signed, eq)
+			}
 		case OpSliceLen:
 			if v.Args[0].Op == OpSliceMake {
 				ft.update(b, v, v.Args[0].Args[1], signed, eq)
diff --git a/test/prove.go b/test/prove.go
index 8daa812e76..5a4be3a5d5 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -2302,6 +2302,23 @@ func transitiveProofsThroughOverflowingUnsignedSub(x, y, z uint64) {
 	}
 }
 
+func resliceString(s string) byte {
+	if len(s) >= 4 {
+		s = s[2:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
+		s = s[1:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
+		return s[0] // ERROR "Proved IsInBounds"
+	}
+	return 0
+}
+func resliceBytes(b []byte) byte {
+	if len(b) >= 4 {
+		b = b[2:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
+		b = b[1:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
+		return b[0] // ERROR "Proved IsInBounds"
+	}
+	return 0
+}
+
 //go:noinline
 func useInt(a int) {
 }