Go: cmd/compile: teach prove about slice expressions

[mvdan]

$ cat f.go
package p

func f(s string) {
        if len(s) >= 2 {
                s = s[1:]
                _ = s[0]
        }
}
$ go version
go version devel +6d5caf38e3 Thu Nov 22 02:59:55 2018 +0000 linux/amd64
$ go build -gcflags=-d=ssa/check_bce/debug=1 f.go
# command-line-arguments
./f.go:6:8: Found IsInBounds

The bounds check disappears as soon as we rewrite the code to not reslice s. This shows up in real code fairly often, for example, I encountered it in a somewhat hot function in the encoding/json decoder:

if len(s) >= 2 && (s[0] == 'e' || s[0] == 'E') {
        s = s[1:]
        if s[0] == '+' || s[0] == '-' { // bounds check isn't eliminated here

I'm not sure how easy it would be to make the prove pass aware of slice expressions. I think handling the simple x = x[N:] case (where N is constant) should be doable, and hopefully remove a few dozen bounds checks across the standard library.

/cc @aclements @rasky @josharian

[egonelbre]

Found an especially bad case of it while debugging gio (https://go.godbolt.org/z/hc44d5):

package ex

import (
    "math"
    "encoding/binary"
)

type Point struct { X, Y float32 }
type Quad  struct { From, Ctrl, To Point }

func EncodeQuad(d []byte, q Quad) {
    if len(d) < 24 {
        return
    }
    binary.LittleEndian.PutUint32(d[0:], math.Float32bits(q.From.X))
    binary.LittleEndian.PutUint32(d[4:], math.Float32bits(q.From.Y))
    binary.LittleEndian.PutUint32(d[8:], math.Float32bits(q.Ctrl.X))
    binary.LittleEndian.PutUint32(d[12:], math.Float32bits(q.Ctrl.Y))
    binary.LittleEndian.PutUint32(d[16:], math.Float32bits(q.To.X))
    binary.LittleEndian.PutUint32(d[20:], math.Float32bits(q.To.Y))
}

Note, the problem disappears when using d = d[:24].

[go101]

Specifying lengths also makes the problem disappear.

    binary.LittleEndian.PutUint32(d[0:4], math.Float32bits(q.From.X))
    binary.LittleEndian.PutUint32(d[4:8], math.Float32bits(q.From.Y))
    binary.LittleEndian.PutUint32(d[8:12], math.Float32bits(q.Ctrl.X))
    binary.LittleEndian.PutUint32(d[12:16], math.Float32bits(q.Ctrl.Y))
    binary.LittleEndian.PutUint32(d[16:20], math.Float32bits(q.To.X))
    binary.LittleEndian.PutUint32(d[20:24], math.Float32bits(q.To.Y))

And the following code doesn't need bound checking:

func EncodeQuad(d []byte, q Quad) {
    if len(d) < 24 {
        return
    }

    _ = d[0:]
    _ = d[4:]
    _ = d[8:]
    _ = d[12:]
    _ = d[16:]
    _ = d[20:]
}

[go101]

More observations indicate this is caused by code inline:

package ex

import (
    "math"
    "encoding/binary"
)

type Point struct { X, Y float32 }
type Quad  struct { From, Ctrl, To Point }

func EncodeQuad(d []byte, q Quad) {
    if len(d) < 24 {
        return
    }

    binary.LittleEndian.PutUint32(d[0:], math.Float32bits(q.From.X))
    PutUint32_NoInline(d[4:], math.Float32bits(q.From.Y))
    PutUint32_MayInline(d[8:], math.Float32bits(q.Ctrl.X)) // bounds check
    t.PutUint32_NoInline(d[12:], math.Float32bits(q.Ctrl.Y))
    t.PutUint32_MayInline(d[16:], math.Float32bits(q.To.X)) // bounds check
    //PutUint32(d[20:], math.Float32bits(q.To.Y))
    {
        b, v := d[20:], math.Float32bits(q.To.Y)
        _ = b[3] // bounds check
        b[0] = byte(v >> 24)
        b[1] = byte(v >> 16)
        b[2] = byte(v >> 8)
        b[3] = byte(v)
    }
}

//go:noinline 
func PutUint32_NoInline(b []byte, v uint32) {
    _ = b[3] // bounds check
    b[0] = byte(v >> 24)
    b[1] = byte(v >> 16)
    b[2] = byte(v >> 8)
    b[3] = byte(v)
}

func PutUint32_MayInline(b []byte, v uint32) {
    _ = b[3] // bounds check
    b[0] = byte(v >> 24)
    b[1] = byte(v >> 16)
    b[2] = byte(v >> 8)
    b[3] = byte(v)
}

type T struct{}
var t T

//go:noinline 
func (T) PutUint32_NoInline(b []byte, v uint32) {
    _ = b[3] // bounds check
    b[0] = byte(v >> 24)
    b[1] = byte(v >> 16)
    b[2] = byte(v >> 8)
    b[3] = byte(v)
}

func (T) PutUint32_MayInline(b []byte, v uint32) {
    _ = b[3] // bounds check
    b[0] = byte(v >> 24)
    b[1] = byte(v >> 16)
    b[2] = byte(v >> 8)
    b[3] = byte(v)
}

[go101]

It is strange that only the first line eliminates bounds check:

    binary.LittleEndian.PutUint32(d[0:], math.Float32bits(q.From.X))
    binary.LittleEndian.PutUint32(d[4:], math.Float32bits(q.From.Y))
    binary.LittleEndian.PutUint32(d[8:], math.Float32bits(q.Ctrl.X))
    binary.LittleEndian.PutUint32(d[12:], math.Float32bits(q.Ctrl.Y))
    binary.LittleEndian.PutUint32(d[16:], math.Float32bits(q.To.X))
    binary.LittleEndian.PutUint32(d[20:], math.Float32bits(q.To.Y))