cmd/compile/internal/ssa: model right shift more precisely

Prove currently checks for 0 sign bit extraction (x>>63) at the
end of the pass, but it is more general and more useful
(and not really more work) to model right shift during
value range tracking. This handles sign bit extraction (both 0 and -1)
but also makes the value ranges available for proving bounds checks.

'go build -a -gcflags=-d=ssa/prove/debug=1 std'
finds 105 new things to prove.
https://gist.github.com/rsc/8ac41176e53ed9c2f1a664fc668e8336

For example, the compiler now recognizes that this code in
strconv does not need to check the second shift for being ≥ 64.

	msb := xHi >> 63
	retMantissa := xHi >> (msb + 38)

nor does this code in regexp:

	return b < utf8.RuneSelf && specialBytes[b%16]&(1<<(b/16)) != 0

This code in math no longer has a bounds check on the first index:

	if 0 <= n && n <= 308 {
		return pow10postab32[uint(n)/32] * pow10tab[uint(n)%32]
	}

The diff shows one "lost" proof in ycbcr.go but it's not really lost:
the expression was folded to a constant instead, and that only shows
up with debug=2. A diff of that output is at
https://gist.github.com/rsc/9139ed46c6019ae007f5a1ba4bb3250f

Change-Id: I84087311e0a303f00e2820d957a6f8b29ee22519
Reviewed-on: https://go-review.googlesource.com/c/go/+/716140
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Auto-Submit: Russ Cox <rsc@golang.org>
Reviewed-by: David Chase <drchase@google.com>

2 files changed, 149 insertions, 38 deletions

diff --git a/test/prove.go b/test/prove.go
index db32d1beb0..365e8ba006 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -971,40 +971,6 @@ func negIndex2(n int) {
 	useSlice(c)
 }
 
-// Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
-// e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
-func sh64(n int64) int64 {
-	if n < 0 {
-		return n
-	}
-	return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
-}
-
-func sh32(n int32) int32 {
-	if n < 0 {
-		return n
-	}
-	return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
-}
-
-func sh32x64(n int32) int32 {
-	if n < 0 {
-		return n
-	}
-	return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
-}
-
-func sh16(n int16) int16 {
-	if n < 0 {
-		return n
-	}
-	return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
-}
-
-func sh64noopt(n int64) int64 {
-	return n >> 63 // not optimized; n could be negative
-}
-
 // These cases are division of a positive signed integer by a power of 2.
 // The opt pass doesnt have sufficient information to see that n is positive.
 // So, instead, opt rewrites the division with a less-than-optimal replacement.
@@ -2584,6 +2550,103 @@ func swapbound(v []int) {
 	}
 }
 
+func rightshift(v *[256]int) int {
+	for i := range 1024 { // ERROR "Induction"
+		if v[i/32] == 0 { // ERROR "Proved Div64 is unsigned" "Proved IsInBounds"
+			return i
+		}
+	}
+	for i := range 1024 { // ERROR "Induction"
+		if v[i>>2] == 0 { // ERROR "Proved IsInBounds"
+			return i
+		}
+	}
+	return -1
+}
+
+func rightShiftBounds(v, s int) {
+	// The ignored "Proved" messages on the shift itself are about whether s >= 0 or s < 32 or 64.
+	// We care about the bounds for x printed on the prove(x) lines.
+
+	if -8 <= v && v <= -2 && 1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-4,-1 "
+	}
+	if -80 <= v && v <= -20 && 1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-40,-3 "
+	}
+	if -8 <= v && v <= 10 && 1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-4,5 "
+	}
+	if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=0,5 "
+	}
+
+	if -8 <= v && v <= -2 && 0 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-8,-1 "
+	}
+	if -80 <= v && v <= -20 && 0 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-80,-3 "
+	}
+	if -8 <= v && v <= 10 && 0 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-8,10 "
+	}
+	if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=0,10 "
+	}
+
+	if -8 <= v && v <= -2 && -1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-8,-1 "
+	}
+	if -80 <= v && v <= -20 && -1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-80,-3 "
+	}
+	if -8 <= v && v <= 10 && -1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=-8,10 "
+	}
+	if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		prove(x) // ERROR "Proved sm,SM=0,10 "
+	}
+}
+
+func unsignedRightShiftBounds(v uint, s int) {
+	if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		proveu(x) // ERROR "Proved sm,SM=0,10 "
+	}
+	if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		proveu(x) // ERROR "Proved sm,SM=0,10 "
+	}
+	if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		proveu(x) // ERROR "Proved sm,SM=0,5 "
+	}
+	if 20 <= v && v <= 100 && 1 <= s && s <= 3 {
+		x := v>>s // ERROR "Proved"
+		proveu(x) // ERROR "Proved sm,SM=2,50 "
+	}
+}
+
+//go:noinline
+func prove(x int) {
+}
+
+//go:noinline
+func proveu(x uint) {
+}
+
 //go:noinline
 func useInt(a int) {
 }
diff --git a/test/prove_constant_folding.go b/test/prove_constant_folding.go
index 1029c8e2d3..46764f9b9d 100644
--- a/test/prove_constant_folding.go
+++ b/test/prove_constant_folding.go
@@ -20,14 +20,62 @@ func f0i(x int) int {
 	return x + 1
 }
 
-func f0u(x uint) uint {
+func f0u(x uint) int {
 	if x == 20 {
-		return x // ERROR "Proved.+is constant 20$"
+		return int(x) // ERROR "Proved.+is constant 20$"
 	}
 
 	if (x + 20) == 20 {
-		return x + 5 // ERROR "Proved.+is constant 0$" "Proved.+is constant 5$" "x\+d >=? w"
+		return int(x + 5) // ERROR "Proved.+is constant 0$" "Proved.+is constant 5$" "x\+d >=? w"
 	}
 
-	return x + 1
+	if x < 1000 {
+		return int(x)>>31 // ERROR "Proved.+is constant 0$"
+	}
+	if x := int32(x); x < -1000 {
+		return int(x>>31) // ERROR "Proved.+is constant -1$"
+	}
+
+	return int(x) + 1
+}
+
+// Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
+// e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
+func sh64(n int64) int64 {
+	if n < 0 {
+		return n
+	}
+	return n >> 63 // ERROR "Proved .+ is constant 0$"
+}
+
+func sh32(n int32) int32 {
+	if n < 0 {
+		return n
+	}
+	return n >> 31 // ERROR "Proved .+ is constant 0$"
+}
+
+func sh32x64(n int32) int32 {
+	if n < 0 {
+		return n
+	}
+	return n >> uint64(31) // ERROR "Proved .+ is constant 0$"
+}
+
+func sh32x64n(n int32) int32 {
+	if n >= 0 {
+		return 0
+	}
+	return n >> 31// ERROR "Proved .+ is constant -1$"
+}
+
+func sh16(n int16) int16 {
+	if n < 0 {
+		return n
+	}
+	return n >> 15 // ERROR "Proved .+ is constant 0$"
+}
+
+func sh64noopt(n int64) int64 {
+	return n >> 63 // not optimized; n could be negative
 }