Flow Typing in VcGenerator

[DavePearce]

Following on from #466, the following currently fails to verify:

type nat is (int x) where x >= 0

function g(nat|bool y) -> int:
    return 1

function f() -> int:
    //
    int|null x = 1
    return g(x)

The reason for the failure is that the type of x at the point of the call in VcGenerator is int|null. This leads to the following verification condition:

type nat is (int r0) where:
    r0 >= 0

function g(bool | test.nat r0) -> (int)

function f() -> (int)

assert "type invariant not satisfied (argument 0)":
    if:
       1 is null | int
    then:
       1 is bool | test.nat

We can see that the problem arises because 1 is null | int doesn't trigger r0 is int.

[DavePearce]

The essential problem here is that the verifier does not reduce the following constraints to be true or false:

1 is int
1 is int|null
!(1 is int|null)

The current rules for dealing with type tests in the verifier are very limited. Indeed, without some reworking they probably have to be (e.g. cannot distinguish integers from reals, etc).