-
Notifications
You must be signed in to change notification settings - Fork 18.4k
Description
This code has two bounds checks but I think it should only need one. This is not entirely obvious but seems within the realm of possibility:
package p
func f(a []uint32, u uint64) {
i := len(a) // i >= 0, i <= len(a)
for u > 0 {
// 0 <= i <= len(a)
var d1 uint32
var d2 uint32
u, d1 = u/10, uint32(u%10)
u, d2 = u/10, uint32(u%10)
i -= 2 // i <= len(a)-2
a[i] = d1 // establish i >= 0
a[i+1] = d2 // 0 < i+1 <= len(a)-1
}
}
The bounds check on a[i] is needed, but the one on a[i+1] should not be, at least if my commentary is correct. Today the compiler emits both.
This may not be as trivial as #75954 and may not be worthwhile unless it is a minor tweak to existing proofs. It would speed up strconv.Itoa a little, although not as much as #75954.
A possibly simpler but similar example that the compiler also does not do is:
package p
func f(a []uint32, u uint64) {
i := 0 // i >= 0
for u > 0 {
// 0 <= i <= len(a)
var d1 uint32
var d2 uint32
u, d1 = u/10, uint32(u%10)
u, d2 = u/10, uint32(u%10)
a[i+1] = d2 // need to check i+1 <= len(a)-1
a[i] = d1 // now 0 <= i < len(a)-2, no check needed
i += 2 // i <= len(a), has not wrapped negative
}
}
Adding an explicit 0 <= i test does reduce to a single bounds check, so it seems that's what the compiler does not see.
package p
func f(a []uint32, u uint64) {
i := 0 // i >= 0
for u > 0 {
// 0 <= i <= len(a)
var d1 uint32
var d2 uint32
u, d1 = u/10, uint32(u%10)
u, d2 = u/10, uint32(u%10)
if 0 <= i {
a[i+1] = d2 // need to check i+1 <= len(a)-1
a[i] = d1 // now 0 <= i < len(a)-2, no check needed
i += 2 // i <= len(a), has not wrapped negative
}
}
}
In the first example I have not yet found an obvious test to add that explains the problem. :-)