Added ability to figure out workspaces from cargo kani. (rust-lang#1421)

* Added ability to figure out workspaces from cargo kani.

* Added doc comment.

* Changed code to use `cargo_metadata` crate not raw json.

Author: Yoshiki Takashima

Cargo.lock

@@ -89,6 +89,37 @@ dependencies = [
  "walkdir",
 ]
 
+[[package]]
+name = "camino"
+version = "1.0.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "869119e97797867fd90f5e22af7d0bd274bd4635ebb9eb68c04f3f513ae6c412"
+dependencies = [
+ "serde",
+]
+
+[[package]]
+name = "cargo-platform"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cbdb825da8a5df079a43676dbe042702f1707b1109f713a01420fbb4cc71fa27"
+dependencies = [
+ "serde",
+]
+
+[[package]]
+name = "cargo_metadata"
+version = "0.15.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3abb7553d5b9b8421c6de7cb02606ff15e0c6eea7d8eadd75ef013fd636bec36"
+dependencies = [
+ "camino",
+ "cargo-platform",
+ "semver",
+ "serde",
+ "serde_json",
+]
+
 [[package]]
 name = "cfg-if"
 version = "1.0.0"
@@ -285,6 +316,7 @@ name = "kani-driver"
 version = "0.7.0"
 dependencies = [
  "anyhow",
+ "cargo_metadata",
  "clap",
  "glob",
  "kani_metadata",
@@ -647,6 +679,15 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd"
 
+[[package]]
+name = "semver"
+version = "1.0.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a2333e6df6d6598f2b1974829f853c2b4c5f4a6e503c10af918081aa6f8564e1"
+dependencies = [
+ "serde",
+]
+
 [[package]]
 name = "serde"
 version = "1.0.138"

kani-driver/Cargo.toml

@@ -13,6 +13,7 @@ publish = false
 
 [dependencies]
 kani_metadata = { path = "../kani_metadata" }
+cargo_metadata = "0.15.0"
 anyhow = "1"
 serde = { version = "1", features = ["derive"] }
 serde_json = "1"

kani-driver/src/call_cargo.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::{Context, Result};
+use cargo_metadata::MetadataCommand;
 use std::ffi::OsString;
 use std::path::{Path, PathBuf};
 use std::process::Command;
@@ -21,11 +22,20 @@ pub struct CargoOutputs {
     pub metadata: Vec<PathBuf>,
 }
 
+/// Finds the "target" directory while considering workspaces,
+fn find_target_dir() -> PathBuf {
+    fn maybe_get_target() -> Option<PathBuf> {
+        Some(MetadataCommand::new().exec().ok()?.target_directory.into())
+    }
+
+    maybe_get_target().unwrap_or(PathBuf::from("target"))
+}
+
 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 target_dir = self.args.target_dir.as_ref().unwrap_or(&PathBuf::from("target")).clone();
+        let target_dir = self.args.target_dir.as_ref().unwrap_or(&find_target_dir()).clone();
         let outdir = target_dir.join(build_target).join("debug/deps");
 
         let flag_env = {