Migrate compiler interface to use StableMIR

Author: celinval

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -1331,7 +1331,7 @@ impl<'tcx> GotocCtx<'tcx> {
             TyKind::RigidTy(RigidTy::Slice(_)) | TyKind::RigidTy(RigidTy::Str) => {
                 let unit_t = match ty.kind() {
                     TyKind::RigidTy(RigidTy::Slice(et)) => et,
-                    TyKind::RigidTy(RigidTy::Str) => rustc_internal::stable(self.tcx.types.u8),
+                    TyKind::RigidTy(RigidTy::Str) => Ty::unsigned_ty(UintTy::U8),
                     _ => unreachable!(),
                 };
                 let unit = self.layout_of_stable(unit_t);

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -16,7 +16,7 @@ use crate::kani_middle::{check_reachable_items, dump_mir_items};
 use crate::kani_queries::QueryDb;
 use cbmc::goto_program::Location;
 use cbmc::irep::goto_binary_serde::write_goto_binary_file;
-use cbmc::RoundingMode;
+use cbmc::{InternString, RoundingMode};
 use cbmc::{InternedString, MachineModel};
 use kani_metadata::artifact::convert_type;
 use kani_metadata::CompilerArtifactStub;
@@ -32,12 +32,10 @@ use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
 use rustc_data_structures::temp_dir::MaybeTempDir;
 use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
 use rustc_hir::def_id::LOCAL_CRATE;
-use rustc_hir::definitions::DefPathHash;
 use rustc_metadata::creader::MetadataLoaderDyn;
 use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
-use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::util::Providers;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
@@ -46,7 +44,7 @@ use rustc_session::Session;
 use rustc_smir::rustc_internal;
 use rustc_target::abi::Endian;
 use rustc_target::spec::PanicStrategy;
-use stable_mir::mir::mono::MonoItem as MonoItemStable;
+use stable_mir::mir::mono::MonoItem;
 use stable_mir::CrateDef;
 use std::any::Any;
 use std::collections::BTreeMap;
@@ -82,10 +80,10 @@ impl GotocCodegenBackend {
     fn codegen_items<'tcx>(
         &self,
         tcx: TyCtxt<'tcx>,
-        starting_items: &[MonoItem<'tcx>],
+        starting_items: &[MonoItem],
         symtab_goto: &Path,
         machine_model: &MachineModel,
-    ) -> (GotocCtx<'tcx>, Vec<MonoItem<'tcx>>) {
+    ) -> (GotocCtx<'tcx>, Vec<MonoItem>) {
         let items = with_timer(
             || collect_reachable_items(tcx, starting_items),
             "codegen reachability analysis",
@@ -103,17 +101,13 @@ impl GotocCodegenBackend {
                 for item in &items {
                     match *item {
                         MonoItem::Fn(instance) => {
-                            let instance = rustc_internal::stable(instance);
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.declare_function(instance),
                                 format!("declare_function: {}", instance.name()),
                                 instance.def,
                             );
                         }
-                        MonoItem::Static(_) => {
-                            let MonoItemStable::Static(def) = rustc_internal::stable(item) else {
-                                unreachable!()
-                            };
+                        MonoItem::Static(def) => {
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.declare_static(def),
                                 format!("declare_static: {}", def.name()),
@@ -128,7 +122,6 @@ impl GotocCodegenBackend {
                 for item in &items {
                     match *item {
                         MonoItem::Fn(instance) => {
-                            let instance = rustc_internal::stable(instance);
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.codegen_function(instance),
                                 format!(
@@ -139,10 +132,7 @@ impl GotocCodegenBackend {
                                 instance.def,
                             );
                         }
-                        MonoItem::Static(_) => {
-                            let MonoItemStable::Static(def) = rustc_internal::stable(item) else {
-                                unreachable!()
-                            };
+                        MonoItem::Static(def) => {
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.codegen_static(def),
                                 format!("codegen_static: {}", def.name()),
@@ -237,28 +227,30 @@ impl CodegenBackend for GotocCodegenBackend {
                 ReachabilityType::Harnesses => {
                     // Cross-crate collecting of all items that are reachable from the crate harnesses.
                     let harnesses = queries.target_harnesses();
-                    let mut items: HashSet<DefPathHash> = HashSet::with_capacity(harnesses.len());
+                    let mut items: HashSet<_> = HashSet::with_capacity(harnesses.len());
                     items.extend(harnesses);
-                    let harnesses = filter_crate_items(tcx, |_, def_id| {
-                        items.contains(&tcx.def_path_hash(def_id))
+                    let harnesses = filter_crate_items(tcx, |_, instance| {
+                        items.contains(&instance.name().intern())
                     });
                     for harness in harnesses {
-                        let model_path = queries
-                            .harness_model_path(&tcx.def_path_hash(harness.def_id()))
-                            .unwrap();
-                        let (gcx, items) =
-                            self.codegen_items(tcx, &[harness], model_path, &results.machine_model);
-                        results.extend(gcx, items, None);
+                        let model_path = queries.harness_model_path(&harness.name()).unwrap();
+                        let (gcx, mono_items) = self.codegen_items(
+                            tcx,
+                            &[MonoItem::Fn(harness)],
+                            model_path,
+                            &results.machine_model,
+                        );
+                        results.extend(gcx, mono_items, None);
                     }
                 }
                 ReachabilityType::Tests => {
                     // We're iterating over crate items here, so what we have to codegen is the "test description" containing the
                     // test closure that we want to execute
                     // TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match.
                     let mut descriptions = vec![];
-                    let harnesses = filter_const_crate_items(tcx, |_, def_id| {
-                        if is_test_harness_description(tcx, def_id) {
-                            descriptions.push(def_id);
+                    let harnesses = filter_const_crate_items(tcx, |_, item| {
+                        if is_test_harness_description(tcx, item.def) {
+                            descriptions.push(item.def);
                             true
                         } else {
                             false
@@ -289,11 +281,10 @@ impl CodegenBackend for GotocCodegenBackend {
                 }
                 ReachabilityType::None => {}
                 ReachabilityType::PubFns => {
-                    let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
-                    let local_reachable = filter_crate_items(tcx, |_, def_id| {
-                        (tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like())
-                            || entry_fn == Some(def_id)
-                    });
+                    let local_reachable = filter_crate_items(tcx, |_, _| true)
+                        .into_iter()
+                        .map(MonoItem::Fn)
+                        .collect::<Vec<_>>();
                     let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
                     let (gcx, items) = self.codegen_items(
                         tcx,
@@ -527,17 +518,17 @@ where
     }
 }
 
-struct GotoCodegenResults<'tcx> {
+struct GotoCodegenResults {
     reachability: ReachabilityType,
     harnesses: Vec<HarnessMetadata>,
     unsupported_constructs: UnsupportedConstructs,
     concurrent_constructs: UnsupportedConstructs,
-    items: Vec<MonoItem<'tcx>>,
+    items: Vec<MonoItem>,
     crate_name: InternedString,
     machine_model: MachineModel,
 }
 
-impl<'tcx> GotoCodegenResults<'tcx> {
+impl GotoCodegenResults {
     pub fn new(tcx: TyCtxt, reachability: ReachabilityType) -> Self {
         GotoCodegenResults {
             reachability,
@@ -585,12 +576,7 @@ impl<'tcx> GotoCodegenResults<'tcx> {
         }
     }
 
-    fn extend(
-        &mut self,
-        gcx: GotocCtx,
-        items: Vec<MonoItem<'tcx>>,
-        metadata: Option<HarnessMetadata>,
-    ) {
+    fn extend(&mut self, gcx: GotocCtx, items: Vec<MonoItem>, metadata: Option<HarnessMetadata>) {
         let mut items = items;
         self.harnesses.extend(metadata);
         self.concurrent_constructs.extend(gcx.concurrent_constructs);
@@ -599,7 +585,7 @@ impl<'tcx> GotoCodegenResults<'tcx> {
     }
 
     /// Prints a report at the end of the compilation.
-    fn print_report(&self, tcx: TyCtxt<'tcx>) {
+    fn print_report(&self, tcx: TyCtxt) {
         // Print all unsupported constructs.
         if !self.unsupported_constructs.is_empty() {
             // Sort alphabetically.
@@ -631,7 +617,7 @@ impl<'tcx> GotoCodegenResults<'tcx> {
 
         // Print some compilation stats.
         if tracing::enabled!(tracing::Level::INFO) {
-            analysis::print_stats(tcx, &self.items);
+            analysis::print_stats(&self.items);
         }
     }
 }

kani-compiler/src/kani_compiler.rs

@@ -25,6 +25,7 @@ use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::stubbing::{self, harness_stub_map};
 use crate::kani_queries::QueryDb;
 use crate::session::init_session;
+use cbmc::{InternString, InternedString};
 use clap::Parser;
 use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
 use rustc_codegen_ssa::traits::CodegenBackend;
@@ -68,7 +69,7 @@ fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<CodegenBackend> {
 }
 
 /// A stable (across compilation sessions) identifier for the harness function.
-type HarnessId = DefPathHash;
+type HarnessId = InternedString;
 
 /// A set of stubs.
 type Stubs = BTreeMap<DefPathHash, DefPathHash>;
@@ -280,14 +281,13 @@ impl KaniCompiler {
         if self.queries.lock().unwrap().args().reachability_analysis == ReachabilityType::Harnesses
         {
             let base_filename = tcx.output_filenames(()).output_path(OutputType::Object);
-            let harnesses = filter_crate_items(tcx, |_, def_id| is_proof_harness(tcx, def_id));
+            let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance));
             let all_harnesses = harnesses
                 .into_iter()
                 .map(|harness| {
-                    let def_id = harness.def_id();
-                    let def_path = tcx.def_path_hash(def_id);
-                    let metadata = gen_proof_metadata(tcx, def_id, &base_filename);
-                    let stub_map = harness_stub_map(tcx, def_id, &metadata);
+                    let def_path = harness.name().intern();
+                    let metadata = gen_proof_metadata(tcx, harness, &base_filename);
+                    let stub_map = harness_stub_map(tcx, harness, &metadata);
                     (def_path, HarnessInfo { metadata, stub_map })
                 })
                 .collect::<HashMap<_, _>>();

kani-compiler/src/kani_middle/analysis.rs

@@ -7,9 +7,6 @@
 //! This module will perform all the analyses requested. Callers are responsible for selecting
 //! when the cost of these analyses are worth it.
 
-use rustc_middle::mir::mono::MonoItem as InternalMonoItem;
-use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::MonoItem;
 use stable_mir::mir::{
     visit::Location, MirVisitor, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
@@ -23,8 +20,7 @@ use std::fmt::Display;
 ///  - Number of items per type (Function / Constant / Shims)
 ///  - Number of instructions per type.
 ///  - Total number of MIR instructions.
-pub fn print_stats<'tcx>(_tcx: TyCtxt<'tcx>, items: &[InternalMonoItem<'tcx>]) {
-    let items: Vec<MonoItem> = items.iter().map(rustc_internal::stable).collect();
+pub fn print_stats(items: &[MonoItem]) {
     let item_types = items.iter().collect::<Counter>();
     let visitor = items
         .iter()

kani-compiler/src/kani_middle/attributes.rs

@@ -13,7 +13,10 @@ use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_middle::ty::{Instance, TyCtxt, TyKind};
 use rustc_session::Session;
+use rustc_smir::rustc_internal;
 use rustc_span::{Span, Symbol};
+use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::CrateDef;
 use std::str::FromStr;
 use strum_macros::{AsRefStr, EnumString};
 
@@ -111,6 +114,10 @@ impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> {
 impl<'tcx> KaniAttributes<'tcx> {
     /// Perform preliminary parsing and checking for the attributes on this
     /// function
+    pub fn for_instance(tcx: TyCtxt<'tcx>, instance: InstanceStable) -> Self {
+        KaniAttributes::for_item(tcx, rustc_internal::internal(instance.def.def_id()))
+    }
+
     pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self {
         let all_attributes = tcx.get_attrs_unchecked(def_id);
         let map = all_attributes.iter().fold(
@@ -511,20 +518,23 @@ pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool {
 
 /// Same as [`KaniAttributes::is_harness`] but more efficient because less
 /// attribute parsing is performed.
-pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool {
+pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool {
+    let def_id = rustc_internal::internal(instance.def.def_id());
     has_kani_attribute(tcx, def_id, |a| {
         matches!(a, KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract)
     })
 }
 
 /// Does this `def_id` have `#[rustc_test_marker]`?
-pub fn is_test_harness_description(tcx: TyCtxt, def_id: DefId) -> bool {
+pub fn is_test_harness_description(tcx: TyCtxt, item: impl CrateDef) -> bool {
+    let def_id = rustc_internal::internal(item.def_id());
     let attrs = tcx.get_attrs_unchecked(def_id);
     attr::contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker)
 }
 
 /// Extract the test harness name from the `#[rustc_test_maker]`
-pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String {
+pub fn test_harness_name(tcx: TyCtxt, def: &impl CrateDef) -> String {
+    let def_id = rustc_internal::internal(def.def_id());
     let attrs = tcx.get_attrs_unchecked(def_id);
     let marker = attr::find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap();
     parse_str_value(&marker).unwrap()

kani-compiler/src/kani_middle/metadata.rs

@@ -7,32 +7,30 @@ use std::path::Path;
 
 use crate::kani_middle::attributes::test_harness_name;
 use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata};
-use rustc_hir::def_id::DefId;
-use rustc_middle::ty::{Instance, InstanceDef, TyCtxt};
+use rustc_middle::ty::TyCtxt;
+use stable_mir::mir::mono::Instance;
+use stable_mir::CrateDef;
 
 use super::{attributes::KaniAttributes, SourceLocation};
 
 /// Create the harness metadata for a proof harness for a given function.
-pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> HarnessMetadata {
-    let attributes = KaniAttributes::for_item(tcx, def_id).harness_attributes();
-    let pretty_name = tcx.def_path_str(def_id);
+pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
+    let def = instance.def;
+    let attributes = KaniAttributes::for_instance(tcx, instance).harness_attributes();
+    let pretty_name = instance.name();
     // Main function a special case in order to support `--function main`
     // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
-    let mangled_name = if pretty_name == "main" {
-        pretty_name.clone()
-    } else {
-        tcx.symbol_name(Instance::mono(tcx, def_id)).to_string()
-    };
+    let mangled_name =
+        if pretty_name == "main" { pretty_name.clone() } else { instance.mangled_name() };
 
-    let body = tcx.instance_mir(InstanceDef::Item(def_id));
-    let loc = SourceLocation::new(tcx, &body.span);
+    let loc = SourceLocation::new(&instance.def.span());
     let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
     let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
 
     HarnessMetadata {
         pretty_name,
         mangled_name,
-        crate_name: tcx.crate_name(def_id.krate).to_string(),
+        crate_name: def.krate().name,
         original_file: loc.filename,
         original_start_line: loc.start_line,
         original_end_line: loc.end_line,
@@ -44,23 +42,22 @@ pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> Harne
 
 /// Create the harness metadata for a test description.
 #[allow(dead_code)]
-pub fn gen_test_metadata<'tcx>(
-    tcx: TyCtxt<'tcx>,
-    test_desc: DefId,
-    test_fn: Instance<'tcx>,
+pub fn gen_test_metadata(
+    tcx: TyCtxt,
+    test_desc: impl CrateDef,
+    test_fn: Instance,
     base_name: &Path,
 ) -> HarnessMetadata {
-    let pretty_name = test_harness_name(tcx, test_desc);
-    let mangled_name = tcx.symbol_name(test_fn).to_string();
-    let body = tcx.instance_mir(InstanceDef::Item(test_desc));
-    let loc = SourceLocation::new(tcx, &body.span);
+    let pretty_name = test_harness_name(tcx, &test_desc);
+    let mangled_name = test_fn.mangled_name();
+    let loc = SourceLocation::new(&test_desc.span());
     let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
     let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
 
     HarnessMetadata {
         pretty_name,
         mangled_name,
-        crate_name: tcx.crate_name(test_desc.krate).to_string(),
+        crate_name: test_desc.krate().name,
         original_file: loc.filename,
         original_start_line: loc.start_line,
         original_end_line: loc.end_line,