function call: parameter "pthread_key_create::destructor" type mismatch when hitting `thread::current()`

[roypat]

When a kani is run with --mir-linker --enable-unstable and encounters thread::current() (or rather, the destructor of a thread object?) it yields the error message from the title.

I tried this code:

fn main() {}

#[kani::proof]
fn crash() {
    std::thread::current();
}

using the following command line invocation:

cargo clean; cargo kani --mir-linker --enable-unstable

with Kani version: cargo-kani 0.12.0

I expected to see this happen: As std::thread interfaces with the OS API (pthread on linux) I'd have expected kani to complain about it reaching some function for which it does not have access to the source code. If I run kani without --mir-linker, this is indeed what happens.

Instead, this happened:

Checking harness crash...
CBMC 5.67.0 (cbmc-5.67.0)
CBMC version 5.67.0 (cbmc-5.67.0) 64-bit x86_64 linux
Reading GOTO program from file /home/ec2-user/kani-reproducer/target/x86_64-unknown-linux-gnu/debug/deps/cbmc-linked.for-crash.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
: function call: parameter "pthread_key_create::destructor" type mismatch:
got struct_tag
  * identifier: tag-_3583338355805481440
expected pointer
  * #source_location: 
    * file: <builtin-library-pthread_key_create>
    * line: 11
    * function: pthread_key_create
    * working_directory: /home/ec2-user/kani-reproducer/src
  * width: 64
  * #failed_symbol: pthread_key_create::destructor$object
  0: code
      * #source_location: 
        * file: <builtin-library-pthread_key_create>
        * line: 11
        * function: pthread_key_create
        * working_directory: /home/ec2-user/kani-reproducer/src
      * return_type: empty
          * #source_location: 
            * file: <builtin-library-pthread_key_create>
            * line: 11
            * function: pthread_key_create
            * working_directory: /home/ec2-user/kani-reproducer/src
      * parameters: 
        0: parameter
            * type: pointer
                * #source_location: 
                  * file: <builtin-library-pthread_key_create>
                  * line: 11
                  * function: pthread_key_create
                  * working_directory: /home/ec2-user/kani-reproducer/src
                * width: 64
                0: empty
                    * #source_location: 
                      * file: <builtin-library-pthread_key_create>
                      * line: 11
                      * function: pthread_key_create
                      * working_directory: /home/ec2-user/kani-reproducer/src
            * #source_location: 
              * file: <builtin-library-pthread_key_create>
              * line: 11
              * function: pthread_key_create
              * working_directory: /home/ec2-user/kani-reproducer/src
Verification Time: 0.81680673s

[tautschnig]

I don't know where any kind of struct would come from, the destructor parameter ought to be a (function) pointer.

[adpaco-aws]

Thanks for the bug report, @roypat !

A first look makes me think this is a bug in the generation of the destructor (as @tautschnig already pointed out). Also, please note that Kani assumes concurrent code to be sequential since concurrent features are currently out of scope.

[celinval]

It looks like we need special handling for transparent structs at FFI boundaries. See https://rust-lang.github.io/rfcs/1758-repr-transparent.html for more details.

In the specific case, the rust standard library uses an Option<unsafe extern "C" fn(*mut u8)> to represent the destructor:

https://github.com/rust-lang/rust/blob/fa0ca783f89a83046e6ce0383385ba5b28296435/library/std/src/sys/unix/thread_local_key.rs#L8-L12

https://github.com/rust-lang/libc/blob/fff5dbe033906f147169c6e458e00b33e347ba41/src/unix/mod.rs#L1089-L1092

This is a minimal test that reproduces the exact same issue:

use libc; // Require libc="0.2" to Cargo.toml

#[kani::proof]
fn check_create() {
    let mut key = 0;
    let _res = unsafe { libc::pthread_key_create(&mut key, None) };
}

[adpaco-aws]

Noted that in Kani 0.21.0, the error also appears for this harness:

#[kani::proof]
fn random_cannot_be_zero() {
    assert_ne!(rand::random::<u32>(), 0);
}

Also, in macOS platforms, the error we get is different:

SUMMARY:
 ** 1 of 6007 failed (6006 undetermined)
Failed Checks: Function `_tlv_atexit` with missing definition is unreachable