From 79f86f96969aebbdfe6b773d596b2cf6891c768e Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 30 Jan 2023 13:56:42 -0800
Subject: [PATCH] Support ICE reporting using json diagnostics (#2167)

This will allow us to retrieve crash information from Kani driver once we merge #2166.
---
 kani-compiler/src/main.rs    | 11 +++++++++-
 kani-compiler/src/session.rs | 39 +++++++++++++++++++++++++++++++++---
 2 files changed, 46 insertions(+), 4 deletions(-)

diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index 4207df95ad4a6..76df9c89542de 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -44,6 +44,9 @@ use kani_queries::{QueryDb, ReachabilityType, UserInput};
 use rustc_data_structures::fx::FxHashMap;
 use rustc_driver::{Callbacks, RunCompiler};
 use rustc_hir::definitions::DefPathHash;
+use rustc_interface::Config;
+use rustc_session::config::ErrorOutputType;
+use session::json_panic_hook;
 use std::ffi::OsStr;
 use std::path::PathBuf;
 use std::rc::Rc;
@@ -141,7 +144,13 @@ fn main() -> Result<(), &'static str> {
 struct KaniCallbacks {}
 
 /// Use default function implementations.
-impl Callbacks for KaniCallbacks {}
+impl Callbacks for KaniCallbacks {
+    fn config(&mut self, config: &mut Config) {
+        if matches!(config.opts.error_format, ErrorOutputType::Json { .. }) {
+            json_panic_hook();
+        }
+    }
+}
 
 /// The Kani root folder has all binaries inside bin/ and libraries inside lib/.
 /// This folder can also be used as a rustc sysroot.
diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs
index 460cffe364f4f..6207a528916b1 100644
--- a/kani-compiler/src/session.rs
+++ b/kani-compiler/src/session.rs
@@ -5,6 +5,10 @@
 
 use crate::parser;
 use clap::ArgMatches;
+use rustc_errors::{
+    emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter,
+    ColorConfig, Diagnostic,
+};
 use std::panic;
 use std::str::FromStr;
 use std::sync::LazyLock;
@@ -18,7 +22,7 @@ const LOG_ENV_VAR: &str = "KANI_LOG";
 const BUG_REPORT_URL: &str =
     "https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md";
 
-// Custom panic hook.
+// Custom panic hook when running under user friendly message format.
 #[allow(clippy::type_complexity)]
 static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
     LazyLock::new(|| {
@@ -30,9 +34,33 @@ static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 's
 
             // Print the Kani message
             eprintln!("Kani unexpectedly panicked during compilation.");
-            eprintln!(
-                "If you are seeing this message, please file an issue here: {BUG_REPORT_URL}"
+            eprintln!("Please file an issue here: {BUG_REPORT_URL}");
+        }));
+        hook
+    });
+
+// Custom panic hook when executing under json error format `--error-format=json`.
+#[allow(clippy::type_complexity)]
+static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
+    LazyLock::new(|| {
+        let hook = panic::take_hook();
+        panic::set_hook(Box::new(|info| {
+            // Print stack trace.
+            let msg = format!("Kani unexpectedly panicked at {info}.",);
+            let fallback_bundle =
+                fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false);
+            let mut emitter = JsonEmitter::basic(
+                false,
+                HumanReadableErrorType::Default(ColorConfig::Never),
+                None,
+                fallback_bundle,
+                None,
+                false,
+                false,
             );
+            let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg);
+            emitter.emit_diagnostic(&diagnostic);
+            (*JSON_PANIC_HOOK)(info);
         }));
         hook
     });
@@ -94,3 +122,8 @@ fn init_panic_hook() {
     // Install panic hook
     LazyLock::force(&PANIC_HOOK); // Install ice hook
 }
+
+pub fn json_panic_hook() {
+    // Install panic hook
+    LazyLock::force(&JSON_PANIC_HOOK); // Install ice hook
+}