Optimize reachability with non-mutating global passes

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -87,7 +87,7 @@ impl GotocCodegenBackend {
         // disadvantage of not having a precomputed call graph for the global passes to use. The
         // call graph could be used, for example, in resolving function pointer or vtable calls for
         // global passes that need this.
-        let (items, call_graph) = with_timer(
+        let (mut items, call_graph) = with_timer(
             || collect_reachable_items(tcx, &mut transformer, starting_items),
             "codegen reachability analysis",
         );
@@ -107,7 +107,7 @@ impl GotocCodegenBackend {
 
         // Apply all transformation passes, including global passes.
         let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx);
-        global_passes.run_global_passes(
+        let any_pass_modified = global_passes.run_global_passes(
             &mut transformer,
             tcx,
             starting_items,
@@ -117,10 +117,12 @@ impl GotocCodegenBackend {
 
         // Re-collect reachable items after global transformations were applied. This is necessary
         // since global pass could add extra calls to instrumentation.
-        let (items, _) = with_timer(
-            || collect_reachable_items(tcx, &mut transformer, starting_items),
-            "codegen reachability analysis (second pass)",
-        );
+        if any_pass_modified {
+            (items, _) = with_timer(
+                || collect_reachable_items(tcx, &mut transformer, starting_items),
+                "codegen reachability analysis (second pass)",
+            );
+        }
 
         // 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/transform/check_uninit/delayed_ub/mod.rs

@@ -65,7 +65,8 @@ impl GlobalPass for DelayedUbPass {
         starting_items: &[MonoItem],
         instances: Vec<Instance>,
         transformer: &mut BodyTransformation,
-    ) {
+    ) -> bool {
+        let mut modified = false;
         // Collect all analysis targets (pointers to places reading and writing from which should be
         // tracked).
         let targets: HashSet<_> = instances
@@ -138,11 +139,13 @@ impl GlobalPass for DelayedUbPass {
                 );
                 // If some instrumentation has been performed, update the cached body in the local transformer.
                 if instrumentation_added {
+                    modified = true;
                     transformer.cache.entry(instance).and_modify(|transformation_result| {
                         *transformation_result = TransformationResult::Modified(body);
                     });
                 }
             }
         }
+        modified
     }
 }

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

@@ -40,7 +40,7 @@ impl GlobalPass for DumpMirPass {
         starting_items: &[MonoItem],
         instances: Vec<Instance>,
         transformer: &mut BodyTransformation,
-    ) {
+    ) -> bool {
         // Create output buffer.
         let file_path = {
             let base_path = tcx.output_filenames(()).path(OutputType::Object);
@@ -65,5 +65,8 @@ impl GlobalPass for DumpMirPass {
             writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap();
             let _ = transformer.body(tcx, *instance).dump(&mut writer, &instance.name());
         }
+
+        // This pass just reads the MIR and thus never modifies it.
+        false
     }
 }

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

@@ -178,15 +178,16 @@ pub(crate) trait GlobalPass: Debug {
     where
         Self: Sized;
 
-    /// Run a transformation pass on the whole codegen unit.
+    /// Run a transformation pass on the whole codegen unit, returning a bool
+    /// for whether modifications were made to the MIR that could affect reachability.
     fn transform(
         &mut self,
         tcx: TyCtxt,
         call_graph: &CallGraph,
         starting_items: &[MonoItem],
         instances: Vec<Instance>,
         transformer: &mut BodyTransformation,
-    );
+    ) -> bool;
 }
 
 /// The transformation result.
@@ -225,16 +226,25 @@ impl GlobalPasses {
     }
 
     /// Run all global passes and store the results in a cache that can later be queried by `body`.
+    /// Returns a boolean for if a pass has modified the MIR bodies.
     pub fn run_global_passes(
         &mut self,
         transformer: &mut BodyTransformation,
         tcx: TyCtxt,
         starting_items: &[MonoItem],
         instances: Vec<Instance>,
         call_graph: CallGraph,
-    ) {
-        for global_pass in self.global_passes.iter_mut() {
-            global_pass.transform(tcx, &call_graph, starting_items, instances.clone(), transformer);
+    ) -> bool {
+        let mut modified = false;
+        for global_pass in &mut self.global_passes {
+            modified |= global_pass.transform(
+                tcx,
+                &call_graph,
+                starting_items,
+                instances.clone(),
+                transformer,
+            );
         }
+        modified
     }
 }