Skip to content

Commit

Permalink
Introduce a function context (#2891)
Browse files Browse the repository at this point in the history 
This is a refactoring PR that introduces a function context, and moves
all the codegen functions from the Boogie context to the new function
context.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
@zhassan-aws
zhassan-aws committed Dec 19, 2023
1 parent dbd5cd1 commit a8724be
Show file tree
Hide file tree
Showing 2 changed files with 78 additions and 88 deletions.
134 changes: 61 additions & 73 deletions kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
Expand All @@ -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(),
Expand All @@ -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()
Expand All @@ -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
}
Expand Down Expand Up @@ -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,
Expand All @@ -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));
Expand Down Expand Up @@ -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()
}
}

Expand Down
32 changes: 17 additions & 15 deletions kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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,
Expand Down

0 comments on commit a8724be

Please sign in to comment.