FFI stubbing for libc crate only works if libc crate is imported via `feature(rustc_private)`

[roypat]

I tried this code:

#[allow(unused)]
mod stubs {
    use libc::{c_int, c_long};

    pub unsafe extern "C" fn sysconf(_input: c_int) -> c_long {
        1
    }
}

#[kani::proof]
#[kani::stub(libc::sysconf, stubs::sysconf)]
fn verify_sysconf_stub() {
    assert_eq!(1, unsafe{ libc::sysconf(libc::_SC_PAGE_SIZE) });
}

using the following command line invocation:

cargo kani --enable-unstable --enable-stubbing

with Kani version: 0.34.0

I expected to see this happen: sysconf to be successfully stubbed and verification to succeed

Instead, this happened: sysconf was not stubbed out, and instead the CMBC model was used. Because of this, verification failed with

``` $ cargo kani --enable-unstable --enable-stubbing Kani Rust Verifier 0.34.0 (cargo plugin) Compiling kani_test v0.1.0 (/home/ANT.AMAZON.COM/roypat/Development/kani_test) Finished dev [unoptimized + debuginfo] target(s) in 0.07s Checking harness verify_sysconf_stub... CBMC 5.89.0 (cbmc-5.89.0) CBMC version 5.89.0 (cbmc-5.89.0) 64-bit x86_64 linux Reading GOTO program from file /home/ANT.AMAZON.COM/roypat/Development/kani_test/target/kani/x86_64-unknown-linux-gnu/debug/deps/kani_test-c8538ab98039f13c__RNvCs1HTYkq7Kxv9_9kani_test19verify_sysconf_stub.out Generating GOTO Program Adding CPROVER library (x86_64) Removal of function pointers and virtual functions Generic Property Instrumentation Running with 16 object bits, 48 offset bits (user-specified) Starting Bounded Model Checking Runtime Symex: 0.00113693s size of program expression: 58 steps slicing removed 29 assignments Generated 8 VCC(s), 2 remaining after simplification Runtime Postprocess Equation: 2.1764e-05s Passing problem to propositional reduction converting SSA Runtime Convert SSA: 0.000108755s Running propositional reduction Post-processing Runtime Post-process: 8.234e-06s Solving with CaDiCaL sc2021 66 variables, 67 clauses SAT checker: instance is SATISFIABLE Runtime Solver: 3.7576e-05s Runtime decision procedure: 0.000179441s RESULTS: Check 1: verify_sysconf_stub.assertion.1 - Status: FAILURE - Description: "assertion failed: 1 == unsafe { libc::sysconf(libc::_SC_PAGE_SIZE) }" - Location: src/main.rs:23:9 in function verify_sysconf_stub Check 2: sysconf.pointer_dereference.1 - Status: SUCCESS - Description: "dereference failure: pointer NULL" - Location: :22 in function sysconf Check 3: sysconf.pointer_dereference.2 - Status: SUCCESS - Description: "dereference failure: pointer invalid" - Location: :22 in function sysconf Check 4: sysconf.pointer_dereference.3 - Status: SUCCESS - Description: "dereference failure: deallocated dynamic object" - Location: :22 in function sysconf Check 5: sysconf.pointer_dereference.4 - Status: SUCCESS - Description: "dereference failure: dead object" - Location: :22 in function sysconf Check 6: sysconf.pointer_dereference.5 - Status: SUCCESS - Description: "dereference failure: pointer outside object bounds" - Location: :22 in function sysconf Check 7: sysconf.pointer_dereference.6 - Status: SUCCESS - Description: "dereference failure: invalid integer address" - Location: :22 in function sysconf SUMMARY: ** 1 of 7 failed Failed Checks: assertion failed: 1 == unsafe { libc::sysconf(libc::_SC_PAGE_SIZE) } File: "/home/ANT.AMAZON.COM/roypat/Development/kani_test/src/main.rs", line 23, in verify_sysconf_stub VERIFICATION:- FAILED Verification Time: 0.016494747s Summary: Verification failed for - verify_sysconf_stub Complete - 0 successfully verified harnesses, 1 failures, 1 total. ```

