Kani always rebuilds when running verify-std

[dawidl022]

I was following the instructions to run Kani on the verify-rust-std project, and everytime I execute the command the entire project gets rebuilt, even when there are no changes to the code. Ideally, if no code changes were made, only the model checker should run.

Seems to be the same behaviour as described in #895, but that should have been fixed by #2232, so I'm not sure if this is specific to just verify-std or a more general issue.

[zhassan-aws]

Thanks for creating this issue @dawidl022. Indeed, this seems to be specific to verify-rust-std. On a normal package, compilation is skipped if the code hasn't changed:

$ cargo clean
     Removed 31 files, 2.7MiB total
$ cargo kani --verbose |& grep kani-compiler
[Kani] Running: `CARGO_ENCODED_RUSTFLAGS="-Coverflow-checks=on-Zunstable-options-Ztrim-diagnostic-paths=no-Zhuman_readable_cgu_names-Zalways-encode-mir--cfg=kani-Zcrate-attr=feature(register_tool)-Zcrate-attr=register_tool(kanitool)--sysroot/home/ubuntu/git/kani/target/kani-L/home/ubuntu/git/kani/target/kani/lib--externkani--externnoprelude:std=/home/ubuntu/git/kani/target/kani/lib/libstd.rlib-Cpanic=abort-Csymbol-mangling-version=v0-Zpanic_abort_tests=yes-Zmir-enable-passes=-RemoveStorageMarkers--check-cfg=cfg(kani)-Clinker=echo--kani-compiler-Cllvm-args=--check-version=0.62.0 --log-level=info --assertion-reach-checks" CARGO_TERM_PROGRESS_WHEN="never" RUSTC="/home/ubuntu/git/kani/target/kani/bin/kani-compiler" RUSTC_BOOTSTRAP="1" cargo +nightly-2025-05-16-x86_64-unknown-linux-gnu rustc --target x86_64-unknown-linux-gnu -Zhost-config -Ztarget-applies-to-host --config=host.rustflags=["--cfg=kani_host"] --target-dir /home/ubuntu/examples/test_compile/target/kani --message-format json-diagnostic-rendered-ansi -v -p path+file:///home/ubuntu/examples/test_compile#0.1.0 --bin test_compile -- -Cllvm-args=--reachability=harnesses`
     Running `/home/ubuntu/git/kani/target/kani/bin/kani-compiler --crate-name bitflags --edition=2021 /home/ubuntu/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/bitflags-2.9.1/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values("arbitrary", "bytemuck", "compiler_builtins", "core", "example_generated", "rustc-dep-of-std", "serde", "std"))' -C metadata=6ba6e3320d5cb950 -C extra-filename=-eb158ddb423f3a6b --out-dir /home/ubuntu/examples/test_compile/target/kani/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -L dependency=/home/ubuntu/examples/test_compile/target/kani/x86_64-unknown-linux-gnu/debug/deps -L dependency=/home/ubuntu/examples/test_compile/target/kani/debug/deps --cap-lints allow -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' --sysroot /home/ubuntu/git/kani/target/kani -L /home/ubuntu/git/kani/target/kani/lib --extern kani --extern 'noprelude:std=/home/ubuntu/git/kani/target/kani/lib/libstd.rlib' -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes -Z mir-enable-passes=-RemoveStorageMarkers '--check-cfg=cfg(kani)' -Clinker=echo --kani-compiler '-Cllvm-args=--check-version=0.62.0 --log-level=info --assertion-reach-checks'`
     Running `/home/ubuntu/git/kani/target/kani/bin/kani-compiler --crate-name test_compile --edition=2024 src/main.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --crate-type bin --emit=dep-info,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata=ff5228fe44d69a1a -C extra-filename=-f4e892eda10eb962 --out-dir /home/ubuntu/examples/test_compile/target/kani/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=/home/ubuntu/examples/test_compile/target/kani/x86_64-unknown-linux-gnu/debug/incremental -L dependency=/home/ubuntu/examples/test_compile/target/kani/x86_64-unknown-linux-gnu/debug/deps -L dependency=/home/ubuntu/examples/test_compile/target/kani/debug/deps --extern bitflags=/home/ubuntu/examples/test_compile/target/kani/x86_64-unknown-linux-gnu/debug/deps/libbitflags-eb158ddb423f3a6b.rlib -Cllvm-args=--reachability=harnesses -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' --sysroot /home/ubuntu/git/kani/target/kani -L /home/ubuntu/git/kani/target/kani/lib --extern kani --extern 'noprelude:std=/home/ubuntu/git/kani/target/kani/lib/libstd.rlib' -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes -Z mir-enable-passes=-RemoveStorageMarkers '--check-cfg=cfg(kani)' -Clinker=echo --kani-compiler '-Cllvm-args=--check-version=0.62.0 --log-level=info --assertion-reach-checks'`
