Expand supported crate-type check (rust-lang#1912)

This change add support to rlib libraries and add proper error handling for crate types that aren't supported. We also no longer crash if there was no supported target found.

Author: celinval

kani-driver/src/call_cargo.rs

@@ -3,14 +3,24 @@
 
 use crate::args::KaniArgs;
 use crate::session::{KaniSession, ReachabilityMode};
-use anyhow::{Context, Result};
+use anyhow::{bail, Context, Result};
 use cargo_metadata::{Metadata, MetadataCommand, Package};
 use std::ffi::OsString;
 use std::fs;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 use tracing::{debug, trace};
 
+//---- Crate types identifier used by cargo.
+const CRATE_TYPE_BIN: &str = "bin";
+const CRATE_TYPE_CDYLIB: &str = "cdylib";
+const CRATE_TYPE_DYLIB: &str = "dylib";
+const CRATE_TYPE_LIB: &str = "lib";
+const CRATE_TYPE_PROC_MACRO: &str = "proc-macro";
+const CRATE_TYPE_RLIB: &str = "rlib";
+const CRATE_TYPE_STATICLIB: &str = "staticlib";
+const CRATE_TYPE_TEST: &str = "test";
+
 /// The outputs of kani-compiler being invoked via cargo on a project.
 pub struct CargoOutputs {
     /// The directory where compiler outputs should be directed.
@@ -90,8 +100,8 @@ impl KaniSession {
         // Only joing them at the end. All kani flags must come first.
         kani_args.extend_from_slice(&rustc_args);
 
+        let mut found_target = false;
         let packages = packages_to_verify(&self.args, &metadata);
-        if packages.is_empty() {}
         for package in packages {
             for target in package_targets(&self.args, package) {
                 let mut cmd = Command::new("cargo");
@@ -104,9 +114,13 @@ impl KaniSession {
                     .env("KANIFLAGS", &crate::util::join_osstring(&kani_args, " "));
 
                 self.run_terminal(cmd)?;
+                found_target = true;
             }
         }
 
+        if !found_target {
+            bail!("No supported targets were found.");
+        }
         if self.args.dry_run {
             // mock an answer: mostly the same except we don't/can't expand the globs
             return Ok(CargoOutputs {
@@ -184,22 +198,81 @@ impl VerificationTarget {
 }
 
 /// Extract the targets inside a package.
+///
 /// If `--tests` is given, the list of targets will include any integration tests.
+///
+/// We use the `target.kind` as documented here. Note that `kind` for library will
+/// match the `crate-type`, despite them not being explicitly listed in the documentation:
+/// <https://docs.rs/cargo_metadata/0.15.0/cargo_metadata/struct.Target.html#structfield.kind>
+///
+/// The documentation for `crate-type` explicitly states that the only time `kind` and
+/// `crate-type` differs is for examples.
+/// <https://docs.rs/cargo_metadata/0.15.0/cargo_metadata/struct.Target.html#structfield.crate_types>
 fn package_targets(args: &KaniArgs, package: &Package) -> Vec<VerificationTarget> {
-    package
+    let mut ignored_tests = vec![];
+    let mut ignored_unsupported = vec![];
+    let verification_targets = package
         .targets
         .iter()
         .filter_map(|target| {
-            debug!(name=?package.name, target=?target.name, kind=?target.kind, "package_targets");
-            if target.kind.contains(&String::from("bin")) {
+            debug!(name=?package.name, target=?target.name, kind=?target.kind, crate_type=?target
+                .crate_types,
+                "package_targets");
+            if target.kind.contains(&String::from(CRATE_TYPE_BIN)) {
+                // Binary targets.
                 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 if target.kind.contains(&String::from(CRATE_TYPE_LIB))
+                || target.kind.contains(&String::from(CRATE_TYPE_RLIB))
+            {
+                // Lib targets.
+                let unsupported_types = target
+                    .kind
+                    .iter()
+                    .filter_map(|kind| {
+                        let kind_str = kind.as_str();
+                        matches!(kind_str,
+                            CRATE_TYPE_CDYLIB | CRATE_TYPE_DYLIB | CRATE_TYPE_STATICLIB |
+                            CRATE_TYPE_PROC_MACRO
+                        ).then_some(kind_str)
+                    })
+                    .collect::<Vec<_>>();
+                if unsupported_types.is_empty() {
+                    Some(VerificationTarget::Lib)
+                } else {
+                    println!(
+                        "warning: Skipped verification of `{}` due to unsupported crate-type: `{}`.",
+                        target.name,
+                        unsupported_types.join("`, `")
+                    );
+                    None
+                }
+            } else if target.kind.contains(&String::from(CRATE_TYPE_TEST)) {
+                // Test target.
+                if args.tests {
+                    Some(VerificationTarget::Test(target.name.clone()))
+                } else {
+                    ignored_tests.push(target.name.as_str());
+                    None
+                }
             } else {
+                ignored_unsupported.push(target.name.as_str());
                 None
             }
         })
-        .collect()
+        .collect();
+
+    if args.verbose {
+        // Print targets that were skipped only on verbose mode.
+        if !ignored_tests.is_empty() {
+            println!("Skipped the following test targets: '{}'.", ignored_tests.join("', '"));
+            println!("    -> Use '--tests' to verify harnesses inside a 'test' crate.");
+        }
+        if !ignored_unsupported.is_empty() {
+            println!(
+                "Skipped the following unsupported targets: '{}'.",
+                ignored_unsupported.join("', '")
+            );
+        }
+    }
+    verification_targets
 }

tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "supported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle supported crate types"
+
+[lib]
+name = "lib"
+crate-type = ["lib", "rlib"]
+path = "../src/lib.rs"

tests/cargo-ui/supported-lib-types/lib-rlib/expected

@@ -0,0 +1,2 @@
+Checking harness check_ok...
+VERIFICATION:- SUCCESSFUL

tests/cargo-ui/supported-lib-types/lib/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "supported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle supported crate types"
+
+[lib]
+name = "lib"
+crate-type = ["lib"]
+path = "../src/lib.rs"

tests/cargo-ui/supported-lib-types/lib/expected

@@ -0,0 +1,2 @@
+Checking harness check_ok...
+VERIFICATION:- SUCCESSFUL

tests/cargo-ui/supported-lib-types/rlib/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "supported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle supported crate types"
+
+[lib]
+name = "lib"
+crate-type = ["rlib"]
+path = "../src/lib.rs"

tests/cargo-ui/supported-lib-types/rlib/expected

@@ -0,0 +1,2 @@
+Checking harness check_ok...
+VERIFICATION:- SUCCESSFUL

tests/cargo-ui/supported-lib-types/src/lib.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// The harness bellow will always succeed. We just want to make sure they are correctly executed.
+
+#[kani::proof]
+fn check_ok() {
+    let b = kani::any();
+    match b {
+        true => assert_eq!(b as u8, 1),
+        false => assert_eq!(b as u8, 0),
+    }
+}

tests/cargo-ui/unsupported-lib-types/cdylib/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "unsupported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle unsupported crate-types"
+
+[lib]
+name = "lib"
+crate-type = ["cdylib"]
+path = "../src/lib.rs"
+
+[package.metadata.kani.flags]
+verbose = true

tests/cargo-ui/unsupported-lib-types/cdylib/expected

@@ -0,0 +1,2 @@
+Skipped the following unsupported targets: 'lib'.
+Error: No supported targets were found.

tests/cargo-ui/unsupported-lib-types/dylib/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "unsupported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle unsupported crate-types"
+
+[lib]
+name = "lib"
+crate-type = ["dylib"]
+path = "../src/lib.rs"
+
+[package.metadata.kani.flags]
+verbose = true

tests/cargo-ui/unsupported-lib-types/dylib/expected

@@ -0,0 +1,2 @@
+Skipped the following unsupported targets: 'lib'.
+Error: No supported targets were found.

tests/cargo-ui/unsupported-lib-types/proc-macro/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "unsupported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle unsupported crate-types"
+
+[lib]
+name = "lib"
+proc-macro = true
+path = "../src/lib.rs"
+
+[package.metadata.kani.flags]
+verbose = true

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

@@ -0,0 +1,2 @@
+Skipped the following unsupported targets: 'lib'.
+Error: No supported targets were found.

tests/cargo-ui/unsupported-lib-types/rlib-cdylib/Cargo.toml

@@ -0,0 +1,14 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "unsupported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle unsupported crate-types"
+
+[lib]
+name = "lib"
+crate-type = ["rlib", "cdylib"]
+path = "../src/lib.rs"
+
+[package.metadata.kani.flags]

tests/cargo-ui/unsupported-lib-types/rlib-cdylib/expected

@@ -0,0 +1,2 @@
+warning: Skipped verification of `lib` due to unsupported crate-type: `cdylib`.
+Error: No supported targets were found.

tests/cargo-ui/unsupported-lib-types/src/lib.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// The harness bellow will be ignored since they are inside an unsupported crate type.
+
+fn fatal_error(msg: &str) -> ! {
+    panic!("[Error]: {}", msg)
+}
+
+#[kani::proof]
+fn check_error() {
+    fatal_error("Oops");
+}

tests/cargo-ui/unsupported-lib-types/staticlib/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "unsupported-lib"
+version = "0.1.0"
+edition = "2021"
+description = "Test that Kani correctly handle unsupported crate-types"
+
+[lib]
+name = "lib"
+crate-type = ["staticlib"]
+path = "../src/lib.rs"
+
+[package.metadata.kani.flags]
+verbose = true

tests/cargo-ui/unsupported-lib-types/staticlib/expected

@@ -0,0 +1,2 @@
+Skipped the following unsupported targets: 'lib'.
+Error: No supported targets were found.