go `cmd/compile`: 教授证明更多类型转换操作 ```markdown `cmd/compile`: 教授证明更多类型转换操作 ```

wqsoz72f 于 4个月前发布在 Go

关注(0)|答案(2)|浏览(40)

#26292 是关于证明通过 x byte 是否小于 N,int(x) 也小于 N。特别是在使用字节变量作为索引时，这似乎意味着隐式转换为 int,这会导致在 encoding/json 热点路径中不必要的边界检查。
以下是一些可能值得尝试的其他情况。我不知道它们对其他软件(如删除标准库中的边界检查)有多大用处。

如果 x uint32 等于 <10,那么 uint(x) < 10 (以及 int32/int 的相同情况)
如果 x uint64 等于 <10 并且我们在 64 位系统上，那么 uint(x) < 10
如果 x uint 等于 <10,那么 byte(x) < 10
如果 x int 为非负数且 <10,那么 uint(x) < 10

/cc @aclements@rasky

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

2条答案

按热度按时间

rxztt3cl1#

Austin的评论：
可能，但这有点棘手，因为这些是有条件的。实际上，目前没有地方可以证明我们通过事实来遍历一个块中的非控制值(这样做可能会很棘手，因为值没有排序)。这就是为什么这个CL在进行其余的证明传递之前，先添加无条件相等的事实。
但是也许我们应该遍历每个块中的其他值并向前推导事实？我有点担心这种方法的性能，以及值排序如何影响它。我们可以进行一次预处理，只标记最终影响控制值的值，这样我们就可以只为那些值进行向前推导。

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

rkttyhzu2#

将文本内容翻译为中文：将价格下调至1.13,1.12已经太晚了，无法进行任何重大操作。

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