From fbf053342eb4fba2f4f68d59eba81346863943c9 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 30 Sep 2022 10:51:42 -0700
Subject: [PATCH] Fix `cargo kani --debug` and remove debug logs from
 `--verbose` (#1730)

- Fix #1348: Fix `cargo kani --debug` by redirecting kani-compiler
  logs to the STDERR so it doesn't conflict with cargo's output
  expectations.
- Fix #1631: Remove `kani-compiler` logs from the output of `--verbose`.
---
 kani-compiler/src/session.rs        |  2 +-
 kani-driver/src/args.rs             |  2 +-
 kani-driver/src/call_single_file.rs |  2 --
 tests/cargo-ui/debug/Cargo.toml     | 11 +++++++++++
 tests/cargo-ui/debug/expected       |  3 +++
 tests/cargo-ui/debug/src/lib.rs     | 10 ++++++++++
 tests/cargo-ui/verbose/Cargo.toml   | 11 +++++++++++
 tests/cargo-ui/verbose/expected     |  2 ++
 tests/cargo-ui/verbose/src/lib.rs   | 10 ++++++++++
 9 files changed, 49 insertions(+), 4 deletions(-)
 create mode 100644 tests/cargo-ui/debug/Cargo.toml
 create mode 100644 tests/cargo-ui/debug/expected
 create mode 100644 tests/cargo-ui/debug/src/lib.rs
 create mode 100644 tests/cargo-ui/verbose/Cargo.toml
 create mode 100644 tests/cargo-ui/verbose/expected
 create mode 100644 tests/cargo-ui/verbose/src/lib.rs

diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs
index bd797b9a278f..288fc66784ab 100644
--- a/kani-compiler/src/session.rs
+++ b/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)
diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
index 6a102195bea0..60046e3ecbe5 100644
--- a/kani-driver/src/args.rs
+++ b/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))]
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index 2a99b6ba8fb5..debaadc96940 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/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());
         }
diff --git a/tests/cargo-ui/debug/Cargo.toml b/tests/cargo-ui/debug/Cargo.toml
new file mode 100644
index 000000000000..d905b3c5fcbb
--- /dev/null
+++ b/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
diff --git a/tests/cargo-ui/debug/expected b/tests/cargo-ui/debug/expected
new file mode 100644
index 000000000000..954eb4a0e0a4
--- /dev/null
+++ b/tests/cargo-ui/debug/expected
@@ -0,0 +1,3 @@
+DEBUG kani_compiler
+goto-cc
+cbmc
diff --git a/tests/cargo-ui/debug/src/lib.rs b/tests/cargo-ui/debug/src/lib.rs
new file mode 100644
index 000000000000..55c48d61caeb
--- /dev/null
+++ b/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() {}
+}
diff --git a/tests/cargo-ui/verbose/Cargo.toml b/tests/cargo-ui/verbose/Cargo.toml
new file mode 100644
index 000000000000..4b05e4a6fb45
--- /dev/null
+++ b/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
diff --git a/tests/cargo-ui/verbose/expected b/tests/cargo-ui/verbose/expected
new file mode 100644
index 000000000000..3455ac3ec3d7
--- /dev/null
+++ b/tests/cargo-ui/verbose/expected
@@ -0,0 +1,2 @@
+goto-cc
+cbmc
diff --git a/tests/cargo-ui/verbose/src/lib.rs b/tests/cargo-ui/verbose/src/lib.rs
new file mode 100644
index 000000000000..1482dd1cf322
--- /dev/null
+++ b/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() {}
+}