diff options
| -rw-r--r-- | src/cmd/compile/internal/ssa/prove.go | 19 | ||||
| -rw-r--r-- | test/prove.go | 14 |
2 files changed, 29 insertions, 4 deletions
diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index af2b9ef0ed..bddc1abe43 100644 --- 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 0de6bd63b4..ce6c02ffc3 100644 --- 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$" |