$ go version
go version devel go1.20-0a4a57de4d Thu Aug 18 21:54:52 2022 +0000 linux/amd64
sort.Search, and its inlined copy in go/token.searchInts, both have code like:
func searchInts(a []int, x int) int {
i, j := 0, len(a)
for i < j {
h := int(uint(i+j) >> 1) // avoid overflow when computing h
// i ≤ h < j
if a[h] <= x { // Found IsInBounds
i = h + 1
} else {
j = h
}
}
return i - 1
}
Note that a[h] causes a bounds check, as the compiler doesn't know that 0 <= h < len(a). We intuitively know that, because h is the middle point between i and j, thus i <= h <= j. i and j themselves start as 0 and len(a) and move closer towards h.
It would be nice if the prove pass could be smart enough to tell that a[h] here does not need a bounds check. I can force its hand via if h >= 0 && h < len(a) && a[h] <= x {, but that doesn't result in a noticeable improvement:
name old time/op new time/op delta
SearchInts-16 16.2ns ± 2% 16.5ns ± 1% +1.50% (p=0.001 n=8+10)
I realize that this request is fairly specific to binary searches, but I reckon that's a common enough occurrence that we should teach prove about it.
cc @egonelbre @golang/compiler
sort.Search, and its inlined copy in go/token.searchInts, both have code like:
Note that
a[h]causes a bounds check, as the compiler doesn't know that0 <= h < len(a). We intuitively know that, becausehis the middle point betweeniandj, thusi <= h <= j.iandjthemselves start as0andlen(a)and move closer towardsh.It would be nice if the prove pass could be smart enough to tell that
a[h]here does not need a bounds check. I can force its hand viaif h >= 0 && h < len(a) && a[h] <= x {, but that doesn't result in a noticeable improvement:I realize that this request is fairly specific to binary searches, but I reckon that's a common enough occurrence that we should teach prove about it.
cc @egonelbre @golang/compiler