If I remove libc from my Cargo.toml and instead put

#![feature(rustc_private)]
extern crate libc;

at the top of my file, verification succeeds as expected. This is why the integration test added for the FFI stubbing feature added in #2658 passes.

[roypat]

The workaround provided in https://github.com/model-checking/kani/issues/2686 for a similar issue (importing the stubbing target by alias and stubbing our that alias) also works in this case:

#[allow(unused)]
mod stubs {
    use libc::{c_int, c_long};

    pub unsafe extern "C" fn sysconf(_input: c_int) -> c_long {
        1
    }
}

use libc::sysconf as sysconf_alias;

#[kani::proof]
#[kani::stub(sysconf_alias, stubs::sysconf)]
fn verify_sysconf_stub() {
    assert_eq!(1, unsafe{ libc::sysconf(libc::_SC_PAGE_SIZE) });
}

leads to

RESULTS:
Check 1: verify_sysconf_stub.assertion.1
    - Status: SUCCESS
    - Description: "assertion failed: 1 == unsafe { libc::sysconf(libc::_SC_PAGE_SIZE) }"
    - Location: src/main.rs:38:5 in function verify_sysconf_stub

SUMMARY:
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.02846472s

[roypat]

Mhh, instead trying to stub out libc::clock_gettime (which is something we'd like to do over at firecracker to make some of our ratelimiter proofs nicer), actually leads to a kani crash:

I tried

mod stubs {
    pub unsafe extern "C" fn clock_gettime(_clock_id: libc::clockid_t, tp: *mut libc::timespec) -> libc::c_int {
        unsafe {
            (*tp).tv_sec = kani::any();
            (*tp).tv_nsec = kani::any();
        }

        0
    }
}

#[kani::proof]
#[kani::stub(libc::clock_gettime, stubs::clock_gettime)]
fn verify_clock_gettime_stub() {
    let i = std::time::Instant::now();
}

and running RUST_BACKTRACE=1 cargo kani --enable-unstable --enable-stubbing leads to

2023-08-16T11:04:50.845806Z ERROR cprover_bindings::goto_program::expr: Argument doesn't check param=Pointer { typ: StructTag("tag-libc::timespec") } arg=Pointer { typ: StructTag("tag-libc::unix::timespec") }
error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:661:9:
                                Function call does not type check:
                                func: Expr { value: Symbol { identifier: "_RNvNtCsgn0tUiWO6QV_10playground5stubs13clock_gettime" }, typ: Code { parameters: [Parameter { typ: Signedbv { width: 32 }, identifier: None, base_name: None }, Parameter { typ: Pointer { typ: StructTag("tag-libc::timespec") }, identifier: None, base_name: None }], return_type: Signedbv { width: 32 } }, location: None, size_of_annotation: None }
                                args: [Expr { value: Symbol { identifier: "_ZN3std3sys4unix4time5inner48_$LT$impl$u20$std..sys..unix..time..Timespec$GT$3now17hbf6b40abeb30b878E::1::var_1::clock" }, typ: Signedbv { width: 32 }, location: None, size_of_annotation: None }, Expr { value: Symbol { identifier: "_ZN3std3sys4unix4time5inner48_$LT$impl$u20$std..sys..unix..time..Timespec$GT$3now17hbf6b40abeb30b878E::1::var_6" }, typ: Pointer { typ: StructTag("tag-libc::unix::timespec") }, location: None, size_of_annotation: None }].

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:661:9:
Function call does not type check:
func: Expr { value: Symbol { identifier: "_RNvNtCsgn0tUiWO6QV_10playground5stubs13clock_gettime" }, typ: Code { parameters: [Parameter { typ: Signedbv { width: 32 }, identifier: None, base_name: None }, Parameter { typ: Pointer { typ: StructTag("tag-libc::timespec") }, identifier: None, base_name: None }], return_type: Signedbv { width: 32 } }, location: None, size_of_annotation: None }
args: [Expr { value: Symbol { identifier: "_ZN3std3sys4unix4time5inner48_$LT$impl$u20$std..sys..unix..time..Timespec$GT$3now17hbf6b40abeb30b878E::1::var_1::clock" }, typ: Signedbv { width: 32 }, location: None, size_of_annotation: None }, Expr { value: Symbol { identifier: "_ZN3std3sys4unix4time5inner48_$LT$impl$u20$std..sys..unix..time..Timespec$GT$3now17hbf6b40abeb30b878E::1::var_6" }, typ: Pointer { typ: StructTag("tag-libc::unix::timespec") }, location: None, size_of_annotation: None }]
stack backtrace:
   0: rust_begin_unwind
             at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/std/src/panicking.rs:617:5
   1: core::panicking::panic_fmt
             at /rustc/474709a9a2a74a8bcf0055fadb335d0ca0d2d939/library/core/src/panicking.rs:67:14
   2: cprover_bindings::goto_program::expr::Expr::call
   3: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator
   4: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
   5: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
   6: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
   7: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
   8: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
   9: rustc_interface::passes::start_codegen
  10: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_span::ErrorGuaranteed>>
  11: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::sys::unix::time::inner::<impl std::sys::unix::time::Timespec>::now
_ZN3std3sys4unix4time5inner48_$LT$impl$u20$std..sys..unix..time..Timespec$GT$3now17hbf6b40abeb30b878E
[Kani] current codegen location: Loc { file: "/github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/unix/time.rs", function: None, start_line: 397, start_col: Some(9), end_line: 397, end_col: Some(55) }
error: could not compile `playground` (bin "playground"); 10 warnings emitted
error: Failed to compile `playground` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:661:9:
                                Function call does not type check:
                                func: Expr { value: Symbol { identifier: "_RNvNtCsgn0tUiWO6QV_10playground5stubs13clock_gettime" }, typ: Code { parameters: [Parameter { typ: Signedbv { width: 32 }, identifier: None, base_name: None }, Parameter { typ: Pointer { typ: StructTag("tag-libc::timespec") }, identifier: None, base_name: None }], return_type: Signedbv { width: 32 } }, location: None, size_of_annotation: None }
                                args: [Expr { value: Symbol { identifier: "_ZN3std3sys4unix4time5inner48_$LT$impl$u20$std..sys..unix..time..Timespec$GT$3now17hbf6b40abeb30b878E::1::var_1::clock" }, typ: Signedbv { width: 32 }, location: None, size_of_annotation: None }, Expr { value: Symbol { identifier: "_ZN3std3sys4unix4time5inner48_$LT$impl$u20$std..sys..unix..time..Timespec$GT$3now17hbf6b40abeb30b878E::1::var_6" }, typ: Pointer { typ: StructTag("tag-libc::unix::timespec") }, location: None, size_of_annotation: None }].

I think this also is a result of the standard library using a "special" version of libc. I tried to match my libc crate version to the version the standard library was compiled against (and also tried all libc versions since 0.2.141), to no avail :(.

Using the rustc_private feature avoids this

[roypat]

Right, so I found a workaround... ish

For some reason, rustc's libc is not a drop-in-replacement for crates.io libc, so just doing #![feature(rustc_private)] will not work for arbitrary crates (e.g. firecracker). It also means that a nightly compiler would be required for normal builds, which is not ideal. I managed to get things to work by adding #![cfg_attr(kani, feature(rustc_private))] and in my Cargo.toml libc_public = { package = "libc", version = "..." } (and then put use libc_public as libc at the top of each module that does not contain a kani libc stub). In modules for kani stubs, I instead do extern crate libc as rustc_libc and write the stubs in terms of rustc_libc (and this is what requires the "normal" libc crate to be renamed in Cargo.toml, as otherwise extern crate libc will refer to the version from crates.io instead of the rustc internal one.

[celinval]

I think the problem here might be related to different versions of the same crate. The libc you are pulling from crates.io might not have the same version as the one that rustc_private points to, hence the mismatched type.

Your workaround makes sense to me, so you can clearly pinpoint which one you are trying to stub. That said, I think we are mishandling this case, and we should fix that. Let us know if you are blocked though.