Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix MIR dump to emit one MIR per-harness #2556

Merged
merged 1 commit into from
Jun 22, 2023
Merged

Fix MIR dump to emit one MIR per-harness #2556

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Fix MIR dump to emit one MIR per-harness
  • Loading branch information
@celinval
celinval committed Jun 22, 2023
commit 22777ad867e29a121930e1ff0e466d28745861c2
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
7 changes: 3 additions & 4 deletions kani-compiler/src/kani_middle/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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)> {
Expand All @@ -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
Expand Down