Add logger to kani-driver (rust-lang#1900)

Author: celinval

Cargo.lock

@@ -467,6 +467,7 @@ name = "kani-driver"
 version = "0.14.1"
 dependencies = [
  "anyhow",
+ "atty",
  "cargo_metadata",
  "clap 2.34.0",
  "comfy-table",
@@ -482,6 +483,9 @@ dependencies = [
  "serde_json",
  "structopt",
  "toml",
+ "tracing",
+ "tracing-subscriber",
+ "tracing-tree",
 ]
 
 [[package]]

docs/src/cheat-sheets.md

@@ -59,6 +59,13 @@ These can help understand what Kani is generating or encountering on an example
 # Enable `debug!` macro logging output when running Kani:
 kani --debug file.rs
 ```
+
+```bash
+# Use KANI_LOG for a finer grain control of the source and verbosity of logs.
+# E.g.: The command below will print all logs from the kani_middle module.
+KANI_LOG="kani_compiler::kani_middle=trace" kani file.rs
+```
+
 ```bash
 # Keep CBMC Symbol Table and Goto-C output (.json and .goto)
 kani --keep-temps file.rs

kani-driver/Cargo.toml

@@ -19,6 +19,7 @@ unsound_experiments = []
 kani_metadata = { path = "../kani_metadata" }
 cargo_metadata = "0.15.0"
 anyhow = "1"
+atty = "0.2.14"
 console = "0.15.1"
 once_cell = "1.13.0"
 serde = { version = "1", features = ["derive"] }
@@ -32,6 +33,9 @@ rustc-demangle = "0.1.21"
 pathdiff = "0.2.1"
 rayon = "1.5.3"
 comfy-table = "6.0.0"
+tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
+tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
+tracing-tree = "0.2.2"
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml

kani-driver/src/call_cargo.rs

@@ -9,6 +9,7 @@ use std::ffi::OsString;
 use std::fs;
 use std::path::{Path, PathBuf};
 use std::process::Command;
+use tracing::{debug, trace};
 
 /// The outputs of kani-compiler being invoked via cargo on a project.
 pub struct CargoOutputs {
@@ -87,6 +88,7 @@ impl KaniSession {
         kani_args.extend_from_slice(&rustc_args);
 
         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");
@@ -138,7 +140,8 @@ fn glob(path: &Path) -> Result<Vec<PathBuf>> {
 ///   - This is because `default_members` is not available in cargo metadata.
 ///     See <https://github.com/rust-lang/cargo/issues/8033>.
 fn packages_to_verify<'a, 'b>(args: &'a KaniArgs, metadata: &'b Metadata) -> Vec<&'b Package> {
-    if !args.package.is_empty() {
+    debug!(package_selection=?args.package, workspace=args.workspace, "packages_to_verify args");
+    let packages = if !args.package.is_empty() {
         args.package
             .iter()
             .map(|pkg_name| {
@@ -154,7 +157,9 @@ fn packages_to_verify<'a, 'b>(args: &'a KaniArgs, metadata: &'b Metadata) -> Vec
             (true, _) | (_, None) => metadata.workspace_packages(),
             (_, Some(root_pkg)) => vec![root_pkg],
         }
-    }
+    };
+    trace!(?packages, "packages_to_verify result");
+    packages
 }
 
 /// Possible verification targets.
@@ -182,6 +187,7 @@ fn package_targets(args: &KaniArgs, package: &Package) -> Vec<VerificationTarget
         .targets
         .iter()
         .filter_map(|target| {
+            debug!(name=?package.name, target=?target.name, kind=?target.kind, "package_targets");
             if target.kind.contains(&String::from("bin")) {
                 Some(VerificationTarget::Bin(target.name.clone()))
             } else if target.kind.contains(&String::from("lib")) {

kani-driver/src/session.rs

@@ -8,6 +8,15 @@ use std::io::Write;
 use std::path::{Path, PathBuf};
 use std::process::{Child, Command, ExitStatus, Stdio};
 use std::sync::Mutex;
+use tracing::level_filters::LevelFilter;
+use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry};
+use tracing_tree::HierarchicalLayer;
+
+/// Environment variable used to control this session log tracing.
+/// This is the same variable used to control `kani-compiler` logs. Note that you can still control
+/// the driver logs separately, by using the logger directives to  select the kani-driver crate.
+/// `export KANI_LOG=kani_driver=debug`.
+const LOG_ENV_VAR: &str = "KANI_LOG";
 
 /// Contains information about the execution environment and arguments that affect operations
 pub struct KaniSession {
@@ -42,6 +51,7 @@ enum InstallType {
 
 impl KaniSession {
     pub fn new(args: KaniArgs) -> Result<Self> {
+        init_logger(&args);
         let install = InstallType::new()?;
 
         Ok(KaniSession {
@@ -260,3 +270,23 @@ fn expect_path(path: PathBuf) -> Result<PathBuf> {
         );
     }
 }
+
+/// Initialize the logger using the KANI_LOG environment variable and `--debug` argument.
+fn init_logger(args: &KaniArgs) {
+    let filter = EnvFilter::from_env(LOG_ENV_VAR);
+    let filter = if args.debug { filter.add_directive(LevelFilter::DEBUG.into()) } else { filter };
+
+    // Use a hierarchical view for now.
+    let use_colors = atty::is(atty::Stream::Stdout);
+    let subscriber = Registry::default().with(filter);
+    let subscriber = subscriber.with(
+        HierarchicalLayer::default()
+            .with_writer(std::io::stderr)
+            .with_indent_lines(true)
+            .with_ansi(use_colors)
+            .with_targets(true)
+            .with_verbose_exit(true)
+            .with_indent_amount(4),
+    );
+    tracing::subscriber::set_global_default(subscriber).unwrap();
+}