mirror of
https://github.com/golang/go
synced 2024-09-04 23:44:16 +00:00
cmd/compile: detect OFORUNTIL inductive facts in prove
Currently, we compile range loops into for loops with the obvious initialization and update of the index variable. In this form, the prove pass can see that the body is dominated by an i < len condition, and findIndVar can detect that i is an induction variable and that 0 <= i < len. GOEXPERIMENT=preemptibleloops compiles range loops to OFORUNTIL and we're preparing to unconditionally switch to a variation of this for #24543. OFORUNTIL moves the increment and condition *after* the body, which makes the bounds on the index variable much less obvious. With OFORUNTIL, proving anything about the index variable requires understanding the phi that joins the index values at the top of the loop body block. This interferes with both prove's ability to see that i < len (this is true on both paths that enter the body, but from two different conditional checks) and with findIndVar's ability to detect the induction pattern. Fix this by teaching prove to detect that the index in the pattern constructed by OFORUNTIL is an induction variable and add both bounds to the facts table. Currently this is done separately from findIndVar because it depends on prove's factsTable, while findIndVar runs before visiting blocks and building the factsTable. Without any GOEXPERIMENT, this has no effect on std or cmd. However, with GOEXPERIMENT=preemptibleloops, this change becomes necessary to prove 90 conditions in std and cmd. Change-Id: Ic025d669f81b53426309da5a6e8010e5ccaf4f49 Reviewed-on: https://go-review.googlesource.com/102603 Run-TryBot: Austin Clements <austin@google.com> TryBot-Result: Gobot Gobot <gobot@golang.org> Reviewed-by: Keith Randall <khr@golang.org>
This commit is contained in:
parent
4816eface1
commit
b812eec928
|
@ -165,30 +165,7 @@ nextb:
|
|||
}
|
||||
|
||||
if f.pass.debug >= 1 {
|
||||
mb1, mb2 := "[", "]"
|
||||
if flags&indVarMinExc != 0 {
|
||||
mb1 = "("
|
||||
}
|
||||
if flags&indVarMaxInc == 0 {
|
||||
mb2 = ")"
|
||||
}
|
||||
|
||||
mlim1, mlim2 := fmt.Sprint(min.AuxInt), fmt.Sprint(max.AuxInt)
|
||||
if !min.isGenericIntConst() {
|
||||
if f.pass.debug >= 2 {
|
||||
mlim1 = fmt.Sprint(min)
|
||||
} else {
|
||||
mlim1 = "?"
|
||||
}
|
||||
}
|
||||
if !max.isGenericIntConst() {
|
||||
if f.pass.debug >= 2 {
|
||||
mlim2 = fmt.Sprint(max)
|
||||
} else {
|
||||
mlim2 = "?"
|
||||
}
|
||||
}
|
||||
b.Func.Warnl(b.Pos, "Induction variable: limits %v%v,%v%v, increment %d", mb1, mlim1, mlim2, mb2, inc.AuxInt)
|
||||
printIndVar(b, ind, min, max, inc.AuxInt, flags)
|
||||
}
|
||||
|
||||
iv = append(iv, indVar{
|
||||
|
@ -215,3 +192,34 @@ func dropAdd64(v *Value) (*Value, int64) {
|
|||
}
|
||||
return v, 0
|
||||
}
|
||||
|
||||
func printIndVar(b *Block, i, min, max *Value, inc int64, flags indVarFlags) {
|
||||
mb1, mb2 := "[", "]"
|
||||
if flags&indVarMinExc != 0 {
|
||||
mb1 = "("
|
||||
}
|
||||
if flags&indVarMaxInc == 0 {
|
||||
mb2 = ")"
|
||||
}
|
||||
|
||||
mlim1, mlim2 := fmt.Sprint(min.AuxInt), fmt.Sprint(max.AuxInt)
|
||||
if !min.isGenericIntConst() {
|
||||
if b.Func.pass.debug >= 2 {
|
||||
mlim1 = fmt.Sprint(min)
|
||||
} else {
|
||||
mlim1 = "?"
|
||||
}
|
||||
}
|
||||
if !max.isGenericIntConst() {
|
||||
if b.Func.pass.debug >= 2 {
|
||||
mlim2 = fmt.Sprint(max)
|
||||
} else {
|
||||
mlim2 = "?"
|
||||
}
|
||||
}
|
||||
extra := ""
|
||||
if b.Func.pass.debug >= 2 {
|
||||
extra = fmt.Sprintf(" (%s)", i)
|
||||
}
|
||||
b.Func.Warnl(b.Pos, "Induction variable: limits %v%v,%v%v, increment %d%s", mb1, mlim1, mlim2, mb2, inc, extra)
|
||||
}
|
||||
|
|
|
@ -827,6 +827,9 @@ func prove(f *Func) {
|
|||
// ft when we unwind.
|
||||
}
|
||||
|
||||
// Add inductive facts for phis in this block.
|
||||
addLocalInductiveFacts(ft, node.block)
|
||||
|
||||
work = append(work, bp{
|
||||
block: node.block,
|
||||
state: simplify,
|
||||
|
@ -965,6 +968,108 @@ func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r rel
|
|||
}
|
||||
}
|
||||
|
||||
// addLocalInductiveFacts adds inductive facts when visiting b, where
|
||||
// b is a join point in a loop. In contrast with findIndVar, this
|
||||
// depends on facts established for b, which is why it happens when
|
||||
// visiting b. addLocalInductiveFacts specifically targets the pattern
|
||||
// created by OFORUNTIL, which isn't detected by findIndVar.
|
||||
//
|
||||
// TODO: It would be nice to combine this with findIndVar.
|
||||
func addLocalInductiveFacts(ft *factsTable, b *Block) {
|
||||
// This looks for a specific pattern of induction:
|
||||
//
|
||||
// 1. i1 = OpPhi(min, i2) in b
|
||||
// 2. i2 = i1 + 1
|
||||
// 3. i2 < max at exit from b.Preds[1]
|
||||
// 4. min < max
|
||||
//
|
||||
// If all of these conditions are true, then i1 < max and i1 >= min.
|
||||
|
||||
for _, i1 := range b.Values {
|
||||
if i1.Op != OpPhi {
|
||||
continue
|
||||
}
|
||||
|
||||
// Check for conditions 1 and 2. This is easy to do
|
||||
// and will throw out most phis.
|
||||
min, i2 := i1.Args[0], i1.Args[1]
|
||||
if i1q, delta := isConstDelta(i2); i1q != i1 || delta != 1 {
|
||||
continue
|
||||
}
|
||||
|
||||
// Try to prove condition 3. We can't just query the
|
||||
// fact table for this because we don't know what the
|
||||
// facts of b.Preds[1] are (in general, b.Preds[1] is
|
||||
// a loop-back edge, so we haven't even been there
|
||||
// yet). As a conservative approximation, we look for
|
||||
// this condition in the predecessor chain until we
|
||||
// hit a join point.
|
||||
uniquePred := func(b *Block) *Block {
|
||||
if len(b.Preds) == 1 {
|
||||
return b.Preds[0].b
|
||||
}
|
||||
return nil
|
||||
}
|
||||
pred, child := b.Preds[1].b, b
|
||||
for ; pred != nil; pred = uniquePred(pred) {
|
||||
if pred.Kind != BlockIf {
|
||||
continue
|
||||
}
|
||||
|
||||
br := unknown
|
||||
if pred.Succs[0].b == child {
|
||||
br = positive
|
||||
}
|
||||
if pred.Succs[1].b == child {
|
||||
if br != unknown {
|
||||
continue
|
||||
}
|
||||
br = negative
|
||||
}
|
||||
|
||||
tr, has := domainRelationTable[pred.Control.Op]
|
||||
if !has {
|
||||
continue
|
||||
}
|
||||
r := tr.r
|
||||
if br == negative {
|
||||
// Negative branch taken to reach b.
|
||||
// Complement the relations.
|
||||
r = (lt | eq | gt) ^ r
|
||||
}
|
||||
|
||||
// Check for i2 < max or max > i2.
|
||||
var max *Value
|
||||
if r == lt && pred.Control.Args[0] == i2 {
|
||||
max = pred.Control.Args[1]
|
||||
} else if r == gt && pred.Control.Args[1] == i2 {
|
||||
max = pred.Control.Args[0]
|
||||
} else {
|
||||
continue
|
||||
}
|
||||
|
||||
// Check condition 4 now that we have a
|
||||
// candidate max. For this we can query the
|
||||
// fact table. We "prove" min < max by showing
|
||||
// that min >= max is unsat. (This may simply
|
||||
// compare two constants; that's fine.)
|
||||
ft.checkpoint()
|
||||
ft.update(b, min, max, tr.d, gt|eq)
|
||||
proved := ft.unsat
|
||||
ft.restore()
|
||||
|
||||
if proved {
|
||||
// We know that min <= i1 < max.
|
||||
if b.Func.pass.debug > 0 {
|
||||
printIndVar(b, i1, min, max, 1, 0)
|
||||
}
|
||||
ft.update(b, min, i1, tr.d, lt|eq)
|
||||
ft.update(b, i1, max, tr.d, lt)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero}
|
||||
|
||||
// simplifyBlock simplifies some constant values in b and evaluates
|
||||
|
|
|
@ -648,6 +648,20 @@ func constsuffix(s string) bool {
|
|||
return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
|
||||
}
|
||||
|
||||
// oforuntil tests the pattern created by OFORUNTIL blocks. These are
|
||||
// handled by addLocalInductiveFacts rather than findIndVar.
|
||||
func oforuntil(b []int) {
|
||||
i := 0
|
||||
if len(b) > i {
|
||||
top:
|
||||
println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
|
||||
i++
|
||||
if i < len(b) {
|
||||
goto top
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//go:noinline
|
||||
func useInt(a int) {
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue