Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Introduce a function context #2891

Merged
merged 1 commit into from
Nov 27, 2023
Merged

Introduce a function context #2891

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
134 changes: 61 additions & 73 deletions kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
View file
Open in desktop
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
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
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
Open in desktop
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
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
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
Loading