I am writing code to count how long a common prefix two slices have, and I can't seem to make it bounds-check-free.
At current master, this function does not eliminate the bounds check for y[j], although it does for x[i]:
func f1(x, y []int, i, j int) int {
i0 := i
if i >= 0 && i < len(x) && j >= 0 && j < len(y) {
for i < len(x) && j < len(y) && x[i] == y[j] {
i++
j++
}
}
return i - i0
}
If I remove the i < len(x) && and the i++, then the y[j] bounds check is eliminated:
func f2(x, y []int, i, j int) int {
i0 := i
if i >= 0 && i < len(x) && j >= 0 && j < len(y) {
for j < len(y) && x[i] == y[j] {
j++
}
}
return i - i0
}
If I leave out the i++ but bring back the (unnecessary) i < len(x), the y[j] bounds check returns:
func f3(x, y []int, i, j int) int {
i0 := i
if i >= 0 && i < len(x) && j >= 0 && j < len(y) {
for i < len(x) && j < len(y) && x[i] == y[j] {
j++
}
}
return i - i0
}
This is a simpler case that also has a bounds check and may share the same root cause:
func g1(x, y []int, i, j int) int {
i0 := i
if i >= 0 {
for ; ; i++ {
if i >= len(x) {
break
}
if x[i] != 0 {
break
}
}
}
return i - i0
}
This equivalent program has no check:
func g2(x, y []int, i, j int) int {
i0 := i
if i >= 0 {
for ; i < len(x) && x[i] != 0; i++ {
}
}
return i - i0
}
This suggests the problem has to do with either the inverted condition or the use of a short-circuit to exit the loop, neither of which should fundamentally change what is being proved.
The same happens counting backward: h0 and h1 have checks (h0 has just one), but h2 is check-free:
func h0(x, y []int, i, j int) int {
i0 := i
if i <= len(x) && j <= len(y) {
for i > 0 && j > 0 && x[i-1] == y[j-1] {
i--
j--
}
}
return i0 - i
}
func h1(x, y []int, i, j int) int {
i0 := i
if i <= len(x) {
for ; ; i-- {
if i <= 0 {
break
}
if x[i-1] != 0 {
break
}
}
}
return i - i0
}
func h2(x, y []int, i, j int) int {
i0 := i
if i <= len(x) {
for ; i > 0 && x[i-1] != 0; i-- {
}
}
return i - i0
}
/cc @aclements @randall77 @rasky @brtzsnr (prove authors as best I can tell from git blame)
I am writing code to count how long a common prefix two slices have, and I can't seem to make it bounds-check-free.
At current master, this function does not eliminate the bounds check for y[j], although it does for x[i]:
If I remove the
i < len(x) &&and thei++, then the y[j] bounds check is eliminated:If I leave out the
i++but bring back the (unnecessary)i < len(x), the y[j] bounds check returns:This is a simpler case that also has a bounds check and may share the same root cause:
This equivalent program has no check:
This suggests the problem has to do with either the inverted condition or the use of a short-circuit to exit the loop, neither of which should fundamentally change what is being proved.
The same happens counting backward: h0 and h1 have checks (h0 has just one), but h2 is check-free:
/cc @aclements @randall77 @rasky @brtzsnr (prove authors as best I can tell from git blame)