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 golang#29502.

Change-Id: Ia9f7d814264b1a3ddf78f52e2ce23377450e6e8a
Reviewed-on: https://go-review.googlesource.com/c/156019
Reviewed-by: David Chase <[email protected]>

src/cmd/compile/internal/ssa/prove.go

@@ -197,6 +197,9 @@ func newFactsTable(f *Func) *factsTable {
 // update updates the set of relations between v and w in domain d
 // restricting it to r.
 func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
+	if parent.Func.pass.debug > 2 {
+		parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r)
+	}
 	// No need to do anything else if we already found unsat.
 	if ft.unsat {
 		return
@@ -234,6 +237,9 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 			panic("unknown relation")
 		}
 		if !ok {
+			if parent.Func.pass.debug > 2 {
+				parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
+			}
 			ft.unsat = true
 			return
 		}
@@ -260,6 +266,9 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 		ft.facts[p] = oldR & r
 		// If this relation is not satisfiable, mark it and exit right away
 		if oldR&r == 0 {
+			if parent.Func.pass.debug > 2 {
+				parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
+			}
 			ft.unsat = true
 			return
 		}
@@ -361,7 +370,7 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 		lim = old.intersect(lim)
 		ft.limits[v.ID] = lim
 		if v.Block.Func.pass.debug > 2 {
-			v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s", parent, v, w, lim.String())
+			v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s %s", parent, v, w, r, lim.String())
 		}
 		if lim.min > lim.max || lim.umin > lim.umax {
 			ft.unsat = true
@@ -442,7 +451,7 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 	if r == gt || r == gt|eq {
 		if x, delta := isConstDelta(v); x != nil && 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)
+				parent.Func.Warnl(parent.Pos, "x+d %s w; x:%v %v delta:%v w:%v d:%v", r, x, parent.String(), delta, w.AuxInt, d)
 			}
 			if !w.isGenericIntConst() {
 				// If we know that x+delta > w but w is not constant, we can derive:
@@ -503,8 +512,10 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
 					// 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)
+							if r&eq == 0 || l.max < min {
+								// x>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)

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$"