Poor performance scaling with ArrayVec #1651
Description
These two programs are pretty similar except that one of them is based on arrays, and the other is based on ArrayVec. The latter is a fixed-size array with a vector-like API, i.e. it does not do any memory reallocations.
Array:
const N: usize = 3;
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(5)]
fn main() {
let mut a: [Option<Box<dyn T>>; N] = core::array::from_fn(|_| None);
a[0] = Some(Box::new(A { x: 5 }));
for i in 1..N {
a[i] = Some(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().unwrap().foo();
val += x;
}
}ArrayVec:
use arrayvec::ArrayVec;
const N: usize = 3;
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(5)]
fn main() {
let mut a: ArrayVec<Box<dyn T>, N> = ArrayVec::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;
}
}(The minimum unwind value for both versions is N+2).
with Kani version: d53296a
Kani scales well with the array version, but doesn't scale with the ArrayVec one:
| N | Array Verification Time (s) | ArrayVec Verification Time (s) |
|---|---|---|
| 1 | 1.1 | 2.0 |
| 2 | 2.6 | 26.3 |
| 3 | 4.8 | 223.9 |
| 4 | 8.9 | 1339.5 |
| 5 | 14.3 | 6014.5 |
| 6 | 21.9 | 22061.3 |
| 7 | 33.8 | ? |