Kani verify-std runs on cached contracts & harnesses

[QinyuanWu]

I found that the kani verify-std command was always running a cached version of the contracts & harnesses after these dependencies and the following changes are added:


I can temporary work around this by deleting all the changes and added files so then kani would run on the latest contract & harness modifications. However, when the command is invoked the subsequent same command would run on the previous data in which I could not tell the effects of the modifications I made. One of my teammate has ran into the same situation and they ran cargo kani setup and resolves it. I tried that too but the issue persists. Appreciates any guidance. Thanks! @zhassan-aws

[carolynzech]

I'm not entirely sure I understand this sentence:

However, when the command is invoked the subsequent same command would run on the previous data in which I could not tell the effects of the modifications I made.

But if the problem is about cached artifacts, can you just run cargo clean between invocations and see if that works?

[QinyuanWu]

cargo clean can workaround this issue but not fully resolve it. We demoed this issue to @zhassan-aws and there might be a kani bug with M2 chip and Zyad is investigating it.

[zhassan-aws]

I was able to reproduce this issue. Apparently, the issue occurs if the kani verify-std command is run from inside verify-rust-std/library. If it is run one level up, things work as expected:

Inside library (Notice the unexepected Adding lines in the output):

$ kani verify-std -Zunstable-options . -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify
Kani Rust Verifier 0.55.0 (standalone)
    Creating library package
      Adding `kani_verify_std` as member of workspace at `/home/zyadh/git/verify-rust-std/library`
note: see more `Cargo.toml` keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
    Updating crates.io index
     Locking 8 packages to latest compatible versions
      Adding proc-macro-error v1.0.4
      Adding proc-macro-error-attr v1.0.4
      Adding proc-macro2 v1.0.87
      Adding quote v1.0.37
      Adding syn v1.0.109 (latest: v2.0.79)
      Adding syn v2.0.79
      Adding unicode-ident v1.0.13
      Adding version_check v0.9.5
   Compiling proc-macro2 v1.0.87
   Compiling version_check v0.9.5
   Compiling unicode-ident v1.0.13
   Compiling syn v1.0.109
   Compiling safety v0.1.0 (/home/zyadh/git/verify-rust-std/library/contracts/safety)
   Compiling compiler_builtins v0.1.123
   Compiling libc v0.2.158
   Compiling memchr v2.5.0
   ...

One level up:

$ git restore .
$ git clean -xffd
$ git status
On branch main
Your branch is behind 'origin/main' by 1 commit, and can be fast-forwarded.
  (use "git pull" to update your local branch)

nothing to commit, working tree clean
$ kani verify-std -Zunstable-options library -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify
Kani Rust Verifier 0.55.0 (standalone)
    Creating library package
note: see more `Cargo.toml` keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
    Updating crates.io index
   Compiling proc-macro2 v1.0.87
   Compiling unicode-ident v1.0.13
   Compiling version_check v0.9.5
   Compiling syn v1.0.109
   Compiling safety v0.1.0 (/home/zyadh/git/verify-rust-std/library/contracts/safety)
   Compiling compiler_builtins v0.1.123
   Compiling libc v0.2.158
   Compiling memchr v2.5.0
   Compiling std v0.0.0 (/home/zyadh/git/verify-rust-std/library/std)
   Compiling proc-macro-error-attr v1.0.4
   Compiling proc-macro-error v1.0.4
   ...

This also removes the need to do a cargo clean in between runs.

@QinyuanWu can you check if this solves the issue?

[zhassan-aws]

I filed model-checking/kani#3574 for tracking the issue.

[QinyuanWu]

@zhassan-aws I ran cargo clean and moved up one level to run the same command(with absolute path to library) and have the following error:

This is my folder structure:

[zhassan-aws]

Actually, not sure if updating the submodules will work. You might need to clean up the workspace, e.g. git clean -xfd.

[zhassan-aws]

You can also just remove the target directory: rm -rf target.

[QinyuanWu]

Umm the same issue persists after I ran all the commands ;-; This is the content of /library/target/kani_verify_std/Cargo.toml but the error says No such file or directory

[zhassan-aws]

What happens if you clone a fresh copy of the verify-rust-std repository and run the kani verify-std command in its root directory?

[QinyuanWu]

@zhassan-aws I cloned the original(not the forked) main branch and typed in the root directory:

kani verify-std -Z unstable-options "/Users/owo/Desktop/verify-rust-std/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify::non_null > verification.log

It compiles successfully and produces output but what was super strange is that it verified 5 harnesses(align_offset_negative, align_offset, addr, new, new_unchecked, basically what I have on my own forked working branch) when there are only 2 in the actual module:

[QinyuanWu]

After debugging with @zhassan-aws this problem is resolved by cargo clean in the library folder, git restore library/Cargo.toml library/Cargo.lock, and delete any existing target folders then re-run kani verify-std in the root folder. The main point is to restore the files to their original version consistent with main.