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>

1 files changed, 39 insertions, 0 deletions

diff --git a/test/prove.go b/test/prove.go
index 7792b432f9..ab893099bf 100644
--- 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)