Advise on using Kani for non-cargo projects

[rodionov]

Hello,

Is there any guidance on how to perform verification of a Rust project with Kani which is built without using Cargo? In other words, there is no Cargo.toml file, both rustc & linker are directly invoked via Makefile where dependencies are provided via --extern argument to rustc.

Thank you!

[celinval]

Hi @rodionov, you should be able to use standalone Kani to do that, even though we don't currently support that use case.

To compile the dependencies, you can set RUSTFLAGS env variables with the flags you pass to rustc and invoke Kani with the following flags: --codegen-only and --keep-temps

[adpaco-aws]

@celinval has kindly provided me with more detailed steps to follow for this case, and I've put together an example to demonstrate them. In the example we consider two separate Rust files defined as:

target.rs

extern crate dependency;

#[kani::proof]
fn main() {
    let x = dependency::add(1, 2);
    assert_eq!(x, 3);
}

dependency.rs

pub fn add(left: usize, right: usize) -> usize {
    left + right
}

First, you need to compile each dependency with standalone Kani (i.e., kani) and the flags --only-codegen and --keep-temps. This will produce one file with the .rlib format for each dependency. In our example, we execute kani --only-codegen --keep-temps dependency.rs and get the libdependency.rlib file.

Then, you need to call standalone Kani again on the main file, passing the --extern flag through RUSTFLAGS to Kani so the dependencies are properly linked. In our example, we execute RUSTFLAGS="--extern dependency=libdependency.rlib" kani target.rs. That should result in the following output:

Kani Rust Verifier 0.47.0 (standalone)
Checking harness main...
[...]
SUMMARY:
 ** 0 of 2 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.021634178s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

Please let us know if these instructions don't work for you for any reason. I might add them to our documentation later in the week in case they're useful to other people 😄

[rodionov]

Many thanks, @celinval and @adpaco-aws for the prompt responses! This perfectly answers my original question!

While trying these instruction above I'm running into other issues related to rustc compiler invocation while executing kani: such as missing or renamed Rust features, for example #![feature(no_coverage)] <--- feature has been removed.

The project I'm attempting to verify is built using a custom rustc compiler and the code implements some Rust features supported/handled by the custom rustc compiler. However, when running kani on the target code I'm getting a bunch of compiler errors during kani-compiler invocation. I wonder if it's possible to somehow override rustc used in kani-compiler to use my custom version of rustc? Documentation at https://model-checking.github.io/kani/rustc-hacks.html#custom-rustc provides a solution. I wonder if there is an easier option without rebuilding Kani from source?

Thank you!
Eugene

[JustusAdam]

Hey Rodinov, I suspect this is won't be possible. The reason is that Kani is itself basically rustc. Now the way it actually works is that rustc compiles to a shared library rustc_driver which Kani links against. You could try and LD_PRELOAD your own rustc_driver version in the hopes that its shared library interface is the same as the rustc that Kani was built against, but I suspect that won't be the case.
I suspect you will have to rebuild Kani at the very least. However the most difficult part of building Kani with a custom compiler is building the various stages of rustc, which you have already done, so it shouldn't be too much effort to build Kani from source (we do it every day and so does the GitHub CI 😉).

The other option would be to use an older version of Kani that is compatible with the rustc that your custom compiler is forked off of. You would want to use such an older version even when building from source, because the rustc internal interfaces that Kani uses change all the time and so a modern Kani would likely need adjustment to compile against your rustc version.

[rodionov]

Many thanks, @JustusAdam! Understood! I guess with all the help in this thread I consider my original question answered :) Thanks a lot!

[celinval]

BTW, if the occurrences of these features are sporadic, you can write conditional code using the kani configuration attribute. Like only enable a feature if kani is not present: #![cfg_attr(not(kani), no_coverage].

[rodionov]

@celinval @adpaco-aws while trying to follow solution described above (run kani directly on crates) I run into some problems due to dependencies. It seems that kani driver determines the value of --crate-name argument for kani-compiler based on the name of the source file. However, in my project pretty much all the decencies have the same root file name -- dep_folder/src/lib.rs As a result, all the dependencies are compiled using --crate-name lib. And this seems to cause some problems when dependencies are resolved...

Here is a small example reproducing the issue. Assuming we are in /tmp folder:

/tmp/a/src/lib.rs:

pub fn add_a(left: usize, right: usize) -> usize {
    left + right
}

/tmp/b/src/lib.rs:

usa a;

pub fn add_b(left: usize, right: usize) -> usize {
    a::add_a(left, right)
}

/tmp/c/src/lib.rs:

usa b;

pub fn add_c(left: usize, right: usize) -> usize {
    b::add_b(left, right)
}

Running the following commands shows the problem with finding crate b when running kani on crate c:

# compile dependency a
RUSTFLAGS="--edition 2021 -L /tmp -C metadata=a" kani --only-codegen --keep-temps a/src/lib.rs --target-dir=/tmp/a
cp a/liblib.rlib ./liba.rlib

# compile dependency b which depends on a
RUSTFLAGS="--edition 2021 -L /tmp -C metadata=b --extern a=/tmp/liba.rlib" kani --only-codegen --keep-temps b/src/lib.rs --target-dir=/tmp/b
cp b/liblib.rlib ./libb.rlib

# finally build c which depends on b
RUSTFLAGS="--edition 2021 -L /tmp -C metadata=c --extern b=/tmp/libb.rlib" kani --only-codegen --keep-temps c/src/lib.rs --target-dir=/tmp/c

Error[E0463]: can't find crate for `lib`
 --> c/src/lib.rs:1:5
  |
1 | use b;
  |     ^ can't find crate

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0463`.

Renaming the source file names fixes the issue (e.g. a/src/lib.rs -> a/src/a.rs). Thus, this hinting that the value of--crate-name argument might be a problem. I attempted to provide --crate-name via RUSTFLAGS variable but kani-compiler complains about providing this argument two times.

@celinval @adpaco-aws what do you think? Or could this be some other problem?
If the issue is in the crate name would it be possible to fix it somehow to support this use case?

Many thanks!

[celinval]

Hi @rodionov, yes, this is something that we could address on our side. We could add --crate-name argument to standalone kani command to let users override the name of their crate.

[adpaco-aws]

I've drafted #3054 but I'm seeing this error when following the same steps:

error[E0463]: can't find crate for `b`
 --> c/src/lib.rs:1:5
  |
1 | use b;
  |     ^ can't find crate

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0463`.

I'd like to try a few more things, but this may indicate that adding the --crate-name feature is not enough to solve the issue when there are transitive dependencies.