Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
roypat opened this issue Oct 13, 2022 · 6 comments · Fixed by #2428
Assignees
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-User Tag user issues / requests

Comments

@roypat
Copy link

roypat commented Oct 13, 2022

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
@roypat roypat added the [C] Bug This is a bug. Something isn't working. label Oct 13, 2022
@tautschnig
Copy link
Member

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

@adpaco-aws
Copy link
Contributor

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 celinval self-assigned this Oct 26, 2022
@adpaco-aws adpaco-aws added the T-User Tag user issues / requests label Nov 9, 2022
@tedinski tedinski added the [F] Crash Kani crashed label Nov 28, 2022
@celinval
Copy link
Contributor

celinval commented Nov 29, 2022

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
Copy link
Contributor

adpaco-aws commented Feb 17, 2023

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

@celinval celinval self-assigned this Mar 6, 2023
tautschnig added a commit to tautschnig/kani that referenced this issue Apr 20, 2023
CBMC's heap allocator will produce objects that aren't just a byte array
when a prior call to `size_of` was involved in computing the number of
bytes to be allocated via malloc/calloc/realloc. This, in turn, permits
type-safe member accesses to heap-allocated objects. This should speed
up copying as well as all other operations on the resulting object
(which will then not have to go through byte extract/byte update
operations).

It also seems that there no longer is a "size_of" intrinsic.

Fixes: model-checking#1286
Fixes: model-checking#1781
tautschnig added a commit to tautschnig/kani that referenced this issue Apr 21, 2023
CBMC's heap allocator will produce objects that aren't just a byte array
when a prior call to `size_of` was involved in computing the number of
bytes to be allocated via malloc/calloc/realloc. This, in turn, permits
type-safe member accesses to heap-allocated objects. This should speed
up copying as well as all other operations on the resulting object
(which will then not have to go through byte extract/byte update
operations).

It also seems that there no longer is a "size_of" intrinsic.

Fixes: model-checking#1286
Fixes: model-checking#1781
tautschnig added a commit to tautschnig/kani that referenced this issue Apr 21, 2023
CBMC's heap allocator will produce objects that aren't just a byte array
when a prior call to `size_of` was involved in computing the number of
bytes to be allocated via malloc/calloc/realloc. This, in turn, permits
type-safe member accesses to heap-allocated objects. This should speed
up copying as well as all other operations on the resulting object
(which will then not have to go through byte extract/byte update
operations).

It also seems that there no longer is a "size_of" intrinsic.

Fixes: model-checking#1286
Fixes: model-checking#1781
tautschnig added a commit to tautschnig/kani that referenced this issue Apr 21, 2023
CBMC's heap allocator will produce objects that aren't just a byte array
when a prior call to `size_of` was involved in computing the number of
bytes to be allocated via malloc/calloc/realloc. This, in turn, permits
type-safe member accesses to heap-allocated objects. This should speed
up copying as well as all other operations on the resulting object
(which will then not have to go through byte extract/byte update
operations).

It also seems that there no longer is a "size_of" intrinsic.

Fixes: model-checking#1286
Fixes: model-checking#1781
tautschnig added a commit to tautschnig/kani that referenced this issue Apr 24, 2023
CBMC's heap allocator will produce objects that aren't just a byte array
when a prior call to `size_of` was involved in computing the number of
bytes to be allocated via malloc/calloc/realloc. This, in turn, permits
type-safe member accesses to heap-allocated objects. This should speed
up copying as well as all other operations on the resulting object
(which will then not have to go through byte extract/byte update
operations).

It also seems that there no longer is a "size_of" intrinsic.

Fixes: model-checking#1286
Fixes: model-checking#1781
tautschnig added a commit to tautschnig/kani that referenced this issue Apr 24, 2023
CBMC's heap allocator will produce objects that aren't just a byte array
when a prior call to `size_of` was involved in computing the number of
bytes to be allocated via malloc/calloc/realloc. This, in turn, permits
type-safe member accesses to heap-allocated objects. This should speed
up copying as well as all other operations on the resulting object
(which will then not have to go through byte extract/byte update
operations).

It also seems that there no longer is a "size_of" intrinsic.

Fixes: model-checking#1286
Fixes: model-checking#1781
tautschnig added a commit to tautschnig/kani that referenced this issue Apr 24, 2023
CBMC's heap allocator will produce objects that aren't just a byte array
when a prior call to `size_of` was involved in computing the number of
bytes to be allocated via malloc/calloc/realloc. This, in turn, permits
type-safe member accesses to heap-allocated objects. This should speed
up copying as well as all other operations on the resulting object
(which will then not have to go through byte extract/byte update
operations).

It also seems that there no longer is a "size_of" intrinsic.

Fixes: model-checking#1286
Fixes: model-checking#1781
@celinval celinval moved this to In Progress in Kani 2023-05-08 May 3, 2023
@celinval
Copy link
Contributor

celinval commented May 3, 2023

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

Hi @adpaco-aws, I think that is a different issue. The issue you are describing is that an extern function that hasn't been defined is being invoked. For that to work, we would either need to provide a stub for this function or compile the C code where this function is defined (like here).

I created #2423 to capture the work to provide proper support to C-FFI. We need to define what is in scope and what is expected from Kani. This case you posted might deserve a new issue on its own. If you do create one, can you please add it to the C-FFI milestone? Thanks!

celinval added a commit to celinval/kani-dev that referenced this issue May 3, 2023
This will also give visibility to the compiler to whether this feature
is enabled or not which is needed to avoid type mismatch issue
(model-checking#1781).
celinval added a commit that referenced this issue May 3, 2023
… support (#2425)

This will also give visibility to the compiler to whether this feature is enabled or not which is needed to avoid type mismatch issue (#1781).

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
@adpaco-aws
Copy link
Contributor

Hi @celinval , thanks for the detailed explanation! I've created a separate issue for it (#2430) and added to the milestone. Thanks!

@github-project-automation github-project-automation bot moved this to Done in Kani 0.14 May 5, 2023
@github-project-automation github-project-automation bot moved this to Done in Kani 0.17 May 5, 2023
@celinval celinval moved this from In Progress to Done in Kani 2023-05-08 May 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-User Tag user issues / requests
Projects
No open projects
Status: Done
Status: Done
Status: No status
Status: Done
Development

Successfully merging a pull request may close this issue.

6 participants