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: BCE does not take transitivity into account #19714

navytux opened this issue Mar 25, 2017 · 5 comments


None yet
5 participants
Copy link

commented Mar 25, 2017

Please answer these questions before submitting your issue. Thanks!

What did you do?

Hello up there. Please consider the following function:

package xxx

func Aaa(b []byte, i int) {
        if !(0 <= i && i < len(b)) {

        for j := 0; j < i; j++ {


here i is in valid range for b and j is iterating in [0,i) so it is also in valid range for b. However Aaa compiles to:

TEXT ·Aaa(SB), $8-32 // loopbce2.go:3
        // SUBQ    $8, SP
        // MOVQ    BP, (SP) (BP save)
        // LEAQ    (SP), BP (BP init)
        // FUNCDATA $0, gclocals·4032f753396f2012ad1784f398b170f4(SB) (args)
        FUNCDATA   $1, gclocals·69c1753bd5f81501d95132d08af04464(SB) (locals)
        MOVQ       i+24(FP), AX           // loopbce2.go:4
        TESTQ      AX, AX
        JLT        $0, pc80
        MOVQ       b+8(FP), CX
        CMPQ       AX, CX
        JGE        $0, pc80
        MOVQ       b+0(FP), DX            // loopbce2.go:8
        MOVQ       $0, BX                 // loopbce2.go:4
        CMPQ       BX, AX                 // loopbce2.go:8
        JGE        $0, pc71
        CMPQ       BX, CX                 // loopbce2.go:9      <-- NOTE
        JCC        $0, pc64                                     <-- NOTE
        MOVBLZX    (DX)(BX*1), SI
        INCL       SI
        MOVB       SIB, (DX)(BX*1)
        INCQ       BX                     // loopbce2.go:8
        JMP        pc39
        PCDATA     $0, $1                 // loopbce2.go:9
        CALL       runtime.panicindex(SB)                       <-- NOTE
        // MOVQ    (SP), BP (BP restore)  // loopbce2.go:11
        // ADDQ    $8, SP (SP restore)
        // MOVQ    (SP), BP (BP restore)  // loopbce2.go:5
        // ADDQ    $8, SP (SP restore)

with b[j] access being bounds checked at runtime.

Just for the reference, if loop for j is in [0,len(b)):

        for j := 0; j < len(b); j++ {

no bounds checking is generated.

So looks like what is needed is to teach BCE that if i1 is in valid bounds, i2 in [0, i1] => i2 is also in valid bounds.

This actually came up as simplified case of

package xxx

func Encode(dst, src []byte) {
        if len(dst) < len(src) {
                return  // panic("dst overflow")

        for i, v := range src {
                dst[i] = v

where bounds checks are unneccessarily generated for dst[i].

The above case in turn tries to model e.g. encoding/hex.Encode in simplified way:

func Encode(dst, src []byte) int {
        //if len(dst) < len(src) * 2 {
        //      panic("dst overflow")

        for i, v := range src {
                dst[i*2] = hextable[v>>4]
                dst[i*2+1] = hextable[v&0x0f]

        return len(src) * 2 

where even if initial check for len(dst) < len(src) * 2 => error is activated, still 2 bounds checks are generated (for dst[i*2] and dst[i*2+1]) making hex.Encode (together with #15808) much slower than it should be:

TEXT ·Encode(SB), $24-56 // hex.go:29
        // MOVQ    (TLS), CX (stack growth prologue)
        // CMPQ    SP, 16(CX)
        // JLS     207
        // SUBQ    $24, SP
        // MOVQ    BP, 16(SP) (BP save)
        // LEAQ    16(SP), BP (BP init)
        // FUNCDATA $0, gclocals·b9de2a960cf046391bcd3b554f7fabca(SB) (args)
        FUNCDATA   $1, gclocals·69c1753bd5f81501d95132d08af04464(SB) (locals)
        MOVQ       src+32(FP), AX         // hex.go:30
        MOVQ       AX, CX
        SHLQ       $1, AX
        MOVQ       dst+8(FP), DX
        CMPQ       DX, AX
        JLT        $0, pc177
        TESTQ      CX, CX                 // hex.go:34
        JLE        $0, pc148
        MOVQ       dst+0(FP), BX
        MOVQ       src+24(FP), SI
        MOVQ       $0, DI                 // hex.go:29
        MOVBLZX    (SI), R8               // hex.go:34
        MOVQ       DI, R9                 // hex.go:35
        SHLQ       $1, DI
        MOVL       R8, R10
        SHRB       $4, R8B
        MOVBLZX    R8B, R8
        LEAQ       go.string."0123456789abcdef"(SB), R11 // hex.go:36  <-- #15808
        MOVBLZX    (R11)(R8*1), R8        // hex.go:35
        CMPQ       DI, DX                                       <-- NOTE
        JCC        $0, pc170                                    <-- NOTE
        MOVB       R8B, (BX)(DI*1)
        LEAQ       1(DI), R8              // hex.go:36
        ANDL       $15, R10
        MOVBLZX    (R11)(R10*1), R10
        CMPQ       R8, DX                                       <-- NOTE
        JCC        $0, pc163                                    <-- NOTE
        MOVB       R10B, 1(BX)(DI*1)
        INCQ       SI                     // hex.go:34
        LEAQ       1(R9), DI
        CMPQ       DI, CX
        JLT        $1, pc71
        MOVQ       AX, _r2+48(FP)         // hex.go:39
        // MOVQ    16(SP), BP (BP restore)
        // ADDQ    $24, SP (SP restore)
        // PCDATA  $0, $1 (stack growth)  // hex.go:36
        // CALL    runtime.panicindex(SB)
        // UNDEF
        // PCDATA  $0, $1                 // hex.go:35
        // CALL    runtime.panicindex(SB)
        // UNDEF
        // LEAQ    type.string(SB), AX    // hex.go:31
        // MOVQ    AX, (SP)
        // LEAQ    ·statictmp_12(SB), AX
        // MOVQ    AX, 8(SP)
        // PCDATA  $0, $1
        // CALL    runtime.gopanic(SB)
        // UNDEF
        // NOP
        // PCDATA  $0, $-1                // hex.go:29
        // CALL    runtime.morestack_noctxt(SB)
        // JMP     0

What did you expect to see?

No runtime bound checks.

What did you see instead?

Runtime bound check present for b[j] access.

Does this issue reproduce with the latest release (go1.8)?


System details

go version devel +ecc6a81617 Sat Mar 25 00:35:35 2017 +0000 linux/amd64
GOGCCFLAGS="-fPIC -m64 -pthread -fmessage-length=0 -fdebug-prefix-map=/tmp/go-build832545546=/tmp/go-build -gno-record-gcc-switches"
GOROOT/bin/go version: go version devel +ecc6a81617 Sat Mar 25 00:35:35 2017 +0000 linux/amd64
GOROOT/bin/go tool compile -V: compile version devel +ecc6a81617 Sat Mar 25 00:35:35 2017 +0000 X:framepointer
uname -sr: Linux 4.9.0-2-amd64
Distributor ID:	Debian
Description:	Debian GNU/Linux 9.0 (stretch)
Release:	9.0
Codename:	stretch
/lib/x86_64-linux-gnu/ GNU C Library (Debian GLIBC 2.24-9) stable release version 2.24, by Roland McGrath et al.
gdb --version: GNU gdb (Debian 7.12-6)

Thanks beforehand,

/cc @randall77, @dr2chase


This comment has been minimized.

Copy link

commented Mar 25, 2017


This comment has been minimized.

Copy link

commented Mar 13, 2018

I just submitted a CL that fixes the initial example.

The more complex example (hextable) has two additional problems: first, prove does not know how to handle loops; I have a solution coming for this though (which is merging loopbce into prove). Second, prove doesn't know how to handle math operations on indices or induction variables. This is harder.

Feel free to re-submit a new issue for the more complex case.


This comment has been minimized.

Copy link

commented Mar 13, 2018

Change mentions this issue: cmd/compile: in prove, add transitive closure of relations


This comment has been minimized.

Copy link
Contributor Author

commented Mar 13, 2018

@rasky thanks for taking a look at this problem.


This comment has been minimized.

Copy link
Contributor Author

commented May 1, 2018

@rasky, thanks again for your work on prove. I've moved simplified hex example to #25197.

@golang golang locked and limited conversation to collaborators May 1, 2019

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