diff --git a/crates/flux-config/src/flags.rs b/crates/flux-config/src/flags.rs index 72755a151fa..70357fb00aa 100644 --- a/crates/flux-config/src/flags.rs +++ b/crates/flux-config/src/flags.rs @@ -48,8 +48,6 @@ pub struct Flags { pub dump_fhir: bool, /// Saves the the `fhir` (debugging) pub dump_rty: bool, - /// Saves the low-level MIR for each analyzed function (debugging) - pub dump_mir: bool, /// Optimistically keeps running flux even after errors are found to get as many errors as possible pub catch_bugs: bool, /// Whether verification for the current crate is enabled. If false (the default), `flux-driver` @@ -73,7 +71,6 @@ impl Default for Flags { dump_checker_trace: None, dump_fhir: false, dump_rty: false, - dump_mir: false, catch_bugs: false, pointer_width: PointerWidth::default(), include: None, @@ -104,7 +101,6 @@ pub(crate) static FLAGS: LazyLock = LazyLock::new(|| { "log-dir" => parse_path_buf(&mut flags.log_dir, value), "dump-constraint" => parse_bool(&mut flags.dump_constraint, value), "dump-checker-trace" => parse_opt_level(&mut flags.dump_checker_trace, value), - "dump-mir" => parse_bool(&mut flags.dump_mir, value), "dump-fhir" => parse_bool(&mut flags.dump_fhir, value), "dump-rty" => parse_bool(&mut flags.dump_rty, value), "catch-bugs" => parse_bool(&mut flags.catch_bugs, value), diff --git a/crates/flux-config/src/lib.rs b/crates/flux-config/src/lib.rs index 504fe490e59..fb42d4ad9d2 100644 --- a/crates/flux-config/src/lib.rs +++ b/crates/flux-config/src/lib.rs @@ -19,10 +19,6 @@ pub fn dump_checker_trace() -> Option { FLAGS.dump_checker_trace } -pub fn dump_mir() -> bool { - FLAGS.dump_mir -} - pub fn dump_constraint() -> bool { FLAGS.dump_constraint } diff --git a/crates/flux-driver/src/callbacks.rs b/crates/flux-driver/src/callbacks.rs index 8a0e44bfecf..882f04005a7 100644 --- a/crates/flux-driver/src/callbacks.rs +++ b/crates/flux-driver/src/callbacks.rs @@ -1,6 +1,6 @@ use std::path::Path; -use flux_common::{bug, cache::QueryCache, dbg, iter::IterExt, result::ResultExt}; +use flux_common::{bug, cache::QueryCache, iter::IterExt, result::ResultExt}; use flux_config::{self as config}; use flux_errors::FluxSession; use flux_infer::fixpoint_encoding::FixQueryCache; @@ -315,17 +315,6 @@ fn mir_borrowck<'tcx>( ConsumerOptions::RegionInferenceContext, ); for (def_id, body_with_facts) in bodies_with_facts { - if config::dump_mir() { - rustc_middle::mir::pretty::write_mir_fn( - tcx, - &body_with_facts.body, - &mut |_, _| Ok(()), - &mut dbg::writer_for_item(tcx, def_id.to_def_id(), "mir").unwrap(), - rustc_middle::mir::pretty::PrettyPrintMirOptions::from_cli(tcx), - ) - .unwrap(); - } - // SAFETY: This is safe because we are feeding in the same `tcx` that is // going to be used as a witness when pulling out the data. unsafe { diff --git a/crates/flux-refineck/src/ghost_statements.rs b/crates/flux-refineck/src/ghost_statements.rs index aa7f5a89af4..dfce46ca218 100644 --- a/crates/flux-refineck/src/ghost_statements.rs +++ b/crates/flux-refineck/src/ghost_statements.rs @@ -3,10 +3,9 @@ mod fold_unfold; mod points_to; -use std::{fmt, io, iter}; +use std::{fmt, iter}; -use flux_common::{bug, dbg}; -use flux_config as config; +use flux_common::bug; use flux_middle::{global_env::GlobalEnv, queries::QueryResult}; use flux_rustc_bridge::{ lowering, @@ -80,11 +79,8 @@ impl GhostStatements { points_to::add_ghost_statements(&mut stmts, genv, body.rustc_body(), fn_sig.as_ref())?; stmts.add_unblocks(genv.tcx(), &body); - if config::dump_mir() { - let mut writer = - dbg::writer_for_item(genv.tcx(), def_id.to_def_id(), "ghost.mir").unwrap(); - stmts.write_mir(genv.tcx(), &body, &mut writer).unwrap(); - } + stmts.dump_ghost_mir(genv.tcx(), &body); + Ok(stmts) }) } @@ -143,48 +139,41 @@ impl GhostStatements { } } - pub(crate) fn write_mir<'tcx, W: io::Write>( - &self, - tcx: TyCtxt<'tcx>, - body: &Body<'tcx>, - w: &mut W, - ) -> io::Result<()> { - use rustc_middle::mir::PassWhere; - rustc_middle::mir::pretty::write_mir_fn( - tcx, - body.inner(), - &mut |pass, w| { - match pass { - PassWhere::BeforeBlock(bb) if bb == START_BLOCK => { - for stmt in &self.at_start { - writeln!(w, " {stmt:?};")?; + pub(crate) fn dump_ghost_mir<'tcx>(&self, tcx: TyCtxt<'tcx>, body: &Body<'tcx>) { + use rustc_middle::mir::{PassWhere, pretty::MirDumper}; + if let Some(dumper) = MirDumper::new(tcx, "ghost", body.inner()) { + dumper + .set_extra_data(&mut |pass, w| { + match pass { + PassWhere::BeforeBlock(bb) if bb == START_BLOCK => { + for stmt in &self.at_start { + writeln!(w, " {stmt:?};")?; + } } - } - PassWhere::BeforeLocation(location) => { - for stmt in self.statements_at(Point::BeforeLocation(location)) { - writeln!(w, " {stmt:?};")?; + PassWhere::BeforeLocation(location) => { + for stmt in self.statements_at(Point::BeforeLocation(location)) { + writeln!(w, " {stmt:?};")?; + } } - } - PassWhere::AfterTerminator(bb) => { - if let Some(map) = self.at_edge.get(&bb) { - writeln!(w)?; - for (target, stmts) in map { - write!(w, " -> {target:?} {{")?; - for stmt in stmts { - write!(w, "\n {stmt:?};")?; + PassWhere::AfterTerminator(bb) => { + if let Some(map) = self.at_edge.get(&bb) { + writeln!(w)?; + for (target, stmts) in map { + write!(w, " -> {target:?} {{")?; + for stmt in stmts { + write!(w, "\n {stmt:?};")?; + } + write!(w, "\n }}")?; } - write!(w, "\n }}")?; + writeln!(w)?; } - writeln!(w)?; } + _ => {} } - _ => {} - } - Ok(()) - }, - w, - rustc_middle::mir::pretty::PrettyPrintMirOptions::from_cli(tcx), - ) + Ok(()) + }) + .dump_mir(body.inner()); + } } } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 5513678e267..969a0a4c1da 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2025-08-29" +channel = "nightly-2025-09-09" components = ["rust-src", "rustc-dev", "llvm-tools", "rustfmt", "clippy"]