Bogus failures in simple vector example

[zhassan-aws]

I tried this code:

fn main() {
    let mut v = Vec::new();
    v.push(0);
    v.push(0);
    v.push(0);
    v.push(0);
    v.push(0);
    assert!(v[0] == 0);
    assert!(v[1] == 0);
    assert!(v[2] == 0);
    assert!(v[3] == 0);
}

using the following command line invocation:

rmc test.rs

with RMC version: 8de5cd67609

I expected to see this happen: Verification successful

Instead, this happened: All four assertions failed:

[main.assertion.1] line 8 assertion failed: v[0] == 0: FAILURE
[main.assertion.2] line 9 assertion failed: v[1] == 0: FAILURE
[main.assertion.3] line 10 assertion failed: v[2] == 0: FAILURE
[main.assertion.4] line 11 assertion failed: v[3] == 0: FAILURE
** 4 of 545 failed (2 iterations)
VERIFICATION FAILED

If I remove one of the push calls, verification passes:

[main.assertion.1] line 8 assertion failed: v[0] == 0: SUCCESS
[main.assertion.2] line 9 assertion failed: v[1] == 0: SUCCESS
[main.assertion.3] line 10 assertion failed: v[2] == 0: SUCCESS
[main.assertion.4] line 11 assertion failed: v[3] == 0: SUCCESS

** 0 of 545 failed (1 iterations)
VERIFICATION SUCCESSFUL

I suspect this is a bug in reallocation; if I print the vector's capacity after each push, I see that it changes from 0 to 4 after the first push (initial allocation) and changes from 4 to 8 after the last push (reallocation).

[tautschnig]

The following C variant thereof seems to be working fine:

#include <assert.h>
#include <stdlib.h>

int main()
{
  char *p1 = malloc(4 * sizeof(char));
  p1[0] = 42;
  p1[1] = 42;
  p1[2] = 42;
  p1[3] = 42;
  p1 = realloc(p1, 8 * sizeof(char));
  assert(p1[0] == 42);
}

[zhassan-aws]

The following Rust program that uses libc::realloc directly works correctly with RMC:

extern crate libc;
use std::mem;

#[no_mangle]
fn main() {
    unsafe {
        let my_num: *mut i32 = libc::malloc(4 * mem::size_of::<i32>() as libc::size_t) as *mut i32;
        if my_num.is_null() {
            panic!("failed to allocate memory");
        }
        *my_num = 0;
        *my_num.offset(1) = 1;
        *my_num.offset(2) = 2;
        *my_num.offset(3) = 3;
        let my_num2: *mut i32 = libc::realloc(my_num as *mut libc::c_void, 8 * mem::size_of::<i32>() as libc::size_t) as *mut i32;
        if my_num2.is_null() {
            panic!("failed to allocate memory");
        }
        assert!(*my_num2 == 0);
        assert!(*my_num2.offset(1) == 1);
        assert!(*my_num2.offset(2) == 2);
        assert!(*my_num2.offset(3) == 3);
        libc::free(my_num2 as *mut libc::c_void);
    }
}

Output:

** 0 of 175 failed (1 iterations)
VERIFICATION SUCCESSFUL

[zhassan-aws]

And the following one that uses std::alloc::realloc directly also passes with RMC:

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

fn main() {
    unsafe {
        let layout = Layout::new::<[u8; 4]>();
        let ptr = alloc(layout);

        *(ptr as *mut u8) = 8;
        *(ptr as *mut u8).offset(1) = 12;
        *(ptr as *mut u8).offset(2) = 15;
        *(ptr as *mut u8).offset(3) = 29;

        let layout = Layout::new::<[u8; 8]>();
        let ptr = realloc(ptr as *mut u8, layout, 8);
        assert_eq!(*(ptr as *mut u8), 8);
        assert_eq!(*(ptr as *mut u8).offset(1), 12);
        assert_eq!(*(ptr as *mut u8).offset(2), 15);
        assert_eq!(*(ptr as *mut u8).offset(3), 29);

        dealloc(ptr, layout);
    }
}

Output:

** 0 of 191 failed (1 iterations)
VERIFICATION SUCCESSFUL

[danielsn]

