Lazily evaluate debug info (#4269)

Internally, Kani uses the `call_with_panic_debug_info()` function to
call closures with a string that explains what they're trying to do,
allowing better error messages if they internally panics. However, this
function is currently called for every harness we codegen and has to
pretty format the harness' function instance--something that calls into
rustc internals and takes a non-negligible amount of time.

We should instead accept a closure that can generate debug info, but
only when (and if) it's needed.

### Results
Based on initial flamegraphing, the formatting passed to
`call_with_panic_debug_info()` went from taking 2.3% of codegen on
`s2n-codec` to not being called a single time (since there are no
compiler errors in a typical execution).

This change made a solid **4.6% reduction in the end to end compile time
of the standard library** (at std commit
[177d0fd](model-checking/verify-rust-std@177d0fd);
assuming #4257, #4259 & #4268 are already merged into Kani).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: AlexanderPortland

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -151,14 +151,14 @@ impl GotocCodegenBackend {
                         MonoItem::Fn(instance) => {
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.declare_function(instance),
-                                format!("declare_function: {}", instance.name()),
+                                move || format!("declare_function: {}", instance.name()),
                                 instance.def,
                             );
                         }
                         MonoItem::Static(def) => {
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.declare_static(def),
-                                format!("declare_static: {}", def.name()),
+                                move || format!("declare_static: {}", def.name()),
                                 def,
                             );
                         }
@@ -172,18 +172,20 @@ impl GotocCodegenBackend {
                         MonoItem::Fn(instance) => {
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.codegen_function(instance),
-                                format!(
-                                    "codegen_function: {}\n{}",
-                                    instance.name(),
-                                    instance.mangled_name()
-                                ),
+                                move || {
+                                    format!(
+                                        "codegen_function: {}\n{}",
+                                        instance.name(),
+                                        instance.mangled_name()
+                                    )
+                                },
                                 instance.def,
                             );
                         }
                         MonoItem::Static(def) => {
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.codegen_static(def),
-                                format!("codegen_static: {}", def.name()),
+                                move || format!("codegen_static: {}", def.name()),
                                 def,
                             );
                         }

kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs

@@ -16,7 +16,8 @@ use tracing::debug;
 // Use a thread-local global variable to track the current codegen item for debugging.
 // If Kani panics during codegen, we can grab this item to include the problematic
 // codegen item in the panic trace.
-thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option<String>, Option<Location>)> = const { RefCell::new((None, None)) });
+type FindCurrentItemFn = Box<dyn Fn() -> String>;
+thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option<FindCurrentItemFn>, Option<Location>)> = const { RefCell::new((None, None)) });
 
 pub fn init() {
     // Install panic hook
@@ -36,9 +37,9 @@ static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicHookInfo<'_>) + Sync + Sen
 
             // Print the current function if available
             CURRENT_CODEGEN_ITEM.with(|cell| {
-                let t = cell.borrow().clone();
-                if let Some(current_item) = t.0 {
-                    eprintln!("[Kani] current codegen item: {current_item}");
+                let t = cell.borrow();
+                if let Some(get_current_item) = &t.0 {
+                    eprintln!("[Kani] current codegen item: {}", get_current_item());
                 } else {
                     eprintln!("[Kani] no current codegen item.");
                 }
@@ -55,14 +56,21 @@ static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicHookInfo<'_>) + Sync + Sen
 impl<'tcx> GotocCtx<'tcx> {
     // Calls the closure while updating the tracked global variable marking the
     // codegen item for panic debugging.
-    pub fn call_with_panic_debug_info<D: CrateDef, F: FnOnce(&mut GotocCtx<'tcx>)>(
+    pub fn call_with_panic_debug_info<
+        D: CrateDef,
+        F: FnOnce(&mut GotocCtx<'tcx>),
+        S: Fn() -> String + 'static,
+    >(
         &mut self,
         call: F,
-        panic_debug: String,
+        debug_str_generator: S,
         def: D,
     ) {
         CURRENT_CODEGEN_ITEM.with(|odb_cell| {
-            odb_cell.replace((Some(panic_debug), Some(self.codegen_span_stable(def.span()))));
+            odb_cell.replace((
+                Some(Box::new(debug_str_generator)),
+                Some(self.codegen_span_stable(def.span())),
+            ));
             call(self);
             odb_cell.replace((None, None));
         });