Switching from u16 to u8 causes the program to run forever

[zhassan-aws]

I tried this code:

fn main() {
    let mut v = Vec::<u8>::new();
    v.push(0);
    v.push(0);
}

using the following command line invocation:

/usr/bin/time -p rmc test.rs

with RMC version: 8de5cd67609

It ran for more than 30 hours without terminating.

If u8 is replaced with u16 or u32, it terminates in ~1 sec:

$ cat test.rs 
fn main() {
    let mut v = Vec::<u16>::new();
    v.push(0);
    v.push(0);
}
$ /usr/bin/time -p rmc test.rs 
.
.
.

** 0 of 502 failed (1 iterations)
VERIFICATION SUCCESSFUL

real 1.31
user 1.17
sys 0.15

[tautschnig]

One problem here is how CBMC tracks points-to sets across unions (not field sensitive) and structs (field sensitive). On this example, the points-to set for one of the variables eventually contains one of the heap-allocated objects because of this imprecision. Such an over-approximation is ok, but may result in a substantially larger formula. In the u8 case the points-to set keeps tracking this spurious alias, and eventually passes this to almost every variable. In the u16 case, however, an integer division (division by 2 to convert to bytes) makes the points-to set switch to unknown, and it therefore no longer keeps passing on this pointer to one of the objects.

What elevates this imprecision and larger formula to a performance deal breaker is the ensuing need to use array theory, which is known to be in need of improvement in CBMC for a long time already.

I'm afraid there might not be very much that RMC can do here, unless there is a magical way of getting rid of unions.

[nchong-at-aws]

I re-tried on a recent version of Kani (fe23c27) with CBMC 5.51.0. The u8 version now verifies in a few seconds on my machine.

[zhassan-aws]

Interesting! This seems to be due to a change in Kani: I tried using CBMC 5.43.0 with the current version of Kani, and it still went through quickly. I'm curious to know what change in Kani impacted this.

[zhassan-aws]

I wasn't able to pin down the specific commit that caused this improvement, but it seems to have been working well since at least 1534ee41e69 (from Jan 7, 2022). Before this commit, I'm getting errors when trying to build.

Closing this issue.