cmd/compile: in prove, fix fence-post implications for unsigned domain

Fence-post implications of the form "x-1 >= w && x > min ⇒ x > w"
were not correctly handling unsigned domain, by always checking signed
limits.

This bug was uncovered once we taught prove that len(x) is always
>= 0 in the signed domain.

In the code being miscompiled (s[len(s)-1]), prove checks
whether len(s)-1 >= len(s) in the unsigned domain; if it proves
that this is always false, it can remove the bound check.

Notice that len(s)-1 >= len(s) can be true for len(s) = 0 because
of the wrap-around, so this is something prove should not be
able to deduce.

But because of the bug, the gate condition for the fence-post
implication was len(s) > MinInt64 instead of len(s) > 0; that
condition would be good in the signed domain but not in the
unsigned domain. And since in CL105635 we taught prove that
len(s) >= 0, the condition incorrectly triggered
(len(s) >= 0 > MinInt64) and things were going downfall.

Fixes #27251
Fixes #27289

Change-Id: I3dbcb1955ac5a66a0dcbee500f41e8d219409be5
Reviewed-on: https://go-review.googlesource.com/132495
Reviewed-by: Keith Randall <khr@golang.org>

1 files changed, 3 insertions, 1 deletions

diff --git a/test/prove.go b/test/prove.go
index 45cee9e8b5..79256893b3 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -542,7 +542,7 @@ func fence2(x, y int) {
 	}
 }
 
-func fence3(b []int, x, y int64) {
+func fence3(b, c []int, x, y int64) {
 	if x-1 >= y {
 		if x <= y { // Can't prove because x may have wrapped.
 			return
@@ -555,6 +555,8 @@ func fence3(b []int, x, y int64) {
 		}
 	}
 
+	c[len(c)-1] = 0 // Can't prove because len(c) might be 0
+
 	if n := len(b); n > 0 {
 		b[n-1] = 0 // ERROR "Proved IsInBounds$"
 	}