diff --git a/boogie_ast/src/boogie_program/mod.rs b/boogie_ast/src/boogie_program/mod.rs index ffd3960e10b1..14b0855d958a 100644 --- a/boogie_ast/src/boogie_program/mod.rs +++ b/boogie_ast/src/boogie_program/mod.rs @@ -6,7 +6,8 @@ mod writer; -use num_bigint::{BigInt, BigUint}; +use num_bigint::BigInt; +use std::ops::Not; struct TypeDeclaration {} struct ConstDeclaration {} @@ -14,6 +15,7 @@ struct VarDeclaration {} struct Axiom {} /// Boogie types +#[derive(Clone, Debug, PartialEq, Eq)] pub enum Type { /// Boolean Bool, @@ -26,6 +28,23 @@ pub enum Type { /// Map type, e.g. `[int]bool` Map { key: Box, value: Box }, + + /// Generic type parameter, e.g. `T` + Parameter { name: String }, +} + +impl Type { + pub fn bv(width: usize) -> Self { + Self::Bv(width) + } + + pub fn parameter(name: String) -> Self { + Self::Parameter { name } + } + + pub fn map(key: Type, value: Type) -> Self { + Self::Map { key: Box::new(key), value: Box::new(value) } + } } /// Function and procedure parameters @@ -46,12 +65,18 @@ pub enum Literal { Bool(bool), /// Bit-vector values, e.g. `5bv8` - Bv { width: usize, value: BigUint }, + Bv { width: usize, value: BigInt }, /// Unbounded integer values, e.g. `1000` or `-456789` Int(BigInt), } +impl Literal { + pub fn bv(width: usize, value: BigInt) -> Self { + Self::Bv { width, value } + } +} + /// Unary operators pub enum UnaryOp { /// Logical negation @@ -115,6 +140,27 @@ pub enum Expr { /// Binary operation BinaryOp { op: BinaryOp, left: Box, right: Box }, + + /// Function call + FunctionCall { symbol: String, arguments: Vec }, +} + +impl Expr { + pub fn literal(l: Literal) -> Self { + Expr::Literal(l) + } + + pub fn function_call(symbol: String, arguments: Vec) -> Self { + Expr::FunctionCall { symbol, arguments } + } +} + +impl Not for Expr { + type Output = Self; + + fn not(self) -> Self::Output { + Expr::UnaryOp { op: UnaryOp::Not, operand: Box::new(self) } + } } /// Statement types @@ -196,6 +242,7 @@ impl Procedure { /// effects, and whose body is an expression) pub struct Function { name: String, + generics: Vec, parameters: Vec, return_type: Type, // a body is optional (e.g. SMT built-ins) @@ -207,12 +254,13 @@ pub struct Function { impl Function { pub fn new( name: String, + generics: Vec, parameters: Vec, return_type: Type, body: Option, attributes: Vec, ) -> Self { - Function { name, parameters, return_type, body, attributes } + Function { name, generics, parameters, return_type, body, attributes } } } /// A boogie program diff --git a/boogie_ast/src/boogie_program/writer.rs b/boogie_ast/src/boogie_program/writer.rs index 3bfd5db64336..2cf18b193d2f 100644 --- a/boogie_ast/src/boogie_program/writer.rs +++ b/boogie_ast/src/boogie_program/writer.rs @@ -46,6 +46,8 @@ //! ... //! //! ``` +use num_bigint::Sign; + use crate::boogie_program::*; use std::io::Write; @@ -140,7 +142,20 @@ impl Function { for attr in &self.attributes { write!(writer, "{{{attr}}} ")?; } - write!(writer, "{}(", self.name)?; + write!(writer, "{}", self.name)?; + // generics + if !self.generics.is_empty() { + write!(writer, "<")?; + for (i, name) in self.generics.iter().enumerate() { + if i > 0 { + write!(writer, ", ")?; + } + write!(writer, "{name}")?; + } + write!(writer, ">")?; + } + // parameters + write!(writer, "(")?; for (i, param) in self.parameters.iter().enumerate() { if i > 0 { write!(writer, ", ")?; @@ -231,6 +246,16 @@ impl Expr { right.write_to(writer)?; write!(writer, ")")?; } + Expr::FunctionCall { symbol, arguments } => { + write!(writer, "{symbol}(")?; + for (i, a) in arguments.iter().enumerate() { + if i > 0 { + write!(writer, ", ")?; + } + a.write_to(writer)?; + } + write!(writer, ")")?; + } } Ok(()) } @@ -366,6 +391,7 @@ impl Type { write!(writer, "]")?; value.write_to(writer)?; } + Type::Parameter { name } => write!(writer, "{name}")?, } Ok(()) } @@ -378,7 +404,11 @@ impl Literal { write!(writer, "{}", value)?; } Literal::Bv { width, value } => { - write!(writer, "{value}bv{width}")?; + if value.sign() != Sign::Minus { + write!(writer, "{value}bv{width}")?; + } else { + todo!("Handle negative integers"); + } } Literal::Int(value) => { write!(writer, "{}", value)?; @@ -433,6 +463,7 @@ mod tests { functions: vec![ Function::new( "isZero".into(), + Vec::new(), vec![Parameter::new("x".into(), Type::Int)], Type::Bool, Some(Expr::BinaryOp { @@ -444,11 +475,12 @@ mod tests { ), Function::new( "$BvAnd".into(), + vec!["T".into()], vec![ - Parameter::new("lhs".into(), Type::Bv(32)), - Parameter::new("rhs".into(), Type::Bv(32)), + Parameter::new("lhs".into(), Type::parameter("T".into())), + Parameter::new("rhs".into(), Type::parameter("T".into())), ], - Type::Bv(32), + Type::parameter("T".into()), None, vec![":bvbuiltin \"bvand\"".into()], ), @@ -523,7 +555,7 @@ function {:inline} isZero(x: int) returns (bool) { (x == 0) } -function {:bvbuiltin \"bvand\"} $BvAnd(lhs: bv32, rhs: bv32) returns (bv32); +function {:bvbuiltin \"bvand\"} $BvAnd(lhs: T, rhs: T) returns (T); // Procedures: procedure main() returns (z: bool) diff --git a/kani-compiler/src/codegen_boogie/compiler_interface.rs b/kani-compiler/src/codegen_boogie/compiler_interface.rs index 5b27c0a16e01..f724b871217e 100644 --- a/kani-compiler/src/codegen_boogie/compiler_interface.rs +++ b/kani-compiler/src/codegen_boogie/compiler_interface.rs @@ -171,7 +171,7 @@ impl BoogieCodegenBackend { if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { let mut pb = boogie_file.to_path_buf(); pb.set_extension("bpl"); - debug!("Writing Boogie file to {}", pb.display()); + println!("Writing Boogie file to {}", pb.display()); let file = File::create(&pb).unwrap(); let mut writer = BufWriter::new(file); bcx.write(&mut writer).unwrap(); diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs index c6295caedb2e..06fd8a67f433 100644 --- a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs +++ b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs @@ -4,14 +4,16 @@ use std::io::Write; use crate::kani_queries::QueryDb; -use boogie_ast::boogie_program::{BinaryOp, BoogieProgram, Expr, Literal, Procedure, Stmt, Type}; +use boogie_ast::boogie_program::{ + BinaryOp, BoogieProgram, Expr, Literal, Procedure, Stmt, Type, UnaryOp, +}; use rustc_data_structures::fx::FxHashMap; use rustc_middle::mir::interpret::Scalar; use rustc_middle::mir::traversal::reverse_postorder; use rustc_middle::mir::{ BasicBlock, BasicBlockData, BinOp, Body, Const as mirConst, ConstOperand, ConstValue, HasLocalDecls, Local, Operand, Place, Rvalue, Statement, StatementKind, Terminator, - TerminatorKind, VarDebugInfoContents, + TerminatorKind, UnOp, VarDebugInfoContents, }; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ @@ -21,9 +23,11 @@ use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy}; use rustc_span::Span; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use std::collections::hash_map::Entry; +use strum::IntoEnumIterator; use tracing::{debug, debug_span, trace}; use super::kani_intrinsic::get_kani_intrinsic; +use super::smt_builtins::{smt_builtin_binop, SmtBvBuiltin}; /// A context that provides the main methods for translating MIR constructs to /// Boogie and stores what has been codegen so far @@ -39,7 +43,23 @@ pub struct BoogieCtx<'tcx> { impl<'tcx> BoogieCtx<'tcx> { pub fn new(tcx: TyCtxt<'tcx>, queries: QueryDb) -> BoogieCtx<'tcx> { - BoogieCtx { tcx, queries, program: BoogieProgram::new() } + let mut program = BoogieProgram::new(); + + // TODO: The current functions in the preamble should be added lazily instead + Self::add_preamble(&mut program); + + BoogieCtx { tcx, queries, program } + } + + fn add_preamble(program: &mut BoogieProgram) { + // Add SMT bv builtins + for bv_builtin in SmtBvBuiltin::iter() { + program.add_function(smt_builtin_binop( + &bv_builtin, + bv_builtin.smt_op_name(), + bv_builtin.is_predicate(), + )); + } } /// Codegen a function into a Boogie procedure. @@ -145,7 +165,8 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { trace!(typ=?ty, "codegen_type"); match ty.kind() { ty::Bool => Type::Bool, - ty::Int(_ity) => Type::Int, // TODO: use Bv + ty::Int(ity) => Type::Bv(ity.bit_width().unwrap_or(64).try_into().unwrap()), + ty::Uint(uty) => Type::Bv(uty.bit_width().unwrap_or(64).try_into().unwrap()), _ => todo!(), } } @@ -210,23 +231,88 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { debug!(rvalue=?rvalue, "codegen_rvalue"); match rvalue { Rvalue::Use(operand) => (None, self.codegen_operand(operand)), + Rvalue::UnaryOp(op, operand) => self.codegen_unary_op(op, operand), Rvalue::BinaryOp(binop, box (lhs, rhs)) => self.codegen_binary_op(binop, lhs, rhs), _ => todo!(), } } + fn codegen_unary_op(&self, op: &UnOp, operand: &Operand<'tcx>) -> (Option, Expr) { + debug!(op=?op, operand=?operand, "codegen_unary_op"); + let o = self.codegen_operand(operand); + let expr = match op { + UnOp::Not => { + // TODO: can this be used for bit-level inversion as well? + Expr::UnaryOp { op: UnaryOp::Not, operand: Box::new(o) } + } + UnOp::Neg => todo!(), + }; + (None, expr) + } + fn codegen_binary_op( &self, binop: &BinOp, lhs: &Operand<'tcx>, rhs: &Operand<'tcx>, ) -> (Option, Expr) { + debug!(binop=?binop, "codegen_binary_op"); + let left = Box::new(self.codegen_operand(lhs)); + let right = Box::new(self.codegen_operand(rhs)); let expr = match binop { - BinOp::Eq => Expr::BinaryOp { - op: BinaryOp::Eq, - left: Box::new(self.codegen_operand(lhs)), - right: Box::new(self.codegen_operand(rhs)), - }, + BinOp::Eq => Expr::BinaryOp { op: BinaryOp::Eq, left, right }, + BinOp::AddUnchecked | BinOp::Add => { + let left_type = self.operand_ty(lhs); + if self.operand_ty(rhs) != left_type { + todo!("Addition of different types is not yet supported"); + } else { + let bv_func = match left_type.kind() { + ty::Int(_) | ty::Uint(_) => SmtBvBuiltin::Add, + _ => todo!(), + }; + Expr::function_call(bv_func.as_ref().to_owned(), vec![*left, *right]) + } + } + BinOp::Lt | BinOp::Ge => { + let left_type = self.operand_ty(lhs); + assert_eq!(left_type, self.operand_ty(rhs)); + let bv_func = match left_type.kind() { + ty::Int(_) => SmtBvBuiltin::SignedLessThan, + ty::Uint(_) => SmtBvBuiltin::UnsignedLessThan, + _ => todo!(), + }; + let call = Expr::function_call(bv_func.as_ref().to_owned(), vec![*left, *right]); + if let BinOp::Lt = binop { call } else { !call } + } + BinOp::Gt | BinOp::Le => { + let left_type = self.operand_ty(lhs); + assert_eq!(left_type, self.operand_ty(rhs)); + let bv_func = match left_type.kind() { + ty::Int(_) => SmtBvBuiltin::SignedGreaterThan, + ty::Uint(_) => SmtBvBuiltin::UnsignedGreaterThan, + _ => todo!(), + }; + let call = Expr::function_call(bv_func.as_ref().to_owned(), vec![*left, *right]); + if let BinOp::Gt = binop { call } else { !call } + } + BinOp::BitAnd => { + Expr::function_call(SmtBvBuiltin::And.as_ref().to_owned(), vec![*left, *right]) + } + BinOp::BitOr => { + Expr::function_call(SmtBvBuiltin::Or.as_ref().to_owned(), vec![*left, *right]) + } + BinOp::Shr => { + let left_ty = self.operand_ty(lhs); + let right_ty = self.operand_ty(lhs); + debug!(?left_ty, ?right_ty, "codegen_binary_op_shr"); + Expr::function_call(SmtBvBuiltin::Shr.as_ref().to_owned(), vec![*left, *right]) + } + BinOp::Shl => { + let left_ty = self.operand_ty(lhs); + let right_ty = self.operand_ty(lhs); + debug!(?left_ty, ?right_ty, "codegen_binary_op_shl"); + Expr::function_call(SmtBvBuiltin::Shl.as_ref().to_owned(), vec![*left, *right]) + } _ => todo!(), }; (None, expr) @@ -343,26 +429,29 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { } fn codegen_scalar(&self, s: Scalar, ty: Ty<'tcx>) -> Expr { + debug!(kind=?ty.kind(), "codegen_scalar"); match (s, ty.kind()) { (Scalar::Int(_), ty::Bool) => Expr::Literal(Literal::Bool(s.to_bool().unwrap())), (Scalar::Int(_), ty::Int(it)) => match it { - IntTy::I8 => Expr::Literal(Literal::Int(s.to_i8().unwrap().into())), - IntTy::I16 => Expr::Literal(Literal::Int(s.to_i16().unwrap().into())), - IntTy::I32 => Expr::Literal(Literal::Int(s.to_i32().unwrap().into())), - IntTy::I64 => Expr::Literal(Literal::Int(s.to_i64().unwrap().into())), - IntTy::I128 => Expr::Literal(Literal::Int(s.to_i128().unwrap().into())), + IntTy::I8 => Expr::Literal(Literal::bv(8, s.to_i8().unwrap().into())), + IntTy::I16 => Expr::Literal(Literal::bv(16, s.to_i16().unwrap().into())), + IntTy::I32 => Expr::Literal(Literal::bv(32, s.to_i32().unwrap().into())), + IntTy::I64 => Expr::Literal(Literal::bv(64, s.to_i64().unwrap().into())), + IntTy::I128 => Expr::Literal(Literal::bv(128, s.to_i128().unwrap().into())), IntTy::Isize => { - Expr::Literal(Literal::Int(s.to_target_isize(self).unwrap().into())) + // TODO: get target width + Expr::Literal(Literal::bv(64, s.to_target_isize(self).unwrap().into())) } }, (Scalar::Int(_), ty::Uint(it)) => match it { - UintTy::U8 => Expr::Literal(Literal::Int(s.to_u8().unwrap().into())), - UintTy::U16 => Expr::Literal(Literal::Int(s.to_u16().unwrap().into())), - UintTy::U32 => Expr::Literal(Literal::Int(s.to_u32().unwrap().into())), - UintTy::U64 => Expr::Literal(Literal::Int(s.to_u64().unwrap().into())), - UintTy::U128 => Expr::Literal(Literal::Int(s.to_u128().unwrap().into())), + UintTy::U8 => Expr::Literal(Literal::bv(8, s.to_u8().unwrap().into())), + UintTy::U16 => Expr::Literal(Literal::bv(16, s.to_u16().unwrap().into())), + UintTy::U32 => Expr::Literal(Literal::bv(32, s.to_u32().unwrap().into())), + UintTy::U64 => Expr::Literal(Literal::bv(64, s.to_u64().unwrap().into())), + UintTy::U128 => Expr::Literal(Literal::bv(128, s.to_u128().unwrap().into())), UintTy::Usize => { - Expr::Literal(Literal::Int(s.to_target_isize(self).unwrap().into())) + // TODO: get target width + Expr::Literal(Literal::bv(64, s.to_target_usize(self).unwrap().into())) } }, _ => todo!(), diff --git a/kani-compiler/src/codegen_boogie/context/mod.rs b/kani-compiler/src/codegen_boogie/context/mod.rs index 76a198335ec1..42fac0b9c9c5 100644 --- a/kani-compiler/src/codegen_boogie/context/mod.rs +++ b/kani-compiler/src/codegen_boogie/context/mod.rs @@ -6,5 +6,6 @@ mod boogie_ctx; mod kani_intrinsic; +mod smt_builtins; pub use boogie_ctx::BoogieCtx; diff --git a/kani-compiler/src/codegen_boogie/context/smt_builtins.rs b/kani-compiler/src/codegen_boogie/context/smt_builtins.rs new file mode 100644 index 000000000000..3526c8dff520 --- /dev/null +++ b/kani-compiler/src/codegen_boogie/context/smt_builtins.rs @@ -0,0 +1,85 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use boogie_ast::boogie_program::{Function, Parameter, Type}; + +/// SMT bit-vector builtin operations, i.e. operations that SMT solvers (e.g. +/// Z3) understand +/// See https://smtlib.cs.uiowa.edu/logics-all.shtml for more details +#[derive(Debug, Clone, PartialEq, Eq, strum_macros::AsRefStr, strum_macros::EnumIter)] +pub(crate) enum SmtBvBuiltin { + // Predicates: + #[strum(serialize = "$BvUnsignedLessThan")] + UnsignedLessThan, + #[strum(serialize = "$BvSignedLessThan")] + SignedLessThan, + #[strum(serialize = "$BvUnsignedGreaterThan")] + UnsignedGreaterThan, + #[strum(serialize = "$BvSignedGreaterThan")] + SignedGreaterThan, + + // Binary operators: + #[strum(serialize = "$BvAdd")] + Add, + #[strum(serialize = "$BvOr")] + Or, + #[strum(serialize = "$BvAnd")] + And, + #[strum(serialize = "$BvShl")] + Shl, + #[strum(serialize = "$BvShr")] + Shr, +} + +impl SmtBvBuiltin { + /// The name of the SMT function corresponding to this bit-vector operation + pub fn smt_op_name(&self) -> &'static str { + match self { + SmtBvBuiltin::UnsignedLessThan => "bvult", + SmtBvBuiltin::SignedLessThan => "bvslt", + SmtBvBuiltin::UnsignedGreaterThan => "bvugt", + SmtBvBuiltin::SignedGreaterThan => "bvsgt", + SmtBvBuiltin::Add => "bvadd", + SmtBvBuiltin::Or => "bvor", + SmtBvBuiltin::And => "bvand", + SmtBvBuiltin::Shl => "bvshl", + SmtBvBuiltin::Shr => "bvlshr", + } + } + + /// Whether the builtin is a predicate (i.e. it returns a boolean) + pub fn is_predicate(&self) -> bool { + match self { + SmtBvBuiltin::UnsignedLessThan + | SmtBvBuiltin::SignedLessThan + | SmtBvBuiltin::UnsignedGreaterThan + | SmtBvBuiltin::SignedGreaterThan => true, + SmtBvBuiltin::Or + | SmtBvBuiltin::And + | SmtBvBuiltin::Add + | SmtBvBuiltin::Shl + | SmtBvBuiltin::Shr => false, + } + } +} + +/// Create a Boogie function for the given SMT bit-vector builtin +/// The function has no body, and is annotated with the SMT annotation +/// `:bvbuiltin "smt_name"` where `smt_name` is the SMT name of the bit-vector +/// builtin +pub(crate) fn smt_builtin_binop( + bv_builtin: &SmtBvBuiltin, + smt_name: &str, + is_predicate: bool, +) -> Function { + let tp_name = String::from("T"); + let tp = Type::parameter(tp_name.clone()); + Function::new( + bv_builtin.as_ref().to_string(), // e.g. $BvOr + vec![tp_name], + vec![Parameter::new("lhs".into(), tp.clone()), Parameter::new("rhs".into(), tp.clone())], + if is_predicate { Type::Bool } else { tp }, + None, + vec![format!(":bvbuiltin \"{}\"", smt_name)], + ) +}