How to just verify one harness? How long does one verification usually take?

[tengjiang]

I'm trying to pick a challenge to start and am running something that's already been developed to get a taste of what it might look like by running the following command:

./scripts/run-kani.sh --kani-args "--harness ptr::not_null::verify::non_null_check_new_unchecked"

However, it seems to be running all the harnesses, not just the one I designated. Also, it tried to re-compile everything from scratch every time I ran the script. It's been hours and it's still running. I'd appreciate it if anyone could give me some pointers on which direction I should be aiming for right now. Thank you!

Compile message

Compiling proc_macro v0.0.0 (/mydata/verify-rust-std/library/proc_macro)
Compiling dummy v0.1.0 (/mydata/verify-rust-std/target/kani_verify_std)
Finished `dev` profile [unoptimized + debuginfo] target(s) in 7m 23s

Seems to be running harnesses that I did not designate:

Checking harness alloc::layout::verify::check_array_i32...
CBMC 6.4.1 (cbmc-6.4.1)
CBMC version 6.4.1 (cbmc-6.4.1) 64-bit x86_64 linux
Reading GOTO program from file /mydata/verify-rust-std/target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/core-2e8dd81abd25a386__RNvNtNtNtCs2AT3ASgq2Ut_4core5alloc6layout6verify15check_array_i32.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)
...

[zhassan-aws]

Hi @tengjiang. Thanks for your interest in this effort. It looks like a bug was introduced in #229 that prevents the arguments from getting passed properly. I opened #232 to fix it. Until the PR is merged, you can apply this patch locally:

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 72aa8ef1760..63df2886d0d 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -288,7 +288,7 @@ main() {
             # Run verification for all harnesses (not in parallel)
             echo "Running Kani verify-std command..."
             "$kani_path" verify-std -Z unstable-options ./library \
-                $unstable_args
+                $unstable_args \
                 $command_args \
                 --enable-unstable \
                 --cbmc-args --object-bits 12

[tengjiang]

Thank you for the timely reply! I'm trying to rerun the commit right now. I'm curious about why it would take so long to recompile everything again, even after the first run (for my machine, it takes ~10 minutes before actually running anything). Any solution to this?

At first, I tried the following command, but after 20 minutes, it told me it did not find the harness. Frankly speaking, I did not expect it to take this long to tell me that a harness could not be found. When I ran it successfully, it told me that the verification takes ~30 seconds, but when you take compiling time into consideration, it's actually 20 minutes even to test out just one harness (and can't be avoided anyhow):

VERIFICATION:- SUCCESSFUL
Verification Time: 28.441355s

Is there a way to avoid this kind of long-run process that hinders iterative testing (or at least we can try to build it once and don't need to repeat it for future runs?)? Thx!

[tengjiang]

Just to follow up, why does ./scripts/run-kani.sh --run list --kani-args also take about 15 minutes and rebuild everything?
This is the output:

Using TOML file: tool_config/kani-version.toml
Using repository URL: https://github.com/model-checking/kani.git
Kani binary is up to date. Skipping build.
Kani executable path: /mydata/verify-rust-std/kani_build/scripts/kani
Running Kani command...
kani 0.56.0
Running Kani list command...
Kani Rust Verifier 0.56.0 (standalone)
warning: /mydata/verify-rust-std/target/kani_verify_std/Cargo.toml: no edition set: defaulting to the 2015 edition while the latest is 2021
    Updating crates.io index
   Compiling proc-macro2 v1.0.92
   Compiling version_check v0.9.5
   Compiling unicode-ident v1.0.14
   Compiling syn v1.0.109
   Compiling safety v0.1.0 (/mydata/verify-rust-std/library/contracts/safety)
   Compiling compiler_builtins v0.1.138
   Compiling libc v0.2.162
   Compiling std v0.0.0 (/mydata/verify-rust-std/library/std)
   Compiling proc-macro-error-attr v1.0.4
   Compiling proc-macro-error v1.0.4
   Compiling quote v1.0.37
   Compiling syn v2.0.90
   Compiling core v0.0.0 (/mydata/verify-rust-std/library/core)
   Compiling rustc-std-workspace-core v1.99.0 (/mydata/verify-rust-std/library/rustc-std-workspace-core)
   Compiling alloc v0.0.0 (/mydata/verify-rust-std/library/alloc)
   Compiling cfg-if v1.0.0
   Compiling memchr v2.7.4
   Compiling adler v1.0.2
   Compiling rustc-demangle v0.1.24
   Compiling unwind v0.0.0 (/mydata/verify-rust-std/library/unwind)
   Compiling rustc-std-workspace-alloc v1.99.0 (/mydata/verify-rust-std/library/rustc-std-workspace-alloc)
   Compiling panic_abort v0.0.0 (/mydata/verify-rust-std/library/panic_abort)
   Compiling panic_unwind v0.0.0 (/mydata/verify-rust-std/library/panic_unwind)
   Compiling gimli v0.29.0
   Compiling hashbrown v0.15.0
   Compiling object v0.36.5
   Compiling miniz_oxide v0.7.4
   Compiling std_detect v0.1.5 (/mydata/verify-rust-std/library/stdarch/crates/std_detect)
   Compiling addr2line v0.22.0
   Compiling proc_macro v0.0.0 (/mydata/verify-rust-std/library/proc_macro)
   Compiling dummy v0.1.0 (/mydata/verify-rust-std/target/kani_verify_std)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 7m 20s
Wrote list results to /mydata/verify-rust-std/kani-list.md

[zhassan-aws]

Can you file an issue on the long compilation time? We can investigate and see if it can be improved.