Implement -p flag for running kani on specific package (rust-lang#1559)

* Implement -p / --package flag.

* Fixed comments.

* Modified tests to check running 2/3 tests.

1/2 does not show up in a way that we can check!

* Fixed -p to match build: multiple packages allowed.

* Forced one of the active packages to fail, enforce expected

* Changed name of test

Author: YoshikiTakashima

kani-driver/src/args.rs

@@ -121,6 +121,9 @@ pub struct KaniArgs {
     /// Run Kani on all packages in the workspace.
     #[structopt(long)]
     pub workspace: bool,
+    /// Run Kani on the specified packages.
+    #[structopt(long, short)]
+    pub package: Vec<String>,
 
     /// Specify the value used for loop unwinding in CBMC
     #[structopt(long)]

kani-driver/src/call_cargo.rs

@@ -52,6 +52,11 @@ impl KaniSession {
             args.push("build".into());
         }
 
+        for package in self.args.package.iter() {
+            args.push("--package".into());
+            args.push(package.into());
+        }
+
         if self.args.all_features {
             args.push("--all-features".into());
         }

tests/cargo-kani/ws-specified/Cargo.toml

@@ -0,0 +1,17 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "topcrate"
+version = "0.1.0"
+edition = "2021"
+
+[workspace]
+members = [
+  "libcrate",
+  "bincrate",
+  "subcrate3",
+]
+
+[package.metadata.kani.flags]
+package = ["libcrate", "bincrate"]

tests/cargo-kani/ws-specified/bincrate/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "bincrate"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+libcrate = { path = "../libcrate" }

tests/cargo-kani/ws-specified/bincrate/src/main.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! One of 3 sub packages used to test specifying packages with -p
+//! flag.
+
+fn main() {
+    println!("Hello, world!");
+}
+
+#[kani::proof]
+fn check_bincrate_proof() {
+    assert!(1 == 1);
+}

tests/cargo-kani/ws-specified/expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/cargo-kani/ws-specified/libcrate/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "libcrate"
+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/ws-specified/libcrate/src/lib.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! One of 3 sub packages used to test specifying packages with -p
+//! flag.
+
+#[kani::proof]
+fn check_libcrate_proof() {
+    assert!(1 == 2);
+}

tests/cargo-kani/ws-specified/src/lib.rs

@@ -0,0 +1,4 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! empty lib for toplevel directory

tests/cargo-kani/ws-specified/subcrate3/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "subcrate3"
+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/ws-specified/subcrate3/src/lib.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! One of 3 sub packages used to test specifying packages with -p
+//! flag.
+
+#[kani::proof]
+fn check_subcrate3_proof() {
+    assert!(1 == 1);
+}