model-checking
FFI stubbing for libc crate only works if libc crate is imported via `feature(rustc_private)`
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: <builtin-library-sysconf>:22 in function sysconf
Check 3: sysconf.pointer_dereference.2
- Status: SUCCESS
- Description: "dereference failure: pointer invalid"
- Location: <builtin-library-sysconf>:22 in function sysconf
Check 4: sysconf.pointer_dereference.3
- Status: SUCCESS
- Description: "dereference failure: deallocated dynamic object"
- Location: <builtin-library-sysconf>:22 in function sysconf
Check 5: sysconf.pointer_dereference.4
- Status: SUCCESS
- Description: "dereference failure: dead object"
- Location: <builtin-library-sysconf>:22 in function sysconf
Check 6: sysconf.pointer_dereference.5
- Status: SUCCESS
- Description: "dereference failure: pointer outside object bounds"
- Location: <builtin-library-sysconf>:22 in function sysconf
Check 7: sysconf.pointer_dereference.6
- Status: SUCCESS
- Description: "dereference failure: invalid integer address"
- Location: <builtin-library-sysconf>: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.
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
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
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.
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.
