]> Cypherpunks repositories - gostls13.git/commitdiff
cmd/compile: fix control flow for unsigned divisions proof relations
authorJorropo <jorropo.pgm@gmail.com>
Tue, 18 Nov 2025 00:26:01 +0000 (01:26 +0100)
committerGopher Robot <gobot@golang.org>
Wed, 19 Nov 2025 21:33:58 +0000 (13:33 -0800)
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>

src/cmd/compile/internal/ssa/prove.go

index 789d7721d42b889665fa7e6a2d1800c21a4d6de1..d4e7ed14b168fea50a9dc82b59f196e3243732ef 100644 (file)
@@ -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)