From 2ca96d218d2cbaad99ba807b3bddd90bbf6a5ba8 Mon Sep 17 00:00:00 2001
From: David Chase <drchase@google.com>
Date: Wed, 17 Sep 2025 17:19:15 -0400
Subject: [PATCH] [dev.simd] cmd/compile: enhance prove to infer bounds in
 slice len/cap calculations

the example comes up in chunked reslicing, e.g. A[i:] where i
has a relationship with len(A)-K.

Change-Id: Ib97dede6cfc7bbbd27b4f384988f741760686604
Reviewed-on: https://go-review.googlesource.com/c/go/+/704875
Reviewed-by: Keith Randall <khr@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Keith Randall <khr@golang.org>
---
 src/cmd/compile/internal/ssa/prove.go | 65 ++++++++++++++++++++++++++-
 1 file changed, 64 insertions(+), 1 deletion(-)

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index b1d49812c7..5ed5be4744 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -1766,7 +1766,8 @@ func (ft *factsTable) flowLimit(v *Value) bool {
 		b := ft.limits[v.Args[1].ID]
 		sub := ft.newLimit(v, a.sub(b, uint(v.Type.Size())*8))
 		mod := ft.detectSignedMod(v)
-		return sub || mod
+		inferred := ft.detectSliceLenRelation(v)
+		return sub || mod || inferred
 	case OpNeg64, OpNeg32, OpNeg16, OpNeg8:
 		a := ft.limits[v.Args[0].ID]
 		bitsize := uint(v.Type.Size()) * 8
@@ -1947,6 +1948,68 @@ func (ft *factsTable) detectSignedMod(v *Value) bool {
 	// TODO: non-powers-of-2
 	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
+//
+// Note that "index" is not useed for indexing in this pattern, but
+// in the motivating example (chunked slice iteration) it is.
+func (ft *factsTable) detectSliceLenRelation(v *Value) (inferred bool) {
+	if v.Op != OpSub64 {
+		return false
+	}
+
+	if !(v.Args[0].Op == OpSliceLen || v.Args[0].Op == OpSliceCap) {
+		return false
+	}
+
+	slice := v.Args[0].Args[0]
+	index := v.Args[1]
+
+	for o := ft.orderings[index.ID]; o != nil; o = o.next {
+		if o.d != signed {
+			continue
+		}
+		or := o.r
+		if or != lt && or != lt|eq {
+			continue
+		}
+		ow := o.w
+		if ow.Op != OpAdd64 && ow.Op != OpSub64 {
+			continue
+		}
+		var lenOffset *Value
+		if bound := ow.Args[0]; bound.Op == OpSliceLen && bound.Args[0] == slice {
+			lenOffset = ow.Args[1]
+		} else if bound := ow.Args[1]; bound.Op == OpSliceLen && bound.Args[0] == slice {
+			lenOffset = ow.Args[0]
+		}
+		if lenOffset == nil || lenOffset.Op != OpConst64 {
+			continue
+		}
+		K := lenOffset.AuxInt
+		if ow.Op == OpAdd64 {
+			K = -K
+		}
+		if K < 0 {
+			continue
+		}
+		if or == lt {
+			K++
+		}
+		if K < 0 { // We hate thinking about overflow
+			continue
+		}
+		inferred = inferred || ft.signedMin(v, K)
+	}
+	return inferred
+}
+
 func (ft *factsTable) detectSignedModByPowerOfTwo(v *Value) bool {
 	// We're looking for:
 	//
-- 
2.52.0