$ cat f.go
package p
func f(i int, data []byte) {
if i >= 0 {
for i < len(data) {
_ = data[i] // bounds check!
i++
}
}
}
$ go build -gcflags=-d=ssa/check_bce/debug=1 f.go
# command-line-arguments
./f.go:6:33: Found IsInBounds
$ go version
go version devel +048c9164a0 Sat Nov 24 23:55:07 2018 +0000 linux/amd64
If we make the index an unsigned integer instead of using the if i >= 0 hint, the bounds check goes away.
I haven't found this in real code, but I tried this hint while trying to remove a bounds check from real code. I was surprised to see that BCE would still not do its thing with the hint. Seems to me like this should be a simple fix somewhere in the prove or BCE passes.
/cc @aclements @rasky
If we make the index an unsigned integer instead of using the
if i >= 0hint, the bounds check goes away.I haven't found this in real code, but I tried this hint while trying to remove a bounds check from real code. I was surprised to see that BCE would still not do its thing with the hint. Seems to me like this should be a simple fix somewhere in the prove or BCE passes.
/cc @aclements @rasky