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