Use cfg=kani_host for host crates

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,14 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[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,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[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);
+    }
+}

tests/script-based-pre/build-rs-conditional/Cargo.toml

@@ -8,4 +8,4 @@ edition = "2021"
 [dependencies]
 
 [lints.rust]
-unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)', 'cfg(kani_host)'] }

tests/script-based-pre/build-rs-conditional/build.rs

@@ -3,7 +3,7 @@
 //! Verify that build scripts can check if they are running under `kani`.
 
 fn main() {
-    if cfg!(kani) {
+    if cfg!(kani_host) {
         println!("cargo:rustc-env=RUNNING_KANI=Yes");
     } else {
         println!("cargo:rustc-env=RUNNING_KANI=No");