`HashMap::new` fails to verify: `syscall` undefined

[zhassan-aws]

I tried this code:

use std::collections::HashMap;

fn main() {
    let h = HashMap::<u32, u32>::new();
}

using the following command line invocation:

rmc test.rs

with RMC version: ab096b6ce6a

I expected to see this happen: Verification successful

Instead, this happened: Verification failed:

function _ZN9hashbrown3raw4sse25Group12static_empty17h72b46d820a0d0565E
[_ZN9hashbrown3raw4sse25Group12static_empty17h72b46d820a0d0565E.assertion.1] assertion false: FAILURE

/home/ubuntu/git/rmc/library/core/src/cell.rs function std::cell::Cell::<T>::get
[std::cell::Cell::<T>::get.pointer_dereference.1] line 442 dereference failure: pointer NULL in *var_2: FAILURE
[std::cell::Cell::<T>::get.pointer_dereference.2] line 442 dereference failure: pointer invalid in *var_2: FAILURE
[std::cell::Cell::<T>::get.pointer_dereference.3] line 442 dereference failure: deallocated dynamic object in *var_2: FAILURE
[std::cell::Cell::<T>::get.pointer_dereference.4] line 442 dereference failure: dead object in *var_2: FAILURE
[std::cell::Cell::<T>::get.pointer_dereference.5] line 442 dereference failure: pointer outside object bounds in *var_2: FAILURE
[std::cell::Cell::<T>::get.pointer_dereference.6] line 442 dereference failure: invalid integer address in *var_2: FAILURE

/home/ubuntu/git/rmc/library/core/src/cell.rs function std::cell::Cell::<T>::replace
[std::cell::Cell::<T>::replace.assertion.1] line 400 resume instruction: SUCCESS
[std::cell::Cell::<T>::replace.pointer_dereference.1] line 403 dereference failure: pointer NULL in *var_3: FAILURE
[std::cell::Cell::<T>::replace.pointer_dereference.2] line 403 dereference failure: pointer invalid in *var_3: FAILURE
[std::cell::Cell::<T>::replace.pointer_dereference.3] line 403 dereference failure: deallocated dynamic object in *var_3: FAILURE
[std::cell::Cell::<T>::replace.pointer_dereference.4] line 403 dereference failure: dead object in *var_3: FAILURE
[std::cell::Cell::<T>::replace.pointer_dereference.5] line 403 dereference failure: pointer outside object bounds in *var_3: FAILURE
[std::cell::Cell::<T>::replace.pointer_dereference.6] line 403 dereference failure: invalid integer address in *var_3: FAILURE

/home/ubuntu/git/rmc/library/core/src/result.rs function std::result::Result::<T, E>::expect
[std::result::Result::<T, E>::expect.assertion.3] line 1299 resume instruction: SUCCESS
[std::result::Result::<T, E>::expect.assertion.2] line 1300 unreachable code: SUCCESS
[std::result::Result::<T, E>::expect.overflow.1] line 1300 arithmetic overflow on unsigned to signed type conversion in (long int)self.case: SUCCESS
[std::result::Result::<T, E>::expect.assertion.1] line 1302 a panicking function std::result::unwrap_failed is invoked: FAILURE

/home/ubuntu/git/rmc/library/std/src/thread/local.rs function std::collections::hash_map::RandomState::new::KEYS::__getit
[std::collections::hash_map::RandomState::new::KEYS::__getit.assertion.1] line 300 The function std::collections::hash_map::RandomState::new::KEYS::__getit is not currently supported by RMC: FAILURE

** 15 of 316 failed (8 iterations)
VERIFICATION FAILED

[zhassan-aws]

One workaround is to implement a custom hasher, e.g.

use std::collections::HashMap;
use std::hash::{BuildHasher, Hasher};

struct MyHasher {}

impl Hasher for MyHasher {
    fn finish(&self) -> u64 {
        0
    }
    fn write(&mut self, _bytes: &[u8]) {}
}

impl BuildHasher for MyHasher {
    type Hasher = MyHasher;

    fn build_hasher(&self) -> Self::Hasher {
        MyHasher {}
    }
}

fn main() {
    let h = MyHasher {};
    let _map: HashMap<i32, i32, _> = HashMap::with_hasher(h);

With that, verification succeeds:

<snip>

SUMMARY: 
 ** 0 of 256 failed

VERIFICATION:- SUCCESSFUL

[zhassan-aws]

With 4488af5249a fails as follows:

SUMMARY: 
 ** 1 of 364 failed (363 undetermined)
Failed Checks: Rvalue::ThreadLocalRef is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/541

VERIFICATION:- FAILED`

[tedinski]

The code in the OP does now compile, is there any other concern here?

[zhassan-aws]

It does compile, but verification still fails:

$ cat new.rs 
use std::collections::HashMap;

#[kani::proof]
fn main() {
    let h = HashMap::<u32, u32>::new();
}

$ kani new.rs
<snip>
SUMMARY:
 ** 2 of 343 failed (341 undetermined)
Failed Checks: unreachable code
 File: "/home/ubuntu/.rustup/toolchains/nightly-2022-08-16-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs", line 627, in std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get
Failed Checks: Function `std::sys::unix::rand::hashmap_random_keys` with missing definition is unreachable

[zhassan-aws]

With the MIR linker, verification fails due to a missing syscall function:

$ kani test.rs --enable-unstable --mir-linker
<snip>

SUMMARY:
 ** 1 of 5582 failed (5581 undetermined)
Failed Checks: Function `syscall` with missing definition is unreachable

VERIFICATION:- FAILED
Verification Time: 3.3889174s

[tedinski]

Hmm. I wonder if we should be mocking a select subset of syscalls. It'd be interesting to see what MIRI does here.

[adpaco-aws]

I think it's even worse now.

    use std::collections::HashMap;
    #[kani::proof]
    fn harness() {
        let mut map = HashMap::<u32,String>::new();
    }

Produces this output:

SUMMARY:
 ** 8 of 4964 failed (4956 undetermined)
Failed Checks: Function `std::sys::unix::rand::imp::getrandom::getrandom` with missing definition is unreachable
Failed Checks: Function `syscall` with missing definition is unreachable
Failed Checks: dereference failure: pointer NULL
Failed Checks: dereference failure: pointer invalid
Failed Checks: dereference failure: deallocated dynamic object
Failed Checks: dereference failure: dead object
Failed Checks: dereference failure: pointer outside object bounds
Failed Checks: dereference failure: invalid integer address

The memory-safety errors could be dangling pointers.

[adpaco-aws]

This issue persists in Kani 0.38.0, though the output hasn't changed much:

SUMMARY:
 ** 8 of 5093 failed (5085 undetermined)
Failed Checks: Function `std::sys::unix::rand::imp::getrandom::getrandom` with missing definition is unreachable
Failed Checks: call to foreign "C" function `syscall` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423
 File: "/home/ubuntu/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.148/src/unix/linux_like/linux/mod.rs", line 4466, in std::sys::unix::rand::imp::getrandom::getrandom
Failed Checks: dereference failure: pointer NULL
Failed Checks: dereference failure: pointer invalid
Failed Checks: dereference failure: deallocated dynamic object
Failed Checks: dereference failure: dead object
Failed Checks: dereference failure: pointer outside object bounds
Failed Checks: dereference failure: invalid integer address

VERIFICATION:- FAILED
** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.
Verification Time: 12.140605s

The main difference is the additional ~100 checks.