function call: parameter "pthread_key_create::destructor" type mismatch when hitting thread::current()
#1781
Comments
|
I don't know where any kind of |
|
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. |
|
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 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) };
} |
|
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: |
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
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
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
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
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
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
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
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! |
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).
When a kani is run with
--mir-linker --enable-unstableand encountersthread::current()(or rather, the destructor of a thread object?) it yields the error message from the title.I tried this code:
using the following command line invocation:
with Kani version: cargo-kani 0.12.0
I expected to see this happen: As
std::threadinterfaces 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:
The text was updated successfully, but these errors were encountered: