Dump the reachable MIR (rust-lang#1750)

* Enable option to dump MIR after reachability analysis

For now, we just tag along the `--emit mir` option that can be provided
to rustc. We use the extension `.kani.mir` to avoid conflict with the
one generated from rustc.

Author: celinval

docs/src/cheat-sheets.md

@@ -68,6 +68,12 @@ kani --keep-temps file.rs
 kani --gen-c file.rs
 ```
 
+```bash
+# Generate a ${INPUT}.kani.mir file with a human friendly MIR dump
+# for all items that are compiled to the respective goto-program.
+RUSTFLAGS="--emit mir" kani ${INPUT}.rs
+```
+
 ## CBMC
 
 ```bash

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -18,16 +18,20 @@ use rustc_hir::def::DefKind;
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::mir::mono::{CodegenUnit, MonoItem};
+use rustc_middle::mir::write_mir_pretty;
 use rustc_middle::ty::query::Providers;
-use rustc_middle::ty::{self, TyCtxt};
+use rustc_middle::ty::{self, InstanceDef, TyCtxt};
 use rustc_session::config::{OutputFilenames, OutputType};
 use rustc_session::cstore::MetadataLoaderDyn;
 use rustc_session::Session;
+use rustc_span::def_id::DefId;
 use rustc_target::abi::Endian;
 use rustc_target::spec::PanicStrategy;
 use std::collections::BTreeMap;
 use std::fmt::Write;
+use std::fs::File;
 use std::io::BufWriter;
+use std::io::Write as IoWrite;
 use std::iter::FromIterator;
 use std::path::Path;
 use std::process::Command;
@@ -74,6 +78,7 @@ impl CodegenBackend for GotocCodegenBackend {
             // 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 {
@@ -299,7 +304,7 @@ where
 {
     let filename = base_filename.with_extension(extension);
     debug!("output to {:?}", filename);
-    let out_file = ::std::fs::File::create(&filename).unwrap();
+    let out_file = File::create(&filename).unwrap();
     let writer = BufWriter::new(out_file);
     if pretty {
         serde_json::to_writer_pretty(writer, &source).unwrap();
@@ -357,7 +362,6 @@ fn codegen_results(
 ///
 /// To be implemented:
 /// - PubFns: Cross-crate reachability analysis that use the local public fns as starting point.
-
 fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
     let tcx = gcx.tcx;
     let reach = gcx.queries.get_reachability_analysis();
@@ -419,3 +423,39 @@ fn symbol_table_to_gotoc(tcx: &TyCtxt, file: &Path) {
         tcx.sess.abort_if_errors();
     }
 }
+
+/// Print MIR for the reachable items if the `--emit mir` option was provided to rustc.
+fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem]) {
+    /// Convert MonoItem into a DefId.
+    /// Skip stuff that we cannot generate the MIR items.
+    fn visible_item<'tcx>(item: &MonoItem<'tcx>) -> Option<(MonoItem<'tcx>, DefId)> {
+        match item {
+            // Exclude FnShims and others that cannot be dumped.
+            MonoItem::Fn(instance)
+                if matches!(
+                    instance.def,
+                    InstanceDef::FnPtrShim(..) | InstanceDef::ClosureOnceShim { .. }
+                ) =>
+            {
+                None
+            }
+            MonoItem::Fn(instance) => Some((*item, instance.def_id())),
+            MonoItem::Static(def_id) => Some((*item, *def_id)),
+            MonoItem::GlobalAsm(_) => None,
+        }
+    }
+
+    if tcx.sess.opts.output_types.contains_key(&OutputType::Mir) {
+        // Create output buffer.
+        let outputs = tcx.output_filenames(());
+        let path = outputs.output_path(OutputType::Mir).with_extension("kani.mir");
+        let out_file = File::create(&path).unwrap();
+        let mut writer = BufWriter::new(out_file);
+
+        // For each def_id, dump their MIR
+        for (item, def_id) in items.iter().filter_map(visible_item) {
+            writeln!(writer, "// Item: {:?}", item).unwrap();
+            write_mir_pretty(tcx, Some(def_id), &mut writer).unwrap();
+        }
+    }
+}