Use stable_mir api instead of internal api

kani-compiler/Cargo.toml

@@ -30,6 +30,7 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"
 default = ['cprover']
 cprover = ['cbmc', 'num', 'serde']
 write_json_symtab = []
+stable_mir = []
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.

kani-compiler/src/kani_middle/analysis.rs

@@ -7,10 +7,13 @@
 //! 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;
-use rustc_middle::mir::visit::Visitor as MirVisitor;
-use rustc_middle::mir::{Location, Rvalue, Statement, StatementKind, Terminator, TerminatorKind};
+use rustc_middle::mir::mono::MonoItem as InternalMonoItem;
 use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
+use stable_mir::mir::{
+ visit::Location, MirVisitor, Rvalue, Statement,
+ StatementKind, Terminator, TerminatorKind,
+};
 use std::collections::HashMap;
 use std::fmt::Display;
 
@@ -20,19 +23,20 @@ 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: &[MonoItem<'tcx>]) {
+pub fn print_stats<'tcx>(tcx: TyCtxt<'tcx>, items: &[InternalMonoItem<'tcx>]) {
  let item_types = items.iter().collect::<Counter>();
  let visitor = items
  .iter()
  .filter_map(|&mono| {
- if let MonoItem::Fn(instance) = mono {
+ if let InternalMonoItem::Fn(instance) = mono {
  Some(tcx.instance_mir(instance.def))
  } else {
  None
  }
  })
  .fold(StatsVisitor::default(), |mut visitor, body| {
- visitor.visit_body(body);
+ let body = rustc_internal::stable(body);
+ visitor.visit_body(&body);
  visitor
  });
  eprintln!("====== Reachability Analysis Result =======");
@@ -54,20 +58,20 @@ struct StatsVisitor {
  exprs: Counter,
 }
 
-impl<'tcx> MirVisitor<'tcx> for StatsVisitor {
- fn visit_statement(&mut self, statement: &Statement<'tcx>, location: Location) {
+impl<'tcx> MirVisitor for StatsVisitor {
+ fn visit_statement(&mut self, statement: &Statement, location: Location) {
  self.stmts.add(statement);
  // Also visit the type of expression.
  self.super_statement(statement, location);
  }
 
- fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, _location: Location) {
+ fn visit_terminator(&mut self, terminator: &Terminator, _location: Location) {
  self.stmts.add(terminator);
  // Stop here since we don't care today about the information inside the terminator.
  // self.super_terminator(terminator, location);
  }
 
- fn visit_rvalue(&mut self, rvalue: &Rvalue<'tcx>, _location: Location) {
+ fn visit_rvalue(&mut self, rvalue: &Rvalue, _location: Location) {
  self.exprs.add(rvalue);
  // Stop here since we don't care today about the information inside the rvalue.
  // self.super_rvalue(rvalue, location);
@@ -115,28 +119,28 @@ impl<T: Into<Key>> FromIterator<T> for Counter {
 #[derive(Debug, Eq, Hash, PartialEq)]
 struct Key(pub &'static str);
 
-impl<'tcx> From<&MonoItem<'tcx>> for Key {
- fn from(value: &MonoItem) -> Self {
+impl<'tcx> From<&InternalMonoItem<'tcx>> for Key {
+ fn from(value: &InternalMonoItem) -> Self {
  match value {
- MonoItem::Fn(_) => Key("function"),
- MonoItem::GlobalAsm(_) => Key("global assembly"),
- MonoItem::Static(_) => Key("static item"),
+ InternalMonoItem::Fn(_) => Key("function"),
+ InternalMonoItem::GlobalAsm(_) => Key("global assembly"),
+ InternalMonoItem::Static(_) => Key("static item"),
  }
  }
 }
 
-impl<'tcx> From<&Statement<'tcx>> for Key {
- fn from(value: &Statement<'tcx>) -> Self {
+impl<'tcx> From<&Statement> for Key {
+ fn from(value: &Statement) -> Self {
  match value.kind {
- StatementKind::Assign(_) => Key("Assign"),
+ StatementKind::Assign(..) => Key("Assign"),
  StatementKind::Deinit(_) => Key("Deinit"),
  StatementKind::Intrinsic(_) => Key("Intrinsic"),
  StatementKind::SetDiscriminant { .. } => Key("SetDiscriminant"),
  // For now, we don't care about the ones below.
- StatementKind::AscribeUserType(_, _)
+ StatementKind::AscribeUserType { .. }
  | StatementKind::Coverage(_)
  | StatementKind::ConstEvalCounter
- | StatementKind::FakeRead(_)
+ | StatementKind::FakeRead(..)
  | StatementKind::Nop
  | StatementKind::PlaceMention(_)
  | StatementKind::Retag(_, _)
@@ -146,29 +150,26 @@ impl<'tcx> From<&Statement<'tcx>> for Key {
  }
 }
 
-impl<'tcx> From<&Terminator<'tcx>> for Key {
- fn from(value: &Terminator<'tcx>) -> Self {
+impl<'tcx> From<&Terminator> for Key {
+ fn from(value: &Terminator) -> Self {
  match value.kind {
+ TerminatorKind::Abort => Key("Abort"),
  TerminatorKind::Assert { .. } => Key("Assert"),
  TerminatorKind::Call { .. } => Key("Call"),
  TerminatorKind::Drop { .. } => Key("Drop"),
  TerminatorKind::CoroutineDrop => Key("CoroutineDrop"),
  TerminatorKind::Goto { .. } => Key("Goto"),
- TerminatorKind::FalseEdge { .. } => Key("FalseEdge"),
- TerminatorKind::FalseUnwind { .. } => Key("FalseUnwind"),
  TerminatorKind::InlineAsm { .. } => Key("InlineAsm"),
- TerminatorKind::UnwindResume => Key("UnwindResume"),
+ TerminatorKind::Resume { .. } => Key("Resume"),
  TerminatorKind::Return => Key("Return"),
  TerminatorKind::SwitchInt { .. } => Key("SwitchInt"),
- TerminatorKind::UnwindTerminate(_) => Key("UnwindTerminate"),
  TerminatorKind::Unreachable => Key("Unreachable"),
- TerminatorKind::Yield { .. } => Key("Yield"),
  }
  }
 }
 
-impl<'tcx> From<&Rvalue<'tcx>> for Key {
- fn from(value: &Rvalue<'tcx>) -> Self {
+impl<'tcx> From<&Rvalue> for Key {
+ fn from(value: &Rvalue) -> Self {
  match value {
  Rvalue::Use(_) => Key("Use"),
  Rvalue::Repeat(_, _) => Key("Repeat"),
@@ -177,8 +178,8 @@ impl<'tcx> From<&Rvalue<'tcx>> for Key {
  Rvalue::AddressOf(_, _) => Key("AddressOf"),
  Rvalue::Len(_) => Key("Len"),
  Rvalue::Cast(_, _, _) => Key("Cast"),
- Rvalue::BinaryOp(_, _) => Key("BinaryOp"),
- Rvalue::CheckedBinaryOp(_, _) => Key("CheckedBinaryOp"),
+ Rvalue::BinaryOp(..) => Key("BinaryOp"),
+ Rvalue::CheckedBinaryOp(..) => Key("CheckedBinaryOp"),
  Rvalue::NullaryOp(_, _) => Key("NullaryOp"),
  Rvalue::UnaryOp(_, _) => Key("UnaryOp"),
  Rvalue::Discriminant(_) => Key("Discriminant"),

kani-compiler/src/main.rs

@@ -26,8 +26,10 @@ extern crate rustc_interface;
 extern crate rustc_metadata;
 extern crate rustc_middle;
 extern crate rustc_session;
+extern crate rustc_smir;
 extern crate rustc_span;
 extern crate rustc_target;
+extern crate stable_mir;
 // We can't add this directly as a dependency because we need the version to match rustc
 extern crate tempfile;