Go version
go version go1.26-devel_c58d075 Sat Nov 15 15:41:23 2025 -0800 linux/amd64
Output of go env in your module/workspace:
Workspace is `go.godbolt.org` on `x86-64 gc (tip)` as above.
What did you do?
[Code below tested here]
Compile the below (edited from test/prove.go)
// Result: No panicBounds sections
func issue57077Div(s []int) (left, right []int) {
middle := len(s) / 2 // ERROR "Proved Div64 is unsigned$"
left = s[:middle] // ERROR "Proved IsSliceInBounds$"
right = s[middle:] // ERROR "Proved IsSliceInBounds$"
return
}
// Result: Two panicBounds sections!
func issue57077Shift(s []int) (left, right []int) {
middle := len(s) >> 1 // no such proof here or below
left = s[:middle]
right = s[middle:]
return
}
What did you see happen?
issue57077Shift contains two extra bounds checks.
What did you expect to see?
The above functions should compile to the same result, namely without extra bounds checks.
This appears to be due to right shifts not given optimizations that this recent CL by @rsc and this older CL by @Jorropo gave division for provably non-negative signed values.
The below are simple cases demonstrating how the compiler treats right shifts differently:
// Result: SHRQ $1, BX
func testLenDiv(s []int) int {
return len(s) / 2
}
// Result: SARQ $1, BX <--- Could be SHRQ as BX >= 0
func testLenShift(s []int) int {
return len(s) >> 1
}
// Result: SHRQ $1, AX (was SHRQ+SARQ in Go 1.24)
func testIfDiv(s int) int {
if s < 0 {
return 0
}
return s / 2
}
// Result: SARQ $1, AX <--- Could be SHRQ as AX >= 0
func testIfShift(s int) int {
if s < 0 {
return 0
}
return s >> 1
}
Go version
go version go1.26-devel_c58d075 Sat Nov 15 15:41:23 2025 -0800 linux/amd64Output of
go envin your module/workspace:What did you do?
[Code below tested here]
Compile the below (edited from test/prove.go)
What did you see happen?
issue57077Shiftcontains two extra bounds checks.What did you expect to see?
The above functions should compile to the same result, namely without extra bounds checks.
This appears to be due to right shifts not given optimizations that this recent CL by @rsc and this older CL by @Jorropo gave division for provably non-negative signed values.
The below are simple cases demonstrating how the compiler treats right shifts differently: