Apply suggestions from code review

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -108,7 +108,7 @@ impl GotocCodegenBackend {
             .collect();
 
         // Apply all transformation passes, including global passes.
-        transformer.apply_passes(tcx, starting_items, instances, call_graph);
+        transformer.run_global_passes(tcx, starting_items, instances, call_graph);
 
         // Follow rustc naming convention (cx is abbrev for context).
         // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions

kani-compiler/src/kani_middle/reachability.rs

@@ -625,20 +625,22 @@ impl CallGraph {
             if !visited.contains(&to_visit) {
                 visited.insert(to_visit.clone());
                 queue.extend(
-                    self.back_edges.get(&to_visit).unwrap().iter().map(|item| item.as_node()),
+                    self.back_edges
+                        .get(&to_visit)
+                        .unwrap()
+                        .iter()
+                        .map(|item| Node::from(item.clone())),
                 );
             }
         }
 
         for node in &visited {
             writeln!(writer, r#""{node}""#)?;
-            for succ in self
-                .edges
-                .get(node)
-                .unwrap()
-                .iter()
-                .filter(|item| visited.contains(&item.as_node()))
-            {
+            let edges = self.edges.get(node).unwrap();
+            for succ in edges.iter().filter(|item| {
+                let node = Node::from((*item).clone());
+                visited.contains(&node)
+            }) {
                 let reason = succ.0.reason;
                 writeln!(writer, r#""{node}" -> "{succ}" [label={reason:?}] "#)?;
             }
@@ -667,8 +669,8 @@ impl Display for CollectedNode {
     }
 }
 
-impl CollectedNode {
-    pub fn as_node(&self) -> Node {
-        Node(self.0.item.clone())
+impl From<CollectedNode> for Node {
+    fn from(value: CollectedNode) -> Self {
+        Node(value.0.item)
     }
 }

kani-compiler/src/kani_middle/transform/dump_mir_pass.rs

@@ -10,13 +10,15 @@ use kani_metadata::ArtifactType;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
 use stable_mir::mir::mono::{Instance, MonoItem};
-use stable_mir::mir::Body;
-use std::fmt::{Debug, Formatter, Result};
 use std::fs::File;
 use std::io::BufWriter;
 use std::io::Write;
+use std::path::PathBuf;
+
+use super::BodyTransformation;
 
 /// Dump all MIR bodies.
+#[derive(Debug)]
 pub struct DumpMirPass {
     enabled: bool,
 }
@@ -27,12 +29,6 @@ impl DumpMirPass {
     }
 }
 
-impl Debug for DumpMirPass {
-    fn fmt(&self, f: &mut Formatter<'_>) -> Result {
-        f.debug_struct("DumpMirPass").field("enabled", &self.enabled).finish()
-    }
-}
-
 impl GlobalPass for DumpMirPass {
     fn is_enabled(&self, _query_db: &QueryDb) -> bool {
         self.enabled
@@ -41,33 +37,33 @@ impl GlobalPass for DumpMirPass {
     fn transform(
         &mut self,
         tcx: TyCtxt,
-        starting_items: &[MonoItem],
-        bodies: Vec<(Body, Instance)>,
         _call_graph: &CallGraph,
-    ) -> Vec<(bool, Body, Instance)> {
+        starting_items: &[MonoItem],
+        instances: Vec<Instance>,
+        transformer: &mut BodyTransformation,
+    ) {
         // Create output buffer.
         let file_path = {
-            let base_path = tcx.output_filenames(()).path(OutputType::Object);
-            let base_name = base_path.as_path();
             let entry_point = (starting_items.len() == 1).then_some(starting_items[0].clone());
+            // If there is a single entry point, use it as a file name.
             if let Some(MonoItem::Fn(starting_instance)) = entry_point {
                 let mangled_name = starting_instance.mangled_name();
-                let file_stem =
-                    format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
-                base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto)
+                PathBuf::from(mangled_name).with_extension(ArtifactType::SymTabGoto)
             } else {
-                base_name.with_extension(ArtifactType::SymTabGoto)
+                // Otherwise, use the object output path from the compiler.
+                tcx.output_filenames(())
+                    .path(OutputType::Object)
+                    .as_path()
+                    .with_extension(ArtifactType::SymTabGoto)
             }
         };
         let out_file = File::create(file_path.with_extension("kani.mir")).unwrap();
         let mut writer = BufWriter::new(out_file);
 
-        // For each def_id, dump their MIR
-        for (body, instance) in bodies.iter() {
+        // For each def_id, dump their MIR.
+        for instance in instances.iter() {
             writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap();
-            let _ = body.dump(&mut writer, &instance.name());
+            let _ = transformer.body(tcx, *instance).dump(&mut writer, &instance.name());
         }
-
-        bodies.into_iter().map(|(body, instance)| (false, body, instance)).collect()
     }
 }

kani-compiler/src/kani_middle/transform/mod.rs

@@ -128,25 +128,19 @@ impl BodyTransformation {
         }
     }
 
-    /// Apply all per-body pass followed by the global passes and store the results in cache that
-    /// can later be queried by `body`.
-    pub fn apply_passes(
+    /// Run all global passes and store the results in a cache that can later be queried by `body`.
+    pub fn run_global_passes(
         &mut self,
         tcx: TyCtxt,
         starting_items: &[MonoItem],
         instances: Vec<Instance>,
         call_graph: CallGraph,
     ) {
-        let bodies: Vec<_> =
-            instances.into_iter().map(|instance| (self.body(tcx, instance), instance)).collect();
-        for global_pass in self.global_passes.iter_mut() {
-            let results = global_pass.transform(tcx, starting_items, bodies.clone(), &call_graph);
-            for (modified, body, instance) in results {
-                if modified {
-                    self.cache.insert(instance, TransformationResult::Modified(body));
-                }
-            }
+        let mut global_passes: Vec<_> = self.global_passes.drain(0..).collect();
+        for global_pass in global_passes.iter_mut() {
+            global_pass.transform(tcx, &call_graph, starting_items, instances.clone(), self);
         }
+        self.global_passes.extend(global_passes);
     }
 
     fn add_pass<P: TransformPass + 'static>(&mut self, query_db: &QueryDb, pass: P) {
@@ -199,10 +193,11 @@ pub(crate) trait GlobalPass: Debug {
     fn transform(
         &mut self,
         tcx: TyCtxt,
-        starting_items: &[MonoItem],
-        bodies: Vec<(Body, Instance)>,
         call_graph: &CallGraph,
-    ) -> Vec<(bool, Body, Instance)>;
+        starting_items: &[MonoItem],
+        instances: Vec<Instance>,
+        transformer: &mut BodyTransformation,
+    );
 }
 
 /// The transformation result.