From 77dc1380308f5129952c16b6940dea7ddd4e17b9 Mon Sep 17 00:00:00 2001
From: Jorropo <jorropo.pgm@gmail.com>
Date: Sat, 25 Oct 2025 09:25:27 +0200
Subject: [PATCH] cmd/compile: teach prove about unsigned rounding-up divide

Change-Id: Ia7b5242c723f83ba85d12e4ca64a19fbbd126016
Reviewed-on: https://go-review.googlesource.com/c/go/+/714622
Auto-Submit: Jorropo <jorropo.pgm@gmail.com>
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Michael Knyszek <mknyszek@google.com>
---
 src/cmd/compile/internal/ssa/prove.go | 35 +++++++++++++++++++++++++++
 test/prove.go                         | 17 +++++++++++++
 2 files changed, 52 insertions(+)

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 5a9e0a65c7..168bb29984 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2473,6 +2473,41 @@ func addLocalFacts(ft *factsTable, b *Block) {
 			OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
 			OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
 			OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
+			switch add := v.Args[0]; add.Op {
+			// round-up division pattern; given:
+			// v = (x + y) / z
+			// if y < z then v <= x
+			case OpAdd64, OpAdd32, OpAdd16, OpAdd8:
+				z := v.Args[1]
+				zl := ft.limits[z.ID]
+				var uminDivisor uint64
+				switch v.Op {
+				case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u:
+					uminDivisor = zl.umin
+				case OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8,
+					OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
+					OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
+					OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
+					uminDivisor = 1 << zl.umin
+				default:
+					panic("unreachable")
+				}
+
+				x := add.Args[0]
+				xl := ft.limits[x.ID]
+				y := add.Args[1]
+				yl := ft.limits[y.ID]
+				if unsignedAddOverflows(xl.umax, yl.umax, add.Type) {
+					continue
+				}
+
+				if xl.umax < uminDivisor {
+					ft.update(b, v, y, unsigned, lt|eq)
+				}
+				if yl.umax < uminDivisor {
+					ft.update(b, v, x, unsigned, lt|eq)
+				}
+			}
 			ft.update(b, v, v.Args[0], unsigned, lt|eq)
 		case OpMod64, OpMod32, OpMod16, OpMod8:
 			a := ft.limits[v.Args[0].ID]
diff --git a/test/prove.go b/test/prove.go
index c48280aa31..31f8d711f1 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -1078,6 +1078,23 @@ func divu(x, y uint) int {
 	return 0
 }
 
+func divuRoundUp(x, y, z uint) int {
+	x &= ^uint(0) >> 8 // can't overflow in add
+	y = min(y, 0xff-1)
+	z = max(z, 0xff)
+	r := (x + y) / z // ERROR "Proved Neq64$"
+	if r <= x {      // ERROR "Proved Leq64U$"
+		return 1
+	}
+	return 0
+}
+
+func divuRoundUpSlice(x []string) {
+	halfRoundedUp := uint(len(x)+1) / 2
+	_ = x[:halfRoundedUp] // ERROR "Proved IsSliceInBounds$"
+	_ = x[halfRoundedUp:] // ERROR "Proved IsSliceInBounds$"
+}
+
 func modu1(x, y uint) int {
 	z := x % y
 	if z < y { // ERROR "Proved Less64U$"
-- 
2.52.0