[dev.simd] cmd/compile: enhance prove to deal with double-offset IsInBounds checks

For chunked iterations (useful for, but not exclusive to,
SIMD calculations) it is common to see the combination of
```
for ; i <= len(m)-4; i += 4 {
```
and
```
r0, r1, r2, r3 := m[i], m[i+1], m[i+2], m[i+3]
``

Prove did not handle the case of len-offset1 vs index+offset2
checking, but this change fixes this.  There may be other
similar cases yet to handle -- this worked for the chunked
loops for simd, as well as a handful in std.

Change-Id: I3785df83028d517e5e5763206653b34b2befd3d0
Reviewed-on: https://go-review.googlesource.com/c/go/+/700696
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 309229b4d753b7268dcc3bdc3d995ccbdba964f0..7b860a6f9ea2b0a6fe5400fccf70f8e1cc6ad46a 100644 (file)
--- 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 6d2bb0962be89471ead55c1065da0114fc34fe4f..bcc023dfec62fd4ede99fba4571b206532579c61 100644 (file)
--- 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]