From 3224cbd564d2053789971d36253759e4c385f646 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 22 Jun 2023 14:25:51 -0700
Subject: [PATCH] Fix MIR dump to emit one MIR per-harness (#2556)

This was a regression introduced by #2439. We were still writing the result of the reachability algorithm to the same file for every harness. Thus, we could only see the MIR for the last harness that was processed.

Use the file name that is specific for the harness instead and generate one MIR file per harness like we do with other files generated by kani-compiler.
---
 .../src/codegen_cprover_gotoc/compiler_interface.rs        | 2 +-
 kani-compiler/src/kani_middle/mod.rs                       | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 5f0c0c92e5d3..985cbe1efc47 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -86,7 +86,7 @@ impl GotocCodegenBackend {
             || collect_reachable_items(tcx, starting_items),
             "codegen reachability analysis",
         );
-        dump_mir_items(tcx, &items);
+        dump_mir_items(tcx, &items, &symtab_goto.with_extension("kani.mir"));
 
         // Follow rustc naming convention (cx is abbrev for context).
         // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index b0599cc214e6..fc60c0cc1a14 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -4,6 +4,7 @@
 //! and transformations.
 
 use std::collections::HashSet;
+use std::path::Path;
 
 use crate::kani_queries::QueryDb;
 use rustc_hir::{def::DefKind, def_id::DefId, def_id::LOCAL_CRATE};
@@ -79,7 +80,7 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
 }
 
 /// Print MIR for the reachable items if the `--emit mir` option was provided to rustc.
-pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem]) {
+pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
     /// 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)> {
@@ -96,9 +97,7 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem]) {
 
     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 out_file = File::create(output).unwrap();
         let mut writer = BufWriter::new(out_file);
 
         // For each def_id, dump their MIR