cmd/compile: learn transitive proofs for safe unsigned subs

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

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

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index cf045629cb9baffc96e58ef17494decc1db04576..0c0581690fe38fd832638b6c631184d0df3f8dcd 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -2164,6 +2164,10 @@ func signedAddOverflowsOrUnderflows(a, b int64, t *types.Type) bool {
        }
 }
 
+func unsignedSubUnderflows(a, b uint64) bool {
+       return a < b
+}
+
 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
@@ -2226,6 +2230,17 @@ func addLocalFacts(ft *factsTable, b *Block) {
                                }
                                ft.update(b, v, v.Args[0], signed, r)
                        }
+               case OpSub64, OpSub32, OpSub16, OpSub8:
+                       x := ft.limits[v.Args[0].ID]
+                       y := ft.limits[v.Args[1].ID]
+                       if !unsignedSubUnderflows(x.umin, y.umax) {
+                               r := lt
+                               if !y.nonzero() {
+                                       r |= eq
+                               }
+                               ft.update(b, v, v.Args[0], unsigned, r)
+                       }
+                       // FIXME: we could also do signed facts but the overflow checks are much trickier and I don't need it yet.
                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 a8a9ce1ce44f5f3d773a15d1193e47593882745e..8daa812e766994173f760eee1b50587168ee0fa2 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -2241,6 +2241,67 @@ func transitiveProofsThroughOverflowingSignedAddNegative(x, y, z int64) {
        }
 }
 
+func transitiveProofsThroughNonOverflowingUnsignedSub(x, y, z uint64) {
+       x |= 0xfff
+       y &= 0xfff
+
+       a := x - y
+       if a < z {
+               return
+       }
+
+       if x < z { // ERROR "Disproved Less64U$"
+               return
+       }
+       if y < z {
+               return
+       }
+       if a == x {
+               return
+       }
+       if a == y {
+               return
+       }
+
+       y |= 1
+       a = x - y
+       if a == x { // ERROR "Disproved Eq64$"
+               return
+       }
+       if a == y {
+               return
+       }
+}
+
+func transitiveProofsThroughOverflowingUnsignedSub(x, y, z uint64) {
+       a := x - y
+       if a < z {
+               return
+       }
+
+       if x < z {
+               return
+       }
+       if y < z {
+               return
+       }
+       if a == x {
+               return
+       }
+       if a == y {
+               return
+       }
+
+       y |= 1
+       a = x - y
+       if a == x {
+               return
+       }
+       if a == y {
+               return
+       }
+}
+
 //go:noinline
 func useInt(a int) {
 }