cmd/compile: learn transitive proofs for safe negative signed adds

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

Change-Id: Ib2c6dbc82fb04f50f2d17fbe6626c9fc322fb478
Reviewed-on: https://go-review.googlesource.com/c/go/+/685820
Auto-Submit: Michael Knyszek <mknyszek@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Michael Knyszek <mknyszek@google.com>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index da42a675bf4370f6e3ab77dd2248f9ee84eaa54d..cf045629cb9baffc96e58ef17494decc1db04576 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2212,6 +2212,20 @@ func addLocalFacts(ft *factsTable, b *Block) {
                                }
                                ft.update(b, v, v.Args[0], signed, r)
                        }
+                       if x.max <= 0 && !signedAddOverflowsOrUnderflows(x.min, y.min, v.Type) {
+                               r := lt
+                               if !x.nonzero() {
+                                       r |= eq
+                               }
+                               ft.update(b, v, v.Args[1], signed, r)
+                       }
+                       if y.max <= 0 && !signedAddOverflowsOrUnderflows(x.min, y.min, v.Type) {
+                               r := lt
+                               if !y.nonzero() {
+                                       r |= eq
+                               }
+                               ft.update(b, v, v.Args[0], signed, r)
+                       }
                case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
                        ft.update(b, v, v.Args[0], unsigned, lt|eq)
                        ft.update(b, v, v.Args[1], unsigned, lt|eq)

diff --git a/test/prove.go b/test/prove.go
index 5ed92ba912623a937b91a95945948ded23a073b7..a8a9ce1ce44f5f3d773a15d1193e47593882745e 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -2171,6 +2171,76 @@ func transitiveProofsThroughOverflowingSignedAddPositive(x, y, z int64) {
        }
 }
 
+func transitiveProofsThroughNonOverflowingSignedAddNegative(x, y, z int64) {
+       if x < math.MinInt64>>1 || x > 0 ||
+               y < math.MinInt64>>1 || y > 0 {
+               return
+       }
+
+       a := x + y
+       if a < z {
+               return
+       }
+
+       if x < z { // ERROR "Disproved Less64$"
+               return
+       }
+       if y < z { // ERROR "Disproved Less64$"
+               return
+       }
+       if a == x {
+               return
+       }
+       if a == y {
+               return
+       }
+
+       if x == 0 && y == 0 {
+               return
+       }
+       a = x + y
+       if a == x { // ERROR "Disproved Eq64$"
+               return
+       }
+       if a == y { // ERROR "Disproved Eq64$"
+               return
+       }
+}
+
+func transitiveProofsThroughOverflowingSignedAddNegative(x, y, z int64) {
+       if x >= 0 || y >= 0 {
+               return
+       }
+
+       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) {
 }