From 414102b5d9a73d03ce051de1f7d759e47b5c593e Mon Sep 17 00:00:00 2001 From: ouz-a Date: Sat, 11 Nov 2023 17:25:34 +0300 Subject: [PATCH] Use stable_mir api instead of internal api --- kani-compiler/Cargo.toml | 1 + kani-compiler/src/kani_middle/analysis.rs | 63 ++++++++++++----------- kani-compiler/src/main.rs | 2 + 3 files changed, 35 insertions(+), 31 deletions(-) diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index c673fb7d9288..6f9d3f3954c4 100644 --- a/kani-compiler/Cargo.toml +++ b/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. diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index e5cced950e01..569f9e9e18e9 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/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::(); 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> FromIterator 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"), diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 0199642f9a60..4316d188c02d 100644 --- a/kani-compiler/src/main.rs +++ b/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;