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 12e22b98267a..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(); @@ -206,104 +206,110 @@ impl CodegenBackend for BoogieCodegenBackend { _need_metadata_module: bool, ) -> Box { let ret_val = rustc_internal::run(tcx, || { + // Queries shouldn't change today once codegen starts. + let queries = self.queries.lock().unwrap().clone(); + check_target(tcx.sess); + check_options(tcx.sess); + + // Codegen all items that need to be processed according to the selected reachability mode: + // + // - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute). + // - Tests: Generate one model per test harnesses. + // - PubFns: Generate code for all reachable logic starting from the local public functions. + // - None: Don't generate code. This is used to compile dependencies. + let base_filename = tcx.output_filenames(()).output_path(OutputType::Object); + let reachability = queries.args().reachability_analysis; + let mut results = BoogieCodegenResults::new(tcx, reachability); + match reachability { + ReachabilityType::Harnesses => { + // Cross-crate collecting of all items that are reachable from the crate harnesses. + let harnesses = queries.target_harnesses(); + let mut items: HashSet = HashSet::with_capacity(harnesses.len()); + items.extend(harnesses); + let harnesses = filter_crate_items(tcx, |_, def_id| { + items.contains(&tcx.def_path_hash(def_id)) + }); + for harness in harnesses { + let model_path = queries + .harness_model_path(&tcx.def_path_hash(harness.def_id())) + .unwrap(); + let (gcx, items) = + self.codegen_items(tcx, &[harness], model_path, &results.machine_model); + results.extend(gcx, items, None); + } + } + ReachabilityType::Tests => { + // We're iterating over crate items here, so what we have to codegen is the "test description" containing the + // test closure that we want to execute + // TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match. + let mut descriptions = vec![]; + let harnesses = filter_const_crate_items(tcx, |_, def_id| { + if is_test_harness_description(tcx, def_id) { + descriptions.push(def_id); + true + } else { + false + } + }); + // Codegen still takes a considerable amount, thus, we only generate one model for + // all harnesses and copy them for each harness. + // We will be able to remove this once we optimize all calls to CBMC utilities. + // https://github.com/model-checking/kani/issues/1971 + let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); + let (bcx, items) = + self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model); + results.extend(bcx, items, None); + + for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) { + let instance = + if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; + let metadata = + gen_test_metadata(tcx, *test_desc, *instance, &base_filename); + let test_model_path = &metadata.goto_file.as_ref().unwrap(); + std::fs::copy(&model_path, test_model_path).expect(&format!( + "Failed to copy {} to {}", + model_path.display(), + test_model_path.display() + )); + results.harnesses.push(metadata); + } + } + ReachabilityType::None => {} + ReachabilityType::PubFns => { + let entry_fn = tcx.entry_fn(()).map(|(id, _)| id); + let local_reachable = filter_crate_items(tcx, |_, def_id| { + (tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like()) + || entry_fn == Some(def_id) + }); + let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); + let (bcx, items) = self.codegen_items( + tcx, + &local_reachable, + &model_path, + &results.machine_model, + ); + results.extend(bcx, items, None); + } + } - // Queries shouldn't change today once codegen starts. - let queries = self.queries.lock().unwrap().clone(); - check_target(tcx.sess); - check_options(tcx.sess); - - // Codegen all items that need to be processed according to the selected reachability mode: - // - // - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute). - // - Tests: Generate one model per test harnesses. - // - PubFns: Generate code for all reachable logic starting from the local public functions. - // - None: Don't generate code. This is used to compile dependencies. - let base_filename = tcx.output_filenames(()).output_path(OutputType::Object); - let reachability = queries.args().reachability_analysis; - let mut results = BoogieCodegenResults::new(tcx, reachability); - match reachability { - ReachabilityType::Harnesses => { - // Cross-crate collecting of all items that are reachable from the crate harnesses. - let harnesses = queries.target_harnesses(); - let mut items: HashSet = HashSet::with_capacity(harnesses.len()); - items.extend(harnesses); - let harnesses = - filter_crate_items(tcx, |_, def_id| items.contains(&tcx.def_path_hash(def_id))); - for harness in harnesses { - let model_path = - queries.harness_model_path(&tcx.def_path_hash(harness.def_id())).unwrap(); - let (gcx, items) = - self.codegen_items(tcx, &[harness], model_path, &results.machine_model); - results.extend(gcx, items, None); - } - } - ReachabilityType::Tests => { - // We're iterating over crate items here, so what we have to codegen is the "test description" containing the - // test closure that we want to execute - // TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match. - let mut descriptions = vec![]; - let harnesses = filter_const_crate_items(tcx, |_, def_id| { - if is_test_harness_description(tcx, def_id) { - descriptions.push(def_id); - true - } else { - false - } - }); - // Codegen still takes a considerable amount, thus, we only generate one model for - // all harnesses and copy them for each harness. - // We will be able to remove this once we optimize all calls to CBMC utilities. - // https://github.com/model-checking/kani/issues/1971 - let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); - let (bcx, items) = - self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model); - results.extend(bcx, items, None); - - for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) { - let instance = - if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; - let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename); - let test_model_path = &metadata.goto_file.as_ref().unwrap(); - std::fs::copy(&model_path, test_model_path).expect(&format!( - "Failed to copy {} to {}", - model_path.display(), - test_model_path.display() - )); - results.harnesses.push(metadata); - } - } - ReachabilityType::None => {} - ReachabilityType::PubFns => { - let entry_fn = tcx.entry_fn(()).map(|(id, _)| id); - let local_reachable = filter_crate_items(tcx, |_, def_id| { - (tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like()) - || entry_fn == Some(def_id) - }); - let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); - let (bcx, items) = - self.codegen_items(tcx, &local_reachable, &model_path, &results.machine_model); - results.extend(bcx, items, None); - } - } - - if reachability != ReachabilityType::None { - // Print compilation report. - results.print_report(tcx); - - if reachability != ReachabilityType::Harnesses { - // In a workspace, cargo seems to be using the same file prefix to build a crate that is - // a package lib and also a dependency of another package. - // To avoid overriding the metadata for its verification, we skip this step when - // reachability is None, even because there is nothing to record. - write_file( - &base_filename, - ArtifactType::Metadata, - &results.generate_metadata(), - queries.args().output_pretty_json, - ); - } - } - codegen_results(tcx, rustc_metadata, &results.machine_model) + if reachability != ReachabilityType::None { + // Print compilation report. + results.print_report(tcx); + + if reachability != ReachabilityType::Harnesses { + // In a workspace, cargo seems to be using the same file prefix to build a crate that is + // a package lib and also a dependency of another package. + // To avoid overriding the metadata for its verification, we skip this step when + // reachability is None, even because there is nothing to record. + write_file( + &base_filename, + ArtifactType::Metadata, + &results.generate_metadata(), + queries.args().output_pretty_json, + ); + } + } + codegen_results(tcx, rustc_metadata, &results.machine_model) }); ret_val.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)], + ) +}