Merge branch 'main' into main

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -7,14 +7,14 @@ use crate::args::ReachabilityType;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::analysis;
 use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes};
+use crate::kani_middle::check_reachable_items;
 use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits};
 use crate::kani_middle::metadata::gen_test_metadata;
 use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
     collect_reachable_items, filter_const_crate_items, filter_crate_items,
 };
-use crate::kani_middle::transform::BodyTransformation;
-use crate::kani_middle::{check_reachable_items, dump_mir_items};
+use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
 use crate::kani_queries::QueryDb;
 use cbmc::goto_program::Location;
 use cbmc::irep::goto_binary_serde::write_goto_binary_file;
@@ -87,11 +87,33 @@ impl GotocCodegenBackend {
         check_contract: Option<InternalDefId>,
         mut transformer: BodyTransformation,
     ) -> (GotocCtx<'tcx>, Vec<MonoItem>, Option<AssignsContract>) {
-        let items = with_timer(
+        let (items, call_graph) = with_timer(
             || collect_reachable_items(tcx, &mut transformer, starting_items),
             "codegen reachability analysis",
         );
-        dump_mir_items(tcx, &mut transformer, &items, &symtab_goto.with_extension("kani.mir"));
+
+        // Retrieve all instances from the currently codegened items.
+        let instances = items
+            .iter()
+            .filter_map(|item| match item {
+                MonoItem::Fn(instance) => Some(*instance),
+                MonoItem::Static(static_def) => {
+                    let instance: Instance = (*static_def).into();
+                    instance.has_body().then_some(instance)
+                }
+                MonoItem::GlobalAsm(_) => None,
+            })
+            .collect();
+
+        // Apply all transformation passes, including global passes.
+        let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx);
+        global_passes.run_global_passes(
+            &mut transformer,
+            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/mod.rs

@@ -4,9 +4,7 @@
 //! and transformations.
 
 use std::collections::HashSet;
-use std::path::Path;
 
-use crate::kani_middle::transform::BodyTransformation;
 use crate::kani_queries::QueryDb;
 use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
 use rustc_middle::span_bug;
@@ -15,18 +13,14 @@ use rustc_middle::ty::layout::{
     LayoutOfHelpers, TyAndLayout,
 };
 use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt};
-use rustc_session::config::OutputType;
 use rustc_smir::rustc_internal;
 use rustc_span::source_map::respan;
 use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
-use stable_mir::mir::mono::{Instance, MonoItem};
+use stable_mir::mir::mono::MonoItem;
 use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind};
 use stable_mir::CrateDef;
-use std::fs::File;
-use std::io::BufWriter;
-use std::io::Write;
 
 use self::attributes::KaniAttributes;
 
@@ -92,41 +86,6 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
     tcx.dcx().abort_if_errors();
 }
 
-/// Print MIR for the reachable items if the `--emit mir` option was provided to rustc.
-pub fn dump_mir_items(
-    tcx: TyCtxt,
-    transformer: &mut BodyTransformation,
-    items: &[MonoItem],
-    output: &Path,
-) {
-    /// Convert MonoItem into a DefId.
-    /// Skip stuff that we cannot generate the MIR items.
-    fn get_instance(item: &MonoItem) -> Option<Instance> {
-        match item {
-            // Exclude FnShims and others that cannot be dumped.
-            MonoItem::Fn(instance) => Some(*instance),
-            MonoItem::Static(def) => {
-                let instance: Instance = (*def).into();
-                instance.has_body().then_some(instance)
-            }
-            MonoItem::GlobalAsm(_) => None,
-        }
-    }
-
-    if tcx.sess.opts.output_types.contains_key(&OutputType::Mir) {
-        // Create output buffer.
-        let out_file = File::create(output).unwrap();
-        let mut writer = BufWriter::new(out_file);
-
-        // For each def_id, dump their MIR
-        for instance in items.iter().filter_map(get_instance) {
-            writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap();
-            let body = transformer.body(tcx, instance);
-            let _ = body.dump(&mut writer, &instance.name());
-        }
-    }
-}
-
 /// Structure that represents the source location of a definition.
 /// TODO: Use `InternedString` once we move it out of the cprover_bindings.
 /// <https://github.com/model-checking/kani/issues/2435>