Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
leitzler opened this Issue Nov 20, 2018 · 4 comments

Comments

Projects
None yet
3 participants
@leitzler
Copy link
Contributor

leitzler commented Nov 20, 2018

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

This comment has been minimized.

Copy link
Contributor

josharian commented Nov 20, 2018

@zdjones

This comment has been minimized.

Copy link

zdjones commented Jan 30, 2019

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

This comment has been minimized.

Copy link

zdjones commented Feb 8, 2019

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.

@zdjones

This comment has been minimized.

Copy link

zdjones commented Feb 24, 2019

Delayed due to my son being born this week!! (I’ll delete this comment, just wanted to notify anyone watching the issue as to why I disappeared after my previous comment)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.