Skip to content

cmd/compile: teach prove pass that x|1 > 0 for unsigned x #46444

@josharian

Description

@josharian
package p

import "math/bits"

func f(x uint32) int {
    return bits.Len32(x|1)
}

Compiles to:

TEXT    "".f(SB), NOSPLIT|ABIInternal, $0-16
        FUNCDATA        $0, gclocals·33cdeccccebe80329f1fdbee7f5874cb(SB)
        FUNCDATA        $1, gclocals·33cdeccccebe80329f1fdbee7f5874cb(SB)
        MOVL    "".x+8(SP), AX
        ORL     $1, AX
        LEAQ    (AX)(AX*1), AX
        LEAQ    1(AX), AX
        BSRQ    AX, AX
        MOVQ    AX, "".~r1+16(SP)
        RET

Instead of the LEAQ/LEAQ/BSRQ triple of instructions, it should be a single BSRL.

There are two parts to this.

Part one is introducing OpBitLenNNNonZero ops, much as we have OpCtzNNNonZero ops, and hooking them up appropriately. This is easy.

Part two is teaching the prove pass that unsigned x|1 > 0.

Seems like it should be a simple thing to teach it, but I always get lost in the prove pass. Any hints?

cc @zdjones @dr2chase @randall77

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions