From: Jonah Uellenberg <JonahUellenberg@gmail.com>
Date: Thu, 29 Jan 2026 19:45:27 +0000 (+0000)
Subject: cmd/compile: make prove use non-equality in subtraction for a stronger bound
X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=14a4cb13e389d8dbc1ba3ba0097e208f1436a22a;p=gostls13.git

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 c9f75daa67..1083874100 100644
--- 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 aabd56c682..ca09e7e7f7 100644
--- 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 e04b510e17..e12b6087d3 100644
--- 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) {
 }