Add proper support to C-FFI calls

[celinval]

Requested feature: Add support to verifying combination of Rust and C code. Use case: Users have C legacy code or external libraries that they would like to verify against their implementation.

It would be nice to provide out-of-box integration with C code when its source is available. Kani could compile the C code using goto-cc and link its generated goto-programs with Kani generated goto-program.

We should probably create an RFC with a proper design as well as what will be expected user experience. What kind of features will be supported? What kind of UBs will be detected? How to properly link C + Rust?

[YoshikiTakashima]

call to foreign "C" function _NSGetArgc is not currently supported by Kani.

Hit during exploration for using https://github.com/secure-foundations/rWasm. Blocking potential customer.

[adpaco-aws]

I'm getting the following failures (regressions when upgrading from 0.27.0 to 0.28.0) for 6 harnesses in a private project:

Failed Checks: call to foreign "C" function `posix_memalign` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423
 File: "/Users/accorell/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.146/src/unix/mod.rs", line 917, in std::sys::unix::alloc::aligned_malloc

[roypat]

One C-FFI issue we run into in firecracker is with libc::clock_gettime - we work around it by stubbing at a higher level, but it requires some ugly workarounds including std::mem::transmute: https://github.com/firecracker-microvm/firecracker/blob/dbd9a84b11a63b5e5bf201e244fe83f0bc76792a/src/rate_limiter/src/lib.rs#L607-L639. If we could stub libc::clock_gettime directly to (essentially) return kani::any() it'd clean up our code quite a bit :)

Note that here simply supporting clock_gettime as a kani-provided CMBC model wouldn't work for us, as our stub has some performance tweaks (the code-under-proof only cares about the delta between two consecutive Instant::now()s, so we have it always return 0 on the first call).

[celinval]

One C-FFI issue we run into in firecracker is with libc::clock_gettime - we work around it by stubbing at a higher level, but it requires some ugly workarounds including std::mem::transmute: https://github.com/firecracker-microvm/firecracker/blob/dbd9a84b11a63b5e5bf201e244fe83f0bc76792a/src/rate_limiter/src/lib.rs#L607-L639. If we could stub libc::clock_gettime directly to (essentially) return kani::any() it'd clean up our code quite a bit :)

Note that here simply supporting clock_gettime as a kani-provided CMBC model wouldn't work for us, as our stub has some performance tweaks (the code-under-proof only cares about the delta between two consecutive Instant::now()s, so we have it always return 0 on the first call).

One C-FFI issue we run into in firecracker is with libc::clock_gettime - we work around it by stubbing at a higher level, but it requires some ugly workarounds including std::mem::transmute: https://github.com/firecracker-microvm/firecracker/blob/dbd9a84b11a63b5e5bf201e244fe83f0bc76792a/src/rate_limiter/src/lib.rs#L607-L639. If we could stub libc::clock_gettime directly to (essentially) return kani::any() it'd clean up our code quite a bit :)

Note that here simply supporting clock_gettime as a kani-provided CMBC model wouldn't work for us, as our stub has some performance tweaks (the code-under-proof only cares about the delta between two consecutive Instant::now()s, so we have it always return 0 on the first call).

That totally makes sense. We have been thinking about extending the stubbing feature to support stubs of extern functions, like C functions. I created #2587 to capture that.

Thanks!

[adpaco-aws]

Just added the label T-User to this issue. A few users need this so we should bump the priority on it.

Happy to collaborate with anyone on a draft of the proposal.

[D-Gr3at]

I'm getting this error while running kani on a single harness in my project:

Failed Checks: call to foreign "C" function _NSGetArgc is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423 File: "/Users/ec2-user/.rustup/toolchains/nightly-2023-04-30-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/unix/args.rs", line 183, in std::sys::unix::args::imp::args

[swaroopmaddu]

I'm also getting the same error while trying to run a harness

