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

Type in symbol table sometimes differs from what codegen_function_sig returns #1350

Closed
fzaiser opened this issue Jul 7, 2022 · 6 comments · Fixed by #2994
Closed

Type in symbol table sometimes differs from what codegen_function_sig returns #1350

fzaiser opened this issue Jul 7, 2022 · 6 comments · Fixed by #2994
Assignees
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@fzaiser
Copy link
Contributor

fzaiser commented Jul 7, 2022

The Rust function core::slice::cmp::memcmp has the symbol name memcmp, which is the intrinsic it compiles to. The intrinsic uses void* 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 of codegen_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 is InstanceDef::Item, not InstanceDef::Intrinsic, so Kani generates code as for a normal function, but still has the problem of mismatched types.

This was discovered in #1338..

@celinval
Copy link
Contributor

This problem seems to be related to many BuiltIn functions. Their C declaration doesn't always match their rust one. For example, memcmp in Rust takes *const u8 while in C they take void*. Another example is how Rust represents void*, they actually use an opaque type *const c_void. See https://rust-lang.github.io/rfcs/1861-extern-types.html and https://doc.rust-lang.org/nomicon/ffi.html#representing-opaque-structs.

celinval added a commit to celinval/kani-dev that referenced this issue Jul 22, 2022
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
@tautschnig
Copy link
Member

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.

@celinval
Copy link
Contributor

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

@celinval celinval moved this to In Progress in Kani v0.7 Jul 22, 2022
@tautschnig
Copy link
Member

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.

@celinval
Copy link
Contributor

celinval commented Jul 26, 2022

I think this might be a name resolution issue. When the user crate invokes libc::bind we see the function signature and types as belonging to libc, however, when we are the signature for the std library call to libc::bind, we are seeing them as if they were inside libc::unix::linux_like::*. For the function signature, the mangled name resolve to bind (problably because this is inside an extern "C"). However, we are generating different types for the parameters. Here is the error I get:

ERROR cprover_bindings::goto_program::expr Argument doesn't check, param=Pointer { typ: StructTag("tag-libc::sockaddr") }, arg=Pointer { typ: StructTag("tag-libc::unix::
linux_like::sockaddr") }

@celinval
Copy link
Contributor

This might be related to #450

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.
Projects
No open projects
Status: Done
Development

Successfully merging a pull request may close this issue.

4 participants