cmd/compile: teach prove about unsigned division, modulus and rsh

Fixes: #57077
Change-Id: Icffcac42e28622eadecdba26e3cd7ceca6c4aacc
Reviewed-on: https://go-review.googlesource.com/c/go/+/455095
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
Auto-Submit: Keith Randall <khr@golang.org>
TryBot-Result: Gopher Robot <gobot@golang.org>
Run-TryBot: Keith Randall <khr@golang.org>
Reviewed-by: David Chase <drchase@google.com>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 908fb5af465e9b8db478d65b9008eb9347226ddf..89098e411b346ed310b4fbbbc60f61c5ba2e25b7 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -859,6 +859,15 @@ func prove(f *Func) {
                        case OpOr64, OpOr32, OpOr16, OpOr8:
                                ft.update(b, v, v.Args[1], unsigned, gt|eq)
                                ft.update(b, v, v.Args[0], unsigned, gt|eq)
+                       case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u,
+                               OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8,
+                               OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
+                               OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
+                               OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
+                               ft.update(b, v, v.Args[0], unsigned, lt|eq)
+                       case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
+                               ft.update(b, v, v.Args[0], unsigned, lt|eq)
+                               ft.update(b, v, v.Args[1], unsigned, lt)
                        case OpPhi:
                                // Determine the min and max value of OpPhi composed entirely of integer constants.
                                //

diff --git a/test/prove.go b/test/prove.go
index 7792b432f964aa38653e8ac49b7b3961272543d9..ab893099bfd72ee3708eb1db4cfe4a345ad9005c 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -1046,6 +1046,45 @@ func and(p []byte) ([]byte, []byte) { // issue #52563
        return blk, rem
 }
 
+func rshu(x, y uint) int {
+       z := x >> y
+       if z <= x { // ERROR "Proved Leq64U$"
+               return 1
+       }
+       return 0
+}
+
+func divu(x, y uint) int {
+       z := x / y
+       if z <= x { // ERROR "Proved Leq64U$"
+               return 1
+       }
+       return 0
+}
+
+func modu1(x, y uint) int {
+       z := x % y
+       if z < y { // ERROR "Proved Less64U$"
+               return 1
+       }
+       return 0
+}
+
+func modu2(x, y uint) int {
+       z := x % y
+       if z <= x { // ERROR "Proved Leq64U$"
+               return 1
+       }
+       return 0
+}
+
+func issue57077(s []int) (left, right []int) {
+       middle := len(s) / 2
+       left = s[:middle] // ERROR "Proved IsSliceInBounds$"
+       right = s[middle:] // ERROR "Proved IsSliceInBounds$"
+       return
+}
+
 func issue51622(b []byte) int {
        if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
                return len(b)