Can I use Kani without Cargo

[lsig]

Hi, I'm building a file system in Rust for Rust-for-linux and I want to verify some of its properties with Kani. However the Linux kernel does not support Cargo, is there a way to use kani without Cargo thus allowing me to integrate it as a dev-tool in the kernel.

Thanks in advance.

[zhassan-aws]

Hi @lsig. Yes, Kani can be used without cargo. See https://model-checking.github.io/kani/usage.html#usage-on-a-single-crate for more information.

[zhassan-aws]

Do you know the sequence of rustc commands for compilation and linking that result from executing the make command?

[lsig]

hmm the kernel build system is pretty complex but from what I can gather they compile different crates (core, kernel, macros) into a series of object files (*.o) that are then linked with the main binary (vmlinux) with ld.

[lsig]

do you think its feasable? kernel also generates rust bindings to C functions which have a bridge through FFI, I'm not sure how kani deals with that.

[zhassan-aws]

Conceptually, it should be possible. The way Kani works with cargo packages is that it invokes cargo with the compiler overriden to the Kani one:

kani/kani-driver/src/call_cargo.rs

Line 220 in 21f3a28

.env("RUSTC", &self.kani_compiler)

and with a bunch of flags set:

kani/kani-driver/src/call_single_file.rs

Line 188 in 21f3a28

pub fn kani_rustc_flags(&self, lib_config: LibConfig) -> Vec<RustcArg> {

The way this behaves it that for each crate, the MIR gets dumped (in a .rlib file), and at the linking stage, the Kani compiler processes the MIR for all the crates starting from the top-level crate.

So it seems we should be able to mimic this behavior in the kernel build system by setting RUSTC to kani-compiler when compiling the individual crates, and then invoke kani-compiler for linking.

CCing @celinval who experimented with this in the past.

kernel also generates rust bindings to C functions which have a bridge through FFI

Kani has limited support for FFIs via the unstable -Z c-ffi option.

[lsig]

Thanks for a great response, I'll try tinkering with the makefiles replacing rustc with the kani-compiler. I'm unsure if this is going to work but will let you know.