Memory blows up on a small program involving String split

[zhassan-aws]

I tried this code:

#[kani::proof]
#[kani::unwind(4)]
#[kani::solver(cadical)]
fn main() {
    let mut s = String::with_capacity(3);
    //let c1 = 'a';
    let c1: char = kani::any();
    kani::assume(c1 == 'a');
    s.push(c1);
    s.push('.');
    let c2 = 'b';
    s.push(c2);
    let v: Vec<&str> = s.split('.').collect();
    assert_eq!(v.len(), 2);
    assert_eq!(v[0], "a");
    assert_eq!(v[1], "b");
}

using the following command line invocation:

kani test.rs

with Kani version: 048b598f730

The version that uses let c1 = 'a'; verifies in ~1 second, but for the version the uses:

    let c1: char = kani::any();
    kani::assume(c1 == 'a');

memory consumption reaches 30 GB.

[zhassan-aws]

The original program I was trying to prove is as follows:

#[kani::proof]
#[kani::unwind(4)]
#[kani::solver(cadical)]
fn main() {
    let mut s = String::with_capacity(3);
    let c1: char = kani::any();
    kani::assume(c1 != '.');
    s.push(c1);
    s.push('.');
    let c2: char = kani::any();
    kani::assume(c2 != '.');
    s.push(c2);
    let v: Vec<&str> = s.split('.').collect();
    assert_eq!(v.len(), 2);
}

hence the need for the assumption.

[tautschnig]

The challenge in this example is that std::char::methods::len_utf8 could return any of {1,2,3,4} for a non-constant char. Consequently, CBMC cannot use a fixed size for the (re-)allocation. This, in turn, means that we need to use the array theory to reason about such programs. CBMC's encoding thereof in the propositional back-end needs improvement. In the meantime, I tried to use the SMT back-end on this example. Running Z3 and CVC5 demonstrates a much lower memory footprint (at most 2 GB), but they are still running for a very long time (more than 15 minutes and still going).