From 27ebc84716f19e1c5b21e3a14de3204d19f28499 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Alexandru=20Mo=C8=99oi?= <brtzsnr@gmail.com>
Date: Sat, 2 Apr 2016 10:29:11 +0200
Subject: [PATCH] cmd/compile: handle non-negatives in prove
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Handle this case:
if 0 <= i && i < len(a) {
        use a[i]
}

Shaves about 5k from pkg/tools/linux_amd64/*.

Change-Id: I6675ff49aa306b0d241b074c5738e448204cd981
Reviewed-on: https://go-review.googlesource.com/21431
Run-TryBot: Alexandru Moșoi <alexandru@mosoi.ro>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Brad Fitzpatrick <bradfitz@golang.org>
---
 src/cmd/compile/internal/ssa/prove.go | 12 ++++++++++--
 test/prove.go                         | 25 ++++++++++++++++++++++---
 2 files changed, 32 insertions(+), 5 deletions(-)

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 6054541c3b..2bda780d02 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -296,6 +296,15 @@ func (ft *factsTable) update(v, w *Value, d domain, r relation) {
 	}
 }
 
+// isNonNegative returns true if v is known to be non-negative.
+func (ft *factsTable) isNonNegative(v *Value) bool {
+	if isNonNegative(v) {
+		return true
+	}
+	l, has := ft.limits[v.ID]
+	return has && (l.min >= 0 || l.umax <= math.MaxInt64)
+}
+
 // checkpoint saves the current state of known relations.
 // Called when descending on a branch.
 func (ft *factsTable) checkpoint() {
@@ -608,8 +617,7 @@ func simplifyBlock(ft *factsTable, b *Block) branch {
 	// to the upper bound than this is proven. Most useful in cases such as:
 	// if len(a) <= 1 { return }
 	// do something with a[1]
-	// TODO: use constant bounds to do isNonNegative.
-	if (c.Op == OpIsInBounds || c.Op == OpIsSliceInBounds) && isNonNegative(c.Args[0]) {
+	if (c.Op == OpIsInBounds || c.Op == OpIsSliceInBounds) && ft.isNonNegative(c.Args[0]) {
 		m := ft.get(a0, a1, signed)
 		if m != 0 && tr.r&m == m {
 			if b.Func.pass.debug > 0 {
diff --git a/test/prove.go b/test/prove.go
index 4fc1d674d8..a78adf03dc 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -29,11 +29,30 @@ func f1(a []int) int {
 }
 
 func f1b(a []int, i int, j uint) int {
-	if i >= 0 && i < len(a) { // TODO: handle this case
-		return a[i]
+	if i >= 0 && i < len(a) {
+		return a[i] // ERROR "Proved non-negative bounds IsInBounds$"
+	}
+	if i >= 10 && i < len(a) {
+		return a[i] // ERROR "Proved non-negative bounds IsInBounds$"
+	}
+	if i >= 10 && i < len(a) {
+		return a[i] // ERROR "Proved non-negative bounds IsInBounds$"
+	}
+	if i >= 10 && i < len(a) { // todo: handle this case
+		return a[i-10]
 	}
 	if j < uint(len(a)) {
-		return a[j] // ERROR "Proved IsInBounds"
+		return a[j] // ERROR "Proved IsInBounds$"
+	}
+	return 0
+}
+
+func f1c(a []int, i int64) int {
+	c := uint64(math.MaxInt64 + 10) // overflows int
+	d := int64(c)
+	if i >= d && i < int64(len(a)) {
+		// d overflows, should not be handled.
+		return a[i]
 	}
 	return 0
 }