diff options
author | Giovanni Bajo <rasky@develer.com> | 2018-08-31 02:15:26 +0200 |
---|---|---|
committer | Giovanni Bajo <rasky@develer.com> | 2018-08-31 08:54:38 +0000 |
commit | 09ea3c08e8fd1915515383f8cb4c0bb237d2b87d (patch) | |
tree | ab09934f225a19d755c4d2c873d53c7494cabb69 /src/cmd/compile/internal/ssa/prove.go | |
parent | 8a2b5f1f39152e45e6cfe6264612f00891d0327e (diff) | |
download | go-09ea3c08e8fd1915515383f8cb4c0bb237d2b87d.tar.gz go-09ea3c08e8fd1915515383f8cb4c0bb237d2b87d.zip |
cmd/compile: in prove, fix fence-post implications for unsigned domain
Fence-post implications of the form "x-1 >= w && x > min ⇒ x > w"
were not correctly handling unsigned domain, by always checking signed
limits.
This bug was uncovered once we taught prove that len(x) is always
>= 0 in the signed domain.
In the code being miscompiled (s[len(s)-1]), prove checks
whether len(s)-1 >= len(s) in the unsigned domain; if it proves
that this is always false, it can remove the bound check.
Notice that len(s)-1 >= len(s) can be true for len(s) = 0 because
of the wrap-around, so this is something prove should not be
able to deduce.
But because of the bug, the gate condition for the fence-post
implication was len(s) > MinInt64 instead of len(s) > 0; that
condition would be good in the signed domain but not in the
unsigned domain. And since in CL105635 we taught prove that
len(s) >= 0, the condition incorrectly triggered
(len(s) >= 0 > MinInt64) and things were going downfall.
Fixes #27251
Fixes #27289
Change-Id: I3dbcb1955ac5a66a0dcbee500f41e8d219409be5
Reviewed-on: https://go-review.googlesource.com/132495
Reviewed-by: Keith Randall <khr@golang.org>
Diffstat (limited to 'src/cmd/compile/internal/ssa/prove.go')
-rw-r--r-- | src/cmd/compile/internal/ssa/prove.go | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index c20f8b7ebc..af2b9ef0ed 100644 --- a/src/cmd/compile/internal/ssa/prove.go +++ b/src/cmd/compile/internal/ssa/prove.go @@ -425,13 +425,13 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) { // // Useful for i > 0; s[i-1]. lim, ok := ft.limits[x.ID] - if ok && lim.min > opMin[v.Op] { + if ok && ((d == signed && lim.min > opMin[v.Op]) || (d == unsigned && lim.umin > 0)) { ft.update(parent, x, w, d, gt) } } else if x, delta := isConstDelta(w); x != nil && delta == 1 { // v >= x+1 && x < max ⇒ v > x lim, ok := ft.limits[x.ID] - if ok && lim.max < opMax[w.Op] { + if ok && ((d == signed && lim.max < opMax[w.Op]) || (d == unsigned && lim.umax < opUMax[w.Op])) { ft.update(parent, v, x, d, gt) } } @@ -527,6 +527,11 @@ var opMax = map[Op]int64{ OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32, } +var opUMax = map[Op]uint64{ + OpAdd64: math.MaxUint64, OpSub64: math.MaxUint64, + OpAdd32: math.MaxUint32, OpSub32: math.MaxUint32, +} + // isNonNegative reports whether v is known to be non-negative. func (ft *factsTable) isNonNegative(v *Value) bool { if isNonNegative(v) { |