cmd/compile: implement loop BCE in prove

Reuse findIndVar to discover induction variables, and then
register the facts we know about them into the facts table
when entering the loop block.

Moreover, handle "x+delta > w" while updating the facts table,
to be able to prove accesses to slices with constant offsets
such as slice[i-10].

Change-Id: I2a63d050ed58258136d54712ac7015b25c893d71
Reviewed-on: https://go-review.googlesource.com/104038
Run-TryBot: Giovanni Bajo <rasky@develer.com>
Reviewed-by: David Chase <drchase@google.com>

3 files changed, 119 insertions, 3 deletions

diff --git a/src/cmd/compile/fmt_test.go b/src/cmd/compile/fmt_test.go
index 8af7cced6a..5dd2fa50be 100644
--- a/src/cmd/compile/fmt_test.go
+++ b/src/cmd/compile/fmt_test.go
@@ -646,6 +646,7 @@ var knownFormats = map[string]string{
 	"cmd/compile/internal/ssa.Op %s":                  "",
 	"cmd/compile/internal/ssa.Op %v":                  "",
 	"cmd/compile/internal/ssa.ValAndOff %s":           "",
+	"cmd/compile/internal/ssa.domain %v":              "",
 	"cmd/compile/internal/ssa.posetNode %v":           "",
 	"cmd/compile/internal/ssa.posetTestOp %v":         "",
 	"cmd/compile/internal/ssa.rbrank %d":              "",
diff --git a/src/cmd/compile/internal/ssa/loopbce.go b/src/cmd/compile/internal/ssa/loopbce.go
index a96d98717d..7f2da4870e 100644
--- a/src/cmd/compile/internal/ssa/loopbce.go
+++ b/src/cmd/compile/internal/ssa/loopbce.go
@@ -137,7 +137,7 @@ nextb:
 			}
 		}
 
-		if f.pass.debug > 1 {
+		if f.pass.debug >= 1 {
 			if min.Op == OpConst64 {
 				b.Func.Warnl(b.Pos, "Induction variable with minimum %d and increment %d", min.AuxInt, inc.AuxInt)
 			} else {
diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 371009a57d..536cfcebf0 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -388,6 +388,77 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 			}
 		}
 	}
+
+	// Process: x+delta > w    (with delta,w constants)
+	//
+	// We want to derive: x+delta > w  ⇒  x > w-delta
+	//
+	// We do this for signed numbers for now, as that allows to prove many
+	// accesses to slices in loops.
+	//
+	// From x+delta > w, we compute (using integers of the correct size):
+	//    min = w - delta
+	//    max = MaxInt - delta
+	//
+	// And we prove that:
+	//    if min<max: min < x AND x <= max
+	//    if min>max: min < x OR  x <= max
+	//
+	// This is always correct, even in case of overflow.
+	//
+	// If the initial fact is x+delta >= w instead, the derived conditions are:
+	//    if min<max: min <= x AND x <= max
+	//    if min>max: min <= x OR  x <= max
+	//
+	// Notice the conditions for max are still <=, as they handle overflows.
+	if r == gt || r == gt|eq {
+		if x, delta := isConstDelta(v); x != nil && w.isGenericIntConst() && d == signed {
+			if parent.Func.pass.debug > 1 {
+				parent.Func.Warnl(parent.Pos, "x+d >= w; x:%v %v delta:%v w:%v d:%v", x, parent.String(), delta, w.AuxInt, d)
+			}
+
+			var min, max int64
+			var vmin, vmax *Value
+			switch x.Type.Size() {
+			case 8:
+				min = w.AuxInt - delta
+				max = int64(^uint64(0)>>1) - delta
+
+				vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min)
+				vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max)
+
+			case 4:
+				min = int64(int32(w.AuxInt) - int32(delta))
+				max = int64(int32(^uint32(0)>>1) - int32(delta))
+
+				vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min)
+				vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max)
+
+			default:
+				panic("unimplemented")
+			}
+
+			if min < max {
+				// Record that x > min and max >= x
+				ft.update(parent, x, vmin, d, r)
+				ft.update(parent, vmax, x, d, r|eq)
+			} else {
+				// We know that either x>min OR x<=max. factsTable cannot record OR conditions,
+				// so let's see if we can already prove that one of them is false, in which case
+				// the other must be true
+				if l, has := ft.limits[x.ID]; has {
+					if l.max <= min {
+						// x>min is impossible, so it must be x<=max
+						ft.update(parent, vmax, x, d, r|eq)
+					} else if l.min > max {
+						// x<=max is impossible, so it must be x>min
+						ft.update(parent, x, vmin, d, r)
+					}
+				}
+			}
+		}
+	}
+
 }
 
 var opMin = map[Op]int64{
@@ -405,8 +476,25 @@ 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)
+
+	// Check if the recorded limits can prove that the value is positive
+	if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= math.MaxInt64) {
+		return true
+	}
+
+	// Check if v = x+delta, and we can use x's limits to prove that it's positive
+	if x, delta := isConstDelta(v); x != nil {
+		if l, has := ft.limits[x.ID]; has {
+			if delta > 0 && l.min >= -delta && l.max <= math.MaxInt64-delta {
+				return true
+			}
+			if delta < 0 && l.min >= -delta {
+				return true
+			}
+		}
+	}
+
+	return false
 }
 
 // checkpoint saves the current state of known relations.
@@ -595,6 +683,16 @@ func prove(f *Func) {
 		}
 	}
 
+	// Find induction variables. Currently, findIndVars
+	// is limited to one induction variable per block.
+	var indVars map[*Block]indVar
+	for _, v := range findIndVar(f) {
+		if indVars == nil {
+			indVars = make(map[*Block]indVar)
+		}
+		indVars[v.entry] = v
+	}
+
 	// current node state
 	type walkState int
 	const (
@@ -634,6 +732,10 @@ func prove(f *Func) {
 		switch node.state {
 		case descend:
 			ft.checkpoint()
+			if iv, ok := indVars[node.block]; ok {
+				addIndVarRestrictions(ft, parent, iv)
+			}
+
 			if branch != unknown {
 				addBranchRestrictions(ft, parent, branch)
 				if ft.unsat {
@@ -688,6 +790,19 @@ func getBranch(sdom SparseTree, p *Block, b *Block) branch {
 	return unknown
 }
 
+// addIndVarRestrictions updates the factsTables ft with the facts
+// learned from the induction variable indVar which drives the loop
+// starting in Block b.
+func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
+	d := signed
+	if isNonNegative(iv.min) && isNonNegative(iv.max) {
+		d |= unsigned
+	}
+
+	addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
+	addRestrictions(b, ft, d, iv.ind, iv.max, lt)
+}
+
 // addBranchRestrictions updates the factsTables ft with the facts learned when
 // branching from Block b in direction br.
 func addBranchRestrictions(ft *factsTable, b *Block, br branch) {