Fix cargo kani --debug and remove debug logs from --verbose (rust-lang#1730)

- Fix rust-lang#1348: Fix `cargo kani --debug` by redirecting kani-compiler
  logs to the STDERR so it doesn't conflict with cargo's output
  expectations.
- Fix rust-lang#1631: Remove `kani-compiler` logs from the output of `--verbose`.

Author: celinval

kani-compiler/src/session.rs

@@ -81,7 +81,7 @@ fn hier_logs(args: &ArgMatches, filter: EnvFilter) {
     let subscriber = Registry::default().with(filter);
     let subscriber = subscriber.with(
         HierarchicalLayer::default()
-            .with_writer(std::io::stdout)
+            .with_writer(std::io::stderr)
             .with_indent_lines(true)
             .with_ansi(use_colors)
             .with_targets(true)

kani-driver/src/args.rs

@@ -69,7 +69,7 @@ pub struct KaniArgs {
     #[structopt(long, short)]
     pub quiet: bool,
     /// Output processing stages and commands, along with minor debug information
-    #[structopt(long, short)]
+    #[structopt(long, short, default_value_if("debug", None, "true"), min_values(0))]
     pub verbose: bool,
     /// Enable usage of unstable options
     #[structopt(long, hidden_short_help(true))]

kani-driver/src/call_single_file.rs

@@ -107,8 +107,6 @@ impl KaniSession {
 
         if self.args.debug {
             flags.push("--log-level=debug".into());
-        } else if self.args.verbose {
-            flags.push("--log-level=info".into());
         } else {
             flags.push("--log-level=warn".into());
         }

tests/cargo-ui/debug/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "debug"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
+[package.metadata.kani.flags]
+debug=true

tests/cargo-ui/debug/expected

@@ -0,0 +1,3 @@
+DEBUG kani_compiler
+goto-cc
+cbmc

tests/cargo-ui/debug/src/lib.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! This is just to test that cargo kani --debug works.
+
+#[cfg(kani)]
+mod harnesses {
+    #[kani::proof]
+    fn harness() {}
+}

tests/cargo-ui/verbose/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "verbose"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
+[package.metadata.kani.flags]
+verbose=true

tests/cargo-ui/verbose/expected

@@ -0,0 +1,2 @@
+goto-cc
+cbmc

tests/cargo-ui/verbose/src/lib.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! This is just to test that cargo kani --verbose works.
+
+#[cfg(kani)]
+mod harnesses {
+    #[kani::proof]
+    fn harness() {}
+}