Failed Checks: call to foreign "C" function dlsym is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423 File: "/Users/ec2-user/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.142/src/unix/mod.rs", line 1194, in std::sys::unix::weak::fetch

[ithinkicancode]

I got this error:

Errors
File [/Users/ec2-user/.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/unix/thread_local_dtor.rs]
Function [std::sys::unix::thread_local_dtor::register_dtor]
Line [69]
[[trace] call to foreign "C" function `_tlv_atexit` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423

But I don't understand why it says "/Users/ec2-user/". I don't have this user on my machine! :)

[celinval]

Hi @swaroopmaddu, hi @ithinkicancode, for missing C functions, I would recommend you to take a look at function stubbing. We have recently added support to stubbing external functions, like C functions.

@ithinkicancode I'll create a separate issue for the incorrect path that you are seeing. Thanks for bringing it up.

[tv42]

I stumbled on a getrandom syscall:

SUMMARY:
 ** 8 of 28349 failed (28341 undetermined)
Failed Checks: call to foreign "C" function `syscall` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423
 File: "/github/home/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.150/src/unix/linux_like/linux/mod.rs", line 4568, in std::sys::pal::unix::rand::imp::getrandom::getrandom
Failed Checks: Function `std::sys::pal::unix::rand::imp::getrandom::getrandom` with missing definition is unreachable

I think the repeated getrandom::getrandom refers to the inner function at https://github.com/rust-lang/rust/blob/cdaa12e3dff109f72a5a8a0a67ea225052122a79/library/std/src/sys/pal/unix/rand.rs#L34-L48

I can't stub that directly:

error: failed to resolve `std::sys::pal::unix::rand::imp::getrandom::getrandom`: unable to find `sys` inside crate `foo`
   --> crates/foo/src/bar.rs:555:5
    |
555 |     #[kani::stub(std::sys::pal::unix::rand::imp::getrandom::getrandom, stub_getrandom)]
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: this error originates in the attribute macro `kani::stub` (in Nightly builds, run with -Z macro-backtrace for more info)

It seems to be looking for sys inside my crate, not inside std. That's weird.

I see no convenient way to figure out who the caller is, to find a higher-level function to stub. (I'm surprised the library functions I'm calling need random numbers! No idea where to start. Grep on the libraries implies it's an indirect call.)

Note also that the /github/home path definitely doesn't exist. Not sure if that's related to what others are reporting above.

Related FAILURE messages from earlier in the log:

Check 1508: std::sys::pal::unix::rand::imp::getrandom::getrandom.missing_definition.1
         - Status: FAILURE
         - Description: "Function `std::sys::pal::unix::rand::imp::getrandom::getrandom` with missing definition is unreacha
ble"
         - Location: Unknown file in function std::sys::pal::unix::rand::imp::getrandom::getrandom

Check 2205: std::sys::pal::unix::rand::imp::getrandom::getrandom.unsupported_construct.1
         - Status: FAILURE
         - Description: "call to foreign "C" function `syscall` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423"
         - Location: ../github/home/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.150/src/unix/linux_like/linux/mod.rs:4568:5 in function std::sys::pal::unix::rand::imp::getrandom::getrandom

[celinval]

Hi @tv42, the error does seem incorrect, probably an issue with our resolution algorithm. The github/home path issue is tracked by https://github.com/model-checking/kani/issues/2681.

BTW, are you using any HashMap / HashSet? Are you able to post your harness?

This is an example where we stub RandomState::new() which invokes get random. Note that this stub replaces get_random by a fixed value since we don't care about the result. If do care, you should consider stubbing it with kani::any().

[tv42]

I discovered the library to be using HashMap, yes. This is enough to trigger the message about getrandom:

#[cfg(kani)]
mod verification {
    use std::collections::HashMap;

    #[kani::proof]
    #[kani::unwind(1)]
    fn hashmap() {
        let m: HashMap<String, String> = HashMap::new();
    }
}

It seems that part is #723.