diff options
| -rw-r--r-- | src/cmd/compile/internal/ssa/prove.go | 66 | ||||
| -rw-r--r-- | test/prove.go | 12 |
2 files changed, 72 insertions, 6 deletions
diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index 309229b4d7..7b860a6f9e 100644 --- a/src/cmd/compile/internal/ssa/prove.go +++ b/src/cmd/compile/internal/ssa/prove.go @@ -2174,6 +2174,65 @@ func unsignedSubUnderflows(a, b uint64) bool { return a < b } +// checkForChunkedIndexBounds looks for index expressions of the form +// A[i+delta] where delta < K and i <= len(A)-K. That is, this is a chunked +// iteration where the index is not directly compared to the length. +func checkForChunkedIndexBounds(ft *factsTable, b *Block, index, bound *Value) bool { + if bound.Op != OpSliceLen { + return false + } + lim := ft.limits[index.ID] + if lim.min < 0 { + return false + } + i, delta := isConstDelta(index) + if i == nil { + return false + } + if delta < 0 { + return false + } + // special case for blocked iteration over a slice. + // slicelen > i + delta && <==== if clauses above + // && index >= 0 <==== if clause above + // delta >= 0 && <==== if clause above + // slicelen-K >/>= x <==== checked below + // && K >=/> delta <==== checked below + // then v > w + // example: i <=/< len - 4/3 means i+{0,1,2,3} are legal indices + for o := ft.orderings[i.ID]; o != nil; o = o.next { + if o.d != signed { + continue + } + if ow := o.w; ow.Op == OpAdd64 { + var lenOffset *Value + if ow.Args[0] == bound { + lenOffset = ow.Args[1] + } else if ow.Args[1] == bound { + lenOffset = ow.Args[0] + } + if lenOffset == nil || lenOffset.Op != OpConst64 { + continue + } + if K := -lenOffset.AuxInt; K >= 0 { + or := o.r + if or == lt { + or = lt | eq + K++ + if K < 0 { + continue + } + } + + if delta < K && or == lt|eq { + return true + } + } + } + } + return false +} + func addLocalFacts(ft *factsTable, b *Block) { // Propagate constant ranges among values in this block. // We do this before the second loop so that we have the @@ -2285,6 +2344,13 @@ func addLocalFacts(ft *factsTable, b *Block) { if v.Args[0].Op == OpSliceMake { ft.update(b, v, v.Args[0].Args[2], signed, eq) } + case OpIsInBounds: + if checkForChunkedIndexBounds(ft, b, v.Args[0], v.Args[1]) { + if b.Func.pass.debug > 0 { + b.Func.Warnl(v.Pos, "Proved %s for blocked indexing", v.Op) + } + ft.booleanTrue(v) + } case OpPhi: addLocalFactsPhi(ft, v) } diff --git a/test/prove.go b/test/prove.go index 6d2bb0962b..bcc023dfec 100644 --- a/test/prove.go +++ b/test/prove.go @@ -773,8 +773,8 @@ func indexGT0(b []byte, n int) { func unrollUpExcl(a []int) int { var i, x int for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$" - x += a[i] // ERROR "Proved IsInBounds$" - x += a[i+1] + x += a[i] // ERROR "Proved IsInBounds$" + x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$" } if i == len(a)-1 { x += a[i] @@ -786,8 +786,8 @@ func unrollUpExcl(a []int) int { func unrollUpIncl(a []int) int { var i, x int for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$" - x += a[i] // ERROR "Proved IsInBounds$" - x += a[i+1] + x += a[i] // ERROR "Proved IsInBounds$" + x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$" } if i == len(a)-1 { x += a[i] @@ -839,7 +839,7 @@ func unrollExclStepTooLarge(a []int) int { var i, x int for i = 0; i < len(a)-1; i += 3 { x += a[i] - x += a[i+1] + x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$" } if i == len(a)-1 { x += a[i] @@ -852,7 +852,7 @@ func unrollInclStepTooLarge(a []int) int { var i, x int for i = 0; i <= len(a)-2; i += 3 { x += a[i] - x += a[i+1] + x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$" } if i == len(a)-1 { x += a[i] |