I just took a preliminary peek, @josharian I think this may relate to #25086. Information from a non-control op (Phi) in a non-branching block is required to complete the inference from i back to len(x) and len(y).
This code:
n := len(x)
if len(y) < n {
n = len(y)
}
concludes with a Plain SSA block containing just a Phi Op
where v8/v9 are len(x)/len(y). This block doesn't branch, so prove doesn't use it. Without the relationship between v47 and len(x)/len(y), the inferential chain from i back to len(x) and len(y) is broken.
Ideally there would be no bounds checks in the loop. Right now there are.
This grew out of a conversation in CL 164966.
cc @rasky @aclements @zdjones
The text was updated successfully, but these errors were encountered: