Add some performance instrumentation to our code

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -17,7 +17,7 @@ use rustc_middle::ty::{self, Instance};
 use std::collections::BTreeMap;
 use std::convert::TryInto;
 use std::iter::FromIterator;
-use tracing::{debug, info_span};
+use tracing::{debug, debug_span};
 
 /// Codegen MIR functions into gotoc
 impl<'tcx> GotocCtx<'tcx> {
@@ -72,9 +72,9 @@ impl<'tcx> GotocCtx<'tcx> {
         let old_sym = self.symbol_table.lookup(&name).unwrap();
 
         let _trace_span =
-            info_span!("CodegenFunction", name = self.current_fn().readable_name()).entered();
+            debug_span!("CodegenFunction", name = self.current_fn().readable_name()).entered();
         if old_sym.is_function_definition() {
-            tracing::info!("Double codegen of {:?}", old_sym);
+            debug!("Double codegen of {:?}", old_sym);
         } else {
             assert!(old_sym.is_function());
             let mir = self.current_fn().mir();

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -41,7 +41,8 @@ use std::iter::FromIterator;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 use std::rc::Rc;
-use tracing::{debug, error, warn};
+use std::time::Instant;
+use tracing::{debug, error, info, warn};
 
 #[derive(Clone)]
 pub struct GotocCodegenBackend {
@@ -82,58 +83,66 @@ impl CodegenBackend for GotocCodegenBackend {
         check_options(tcx.sess, need_metadata_module);
         check_crate_items(&gcx);
 
-        let items = collect_codegen_items(&gcx);
+        let items = with_timer(|| collect_codegen_items(&gcx), "codegen reachability analysis");
         if items.is_empty() {
             // There's nothing to do.
             return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model());
         }
         dump_mir_items(tcx, &items);
 
-        // we first declare all items
-        for item in &items {
-            match *item {
-                MonoItem::Fn(instance) => {
-                    gcx.call_with_panic_debug_info(
-                        |ctx| ctx.declare_function(instance),
-                        format!("declare_function: {}", gcx.readable_instance_name(instance)),
-                        instance.def_id(),
-                    );
+        with_timer(
+            || {
+                // we first declare all items
+                for item in &items {
+                    match *item {
+                        MonoItem::Fn(instance) => {
+                            gcx.call_with_panic_debug_info(
+                                |ctx| ctx.declare_function(instance),
+                                format!(
+                                    "declare_function: {}",
+                                    gcx.readable_instance_name(instance)
+                                ),
+                                instance.def_id(),
+                            );
+                        }
+                        MonoItem::Static(def_id) => {
+                            gcx.call_with_panic_debug_info(
+                                |ctx| ctx.declare_static(def_id, *item),
+                                format!("declare_static: {def_id:?}"),
+                                def_id,
+                            );
+                        }
+                        MonoItem::GlobalAsm(_) => {} // Ignore this. We have already warned about it.
+                    }
                 }
-                MonoItem::Static(def_id) => {
-                    gcx.call_with_panic_debug_info(
-                        |ctx| ctx.declare_static(def_id, *item),
-                        format!("declare_static: {def_id:?}"),
-                        def_id,
-                    );
-                }
-                MonoItem::GlobalAsm(_) => {} // Ignore this. We have already warned about it.
-            }
-        }
 
-        // then we move on to codegen
-        for item in items {
-            match item {
-                MonoItem::Fn(instance) => {
-                    gcx.call_with_panic_debug_info(
-                        |ctx| ctx.codegen_function(instance),
-                        format!(
-                            "codegen_function: {}\n{}",
-                            gcx.readable_instance_name(instance),
-                            gcx.symbol_name(instance)
-                        ),
-                        instance.def_id(),
-                    );
+                // then we move on to codegen
+                for item in items {
+                    match item {
+                        MonoItem::Fn(instance) => {
+                            gcx.call_with_panic_debug_info(
+                                |ctx| ctx.codegen_function(instance),
+                                format!(
+                                    "codegen_function: {}\n{}",
+                                    gcx.readable_instance_name(instance),
+                                    gcx.symbol_name(instance)
+                                ),
+                                instance.def_id(),
+                            );
+                        }
+                        MonoItem::Static(def_id) => {
+                            gcx.call_with_panic_debug_info(
+                                |ctx| ctx.codegen_static(def_id, item),
+                                format!("codegen_static: {def_id:?}"),
+                                def_id,
+                            );
+                        }
+                        MonoItem::GlobalAsm(_) => {} // We have already warned above
+                    }
                 }
-                MonoItem::Static(def_id) => {
-                    gcx.call_with_panic_debug_info(
-                        |ctx| ctx.codegen_static(def_id, item),
-                        format!("codegen_static: {def_id:?}"),
-                        def_id,
-                    );
-                }
-                MonoItem::GlobalAsm(_) => {} // We have already warned above
-            }
-        }
+            },
+            "codegen",
+        );
 
         // Print compilation report.
         print_report(&gcx, tcx);
@@ -401,11 +410,15 @@ fn symbol_table_to_gotoc(tcx: &TyCtxt, file: &Path) -> PathBuf {
     // TODO get symtab2gb path from self
     let mut cmd = Command::new("symtab2gb");
     cmd.args(args);
-    debug!("calling: `{:?} {:?}`", cmd.get_program(), cmd.get_args());
+    info!("[Kani] Running: `{:?} {:?}`", cmd.get_program(), cmd.get_args());
 
-    let result = cmd
-        .output()
-        .expect(&format!("Failed to generate goto model for {}", input_filename.display()));
+    let result = with_timer(
+        || {
+            cmd.output()
+                .expect(&format!("Failed to generate goto model for {}", input_filename.display()))
+        },
+        "symtab2gb",
+    );
     if !result.status.success() {
         error!("Symtab error output:\n{}", String::from_utf8_lossy(&result.stderr));
         error!("Symtab output:\n{}", String::from_utf8_lossy(&result.stdout));
@@ -490,3 +503,16 @@ where
         serde_json::to_writer(writer, &source).unwrap();
     }
 }
+
+/// Execute the provided function and measure the clock time it took for its execution.
+/// Log the time with the given description.
+pub fn with_timer<T, F>(func: F, description: &str) -> T
+where
+    F: FnOnce() -> T,
+{
+    let start = Instant::now();
+    let ret = func();
+    let elapsed = start.elapsed();
+    info!("Finished {description} in {}s", elapsed.as_secs_f32());
+    ret
+}

kani-driver/src/call_single_file.rs

@@ -117,6 +117,9 @@ impl KaniSession {
 
         if self.args.debug {
             flags.push("--log-level=debug".into());
+        } else if self.args.verbose {
+            // Print the symtab command being invoked.
+            flags.push("--log-level=info".into());
         } else {
             flags.push("--log-level=warn".into());
         }

kani-driver/src/harness_runner.rs

@@ -100,7 +100,7 @@ impl KaniSession {
             // Strictly speaking, we're faking success here. This is more "no error"
             Ok(VerificationResult::mock_success())
         } else {
-            let result = self.run_cbmc(binary, harness)?;
+            let result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cmbc")?;
 
             // When quiet, we don't want to print anything at all.
             // When output is old, we also don't have real results to print.

kani-driver/src/session.rs

@@ -8,10 +8,10 @@ use std::io::Write;
 use std::path::{Path, PathBuf};
 use std::process::{Child, Command, ExitStatus, Stdio};
 use std::sync::Mutex;
+use std::time::Instant;
 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.
@@ -129,9 +129,14 @@ impl KaniSession {
         if self.args.verbose {
             println!("[Kani] Running: `{}`", render_command(&cmd).to_string_lossy());
         }
-        let result = cmd
-            .status()
-            .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))?;
+        let program = cmd.get_program().to_string_lossy().to_string();
+        let result = self.with_timer(
+            || {
+                cmd.status()
+                    .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))
+            },
+            &program,
+        )?;
         if !result.success() {
             bail!("{} exited with status {}", cmd.get_program().to_string_lossy(), result);
         }
@@ -171,7 +176,14 @@ impl KaniSession {
         let output_file = std::fs::File::create(&stdout)?;
         cmd.stdout(output_file);
 
-        cmd.status().context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))
+        let program = cmd.get_program().to_string_lossy().to_string();
+        self.with_timer(
+            || {
+                cmd.status()
+                    .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))
+            },
+            &program,
+        )
     }
 
     /// Run a job and pipe its output to this process.
@@ -191,6 +203,21 @@ impl KaniSession {
 
         Ok(Some(process))
     }
+
+    /// Execute the provided function and measure the clock time it took for its execution.
+    /// Print the time with the given description if we are on verbose or debug mode.
+    pub fn with_timer<T, F>(&self, func: F, description: &str) -> T
+    where
+        F: FnOnce() -> T,
+    {
+        let start = Instant::now();
+        let ret = func();
+        if self.args.verbose || self.args.debug {
+            let elapsed = start.elapsed();
+            println!("Finished {description} in {}s", elapsed.as_secs_f32())
+        }
+        ret
+    }
 }
 
 /// Return the path for the folder where the current executable is located.