Add SMT bit-vector builtin operations

boogie_ast/src/boogie_program/mod.rs

@@ -6,14 +6,16 @@
 
 mod writer;
 
-use num_bigint::{BigInt, BigUint};
+use num_bigint::BigInt;
+use std::ops::Not;
 
 struct TypeDeclaration {}
 struct ConstDeclaration {}
 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<Type>, value: Box<Type> },
+
+ /// 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<Expr>, right: Box<Expr> },
+
+ /// Function call
+ FunctionCall { symbol: String, arguments: Vec<Expr> },
+}
+
+impl Expr {
+ pub fn literal(l: Literal) -> Self {
+ Expr::Literal(l)
+ }
+
+ pub fn function_call(symbol: String, arguments: Vec<Expr>) -> 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<String>,
  parameters: Vec<Parameter>,
  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<String>,
  parameters: Vec<Parameter>,
  return_type: Type,
  body: Option<Expr>,
  attributes: Vec<String>,
  ) -> Self {
- Function { name, parameters, return_type, body, attributes }
+ Function { name, generics, parameters, return_type, body, attributes }
  }
 }
 /// A boogie program

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<T>(lhs: T, rhs: T) returns (T);
 
 // Procedures:
 procedure main() returns (z: bool)

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();