Use cfg=kani_host for host crates (rust-lang#3244)

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 rust-lang#3101, rust-lang#3238

docs/src/usage.md

@@ -80,10 +80,11 @@ For more information please consult this [blog post](https://blog.rust-lang.org/
 
 ## The build process
 
-When Kani builds your code, it does two important things:
+When Kani builds your code, it does three important things:
 
-1. It sets `cfg(kani)`.
+1. It sets `cfg(kani)` for target crate compilation (including dependencies).
 2. It injects the `kani` crate.
+3. It sets `cfg(kani_host)` for host build targets such as any build script and procedural macro crates.
 
 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()
@@ -561,7 +561,7 @@ fn package_targets(args: &VerificationArgs, package: &Package) -> Vec<Verificati
         }
         if !ignored_unsupported.is_empty() {
             println!(
-                "Skipped the following unsupported targets: '{}'.",
+                "Skipped verification of the following unsupported targets: '{}'.",
                 ignored_unsupported.join("', '")
             );
         }

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

@@ -0,0 +1,2 @@
+This repo contains contains a minimal example that used to break compilation
+when using Kani. See https://github.com/model-checking/kani/issues/3101.

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,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+
+use constants::SOME_CONSTANT;
+
+fn main() {
+    // build.rs changes should trigger rebuild
+    println!("cargo:rerun-if-changed=build.rs");
+
+    #[cfg(not(kani_host))]
+    assert_eq!(constants::SOME_CONSTANT, 0);
+    #[cfg(kani_host)]
+    assert_eq!(constants::SOME_CONSTANT, 2);
+}

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

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+// This file demonstrates that Kani is working on the `binary` crate itself.
+
+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,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "constants"
+version = "0.1.0"
+edition = "2021"
+
+
+[dependencies]

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

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// From https://github.com/model-checking/kani/issues/3101
+
+#[cfg(not(any(kani, kani_host)))]
+pub const SOME_CONSTANT: u32 = 0;
+#[cfg(kani)]
+pub const SOME_CONSTANT: u32 = 1;
+#[cfg(kani_host)]
+pub const SOME_CONSTANT: u32 = 2;
+
+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 one() {
+        assert_eq!(constants::SOME_CONSTANT, 1);
+    }
+}

tests/cargo-ui/unsupported-lib-types/proc-macro/expected

@@ -1,2 +1,2 @@
-Skipped the following unsupported targets: 'lib'.
+Skipped verification of the following unsupported targets: 'lib'.
 error: No supported targets were found.

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");