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>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 0656bb45c59d848c7ce3686a591023b46a056c4d..1e5f4e9c6cce28530a14717913e20956a3df7ee9 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/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)

diff --git a/test/prove.go b/test/prove.go
index a881b2d6e2ef873ebbafe215ef6a419aab9a0300..eb0fb2a15e813fd7eb2e661b33eadc5bca279c70 100644 (file)
--- 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$"