Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Issue injecting Kani module to dependency (zerocopy) #3238

Closed
zi0Black opened this issue Jun 7, 2024 · 6 comments
Closed

Issue injecting Kani module to dependency (zerocopy) #3238

zi0Black opened this issue Jun 7, 2024 · 6 comments
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@zi0Black
Copy link

zi0Black commented Jun 7, 2024

I tried to just create a basic proof on the Aptos-Core project, but I faced an issue with building with Kani, likely a bug with module injection:

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8238:9
     |
8238 |         kani::assume(matches!(base.size_info, SizeInfo::SliceDst(..)));
     |         ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8247:33
     |
8247 |         let layout: DstLayout = kani::any();
     |                                 ^^^^ use of undeclared crate or module `kani`

error: aborting due to 37 previous errors

For more information about this error, try `rustc --explain E0433`.
error: could not compile `zerocopy` (lib) due to 38 previous errors
warning: build failed, waiting for other jobs to finish...
error: Failed to execute cargo (exit status: 101). Found 38 compilation errors.

I believe this bug triggers only on certain combination of features, cargo build environment, and previous issue: #3109, where there was some issue with replicating the environment.

I tried this code:

  1. Clone Aptos Core: git clone https://github.com/aptos-labs/aptos-core
  2. Run dev setup: ./scripts/dev_setup.sh
  3. Install and setup Kani
  4. Open consensus/src/transaction_shuffler/sender_aware.rs
  5. Add the following code at the bottom:
#[cfg(kani)]
mod verification {
    use super::*;

    #[kani::proof]
    pub fn test_3_sender_shuffling() {

    }
}
  1. Run: cargo kani --package aptos-consensus --harness transaction_shuffler::sender_aware::verification::test_3_sender_shuffling

with Kani version: 0.52

I expected to see this happen: Kani building the project.

Instead, this happened: A dependency which uses Kani, zerocopy, fails to build because there is a missing Kani module.

xcd@ttt:~/aptos-core$ RUST_BACKTRACE=1 cargo kani --package aptos-consensus --harness transaction_shuffler::sender_aware::verification::test_3_sender_shuffling
Kani Rust Verifier 0.52.0 (cargo plugin)
warning: /home/xcd/aptos-core/crates/aptos-push-metrics/Cargo.toml: `default_features` is deprecated in favor of `default-features` and will not work in the 2024 edition
(in the `ureq` dependency)
warning: /home/xcd/aptos-core/aptos-node/Cargo.toml: `default_features` is deprecated in favor of `default-features` and will not work in the 2024 edition
(in the `rstack-self` dependency)
warning: /home/xcd/aptos-core/crates/aptos-github-client/Cargo.toml: `default_features` is deprecated in favor of `default-features` and will not work in the 2024 edition
(in the `ureq` dependency)
warning: /home/xcd/aptos-core/crates/aptos-crypto/Cargo.toml: `default_features` is deprecated in favor of `default-features` and will not work in the 2024 edition
(in the `neptune` dependency)
warning: /home/xcd/aptos-core/crates/aptos-system-utils/Cargo.toml: `default_features` is deprecated in favor of `default-features` and will not work in the 2024 edition
(in the `rstack-self` dependency)
warning: /home/xcd/aptos-core/secure/storage/vault/Cargo.toml: `default_features` is deprecated in favor of `default-features` and will not work in the 2024 edition
(in the `ureq` dependency)
   Compiling zerocopy v0.7.34
   Compiling serde v1.0.197
   Compiling zeroize v1.7.0
   Compiling num-bigint v0.4.4
   Compiling thiserror v1.0.56
   Compiling num-iter v0.1.43
   Compiling rand v0.7.3
   Compiling rusty-fork v0.3.0
   Compiling indexmap v1.9.3
   Compiling radium v0.7.0
   Compiling block-padding v0.2.1
   Compiling time-core v0.1.2
   Compiling ethnum v1.5.0
   Compiling crossbeam-epoch v0.9.18
   Compiling wyz v0.5.1
   Compiling fixed-hash v0.7.0
   Compiling ref-cast v1.0.22
   Compiling arbitrary v1.3.2
   Compiling funty v2.0.0
   Compiling gimli v0.28.1
   Compiling backtrace v0.3.69
   Compiling socket2 v0.5.5
   Compiling tracing-core v0.1.32
   Compiling object v0.32.2
   Compiling fnv v1.0.7
   Compiling rand_core v0.5.1
   Compiling rustc-demangle v0.1.23
   Compiling unicode-width v0.1.11
   Compiling rand_xorshift v0.3.0
   Compiling aho-corasick v1.1.2
error[E0433]: failed to resolve: use of undeclared crate or module `kani`
   --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/util.rs:766:7
    |
766 |     #[kani::proof]
    |       ^^^^ use of undeclared crate or module `kani`

   Compiling generic-array v0.14.7
   Compiling anyhow v1.0.79
error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8102:7
     |
8102 |     #[kani::proof]
     |       ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8226:7
     |
8226 |     #[kani::proof]
     |       ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8227:7
     |
8227 |     #[kani::should_panic]
     |       ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8243:7
     |
8243 |     #[kani::proof]
     |       ^^^^ use of undeclared crate or module `kani`

   Compiling same-file v1.0.6
   Compiling proptest v1.4.0
   Compiling regex-syntax v0.8.2
   Compiling ryu v1.0.16
   Compiling rustversion v1.0.14
   Compiling time-macros v0.2.16
error[E0433]: failed to resolve: use of undeclared crate or module `kani`
   --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/util.rs:774:35
    |
774 |         let align: NonZeroUsize = kani::any();
    |                                   ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
   --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/util.rs:775:9
    |
