Type in symbol table sometimes differs from what `codegen_function_sig` returns

[fzaiser]

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]

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.

[tautschnig]

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]

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

[tautschnig]

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]

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]

This might be related to https://github.com/model-checking/kani/issues/450