From e5f202bb60b246a7aee2a14b95ca399fd243accd Mon Sep 17 00:00:00 2001
From: Jorropo <jorropo.pgm@gmail.com>
Date: Fri, 4 Jul 2025 09:21:03 +0200
Subject: cmd/compile: learn transitive proofs for safe unsigned adds

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

Change-Id: Iaab5f0bd2ad51e86ced8c6b8fbd371eb75eeef14
Reviewed-on: https://go-review.googlesource.com/c/go/+/685815
Reviewed-by: Michael Knyszek <mknyszek@google.com>
Reviewed-by: Keith Randall <khr@golang.org>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Auto-Submit: Michael Knyszek <mknyszek@google.com>
Reviewed-by: Mark Freeman <mark@golang.org>
---
 test/prove.go | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)

(limited to 'test')

diff --git a/test/prove.go b/test/prove.go
index faf0b79237..e843edcbf0 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -2041,6 +2041,69 @@ func cvtBoolToUint8BCE(b bool, a [2]int64) int64 {
 	return a[c] // ERROR "Proved IsInBounds$"
 }
 
+func transitiveProofsThroughNonOverflowingUnsignedAdd(x, y, z uint64) {
+	x &= 1<<63 - 1
+	y &= 1<<63 - 1
+
+	a := x + y
+	if a > z {
+		return
+	}
+
+	if x > z { // ERROR "Disproved Less64U$"
+		return
+	}
+	if y > z { // ERROR "Disproved Less64U$"
+		return
+	}
+	if a == x {
+		return
+	}
+	if a == y {
+		return
+	}
+
+	x |= 1
+	y |= 1
+	a = x + y
+	if a == x { // ERROR "Disproved Eq64$"
+		return
+	}
+	if a == y { // ERROR "Disproved Eq64$"
+		return
+	}
+}
+
+func transitiveProofsThroughOverflowingUnsignedAdd(x, y, z uint64) {
+	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) {
 }
-- 
cgit v1.3