Ranges don't always automatically work

[mvdan]

$ cat foo.wuffs
packageid "xxxx"

pri const arr[4] u8 = $(1, 2, 3, 4)

pub func foo(a u8)() {
        var b u8 = in.a >> 6
        var elem u8 = arr[b]
}
$ wuffs-c gen -package_name xxxx foo.wuffs
cannot prove "b < 4": failed at foo.wuffs:7. Facts:
        b == (in.a >> 6)

However, all of the cases below work:

var b u8 = in.a >> 6
if b < 4 { // always true, redundant
        var elem u8 = arr[b]
}

var b u8 = in.a >> 6
var elem u8 = arr[b & 0x03]

Funnily enough though, this doesn't work - I presume because the fact gets lost between statements:

var b u8 = (in.a >> 6) & 0x03
var elem u8 = arr[b]

Might be related to #5.

[mvdan]

This also seems to work:

var elem u8 = arr[in.a >> 6]

[mvdan]

I see now that I am supposed to be explicit about ranges when declaring vars:

var b u8[..0x3] = in.a >> 6
var elem u8 = arr[b]

If that's what I should be doing, then please do close this issue. Though I would argue that this should be in an FAQ somewhere; I assumed that Wuffs automatically did this.

[nigeltao]

Yeah, that will work for now, but longer term, you probably shouldn't need the [..0x3] range refinement. Currently, after an assignment like x = y, we automatically add the fact x == y. In the future, we might also add facts x >= min_possible_y and x <= max_possible_y, although specifying exactly how to calculate the min and max values, especially if y is an expression, could be tricky. In your case, after b = in.a >> 6, that should implicitly assert that b <= 3, and so the array index arr[b] is proved in bounds, without needing the [..0x3].

But, yeah, in the very short term, adding [..0x3] will keep you moving.

[mvdan]

Awesome, thanks. Should this issue stay open then? I no longer have a blocking issue in the short term, but it would still be nice if this worked automatically.

[nigeltao]

Let's keep the issue open for now.