Fix target selection for MIR Linker (rust-lang#1789)

When running MIR Linker with multiple targets (e.g., unit tests), we
were failing to compile since the call to `cargo rustc` would have
multiple targets.

Invoke separate calls for each target for now.

Author: celinval

kani-driver/src/call_cargo.rs

@@ -4,7 +4,7 @@
 use crate::args::KaniArgs;
 use crate::session::KaniSession;
 use anyhow::{Context, Result};
-use cargo_metadata::{Metadata, MetadataCommand};
+use cargo_metadata::{Metadata, MetadataCommand, Package};
 use std::ffi::OsString;
 use std::path::{Path, PathBuf};
 use std::process::Command;
@@ -26,7 +26,7 @@ impl KaniSession {
     /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`
     pub fn cargo_build(&self) -> Result<CargoOutputs> {
         let build_target = env!("TARGET"); // see build.rs
-        let metadata = MetadataCommand::new().exec().expect("Failed to get cargo metadata.");
+        let metadata = MetadataCommand::new().exec().context("Failed to get cargo metadata.")?;
         let target_dir = self
             .args
             .target_dir
@@ -39,10 +39,6 @@ impl KaniSession {
         let rustc_args = self.kani_rustc_flags();
 
         let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
-        if self.args.tests {
-            cargo_args.push("--tests".into());
-        }
-
         if self.args.all_features {
             cargo_args.push("--all-features".into());
         }
@@ -53,6 +49,13 @@ impl KaniSession {
         cargo_args.push("--target-dir".into());
         cargo_args.push(target_dir.into());
 
+        if self.args.tests {
+            // Use test profile in order to pull dev-dependencies and compile using `--test`.
+            // Initially the plan was to use `--tests` but that brings in multiple targets.
+            cargo_args.push("--profile".into());
+            cargo_args.push("test".into());
+        }
+
         if self.args.verbose {
             cargo_args.push("-v".into());
         }
@@ -75,17 +78,20 @@ impl KaniSession {
         // Only joing them at the end. All kani flags must come first.
         kani_args.extend_from_slice(&rustc_args);
 
-        let members = project_members(&self.args, &metadata);
-        for member in members {
-            let mut cmd = Command::new("cargo");
-            cmd.args(&cargo_args)
-                .args(vec!["-p", &member])
-                .args(&pkg_args)
-                .env("RUSTC", &self.kani_compiler)
-                .env("RUSTFLAGS", "--kani-flags")
-                .env("KANIFLAGS", &crate::util::join_osstring(&kani_args, " "));
-
-            self.run_terminal(cmd)?;
+        let packages = packages_to_verify(&self.args, &metadata);
+        for package in packages {
+            for target in package_targets(&self.args, package) {
+                let mut cmd = Command::new("cargo");
+                cmd.args(&cargo_args)
+                    .args(vec!["-p", &package.name])
+                    .args(&target.to_args())
+                    .args(&pkg_args)
+                    .env("RUSTC", &self.kani_compiler)
+                    .env("RUSTFLAGS", "--kani-flags")
+                    .env("KANIFLAGS", &crate::util::join_osstring(&kani_args, " "));
+
+                self.run_terminal(cmd)?;
+            }
         }
 
         if self.args.dry_run {
@@ -123,15 +129,60 @@ fn glob(path: &Path) -> Result<Vec<PathBuf>> {
 ///   - I.e.: Do whatever cargo does when there's no default_members.
 ///   - This is because `default_members` is not available in cargo metadata.
 ///     See <https://github.com/rust-lang/cargo/issues/8033>.
-fn project_members(args: &KaniArgs, metadata: &Metadata) -> Vec<String> {
+fn packages_to_verify<'a, 'b>(args: &'a KaniArgs, metadata: &'b Metadata) -> Vec<&'b Package> {
     if !args.package.is_empty() {
-        args.package.clone()
+        args.package
+            .iter()
+            .map(|pkg_name| {
+                metadata
+                    .packages
+                    .iter()
+                    .find(|pkg| pkg.name == *pkg_name)
+                    .expect(&format!("Cannot find package '{}'", pkg_name))
+            })
+            .collect()
     } else {
         match (args.workspace, metadata.root_package()) {
-            (true, _) | (_, None) => {
-                metadata.workspace_members.iter().map(|id| metadata[id].name.clone()).collect()
-            }
-            (_, Some(root_pkg)) => vec![root_pkg.name.clone()],
+            (true, _) | (_, None) => metadata.workspace_packages(),
+            (_, Some(root_pkg)) => vec![root_pkg],
         }
     }
 }
+
+/// Possible verification targets.
+enum VerificationTarget {
+    Bin(String),
+    Lib,
+    Test(String),
+}
+
+impl VerificationTarget {
+    /// Convert to cargo argument that select the specific target.
+    fn to_args(&self) -> Vec<String> {
+        match self {
+            VerificationTarget::Test(name) => vec![String::from("--test"), name.clone()],
+            VerificationTarget::Bin(name) => vec![String::from("--bin"), name.clone()],
+            VerificationTarget::Lib => vec![String::from("--lib")],
+        }
+    }
+}
+
+/// Extract the targets inside a package.
+/// If `--tests` is given, the list of targets will include any integration tests.
+fn package_targets(args: &KaniArgs, package: &Package) -> Vec<VerificationTarget> {
+    package
+        .targets
+        .iter()
+        .filter_map(|target| {
+            if target.kind.contains(&String::from("bin")) {
+                Some(VerificationTarget::Bin(target.name.clone()))
+            } else if target.kind.contains(&String::from("lib")) {
+                Some(VerificationTarget::Lib)
+            } else if target.kind.contains(&String::from("test")) && args.tests {
+                Some(VerificationTarget::Test(target.name.clone()))
+            } else {
+                None
+            }
+        })
+        .collect()
+}

rfc/src/rfcs/0001-mir-linker.md

@@ -1,8 +1,8 @@
 - **Feature Name:** MIR Linker (mir_linker)
 - **RFC Tracking Issue**: <https://github.com/model-checking/kani/issues/1588>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1600>
-- **Status:** In Progress
-- **Version:** 1
+- **Status:** Unstable
+- **Version:** 2
 
 -------------------
 
@@ -236,8 +236,8 @@ These results were obtained by looking at the artifacts generated during the sam
   Thus, it shouldn't have any side effect.
   That relies on all constant initializers being evaluated during compilation.
 - ~~What's the best way to handle `cargo kani --tests`?~~
-  We will use similar mechanism to regular Kani runs:
-  - `cargo rustc --tests -- --reachability=harnesses`
+  For now, we are going to use the test profile and iterate over all the targets available in the crate:
+  - `cargo rustc --profile test -- --reachability=harnesses`
 
 
 ## Future possibilities

tests/cargo-ui/ws-integ-tests/Cargo.toml

@@ -0,0 +1,19 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Create a workspace with three independent libraries that have integration tests.
+# The `in_src_harness` has a proof harness co-located with the code.
+# The `integ_harness` has a proof harness co-located with an integration test.
+# The `all_harness` has proof harnesses with src and integration tests.
+[workspace]
+members = [
+  "in_src_harness",
+  "integ_harness",
+  "all_harness",
+]
+
+[workspace.metadata.kani.flags]
+workspace = true
+tests = true
+enable-unstable=true
+mir-linker=true

tests/cargo-ui/ws-integ-tests/all_harness/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "all_harness"
+version = "0.1.0"
+edition = "2021"
+description = "Package with harnesses that co-located with integration tests and src"
+
+[dependencies]
+integ_harness = { path= "../integ_harness" }
+in_src_harness = { path= "../in_src_harness" }

tests/cargo-ui/ws-integ-tests/all_harness/src/lib.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Dummy harness and library that check left rotation.
+use in_src_harness::rotate_left;
+use integ_harness::rotate_right;
+
+/// Returns if any rotation would result in wrapping bits.
+pub fn will_rotate_wrap(num: u8, rhs: u32) -> bool {
+    rotate_left(num, rhs).1 || rotate_right(num, rhs).1
+}
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    #[kani::proof]
+    fn check_propagate() {
+        let num = kani::any();
+        let shift = kani::any();
+        kani::assume(rotate_right(num, shift).1);
+        assert!(will_rotate_wrap(num, shift));
+    }
+}

tests/cargo-ui/ws-integ-tests/all_harness/tests/check_result.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use all_harness::*;
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    #[kani::proof]
+    fn with_no_panic() {
+        will_rotate_wrap(kani::any(), kani::any());
+    }
+}

tests/cargo-ui/ws-integ-tests/expected

@@ -0,0 +1,14 @@
+Checking harness proofs::check_propagate...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness proofs::with_no_panic...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness proofs::no_panic...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness proofs::will_not_panic...
+VERIFICATION:- SUCCESSFUL
+
+
+Complete - 4 successfully verified harnesses, 0 failures, 4 total.

tests/cargo-ui/ws-integ-tests/in_src_harness/Cargo.toml

@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "in_src_harness"
+version = "0.1.0"
+edition = "2021"
+description = "Package with a harness that is co-located with the library code"
+
+[dependencies]

tests/cargo-ui/ws-integ-tests/in_src_harness/src/lib.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Dummy harness and library that check left rotation.
+
+/// Return the left rotation of the give number and whether the result had wrapped bits.
+pub fn rotate_left(num: u8, rhs: u32) -> (u8, bool) {
+    let result = num.rotate_left(rhs);
+    let wrapped = if rhs >= 8 { num != 0 } else { result > (num << rhs) };
+    (result, wrapped)
+}
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    #[kani::proof]
+    fn will_not_panic() {
+        rotate_left(kani::any(), kani::any());
+    }
+}

tests/cargo-ui/ws-integ-tests/in_src_harness/tests/check_result.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use in_src_harness::*;
+
+#[test]
+fn test_no_overflow() {
+    assert_eq!(rotate_left(0x0, 0), (0x0, false));
+    assert_eq!(rotate_left(0x0, 100), (0x0, false));
+    assert_eq!(rotate_left(0xF, 0), (0xF, false));
+    assert_eq!(rotate_left(0x1, 7), (0x80, false));
+}

tests/cargo-ui/ws-integ-tests/integ_harness/Cargo.toml

@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "integ_harness"
+version = "0.1.0"
+edition = "2021"
+description = "Package with a harness that is co-located with integration tests"
+
+[dependencies]

tests/cargo-ui/ws-integ-tests/integ_harness/src/lib.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Dummy harness and library that check left rotation.
+
+/// Return the right rotation of the give number and whether the result has wrapped bits.
+pub fn rotate_right(num: u8, rhs: u32) -> (u8, bool) {
+    let result = num.rotate_right(rhs);
+    let wrapped = if rhs >= 8 { num != 0 } else { result < (num >> rhs) };
+    (result, wrapped)
+}

tests/cargo-ui/ws-integ-tests/integ_harness/tests/check_result.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use integ_harness::*;
+
+#[test]
+fn test_no_overflow() {
+    assert_eq!(rotate_right(0x0, 0), (0x0, false));
+    assert_eq!(rotate_right(0x0, 100), (0x0, false));
+    assert_eq!(rotate_right(0xF, 0), (0xF, false));
+    assert_eq!(rotate_right(0x80, 7), (0x1, false));
+}
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    #[kani::proof]
+    fn no_panic() {
+        rotate_right(kani::any(), kani::any());
+    }
+}