From 414102b5d9a73d03ce051de1f7d759e47b5c593e Mon Sep 17 00:00:00 2001 From: ouz-a Date: Sat, 11 Nov 2023 17:25:34 +0300 Subject: [PATCH 1/3] 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; From d2523aaeef87bb0f5a365d0404ba1a762c48fbf0 Mon Sep 17 00:00:00 2001 From: ouz-a Date: Tue, 14 Nov 2023 17:20:44 +0300 Subject: [PATCH 2/3] address reviews --- kani-compiler/Cargo.toml | 1 - kani-compiler/src/kani_middle/analysis.rs | 59 ++++++++++++----------- 2 files changed, 30 insertions(+), 30 deletions(-) diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 6f9d3f3954c4..c673fb7d9288 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -30,7 +30,6 @@ 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 569f9e9e18e9..590b92086bda 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -10,9 +10,9 @@ 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, + visit::Location, MirVisitor, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }; use std::collections::HashMap; use std::fmt::Display; @@ -24,29 +24,30 @@ use std::fmt::Display; /// - Number of instructions per type. /// - Total number of MIR instructions. 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 InternalMonoItem::Fn(instance) = mono { - Some(tcx.instance_mir(instance.def)) - } else { - None - } - }) - .fold(StatsVisitor::default(), |mut visitor, body| { - let body = rustc_internal::stable(body); - visitor.visit_body(&body); - visitor - }); - eprintln!("====== Reachability Analysis Result ======="); - eprintln!("Total # items: {}", item_types.total()); - eprintln!("Total # statements: {}", visitor.stmts.total()); - eprintln!("Total # expressions: {}", visitor.exprs.total()); - eprintln!("\nReachable Items:\n{item_types}"); - eprintln!("Statements:\n{}", visitor.stmts); - eprintln!("Expressions:\n{}", visitor.exprs); - eprintln!("-------------------------------------------") + rustc_internal::run(tcx, || { + let item_types = items.iter().collect::(); + let visitor = items + .iter() + .filter_map(|&mono| { + if let MonoItem::Fn(instance) = rustc_internal::stable(&mono) { + Some(instance) + } else { + None + } + }) + .fold(StatsVisitor::default(), |mut visitor, body| { + visitor.visit_body(&body.body()); + visitor + }); + eprintln!("====== Reachability Analysis Result ======="); + eprintln!("Total # items: {}", item_types.total()); + eprintln!("Total # statements: {}", visitor.stmts.total()); + eprintln!("Total # expressions: {}", visitor.exprs.total()); + eprintln!("\nReachable Items:\n{item_types}"); + eprintln!("Statements:\n{}", visitor.stmts); + eprintln!("Expressions:\n{}", visitor.exprs); + eprintln!("-------------------------------------------") + }); } #[derive(Default)] @@ -58,7 +59,7 @@ struct StatsVisitor { exprs: Counter, } -impl<'tcx> MirVisitor for StatsVisitor { +impl MirVisitor for StatsVisitor { fn visit_statement(&mut self, statement: &Statement, location: Location) { self.stmts.add(statement); // Also visit the type of expression. @@ -129,7 +130,7 @@ impl<'tcx> From<&InternalMonoItem<'tcx>> for Key { } } -impl<'tcx> From<&Statement> for Key { +impl From<&Statement> for Key { fn from(value: &Statement) -> Self { match value.kind { StatementKind::Assign(..) => Key("Assign"), @@ -150,7 +151,7 @@ impl<'tcx> From<&Statement> for Key { } } -impl<'tcx> From<&Terminator> for Key { +impl From<&Terminator> for Key { fn from(value: &Terminator) -> Self { match value.kind { TerminatorKind::Abort => Key("Abort"), @@ -168,7 +169,7 @@ impl<'tcx> From<&Terminator> for Key { } } -impl<'tcx> From<&Rvalue> for Key { +impl From<&Rvalue> for Key { fn from(value: &Rvalue) -> Self { match value { Rvalue::Use(_) => Key("Use"), From d4c51ab8a539dffc2d661fffc2e3b419b07c0982 Mon Sep 17 00:00:00 2001 From: ouz-a Date: Tue, 14 Nov 2023 22:38:19 +0300 Subject: [PATCH 3/3] use monoitems instead of internalmonoitems --- kani-compiler/src/kani_middle/analysis.rs | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index 590b92086bda..5a26fa071a19 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -25,16 +25,15 @@ use std::fmt::Display; /// - Total number of MIR instructions. pub fn print_stats<'tcx>(tcx: TyCtxt<'tcx>, items: &[InternalMonoItem<'tcx>]) { rustc_internal::run(tcx, || { + let items: Vec = items.iter().map(rustc_internal::stable).collect(); let item_types = items.iter().collect::(); let visitor = items .iter() - .filter_map(|&mono| { - if let MonoItem::Fn(instance) = rustc_internal::stable(&mono) { - Some(instance) - } else { - None - } - }) + .filter_map( + |mono| { + if let MonoItem::Fn(instance) = mono { Some(instance) } else { None } + }, + ) .fold(StatsVisitor::default(), |mut visitor, body| { visitor.visit_body(&body.body()); visitor @@ -120,12 +119,12 @@ impl> FromIterator for Counter { #[derive(Debug, Eq, Hash, PartialEq)] struct Key(pub &'static str); -impl<'tcx> From<&InternalMonoItem<'tcx>> for Key { - fn from(value: &InternalMonoItem) -> Self { +impl From<&MonoItem> for Key { + fn from(value: &stable_mir::mir::mono::MonoItem) -> Self { match value { - InternalMonoItem::Fn(_) => Key("function"), - InternalMonoItem::GlobalAsm(_) => Key("global assembly"), - InternalMonoItem::Static(_) => Key("static item"), + MonoItem::Fn(_) => Key("function"), + MonoItem::GlobalAsm(_) => Key("global assembly"), + MonoItem::Static(_) => Key("static item"), } } }