go ``` cmd/compile: teach prove about min ```

wwtsj6pe 于 5个月前发布在 Go

关注(0)|答案(1)|浏览(44)

package p

func f(x, y []int) {
	n := len(x)
	if len(y) < n {
		n = len(y)
	}
	for i := 0; i < n; i++ {
		_ = x[i]
		_ = y[i]
	}
}

理想情况下，循环中不应该有边界检查。现在确实有。
这个问题源于CL 164966中的一次讨论。
cc @rasky@aclements@zdjones

go

来源：https://github.com/golang/go/issues/30584

1条答案

按热度按时间

qij5mzcb1#

我刚刚初步查看了一下，@josharian 我认为这可能与 #25086 有关。在非分支块中的非控制操作(Phi)需要完成从 i 回溯到 len(x) 和 len(y) 的推理。
这段代码：

n := len(x)
if len(y) < n {
	n = len(y)
}

以包含一个纯SSA块的Phi Op结尾

b2: ← b3 b4
    v47 = Phi <int> v9 v8 (n[int])
Plain → b5

其中 v8/v9 是 len(x)/len(y) 。这个块不分支，因此证明不会使用它。如果没有 v47 和 len(x)/len(y) 之间的关系，那么从 i 回溯到 len(x) 和 len(y) 的推理链就会断裂。

v8 = SliceLen <int> v6 (n[int])
v9 = SliceLen <int> v7
...
v47 = Phi <int> v9 v8 (n[int])
...
v16 = Less64 <bool> v14 v47
...
    v20 = IsInBounds <bool> v14 v8
...
    v30 = IsInBounds <bool> v14 v9

赞(0）回复(0）举报 5个月前

我来回答

go ``` cmd/compile: teach prove about min ```

1条答案

相关问题

热门标签

最新问答