High memory usage with a simple string vector example

[zhassan-aws]

I tried this code:

const N: usize = 9;

#[cfg_attr(kani, kani::proof, kani::unwind(10))]
fn main() {
    let mut v: Vec<String> = Vec::new();
    for _i in 0..N {
        v.push(String::from("ABC"));
    }
    assert_eq!(v.len(), N);
    let index: usize = kani::any();
    kani::assume(index < v.len());
    let x = &v[index];
    assert_eq!(*x, "ABC");
}

using the following command line invocation:

kani push_string.rs

with Kani version: 0fa9ee3

This finished in ~8.5 minutes and used ~23 GB of memory:

Although at some point, memory usage went up to ~27 GB.

If I bump N to 10 (and unwind to 11), it runs out of memory (>32 GB).

[zhassan-aws]

As with #1657, if I replace this line:

    let mut v: Vec<String> = Vec::new();

with:

    let mut v: Vec<String> = Vec::with_capacity(N);

Verification time goes down to 22 seconds, and memory usage down to 143 MB!

[zhassan-aws]

If I use a poor man's vector implementation such as the one below, I don't observe any blowups in memory:

use std::alloc::{alloc, dealloc, Layout};

const N: usize = 15;

type T = String;

struct MyVec {
    size: usize,
    capacity: usize,
    layout: Layout,
    data: *mut T,
}

impl MyVec {
    fn new(capacity: usize) -> Self {
        let layout = Layout::array::<T>(capacity).unwrap();
        let data = unsafe { alloc(layout) } as *mut T;
        Self { size: 0, capacity, layout, data }
    }

    fn push(&mut self, value: T) {
        unsafe {
            if self.size == self.capacity {
                self.capacity *= 2;
                let layout = Layout::array::<T>(self.capacity).unwrap();
                let data = alloc(layout) as *mut T;
                std::ptr::copy_nonoverlapping(self.data, data, self.size);
                dealloc(self.data as *mut u8, self.layout);
                self.data = data;
                self.layout = layout;
                //self.data = realloc(self.data, self.layout, self.capacity);
            }
            std::ptr::write(self.data.add(self.size), value);
            self.size += 1;
        }
    }

    fn get(&self, index: usize) -> &T {
        unsafe {
            &(*self.data.add(index))
        }
    }

    fn len(&self) -> usize {
        self.size
    }
}

#[cfg_attr(kani, kani::proof, kani::unwind(16))]
fn main() {
    let mut v: MyVec = MyVec::new(1);
    for _i in 0..N {
        v.push(String::from("ABC"));
    }
    assert_eq!(v.len(), N);
    let index: usize = kani::any();
    kani::assume(index < v.len());
    let x = v.get(index);
    assert_eq!(*x, "ABC");
}

With N = 15, verification time is 75 seconds, and memory usage is under 200 MB.

[tautschnig]

Still WIP, but diffblue/cbmc#7230 might help here: the example at the top of this issue takes 18 seconds instead of 428 on my machine.

[tautschnig]

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

[zhassan-aws]

Awesome! Thanks @tautschnig! Did the memory usage go down as well?

[tautschnig]

Memory consumption appears to be below 250 MB :-)

[zhassan-aws]

Nice!