Using v.reserve() to explicitly do the realloc also seems to work

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Failing example from https://github.com/model-checking/kani/issues/702
// Push 5 elements to force the vector to resize, then check that the values were correctly copied.
fn main() {
    let mut v = Vec::new();
    assert!(v.capacity() == 0);
    assert!(v.len() == 0);

    v.push(72);
    assert!(v.capacity() == 4);
    assert!(v.len() == 1);
    assert!(v[0] == 72);

    v.reserve(4);
    // assert!(v.capacity() == 8);
    // assert!(v.len() == 1);
    // assert!(v[0] == 72);

    v.push(2);
   // assert!(v.capacity() == 4);
    assert!(v.len() == 2);
    assert!(v[0] == 72);

    v.push(3);
  //  assert!(v.capacity() == 4);
    assert!(v.len() == 3);
    assert!(v[0] == 72);

    v.push(4);
  //  assert!(v.capacity() == 4);
    assert!(v.len() == 4);
    assert!(v[0] == 72);

    v.push(987);
 //   assert!(v.capacity() == 8);
    assert!(v.len() == 5);
    assert!(v[0] == 72);

    // assert!(v[0] == 72);
    // assert!(v[1] == 2);
    // assert!(v[2] == 3);
    // assert!(v[3] == 4);
  //  assert!(v[4] == 5);
}

[danielsn]

But this fails

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

// Failing example from https://github.com/model-checking/kani/issues/702
// Push 5 elements to force the vector to resize, then check that the values were correctly copied.
fn main() {
    let mut v = Vec::new();
    assert!(v.capacity() == 0);
    assert!(v.len() == 0);

    v.push(72);
    assert!(v.capacity() == 4);
    assert!(v.len() == 1);
    assert!(v[0] == 72);

    // assert!(v.capacity() == 8);
    // assert!(v.len() == 1);
    // assert!(v[0] == 72);

    v.push(2);
   // assert!(v.capacity() == 4);
    assert!(v.len() == 2);
    assert!(v[0] == 72);

    v.reserve(4);
    v.push(3);
  //  assert!(v.capacity() == 4);
    assert!(v.len() == 3);
    assert!(v[0] == 72);

    v.push(4);
  //  assert!(v.capacity() == 4);
    assert!(v.len() == 4);
    assert!(v[0] == 72);

    v.push(987);
 //   assert!(v.capacity() == 8);
    assert!(v.len() == 5);
    assert!(v[0] == 72);

    // assert!(v[0] == 72);
    // assert!(v[1] == 2);
    // assert!(v[2] == 3);
    // assert!(v[3] == 4);
  //  assert!(v[4] == 5);
}

[danielsn]

Even smaller reproduce

fn main() {
    let mut v = Vec::new();
    v.push(72);
    v.push(2);
    v.reserve(4);
    assert!(v[0] == 72);
}

[zhassan-aws]

I was able to reproduce a similar bug with VecDeque:

use std::collections::VecDeque;

#[kani::proof]
fn main() {
    let mut v: VecDeque<i32> = VecDeque::new();
    v.push_back(5);
    v.reserve(8);
    v.reserve(10);
    v.reserve(16);
    assert!(v[0] == 5);
}

running with kani test.rs produces:

<snip>
SUMMARY: 
 ** 1 of 511 failed
Failed Checks: assertion failed: v[0] == 5
 File: "/home/ubuntu/examples/debug/iss702/no_unwrap/vecdeque/test.rs", line 10, in main

If I remove any of the 3 reserve statements, the assertion passes.

[zhassan-aws]

@tautschnig: @danielsn and I wrote a C implementation of the low-level __rust_realloc that is very similar to the CBMC one:

uint8_t* __rust_realloc(uint8_t* ptr, size_t old_size, size_t align, size_t new_size) {
    // if current ptr is NULL, this behaves like malloc
    if (ptr == 0)
        return malloc(new_size);

    // if malloc-size is 0, free original object and return malloc(0) which
    // returns an invalid pointer
    if (new_size == 0) {
        free(ptr);
        return malloc(0);
    }

    uint8_t* result = malloc(new_size);
    if (result) {
        size_t bytes_to_copy = new_size < old_size ? new_size : old_size;
        memcpy(result, ptr, bytes_to_copy);
        free(ptr);
    }

    return result;
}

The two differences w.r.t the CBMC version are:

1. It has access to the new and old sizes, so it passes the right size to copy to memcpy
2. When new_size == 0, it returns malloc(0) and not malloc(1). Interestingly, if I change it to return malloc(1), verification fails on the examples above, so I'm suspecting that the malloc(1) is somehow causing an issue. We might want to try changing the corresponding line in the CBMC implementation of realloc to malloc(0) instead (which if I understand correctly, returns an invalid pointer), and check if it fixes the bug.