cmd/compile: Improve BCE when using positive int as slice index

[leitzler]

What version of Go are you using (go version)?

$ go version
go version go1.11.2 linux/amd64

Does this issue reproduce with the latest release?

Yes

What operating system and processor architecture are you using (go env)?

go env Output

$ go env
GOARCH="amd64"
GOBIN=""
GOCACHE="/home/leitzler/.cache/go-build"
GOEXE=""
GOFLAGS=""
GOHOSTARCH="amd64"
GOHOSTOS="linux"
GOOS="linux"
GOPATH="/home/leitzler/go"
GOPROXY=""
GORACE=""
GOROOT="/usr/local/go"
GOTMPDIR=""
GOTOOLDIR="/usr/local/go/pkg/tool/linux_amd64"
GCCGO="gccgo"
CC="gcc"
CXX="g++"
CGO_ENABLED="1"
GOMOD=""
CGO_CFLAGS="-g -O2"
CGO_CPPFLAGS=""
CGO_CXXFLAGS="-g -O2"
CGO_FFLAGS="-g -O2"
CGO_LDFLAGS="-g -O2"
PKG_CONFIG="pkg-config"
GOGCCFLAGS="-fPIC -m64 -pthread -fmessage-length=0 -fdebug-prefix-map=/tmp/go-build416756199=/tmp/go-build -gno-record-gcc-switches"

What did you do?

package main  

// Should be enough with the first bounds check (?)
func foo(b []byte, n int) {  
    _ = b[n]  // Bounds check  
    _ = b[25] // Bounds check  
  
    for i := n; i <= 25; i++ {  
        b[i] = 123 // Bounds check  
    }  
}  

// prove should be able to eliminate bounds check in the for-loop here
func foo2(b []byte, n int) {  
    if n < 0 {  
        panic("")  
    }  
  
    _ = b[n]  // Bounds check  
    _ = b[25] // Bounds check  
  
    for i := n; i <= 25; i++ {  
        b[i] = 123 // Bounds check  
    }  
}  

// when using uint, it works as expected and eliminates bounds check in the loop  
func foo3(b []byte, n uint) {  
    _ = b[25] // Bounds check  
  
    for i := n; i <= 25; i++ {  
        b[i] = 123 // Bounds check elimintated  
    }  
}  

What did you expect to see?

BCE in all examples above.

What did you see instead?

BCE in the third example only.

[josharian]

@rasky @aclements

[zdjones]

I think this second example, foo2() broadens the issue and includes a second issue addressed in #28956. Can I suggest narrowing this issue to just include foo() and focus this issue on using _ = b[n] and _ = b[25] as a hint for BCE?

My reasoning (which could be mistaken):

In order to do BCE in this loop, prove must:

1. Learn facts about n, and
2. Correctly propagate/reference that information when considering the bounds check in the loop.

As far as I can tell, from debugging the prove pass of foo():

1. Should learn 0 <= n < len(b) from _ = b[n], but only learns n < len(b)
2. It correctly propagates n < len(b) to the bounds check in the loop, but we don't know if it can correctly propagate 0 <= n because it never learned it.

As far as I can tell, from debugging the prove pass of foo2()

1. a. Correctly learns n >= 0 from if n < 0 { panic("")}
   b. As in foo() Should learn 0 <= n < len(b) from _ = b[n], but only learns n < len(b)
2. Fails to correctly propagate n >= 0 to the bounds check in the loop

So:

The _ = b[n] hint is currently only known to be a learning problem ( I suspect it will also suffer from the same propagation problem as below).
The if n < 0 hint is a propagation/reference problem, which will hopefully be fixed by my patch to #28956.

[zdjones]

I've submitted patch https://golang.org/cl/161437 cmd/compile: make prove use poset to check non-negatives, which fixes #28956, the hint propagation problem from step 2 in my comment above.

I've got another patch ready that fixes the remaining issue here, step 1 in my comment above, learning 0 <= n from _ = [n]. The patch for this problem is dependent on the patch I just linked to, which I just need to benchmark. I then hope to submit the patch for this issue in the next few days.

[gopherbot]

Change https://golang.org/cl/170121 mentions this issue: cmd/compile: make prove learn index >= 0 from successful bounds checks