From d574856482859d259a95826dea404e648cbb8fef Mon Sep 17 00:00:00 2001
From: Jorropo <jorropo.pgm@gmail.com>
Date: Fri, 4 Jul 2025 09:25:23 +0200
Subject: [PATCH] cmd/compile: learn transitive proofs for safe negative signed
 adds

I've split this into it's own CL to make git bisect more effective.

Change-Id: Ib2c6dbc82fb04f50f2d17fbe6626c9fc322fb478
Reviewed-on: https://go-review.googlesource.com/c/go/+/685820
Auto-Submit: Michael Knyszek <mknyszek@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Michael Knyszek <mknyszek@google.com>
---
 src/cmd/compile/internal/ssa/prove.go | 14 ++++++
 test/prove.go                         | 70 +++++++++++++++++++++++++++
 2 files changed, 84 insertions(+)

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index da42a675bf..cf045629cb 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2212,6 +2212,20 @@ func addLocalFacts(ft *factsTable, b *Block) {
 				}
 				ft.update(b, v, v.Args[0], signed, r)
 			}
+			if x.max <= 0 && !signedAddOverflowsOrUnderflows(x.min, y.min, v.Type) {
+				r := lt
+				if !x.nonzero() {
+					r |= eq
+				}
+				ft.update(b, v, v.Args[1], signed, r)
+			}
+			if y.max <= 0 && !signedAddOverflowsOrUnderflows(x.min, y.min, v.Type) {
+				r := lt
+				if !y.nonzero() {
+					r |= eq
+				}
+				ft.update(b, v, v.Args[0], signed, r)
+			}
 		case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
 			ft.update(b, v, v.Args[0], unsigned, lt|eq)
 			ft.update(b, v, v.Args[1], unsigned, lt|eq)
diff --git a/test/prove.go b/test/prove.go
index 5ed92ba912..a8a9ce1ce4 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -2171,6 +2171,76 @@ func transitiveProofsThroughOverflowingSignedAddPositive(x, y, z int64) {
 	}
 }
 
+func transitiveProofsThroughNonOverflowingSignedAddNegative(x, y, z int64) {
+	if x < math.MinInt64>>1 || x > 0 ||
+		y < math.MinInt64>>1 || y > 0 {
+		return
+	}
+
+	a := x + y
+	if a < z {
+		return
+	}
+
+	if x < z { // ERROR "Disproved Less64$"
+		return
+	}
+	if y < z { // ERROR "Disproved Less64$"
+		return
+	}
+	if a == x {
+		return
+	}
+	if a == y {
+		return
+	}
+
+	if x == 0 && y == 0 {
+		return
+	}
+	a = x + y
+	if a == x { // ERROR "Disproved Eq64$"
+		return
+	}
+	if a == y { // ERROR "Disproved Eq64$"
+		return
+	}
+}
+
+func transitiveProofsThroughOverflowingSignedAddNegative(x, y, z int64) {
+	if x >= 0 || y >= 0 {
+		return
+	}
+
+	a := x + y
+	if a < z {
+		return
+	}
+
+	if x < z {
+		return
+	}
+	if y < z {
+		return
+	}
+	if a == x {
+		return
+	}
+	if a == y {
+		return
+	}
+
+	x |= 1
+	y |= 1
+	a = x + y
+	if a == x {
+		return
+	}
+	if a == y {
+		return
+	}
+}
+
 //go:noinline
 func useInt(a int) {
 }
-- 
2.51.0