775 |         kani::assume(align.get().is_power_of_two());
    |         ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
   --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/util.rs:776:24
    |
776 |         let n: usize = kani::any();
    |                        ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8045:10
     |
8045 |     impl kani::Arbitrary for DstLayout {
     |          ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8047:39
     |
8047 |             let align: NonZeroUsize = kani::any();
     |                                       ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8048:39
     |
8048 |             let size_info: SizeInfo = kani::any();
     |                                       ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8050:13
     |
8050 |             kani::assume(align.is_power_of_two());
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8051:13
     |
8051 |             kani::assume(align < DstLayout::THEORETICAL_MAX_ALIGN);
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8057:13
     |
8057 |             kani::assume(
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8073:10
     |
8073 |     impl kani::Arbitrary for SizeInfo {
     |          ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8075:34
     |
8075 |             let is_sized: bool = kani::any();
     |                                  ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8079:39
     |
8079 |                     let size: usize = kani::any();
     |                                       ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8081:21
     |
8081 |                     kani::assume(size <= isize::MAX as _);
     |                     ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8085:45
     |
8085 |                 false => SizeInfo::SliceDst(kani::any()),
     |                                             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8090:10
     |
8090 |     impl kani::Arbitrary for TrailingSliceLayout {
     |          ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8092:36
     |
8092 |             let elem_size: usize = kani::any();
     |                                    ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8093:33
     |
8093 |             let offset: usize = kani::any();
     |                                 ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8095:13
     |
8095 |             kani::assume(elem_size < isize::MAX as _);
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8096:13
     |
8096 |             kani::assume(offset < isize::MAX as _);
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8106:31
     |
8106 |         let base: DstLayout = kani::any();
     |                               ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8107:32
     |
8107 |         let field: DstLayout = kani::any();
     |                                ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8108:44
     |
8108 |         let packed: Option<NonZeroUsize> = kani::any();
     |                                            ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8111:13
     |
8111 |             kani::assume(max_align.is_power_of_two());
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8112:13
     |
8112 |             kani::assume(base.align <= max_align);
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8116:9
     |
8116 |         kani::assume(matches!(base.size_info, SizeInfo::Sized { .. }));
     |         ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8229:31
     |
8229 |         let base: DstLayout = kani::any();
     |                               ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8230:32
     |
8230 |         let field: DstLayout = kani::any();
     |                                ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8231:44
     |
8231 |         let packed: Option<NonZeroUsize> = kani::any();
     |                                            ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8234:13
     |
8234 |             kani::assume(max_align.is_power_of_two());
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8235:13
     |
8235 |             kani::assume(base.align <= max_align);
     |             ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8238:9
     |
8238 |         kani::assume(matches!(base.size_info, SizeInfo::SliceDst(..)));
     |         ^^^^ use of undeclared crate or module `kani`

error[E0433]: failed to resolve: use of undeclared crate or module `kani`
    --> /home/xcd/.cargo/registry/src/index.crates.io-6f17d22bba15001f/zerocopy-0.7.34/src/lib.rs:8247:33
     |
8247 |         let layout: DstLayout = kani::any();
     |                                 ^^^^ use of undeclared crate or module `kani`

error: aborting due to 37 previous errors

For more information about this error, try `rustc --explain E0433`.
error: could not compile `zerocopy` (lib) due to 38 previous errors
warning: build failed, waiting for other jobs to finish...
error: Failed to execute cargo (exit status: 101). Found 38 compilation errors.
@zi0Black zi0Black added the [C] Bug This is a bug. Something isn't working. label Jun 7, 2024
@tautschnig
Copy link
Member

This might be the same problem as #3101. We are investigating.

@tautschnig
Copy link
Member

I believe the (pending) fix for #3101 also addresses the Kani issue here, but then I actually get build failures unrelated to Kani on this project (when building the time crate; after issuing cargo update I now get build failures in the ring crate).

tautschnig added a commit to tautschnig/kani that referenced this issue Jun 8, 2024
@tautschnig
Use cfg=kani_host for host crates
a5038a7 
We want to run the proofs in the target crate and don't need to build
(or run) the proofs in any of the host crates. This avoids a need to
make available the `kani` crate to any such host crates.

Resolves model-checking#3101, model-checking#3238
@tautschnig tautschnig mentioned this issue Jun 8, 2024
Merged
@zi0Black
Copy link
Author

zi0Black commented Jun 8, 2024

I believe the (pending) fix for #3101 also addresses the Kani issue here, but then I actually get build failures unrelated to Kani on this project (when building the time crate; after issuing cargo update I now get build failures in the ring crate).

I tried too, I think this is given by the version of rust compiler used by Kani! A quick check with cargo +nightly-2024-05-28 build confirmed this.

tautschnig added a commit that referenced this issue Jun 10, 2024
@tautschnig
Use cfg=kani_host for host crates (#3244)
d4a3f7b 
We want to run the proofs in the target crate and don't need to build
(or run) the proofs in any of the host crates. This avoids a need to
make available the `kani` crate to any such host crates.

Resolves #3101, #3238
@tautschnig
Copy link
Member

Fixed by #3244.

@tautschnig
Copy link
Member

I tried too, I think this is given by the version of rust compiler used by Kani! A quick check with cargo +nightly-2024-05-28 build confirmed this.

If you're up for building the the latest version of kani: we now have both the fix from #3244 merged as well as a more recent toolchain/rust compiler, which might fix those problems.

@zi0Black
Copy link
Author

@tautschnig I saw that the build chain can be easily replaced while compiling locally. I'm just curious why Kani sticks so quickly with nightly releases.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@tautschnig @zi0Black