Memory reallocation with Vec kills performance

[zhassan-aws]

This example is from #1651, implemented using a vector:

const N: usize = 4;
const M: usize = N+1;

trait T {
    fn foo(&self) -> i32;
}

struct A {
    x: i32,
}

impl T for A {
    fn foo(&self) -> i32 {
        self.x
    }
}

struct B {
    x: i32,
}

impl T for B {
    fn foo(&self) -> i32 {
        self.x
    }
}

#[kani::proof]
#[kani::unwind(6)]
fn main() {
    //let mut a: Vec<Box<dyn T>> = Vec::with_capacity(N);
    let mut a: Vec<Box<dyn T>> = Vec::new();
    a.push(Box::new(A { x: 5 }));
    for i in 1..N {
        a.push(Box::new(B { x: 9 }));
    }
    let mut val: i32 = 0;
    for _i in 0..M {
        let index: usize = kani::any();
        kani::assume(index < a.len());
        let x = a[index].as_mut().foo();
        val += x;
    }
}

with Kani version: d53296a

When the vector is created with Vec::with_capacity to pre-allocate memory, verification time is 3.2 seconds, and consumes less than 1 GB of memory. But when using Vec::new(), verification takes 160 seconds, and consumes more than 14 GB of memory.

If I bump N to 5 (and the unwind value to 7), the Vec::with_capacity version finishes in 7 seconds, and consumes less than 1 GB, and the Vec::new version runs out of memory (>32 GB) after running for about 3 minutes.

[tautschnig]

With diffblue/cbmc#7230 on top of diffblue/cbmc@70b7cf7baf735f I get "Verification Time: 1.3950623s" when it takes 238.199s using diffblue/cbmc@70b7cf7baf735f and Kani revision 057926b.