From: Jorropo <jorropo.pgm@gmail.com>
Date: Tue, 18 Nov 2025 00:26:01 +0000 (+0100)
Subject: cmd/compile: fix control flow for unsigned divisions proof relations
X-Git-Tag: go1.26rc1~240
X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=dc42565a20;p=gostls13.git

cmd/compile: fix control flow for unsigned divisions proof relations

The continue used to make sense since I first wrote this patch with a loop,
for testing the commutativity of the add.

This was refactored to just try both but I forgot to fix the continue.

Change-Id: I91466a052d5d8ee7193084a71faf69bd27e36d2a
Reviewed-on: https://go-review.googlesource.com/c/go/+/721204
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Mark Freeman <markfreeman@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Auto-Submit: Jorropo <jorropo.pgm@gmail.com>
---

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 789d7721d4..d4e7ed14b1 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2503,15 +2503,13 @@ func addLocalFacts(ft *factsTable, b *Block) {
 				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)
+				if !unsignedAddOverflows(xl.umax, yl.umax, add.Type) {
+					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)