Use cfg=kani_host for host crates

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

docs/src/usage.md

@@ -84,6 +84,7 @@ When Kani builds your code, it does two important things:
 
 1. It sets `cfg(kani)`.
 2. It injects the `kani` crate.
+3. For host crates (crates that your target crate depends on), Kani sets `cfg(kani_host)`.
 
 A proof harness (which you can [learn more about in the tutorial](./kani-tutorial.md)), is a function annotated with `#[kani::proof]` much like a test is annotated with `#[test]`.
 But you may experience a similar problem using Kani as you would with `dev-dependencies`: if you try writing `#[kani::proof]` directly in your code, `cargo build` will fail because it doesn't know what the `kani` crate is.

kani-driver/src/call_cargo.rs

@@ -326,10 +326,10 @@ pub fn cargo_config_args() -> Vec<OsString> {
  [
  "--target",
  env!("TARGET"),
- // Propagate `--cfg=kani` to build scripts.
+ // Propagate `--cfg=kani_host` to build scripts.
  "-Zhost-config",
  "-Ztarget-applies-to-host",
- "--config=host.rustflags=[\"--cfg=kani\"]",
+ "--config=host.rustflags=[\"--cfg=kani_host\"]",
  ]
  .map(OsString::from)
  .to_vec()

tests/cargo-kani/build-rs-plus-host-with-kani-proofs/README.md

@@ -0,0 +1,10 @@
+This repo contains contains a minimal example that breaks compilation when using [kani](https://github.com/model-checking/kani), where I would expect compilation to work.
+
+Deleting the `binary/build.rs` script makes the compilation work suddenly, despite it being skipped anyways:
+
+```
+binary$ cargo kani -v
+Kani Rust Verifier 0.48.0 (cargo plugin)
+Skipped the following unsupported targets: 'build-script-build'.
+...
+```

tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "binary"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+constants = { path = "../constants" }
+
+[build-dependencies]
+constants = { path = "../constants" }

tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/build.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+
+use constants::SOME_CONSTANT;
+
+// Having a build script that depends on the constants package
+// breaks kani compilation of that package, when compiling the build script.
+// I assume it's because the build compile does not set cfg(kani) on the constants package dependency.
+
+fn main() {
+ // build.rs changes should trigger rebuild
+ println!("cargo:rerun-if-changed=build.rs");
+
+ // Here we have an assertion that gives us additional compile-time checks.
+ // In reality, here I read a linker script and assert certain properties in relation to constants defined in the constants package.
+ assert_eq!(SOME_CONSTANT, 42);
+}

tests/cargo-kani/build-rs-plus-host-with-kani-proofs/binary/src/main.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+
+use constants::SomeStruct;
+
+fn function_that_does_something(b: bool) -> SomeStruct {
+ SomeStruct { some_field: if b { 42 } else { 24 } }
+}
+
+fn main() {
+ println!("The constant is {}", constants::SOME_CONSTANT);
+
+ let some_struct = function_that_does_something(true);
+
+ println!("some_field is {:?}", some_struct.some_field);
+}
+
+#[cfg(kani)]
+mod verification {
+ use super::*;
+
+ #[kani::proof]
+ fn function_never_returns_zero_struct() {
+ let input: bool = kani::any();
+ let output = function_that_does_something(input);
+
+ assert!(output.some_field != 0);
+ }
+}

tests/cargo-kani/build-rs-plus-host-with-kani-proofs/constants/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "constants"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/cargo-kani/build-rs-plus-host-with-kani-proofs/constants/src/lib.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+
+pub const SOME_CONSTANT: u32 = 42;
+
+pub struct SomeStruct {
+ pub some_field: u32,
+}
+
+#[cfg(kani)]
+impl kani::Arbitrary for SomeStruct {
+ fn any() -> Self {
+ SomeStruct { some_field: kani::any() }
+ }
+}
+
+#[cfg(kani)]
+mod verification {
+ use super::*;
+
+ #[kani::proof]
+ fn zero() {
+ assert_ne!(SOME_CONSTANT, 0);
+ }
+}