$ cargo kani --verbose |& grep kani-compiler
[Kani] Running: `CARGO_ENCODED_RUSTFLAGS="-Coverflow-checks=on-Zunstable-options-Ztrim-diagnostic-paths=no-Zhuman_readable_cgu_names-Zalways-encode-mir--cfg=kani-Zcrate-attr=feature(register_tool)-Zcrate-attr=register_tool(kanitool)--sysroot/home/ubuntu/git/kani/target/kani-L/home/ubuntu/git/kani/target/kani/lib--externkani--externnoprelude:std=/home/ubuntu/git/kani/target/kani/lib/libstd.rlib-Cpanic=abort-Csymbol-mangling-version=v0-Zpanic_abort_tests=yes-Zmir-enable-passes=-RemoveStorageMarkers--check-cfg=cfg(kani)-Clinker=echo--kani-compiler-Cllvm-args=--check-version=0.62.0 --log-level=info --assertion-reach-checks" CARGO_TERM_PROGRESS_WHEN="never" RUSTC="/home/ubuntu/git/kani/target/kani/bin/kani-compiler" RUSTC_BOOTSTRAP="1" cargo +nightly-2025-05-16-x86_64-unknown-linux-gnu rustc --target x86_64-unknown-linux-gnu -Zhost-config -Ztarget-applies-to-host --config=host.rustflags=["--cfg=kani_host"] --target-dir /home/ubuntu/examples/test_compile/target/kani --message-format json-diagnostic-rendered-ansi -v -p path+file:///home/ubuntu/examples/test_compile#0.1.0 --bin test_compile -- -Cllvm-args=--reachability=harnesses`

I suspect this happens in verify-rust-std because Kani is not run in cargo mode, so it cannot rely on the normal cargo machinery to check if code has changed.

CC @carolynzech @tautschnig

[carolynzech]

Hi @dawidl022,

