Skip to content

Commit 4dcbb00

Browse files
committed
cmd/compile: teach prove about min/max phi operations
If there is a phi that is computing the minimum of its two inputs, then we know the result of the phi is smaller than or equal to both of its inputs. Similarly for maxiumum (although max seems less useful). This pattern happens for the case n := copy(a, b) n is the minimum of len(a) and len(b), so with this optimization we know both n <= len(a) and n <= len(b). That extra information is helpful for subsequent slicing of a or b. Fixes #16833 Change-Id: Ib4238fd1edae0f2940f62a5516a6b363bbe7928c Reviewed-on: https://go-review.googlesource.com/c/go/+/622240 Reviewed-by: Carlos Amedee <carlos@golang.org> LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com> Reviewed-by: Josh Bleecher Snyder <josharian@gmail.com> Reviewed-by: David Chase <drchase@google.com>
1 parent f5526b5 commit 4dcbb00

File tree

3 files changed

+129
-1
lines changed

3 files changed

+129
-1
lines changed

src/cmd/compile/internal/ssa/block.go

+9
Original file line numberDiff line numberDiff line change
@@ -366,6 +366,15 @@ func (b *Block) removePhiArg(phi *Value, i int) {
366366
phielimValue(phi)
367367
}
368368

369+
// uniquePred returns the predecessor of b, if there is exactly one.
370+
// Returns nil otherwise.
371+
func (b *Block) uniquePred() *Block {
372+
if len(b.Preds) != 1 {
373+
return nil
374+
}
375+
return b.Preds[0].b
376+
}
377+
369378
// LackingPos indicates whether b is a block whose position should be inherited
370379
// from its successors. This is true if all the values within it have unreliable positions
371380
// and if it is "plain", meaning that there is no control flow that is also very likely

src/cmd/compile/internal/ssa/prove.go

+78-1
Original file line numberDiff line numberDiff line change
@@ -2026,8 +2026,85 @@ func addLocalFacts(ft *factsTable, b *Block) {
20262026
if v.Args[0].Op == OpSliceMake {
20272027
ft.update(b, v, v.Args[0].Args[2], signed, eq)
20282028
}
2029-
}
2029+
case OpPhi:
2030+
addLocalFactsPhi(ft, v)
2031+
}
2032+
}
2033+
}
2034+
2035+
func addLocalFactsPhi(ft *factsTable, v *Value) {
2036+
// Look for phis that implement min/max.
2037+
// z:
2038+
// c = Less64 x y (or other Less/Leq operation)
2039+
// If c -> bx by
2040+
// bx: <- z
2041+
// -> b ...
2042+
// by: <- z
2043+
// -> b ...
2044+
// b: <- bx by
2045+
// v = Phi x y
2046+
// Then v is either min or max of x,y.
2047+
// If it is the min, then we deduce v <= x && v <= y.
2048+
// If it is the max, then we deduce v >= x && v >= y.
2049+
// The min case is useful for the copy builtin, see issue 16833.
2050+
if len(v.Args) != 2 {
2051+
return
2052+
}
2053+
b := v.Block
2054+
x := v.Args[0]
2055+
y := v.Args[1]
2056+
bx := b.Preds[0].b
2057+
by := b.Preds[1].b
2058+
var z *Block // branch point
2059+
switch {
2060+
case bx == by: // bx == by == z case
2061+
z = bx
2062+
case by.uniquePred() == bx: // bx == z case
2063+
z = bx
2064+
case bx.uniquePred() == by: // by == z case
2065+
z = by
2066+
case bx.uniquePred() == by.uniquePred():
2067+
z = bx.uniquePred()
2068+
}
2069+
if z == nil || z.Kind != BlockIf {
2070+
return
2071+
}
2072+
c := z.Controls[0]
2073+
if len(c.Args) != 2 {
2074+
return
2075+
}
2076+
var isMin bool // if c, a less-than comparison, is true, phi chooses x.
2077+
if bx == z {
2078+
isMin = b.Preds[0].i == 0
2079+
} else {
2080+
isMin = bx.Preds[0].i == 0
2081+
}
2082+
if c.Args[0] == x && c.Args[1] == y {
2083+
// ok
2084+
} else if c.Args[0] == y && c.Args[1] == x {
2085+
// Comparison is reversed from how the values are listed in the Phi.
2086+
isMin = !isMin
2087+
} else {
2088+
// Not comparing x and y.
2089+
return
2090+
}
2091+
var dom domain
2092+
switch c.Op {
2093+
case OpLess64, OpLess32, OpLess16, OpLess8, OpLeq64, OpLeq32, OpLeq16, OpLeq8:
2094+
dom = signed
2095+
case OpLess64U, OpLess32U, OpLess16U, OpLess8U, OpLeq64U, OpLeq32U, OpLeq16U, OpLeq8U:
2096+
dom = unsigned
2097+
default:
2098+
return
2099+
}
2100+
var rel relation
2101+
if isMin {
2102+
rel = lt | eq
2103+
} else {
2104+
rel = gt | eq
20302105
}
2106+
ft.update(b, v, x, dom, rel)
2107+
ft.update(b, v, y, dom, rel)
20312108
}
20322109

20332110
var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero}

test/prove.go

+42
Original file line numberDiff line numberDiff line change
@@ -1670,6 +1670,48 @@ func neg64mightOverflowDuringNeg(a uint64, ensureAllBranchesCouldHappen func() b
16701670
return z
16711671
}
16721672

1673+
func phiMin(a, b []byte) {
1674+
_ = a[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
1675+
_ = b[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
1676+
_ = a[:max(len(a), len(b))]
1677+
_ = b[:max(len(a), len(b))]
1678+
x := len(a)
1679+
if x > len(b) {
1680+
x = len(b)
1681+
useInt(0)
1682+
}
1683+
_ = a[:x] // ERROR "Proved IsSliceInBounds"
1684+
y := len(a)
1685+
if y > len(b) {
1686+
y = len(b)
1687+
useInt(0)
1688+
} else {
1689+
useInt(1)
1690+
}
1691+
_ = b[:y] // ERROR "Proved IsSliceInBounds"
1692+
}
1693+
1694+
func issue16833(a, b []byte) {
1695+
n := copy(a, b)
1696+
_ = a[n:] // ERROR "Proved IsSliceInBounds"
1697+
_ = b[n:] // ERROR "Proved IsSliceInBounds"
1698+
_ = a[:n] // ERROR "Proved IsSliceInBounds"
1699+
_ = b[:n] // ERROR "Proved IsSliceInBounds"
1700+
}
1701+
1702+
func clampedIdx1(x []int, i int) int {
1703+
if len(x) == 0 {
1704+
return 0
1705+
}
1706+
return x[min(max(0, i), len(x)-1)] // ERROR "Proved IsInBounds"
1707+
}
1708+
func clampedIdx2(x []int, i int) int {
1709+
if len(x) == 0 {
1710+
return 0
1711+
}
1712+
return x[max(min(i, len(x)-1), 0)] // TODO: can't get rid of this bounds check yet
1713+
}
1714+
16731715
//go:noinline
16741716
func useInt(a int) {
16751717
}

0 commit comments

Comments
 (0)