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

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

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

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 8fe1bb7050b1f5b15273fe0372229ec8bdb00d4e..da42a675bf4370f6e3ab77dd2248f9ee84eaa54d 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2148,6 +2148,22 @@ func unsignedAddOverflows(a, b uint64, t *types.Type) bool {
        }
 }
 
+func signedAddOverflowsOrUnderflows(a, b int64, t *types.Type) bool {
+       r := a + b
+       switch t.Size() {
+       case 8:
+               return (a >= 0 && b >= 0 && r < 0) || (a < 0 && b < 0 && r >= 0)
+       case 4:
+               return r < math.MinInt32 || math.MaxInt32 < r
+       case 2:
+               return r < math.MinInt16 || math.MaxInt16 < r
+       case 1:
+               return r < math.MinInt8 || math.MaxInt8 < r
+       default:
+               panic("unreachable")
+       }
+}
+
 func addLocalFacts(ft *factsTable, b *Block) {
        // Propagate constant ranges among values in this block.
        // We do this before the second loop so that we have the
@@ -2182,6 +2198,20 @@ func addLocalFacts(ft *factsTable, b *Block) {
                                }
                                ft.update(b, v, v.Args[0], unsigned, r)
                        }
+                       if x.min >= 0 && !signedAddOverflowsOrUnderflows(x.max, y.max, v.Type) {
+                               r := gt
+                               if !x.nonzero() {
+                                       r |= eq
+                               }
+                               ft.update(b, v, v.Args[1], signed, r)
+                       }
+                       if y.min >= 0 && !signedAddOverflowsOrUnderflows(x.max, y.max, v.Type) {
+                               r := gt
+                               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 e843edcbf0a29fc1d1a3b3bf77f8f4c929d861ec..5ed92ba912623a937b91a95945948ded23a073b7 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -2104,6 +2104,73 @@ func transitiveProofsThroughOverflowingUnsignedAdd(x, y, z uint64) {
        }
 }
 
+func transitiveProofsThroughNonOverflowingSignedAddPositive(x, y, z int64) {
+       x &= 1<<62 - 1
+       y &= 1<<62 - 1
+
+       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
+       }
+
+       x |= 1
+       y |= 1
+       a = x + y
+       if a == x { // ERROR "Disproved Eq64$"
+               return
+       }
+       if a == y { // ERROR "Disproved Eq64$"
+               return
+       }
+}
+
+func transitiveProofsThroughOverflowingSignedAddPositive(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 { // ERROR "Disproved Eq64$"
+               return
+       }
+       if a == y { // ERROR "Disproved Eq64$"
+               return
+       }
+}
+
 //go:noinline
 func useInt(a int) {
 }

diff --git a/test/prove_constant_folding.go b/test/prove_constant_folding.go
index bca96847ba644174259b706edff1803defa7fac8..366c446b8303f865a84e66f3c54bcc32c85182f6 100644 (file)
--- a/test/prove_constant_folding.go
+++ b/test/prove_constant_folding.go
@@ -9,25 +9,25 @@
 package main
 
 func f0i(x int) int {
-  if x == 20 {
-    return x // ERROR "Proved.+is constant 20$"
-  }
+       if x == 20 {
+               return x // ERROR "Proved.+is constant 20$"
+       }
 
-  if (x + 20) == 20 {
-    return x + 5 // ERROR "Proved.+is constant 0$" "Proved.+is constant 5$"
-  }
+       if (x + 20) == 20 {
+               return x + 5 // ERROR "Proved.+is constant 0$" "Proved.+is constant 5$" "x\+d >=? w"
+       }
 
-  return x / 2
+       return x / 2
 }
 
 func f0u(x uint) uint {
-  if x == 20 {
-    return x // ERROR "Proved.+is constant 20$"
-  }
+       if x == 20 {
+               return x // ERROR "Proved.+is constant 20$"
+       }
 
-  if (x + 20) == 20 {
-    return x + 5 // ERROR "Proved.+is constant 0$" "Proved.+is constant 5$"
-  }
+       if (x + 20) == 20 {
+               return x + 5 // ERROR "Proved.+is constant 0$" "Proved.+is constant 5$" "x\+d >=? w"
+       }
 
-  return x / 2
+       return x / 2
 }