The verify-std subcommand creates a dummy crate, then runs cargo build -Z build-std, overriding the __CARGO_TESTS_ONLY_SRC_ROOT env variable, which tells Cargo to find the standard library source in the library/ folder instead (c.f. https://internals.rust-lang.org/t/how-can-we-patch-the-core-crate-in-cargo-toml/21028):

kani/kani-driver/src/call_cargo.rs

Line 117 in 39d85fc

.env("__CARGO_TESTS_ONLY_SRC_ROOT", full_path.as_os_str());

The behavior you're seeing is because of this logic:

kani/kani-driver/src/project.rs

Lines 308 to 313 in 0b68df0

	// Create dummy crate needed to build using `cargo -Z build-std`
	let dummy_crate = outdir.join("kani_verify_std");
	if dummy_crate.exists() {
	fs::remove_dir_all(&dummy_crate)?;
	}
	session.cargo_init_lib(&dummy_crate)?;

If I change this to be:

 // Create dummy crate needed to build using `cargo -Z build-std`
  let dummy_crate = outdir.join("kani_verify_std");
  if !dummy_crate.exists() {
      session.cargo_init_lib(&dummy_crate)?;
  }

Then if I run kani verify-std twice in a row, then cargo won't recompile the second time, which is good.

First compilation:

Kani Rust Verifier 0.62.0 (standalone)
warning: /Users/cmzech/rust/target/kani_verify_std/Cargo.toml: no edition set: defaulting to the 2015 edition while the latest is 2024
   Compiling proc-macro2 v1.0.94
   Compiling unicode-ident v1.0.18
   Compiling version_check v0.9.5
   Compiling syn v1.0.109
   Compiling safety v0.1.0 (/Users/cmzech/rust/library/contracts/safety)
   Compiling compiler_builtins v0.1.156
   Compiling libc v0.2.172
   Compiling object v0.36.7
   Compiling std v0.0.0 (/Users/cmzech/rust/library/std)
   Compiling proc-macro-error-attr v1.0.4
   Compiling proc-macro-error v1.0.4
   Compiling quote v1.0.40
   Compiling syn v2.0.100
   Compiling core v0.0.0 (/Users/cmzech/rust/library/core)
   Compiling rustc-std-workspace-core v1.99.0 (/Users/cmzech/rust/library/rustc-std-workspace-core)
   Compiling alloc v0.0.0 (/Users/cmzech/rust/library/alloc)
   Compiling cfg-if v1.0.0
   Compiling adler2 v2.0.0
   Compiling memchr v2.7.4
   Compiling rustc-demangle v0.1.24
   Compiling unwind v0.0.0 (/Users/cmzech/rust/library/unwind)
   Compiling rustc-std-workspace-alloc v1.99.0 (/Users/cmzech/rust/library/rustc-std-workspace-alloc)
   Compiling panic_abort v0.0.0 (/Users/cmzech/rust/library/panic_abort)
   Compiling panic_unwind v0.0.0 (/Users/cmzech/rust/library/panic_unwind)
   Compiling gimli v0.31.1
   Compiling hashbrown v0.15.2
   Compiling std_detect v0.1.5 (/Users/cmzech/rust/library/stdarch/crates/std_detect)
   Compiling miniz_oxide v0.8.8
   Compiling addr2line v0.24.2
   Compiling rustc-std-workspace-std v1.99.0 (/Users/cmzech/rust/library/rustc-std-workspace-std)
   Compiling rustc-literal-escaper v0.0.2
   Compiling proc_macro v0.0.0 (/Users/cmzech/rust/library/proc_macro)
   Compiling dummy v0.1.0 (/Users/cmzech/rust/target/kani_verify_std)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 21m 21s
Checking harness collections::vec_deque::verify::check_vecdeque_swap...

Second compilation:

Kani Rust Verifier 0.62.0 (standalone)
warning: /Users/cmzech/rust/target/kani_verify_std/Cargo.toml: no edition set: defaulting to the 2015 edition while the latest is 2024
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.16s
Checking harness collections::vec_deque::verify::check_vecdeque_swap...

The problem is that if I go change code in library/ and then run again, Cargo won't detect the changes, so it runs verification on stale code. So it seems at the moment we need to choose between recompiling every time or not recompiling on changes, and of course the former is really the only viable course.

I'm going to leave this issue open there is some way to only recompile the changed folders that I'm not thinking of, but I at least wanted to provide some context for why things work the way they do.

[zjp-CN]

So it seems at the moment we need to choose between recompiling every time or not recompiling on changes, and of course the former is really the only viable course.

I wonder why kani builds libcore so slow. It takes at least 20 mins to compile libcore and then start verifying.

While distributed-verification the tool I'm working on for GSoC 2025 takes no more than 2 mins to compile libcore, but only doing reachability analysis and traversal hash computation.

What heavy computation does kani perform? Could the computation be split into stages and generate verification related stuff on demand?

[zjp-CN]

I just found we can run single harness quickly. Not sure if the followings are documented:

When using kani autohaness

• --include-pattern reduces time by skipping mismatched autoharness
• --harness reduces time by running the exact harness verification

They must be used together, because sole --include-pattern runs all matched harnesses, while sole --harness scans and analyzes all autoharnesses, both of which case greatly extend the total time.

Example

kani autoharness -Z autoharness -Z function-contracts -Z mem-predicates \
    -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing \
    --std ./library -Z unstable-options --harness-timeout 10m --default-unwind 1000 \
    --include-pattern intrinsics::verify::should_succeed_i32_to_u32 \
    --harness intrinsics::verify::should_succeed_i32_to_u32 

Sidenote: I only tested the kani autoharness command rather than kani, because it's how kani is used in verify-rust-std to search and verify proofs.

Sidenote2: the trick still rebuilds crates, but cuts total time significantly from 20mins to 40s.