[release-branch.go1.11] cmd/compile: fix deriving from x+d >= w on overflow in prove...

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.

Updates #29502.
Fixes #29503.

Change-Id: Ia9f7d814264b1a3ddf78f52e2ce23377450e6e8a
Reviewed-on: https://go-review.googlesource.com/c/156019
Reviewed-by: David Chase <drchase@google.com>
(cherry picked from commit 2e217fa726a624093eea5b099d1531c79e27a423)
Reviewed-on: https://go-review.googlesource.com/c/163724
Run-TryBot: Cherry Zhang <cherryyz@google.com>
Reviewed-by: Brad Fitzpatrick <bradfitz@golang.org>
TryBot-Result: Gobot Gobot <gobot@golang.org>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index af2b9ef0ed79c68a833c7d2a6396bbddafd01566..bddc1abe43b729ad72bf2f66ad084d93a2bf213a 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 0de6bd63b4047861c4dc73323f10f2704c677c6f..ce6c02ffc34ad75c8a650fb7f7875db82a06107a 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$"