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>
This commit is contained in:
Jorropo 2025-11-18 01:26:01 +01:00 committed by Gopher Robot
parent e64023dcbf
commit dc42565a20

View file

@ -2503,15 +2503,13 @@ func addLocalFacts(ft *factsTable, b *Block) {
xl := ft.limits[x.ID] xl := ft.limits[x.ID]
y := add.Args[1] y := add.Args[1]
yl := ft.limits[y.ID] yl := ft.limits[y.ID]
if unsignedAddOverflows(xl.umax, yl.umax, add.Type) { if !unsignedAddOverflows(xl.umax, yl.umax, add.Type) {
continue if xl.umax < uminDivisor {
} ft.update(b, v, y, unsigned, lt|eq)
}
if xl.umax < uminDivisor { if yl.umax < uminDivisor {
ft.update(b, v, y, unsigned, lt|eq) ft.update(b, v, x, 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) ft.update(b, v, v.Args[0], unsigned, lt|eq)