diff options
author | Cherry Zhang <cherryyz@google.com> | 2019-01-02 12:27:55 -0500 |
---|---|---|
committer | Cherry Zhang <cherryyz@google.com> | 2019-01-02 19:28:06 +0000 |
commit | 2e217fa726a624093eea5b099d1531c79e27a423 (patch) | |
tree | 131e5ce6fed36142a3eb9240ce1c89d1872d934c /src/cmd/compile/internal/ssa/prove.go | |
parent | 1f035d036c2a49c1b858af3260552ccaac80858d (diff) | |
download | go-2e217fa726a624093eea5b099d1531c79e27a423.tar.gz go-2e217fa726a624093eea5b099d1531c79e27a423.zip |
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>
Diffstat (limited to 'src/cmd/compile/internal/ssa/prove.go')
-rw-r--r-- | src/cmd/compile/internal/ssa/prove.go | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index 0656bb45c5..1e5f4e9c6c 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) |