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
}
funcf(x, y []int, i, jint) int {
i0:=ifori>=0&&i<len(x) &&j>=0&&j<len(y) &&x[i] ==y[j] {
i++j++
}
returni-i0
}
Seems to be equivalent, has no bounds checks, generates considerably shorter code. The key piece is the addition of && j >= 0 to the inner loop condition. (Note that this should have no cost, as the compiler should optimize 0 <= j < len(y) into a single unsigned comparison.) Then I removed the outer if statement, as it was almost entirely redundant with the inner loop.
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)
The text was updated successfully, but these errors were encountered: