Rust SmallVec Insert Optimization
Optimization using lots of unsafe code.

In Rust’s smallvec crate, there was an optimization done to the insert method using a lot of unsafe code in this commit. The optimization was done to eliminate calls to copy when insertion was at the end of the vector. I created a verification job to verify that this did not introduce any issues.

Verification Code

pub extern "C" fn entrypt() {
    let mut v: SmallVec<[u32; 8]> = SmallVec::new();

    let len: usize = sea::nd_usize();
    sea::assume(len < 8);

    for _i in 0..len {

    let insert_point: usize = sea::nd_usize();
    sea::assume(insert_point <= len);

    v.insert(insert_point, sea::nd_u32());

    if insert_point == len {
        sea::sassert!(v.copied() == false);
    } else {
        sea::sassert!(v.copied() == true);

    sea::sassert!(v.len() == len + 1);

I slightly modified the SmallVec source code to include a copied flag that tracks whether the vector has been copied or not. This flag is set to true when the vector is copied and false when it is not. This test case pushes non-deterministic values to a vector and then inserts a value at a random index. If the index is at the end of the vector, then the vector should not be copied, but if it is not, then the vector should be copied. This test case worked pretty much right away without any significant issues.

Written by SeaHorn on 31 August 2023