-
Notifications
You must be signed in to change notification settings - Fork 100
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
Type in symbol table sometimes differs from what codegen_function_sig
returns
#1350
Comments
This problem seems to be related to many BuiltIn functions. Their C declaration doesn't always match their rust one. For example, |
Rust function signature for `memcmp` differs from CBMC built-in function. Rust follows llvm intrinsic and take `*cost u8` as arguments: ```rust fn memcmp(s1: *const u8, s2: *const u8, n: usize) -> ffi::c_int; ``` While CBMC's follow C's definition which takes a `void` pointer. ```c int memcmp(const void* ptr1, const void* ptr2, size_t num); ``` Fixes model-checking#1350
I believe CBMC would be quite ok with inserting the necessary type casts (to use the C library functions) if you just consistently go with the Rust/LLVM declarations. |
I changed Kani to insert the casts. I have another blocker with the std sockets library. I haven't had time to figure out what's wrong |
I wouldn't be surprised if you get to see transparent unions on that one. |
I think this might be a name resolution issue. When the user crate invokes
|
This might be related to #450 |
The Rust function
core::slice::cmp::memcmp
has the symbol namememcmp
, which is the intrinsic it compiles to. The intrinsic usesvoid*
pointers (which is the type stored in the symbol table), but they are*const u8
on the Rust side. This means that we cannot trust the type in the symbol table, so we have to use the output ofcodegen_function_sig
to generate the correct Rust type, which adds redundancy and confusion.Maybe the correct solution for this would be to treat
core::slice::cmp::memcmp
as an intrinsic. Currently, the instance returned isInstanceDef::Item
, notInstanceDef::Intrinsic
, so Kani generates code as for a normal function, but still has the problem of mismatched types.This was discovered in #1338..
The text was updated successfully, but these errors were encountered: