cmd/compile: missed prove inferences with uint conversions

[josharian]

[moved from private email with @brtzsnr]

Consider this code, adapted from test/prove.go:

package p

func f(a []int, i int) int {
    if i >= 0 && i < len(a) {
        return a[i]
    }
    if i >= 10 && i < len(a) {
        return a[i]
    }
    return 0
}

func g(a []int, i int) int {
    if uint(i) < uint(len(a)) {
        return a[i]
    }
    if i >= 10 && i < len(a) {
        return a[i]
    }
    return 0
}

Functions f and g are equivalent. The only difference between them is the expression i >= 0 && i < len(a) in f vs uint(i) < uint(len(a)). And these are equivalent, because we know that len(a) is non-negative. But compiling with go tool compile -d=ssa/prove/debug=3 x.go, we get:

x.go:5: Proved non-negative bounds IsInBounds
x.go:8: Proved non-negative bounds IsInBounds
x.go:15: Proved IsInBounds
x.go:18: Disproved IsInBounds

Going from "x.go:5: Proved non-negative bounds IsInBounds" to "x.go:15: Proved IsInBounds" is a bit unfortunate, but ok. Going from "x.go:8: Proved non-negative bounds IsInBounds" to "x.go:18: Disproved IsInBounds" seems incorrect.

[brtzsnr]

The problem in this case is that the second return a[i] is deadcode. The second condition can be reached only if i >= len(a) so the index is out of bounds which is why prove prints "Disproved".

There is indeed a missed optimization and the second condition is not fully removed. If you find a correctness issue, let me know. Otherwise, I'll address this once the go1.8 opens and I have some spare time.

edit: The difference between the output is because it looks at different facts to establish the truth value. For f it uses i >= 10 && i < len(a) and for g it uses uint(i) < uint(len(a)).

tl;dr: It's not a bug. It's dead code.

[josharian]

Thanks, Alexandru. I have a CL that I hope to mail soon (that you know about) that will make this kind of show up a lot more. Good to know that I don't have to hold that CL for this. :)

[gopherbot]

CL https://golang.org/cl/27652 mentions this issue.

[zdjones]

@josharian Can we close this issue?
Prove has changed since then, but still never reaches the bounds check on line 18 because it's dead code. Prove knows that the conditional on line 17 can't be true, so it prunes the if block without looking inside it.

f.go:5:11: Proved IsInBounds (v20)
f.go:8:11: Proved IsInBounds (v41)
f.go:15:11: Proved IsInBounds (v17)
f.go:17:2: Disproved Less64 (v32)

I don't think there is an issue here to fix, unless we want to optimize dead code before we remove it.