cmd/compile: fix deriving from x+d >= w on overflow in prove pass

In the case of x+d >= w, where d and w are constants, we are
deriving x is within the bound of min=w-d and max=maxInt-d. When
there is an overflow (min >= max), we know only one of x >= min
or x <= max is true, and we derive this by excluding the other.
When excluding x >= min, we did not consider the equal case, so
we could incorrectly derive x <= max when x == min.

Fixes #29502.

Change-Id: Ia9f7d814264b1a3ddf78f52e2ce23377450e6e8a
Reviewed-on: https://go-review.googlesource.com/c/156019
Reviewed-by: David Chase <drchase@google.com>

1 files changed, 14 insertions, 0 deletions

diff --git a/test/prove.go b/test/prove.go
index a881b2d6e2..eb0fb2a15e 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -488,6 +488,20 @@ func f18(b []int, x int, y uint) {
 	}
 }
 
+func f19() (e int64, err error) {
+	// Issue 29502: slice[:0] is incorrectly disproved.
+	var stack []int64
+	stack = append(stack, 123)
+	if len(stack) > 1 {
+		panic("too many elements")
+	}
+	last := len(stack) - 1
+	e = stack[last]
+	// Buggy compiler prints "Disproved Geq64" for the next line.
+	stack = stack[:last] // ERROR "Proved IsSliceInBounds"
+	return e, nil
+}
+
 func sm1(b []int, x int) {
 	// Test constant argument to slicemask.
 	useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"