Memory reallocation with Vec kills performance #1657
Description
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.