Skip to content

Commit

Permalink
Introduce a function context
Browse files Browse the repository at this point in the history
  • Loading branch information
@zhassan-aws
zhassan-aws committed Nov 22, 2023
1 parent dd0e36b commit 6597131
Show file tree
Hide file tree
Showing 2 changed files with 77 additions and 79 deletions.
124 changes: 60 additions & 64 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 @@ -22,7 +22,7 @@ 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, KaniIntrinsic};

/// A context that provides the main methods for translating MIR constructs to
/// Boogie and stores what has been codegen so far
Expand Down Expand Up @@ -52,12 +52,13 @@ impl<'tcx> BoogieCtx<'tcx> {
/// 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 +69,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 +118,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 +199,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 +248,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 +332,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 6597131

Please sign in to comment.