diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs index 32c947ee8297..a52ec87ee19b 100644 --- a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs +++ b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs @@ -8,8 +8,8 @@ use boogie_ast::boogie_program::{BinaryOp, BoogieProgram, Expr, Literal, Procedu use rustc_middle::mir::interpret::Scalar; use rustc_middle::mir::traversal::reverse_postorder; use rustc_middle::mir::{ - BasicBlock, BasicBlockData, BinOp, Const as mirConst, ConstOperand, ConstValue, HasLocalDecls, - Local, LocalDecls, Operand, Place, Rvalue, Statement, StatementKind, Terminator, + BasicBlock, BasicBlockData, BinOp, Body, Const as mirConst, ConstOperand, ConstValue, + HasLocalDecls, Local, Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, }; use rustc_middle::span_bug; @@ -19,10 +19,9 @@ use rustc_middle::ty::layout::{ use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy}; use rustc_span::Span; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use strum::VariantNames; use tracing::{debug, debug_span, trace}; -use super::kani_intrinsic::KaniIntrinsic; +use super::kani_intrinsic::get_kani_intrinsic; /// A context that provides the main methods for translating MIR constructs to /// Boogie and stores what has been codegen so far @@ -34,30 +33,24 @@ pub struct BoogieCtx<'tcx> { pub queries: QueryDb, /// the Boogie program program: BoogieProgram, - /// Kani intrinsics - pub intrinsics: Vec, } impl<'tcx> BoogieCtx<'tcx> { pub fn new(tcx: TyCtxt<'tcx>, queries: QueryDb) -> BoogieCtx<'tcx> { - BoogieCtx { - tcx, - queries, - program: BoogieProgram::new(), - intrinsics: KaniIntrinsic::VARIANTS.iter().map(|s| (*s).into()).collect(), - } + BoogieCtx { tcx, queries, program: BoogieProgram::new() } } /// Codegen a function into a Boogie procedure. /// Returns `None` if the function is a hook. pub fn codegen_function(&self, instance: Instance<'tcx>) -> Option { debug!(?instance, "boogie_codegen_function"); - if self.kani_intrinsic(instance).is_some() { + if get_kani_intrinsic(self.tcx, instance).is_some() { debug!("skipping kani intrinsic `{instance}`"); return None; } - let mut decl = self.codegen_declare_variables(instance); - let body = self.codegen_body(instance); + let fcx = FunctionCtx::new(self, instance); + let mut decl = fcx.codegen_declare_variables(); + let body = fcx.codegen_body(); decl.push(body); Some(Procedure::new( self.tcx.symbol_name(instance).name.to_string(), @@ -68,9 +61,29 @@ impl<'tcx> BoogieCtx<'tcx> { )) } - fn codegen_declare_variables(&self, instance: Instance<'tcx>) -> Vec { - let mir = self.tcx.instance_mir(instance.def); - let ldecls = mir.local_decls(); + pub fn add_procedure(&mut self, procedure: Procedure) { + self.program.add_procedure(procedure); + } + + /// Write the program to the given writer + pub fn write(&self, writer: &mut T) -> std::io::Result<()> { + self.program.write_to(writer)?; + Ok(()) + } +} + +pub(crate) struct FunctionCtx<'a, 'tcx> { + bcx: &'a BoogieCtx<'tcx>, + mir: &'a Body<'tcx>, +} + +impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { + pub fn new(bcx: &'a BoogieCtx<'tcx>, instance: Instance<'tcx>) -> FunctionCtx<'a, 'tcx> { + Self { bcx, mir: bcx.tcx.instance_mir(instance.def) } + } + + fn codegen_declare_variables(&self) -> Vec { + let ldecls = self.mir.local_decls(); let decls: Vec = ldecls .indices() .enumerate() @@ -97,34 +110,27 @@ impl<'tcx> BoogieCtx<'tcx> { } } - fn codegen_body(&self, instance: Instance<'tcx>) -> Stmt { - let mir = self.tcx.instance_mir(instance.def); - let statements: Vec = reverse_postorder(mir) - .map(|(bb, bbd)| self.codegen_block(mir.local_decls(), bb, bbd)) - .collect(); + fn codegen_body(&self) -> Stmt { + let statements: Vec = + reverse_postorder(self.mir).map(|(bb, bbd)| self.codegen_block(bb, bbd)).collect(); Stmt::Block { statements } } - fn codegen_block( - &self, - local_decls: &LocalDecls<'tcx>, - bb: BasicBlock, - bbd: &BasicBlockData<'tcx>, - ) -> Stmt { + fn codegen_block(&self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) -> Stmt { debug!(?bb, ?bbd, "codegen_block"); // the first statement should be labelled. if there is no statements, then the // terminator should be labelled. let statements = match bbd.statements.len() { 0 => { let term = bbd.terminator(); - let tcode = self.codegen_terminator(local_decls, term); + let tcode = self.codegen_terminator(term); vec![tcode] } _ => { let mut statements: Vec = bbd.statements.iter().map(|stmt| self.codegen_statement(stmt)).collect(); - let term = self.codegen_terminator(local_decls, bbd.terminator()); + let term = self.codegen_terminator(bbd.terminator()); statements.push(term); statements } @@ -185,18 +191,13 @@ impl<'tcx> BoogieCtx<'tcx> { (None, expr) } - fn codegen_terminator(&self, local_decls: &LocalDecls<'tcx>, term: &Terminator<'tcx>) -> Stmt { + fn codegen_terminator(&self, term: &Terminator<'tcx>) -> Stmt { let _trace_span = debug_span!("CodegenTerminator", statement = ?term.kind).entered(); debug!("handling terminator {:?}", term); match &term.kind { - TerminatorKind::Call { func, args, destination, target, .. } => self.codegen_funcall( - local_decls, - func, - args, - destination, - target, - term.source_info.span, - ), + TerminatorKind::Call { func, args, destination, target, .. } => { + self.codegen_funcall(func, args, destination, target, term.source_info.span) + } TerminatorKind::Return => Stmt::Return, _ => todo!(), } @@ -204,7 +205,6 @@ impl<'tcx> BoogieCtx<'tcx> { fn codegen_funcall( &self, - local_decls: &LocalDecls<'tcx>, func: &Operand<'tcx>, args: &[Operand<'tcx>], destination: &Place<'tcx>, @@ -212,15 +212,19 @@ impl<'tcx> BoogieCtx<'tcx> { span: Span, ) -> Stmt { debug!(?func, ?args, ?destination, ?span, "codegen_funcall"); - let fargs = self.codegen_funcall_args(local_decls, args); - let funct = self.operand_ty(local_decls, func); + let fargs = self.codegen_funcall_args(args); + let funct = self.operand_ty(func); // TODO: Only Kani intrinsics are handled currently match &funct.kind() { ty::FnDef(defid, substs) => { - let instance = - Instance::expect_resolve(self.tcx, ty::ParamEnv::reveal_all(), *defid, substs); - - if let Some(intrinsic) = self.kani_intrinsic(instance) { + let instance = Instance::expect_resolve( + self.tcx(), + ty::ParamEnv::reveal_all(), + *defid, + substs, + ); + + if let Some(intrinsic) = get_kani_intrinsic(self.tcx(), instance) { return self.codegen_kani_intrinsic( intrinsic, instance, @@ -236,15 +240,11 @@ impl<'tcx> BoogieCtx<'tcx> { } } - fn codegen_funcall_args( - &self, - local_decls: &LocalDecls<'tcx>, - args: &[Operand<'tcx>], - ) -> Vec { + fn codegen_funcall_args(&self, args: &[Operand<'tcx>]) -> Vec { debug!(?args, "codegen_funcall_args"); args.iter() .filter_map(|o| { - let ty = self.operand_ty(local_decls, o); + let ty = self.operand_ty(o); // TODO: handle non-primitive types if ty.is_primitive() { return Some(self.codegen_operand(o)); @@ -324,19 +324,13 @@ impl<'tcx> BoogieCtx<'tcx> { } } - /// Write the program to the given writer - pub fn write(&self, writer: &mut T) -> std::io::Result<()> { - self.program.write_to(writer)?; - Ok(()) - } - - fn operand_ty(&self, local_decls: &LocalDecls<'tcx>, o: &Operand<'tcx>) -> Ty<'tcx> { + fn operand_ty(&self, o: &Operand<'tcx>) -> Ty<'tcx> { // TODO: monomorphize - o.ty(local_decls, self.tcx) + o.ty(self.mir.local_decls(), self.bcx.tcx) } } -impl<'tcx> LayoutOfHelpers<'tcx> for BoogieCtx<'tcx> { +impl<'a, 'tcx> LayoutOfHelpers<'tcx> for FunctionCtx<'a, 'tcx> { type LayoutOfResult = TyAndLayout<'tcx>; fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: Ty<'tcx>) -> ! { @@ -344,27 +338,21 @@ impl<'tcx> LayoutOfHelpers<'tcx> for BoogieCtx<'tcx> { } } -impl<'tcx> HasParamEnv<'tcx> for BoogieCtx<'tcx> { +impl<'a, 'tcx> HasParamEnv<'tcx> for FunctionCtx<'a, 'tcx> { fn param_env(&self) -> ty::ParamEnv<'tcx> { ty::ParamEnv::reveal_all() } } -impl<'tcx> HasTyCtxt<'tcx> for BoogieCtx<'tcx> { +impl<'a, 'tcx> HasTyCtxt<'tcx> for FunctionCtx<'a, 'tcx> { fn tcx(&self) -> TyCtxt<'tcx> { - self.tcx + self.bcx.tcx } } -impl<'tcx> HasDataLayout for BoogieCtx<'tcx> { +impl<'a, 'tcx> HasDataLayout for FunctionCtx<'a, 'tcx> { fn data_layout(&self) -> &TargetDataLayout { - self.tcx.data_layout() - } -} - -impl<'tcx> BoogieCtx<'tcx> { - pub fn add_procedure(&mut self, procedure: Procedure) { - self.program.add_procedure(procedure); + self.bcx.tcx.data_layout() } } diff --git a/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs b/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs index 1411b88350ed..38c4bc4ce738 100644 --- a/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs +++ b/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs @@ -5,11 +5,11 @@ //! is defined in the Kani compiler. These items are defined in the `kani` //! library and are annotated with a `rustc_diagnostic_item`. -use crate::codegen_boogie::BoogieCtx; +use super::boogie_ctx::FunctionCtx; use boogie_ast::boogie_program::{Expr, Stmt}; use rustc_middle::mir::{BasicBlock, Place}; -use rustc_middle::ty::Instance; +use rustc_middle::ty::{Instance, TyCtxt}; use rustc_span::Span; use std::str::FromStr; use strum::VariantNames; @@ -26,23 +26,25 @@ pub enum KaniIntrinsic { KaniAssume, } -impl<'tcx> BoogieCtx<'tcx> { - /// If provided function is a Kani intrinsic (e.g. assert, assume, cover), returns it - // TODO: move this function up to `kani_middle` along with the enum - pub fn kani_intrinsic(&self, instance: Instance<'tcx>) -> Option { - let intrinsics = KaniIntrinsic::VARIANTS; - for intrinsic in intrinsics { - let attr_sym = rustc_span::symbol::Symbol::intern(intrinsic); - if let Some(attr_id) = self.tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) { - if instance.def.def_id() == *attr_id { - debug!("matched: {:?} {:?}", attr_id, attr_sym); - return Some(KaniIntrinsic::from_str(intrinsic).unwrap()); - } +/// If provided function is a Kani intrinsic (e.g. assert, assume, cover), returns it +// TODO: move this function up to `kani_middle` along with the enum +pub fn get_kani_intrinsic<'tcx>( + tcx: TyCtxt<'tcx>, + instance: Instance<'tcx>, +) -> Option { + for intrinsic in KaniIntrinsic::VARIANTS { + let attr_sym = rustc_span::symbol::Symbol::intern(intrinsic); + if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) { + if instance.def.def_id() == *attr_id { + debug!("matched: {:?} {:?}", attr_id, attr_sym); + return Some(KaniIntrinsic::from_str(intrinsic).unwrap()); } } - None } + None +} +impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { pub fn codegen_kani_intrinsic( &self, intrinsic: KaniIntrinsic,