Introduce a function context

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<String>,
 }
 
 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<Procedure> {
  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<Stmt> {
- 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<T: 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<Stmt> {
+ let ldecls = self.mir.local_decls();
  let decls: Vec<Stmt> = 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<Stmt> = reverse_postorder(mir)
- .map(|(bb, bbd)| self.codegen_block(mir.local_decls(), bb, bbd))
- .collect();
+ fn codegen_body(&self) -> Stmt {
+ let statements: Vec<Stmt> =
+ 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<Stmt> =
  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,42 +191,40 @@ 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!(),
  }
  }
 
  fn codegen_funcall(
  &self,
- local_decls: &LocalDecls<'tcx>,
  func: &Operand<'tcx>,
  args: &[Operand<'tcx>],
  destination: &Place<'tcx>,
  target: &Option<BasicBlock>,
  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<Expr> {
+ fn codegen_funcall_args(&self, args: &[Operand<'tcx>]) -> Vec<Expr> {
  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,47 +324,35 @@ impl<'tcx> BoogieCtx<'tcx> {
  }
  }
 
- /// Write the program to the given writer
- pub fn write<T: 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>) -> ! {
  span_bug!(span, "failed to get layout for `{}`: {}", ty, err)
  }
 }
 
-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()
  }
 }
 

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<KaniIntrinsic> {
-  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<KaniIntrinsic> {
+ 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,