Add missing implementation for functions in Boogie AST

boogie_ast/src/boogie_program/mod.rs

@@ -34,6 +34,12 @@ pub struct Parameter {
  typ: Type,
 }
 
+impl Parameter {
+ pub fn new(name: String, typ: Type) -> Self {
+ Self { name, typ }
+ }
+}
+
 /// Literal types
 pub enum Literal {
  /// Boolean values: `true`/`false`
@@ -188,8 +194,27 @@ impl Procedure {
 /// Function definition
 /// A function in Boogie is a mathematical function (deterministic, has no side
 /// effects, and whose body is an expression)
-struct Function {}
+pub struct Function {
+ name: String,
+ parameters: Vec<Parameter>,
+ return_type: Type,
+ // a body is optional (e.g. SMT built-ins)
+ body: Option<Expr>,
+ // Boogie attributes, e.g. `{:bvbuiltin "bvnot}`
+ attributes: Vec<String>,
+}
 
+impl Function {
+ pub fn new(
+ name: String,
+ parameters: Vec<Parameter>,
+ return_type: Type,
+ body: Option<Expr>,
+ attributes: Vec<String>,
+ ) -> Self {
+ Function { name, parameters, return_type, body, attributes }
+ }
+}
 /// A boogie program
 pub struct BoogieProgram {
  type_declarations: Vec<TypeDeclaration>,
@@ -215,4 +240,8 @@ impl BoogieProgram {
  pub fn add_procedure(&mut self, procedure: Procedure) {
  self.procedures.push(procedure);
  }
+
+ pub fn add_function(&mut self, function: Function) {
+ self.functions.push(function);
+ }
 }

boogie_ast/src/boogie_program/writer.rs

@@ -118,8 +118,8 @@ impl BoogieProgram {
  }
  if !self.functions.is_empty() {
  writeln!(writer, "// Functions:")?;
- for _f in &self.functions {
- todo!()
+ for f in &self.functions {
+ f.write_to(&mut writer)?;
  }
  }
  if !self.procedures.is_empty() {
@@ -132,6 +132,41 @@ impl BoogieProgram {
  }
 }
 
+impl Function {
+ fn write_to<T: Write>(&self, writer: &mut Writer<T>) -> std::io::Result<()> {
+ // signature
+ write!(writer, "function ")?;
+ // attributes
+ for attr in &self.attributes {
+ write!(writer, "{{{attr}}} ")?;
+ }
+ write!(writer, "{}(", self.name)?;
+ for (i, param) in self.parameters.iter().enumerate() {
+ if i > 0 {
+ write!(writer, ", ")?;
+ }
+ write!(writer, "{}: ", param.name)?;
+ param.typ.write_to(writer)?;
+ }
+ write!(writer, ") returns (")?;
+ self.return_type.write_to(writer)?;
+ write!(writer, ")")?;
+ if let Some(body) = &self.body {
+ writeln!(writer, " {{")?;
+ writer.increase_indent();
+ writer.indent()?;
+ body.write_to(writer)?;
+ writer.decrease_indent();
+ writer.newline()?;
+ writeln!(writer, "}}")?;
+ } else {
+ writeln!(writer, ";")?;
+ }
+ writer.newline()?;
+ Ok(())
+ }
+}
+
 impl Procedure {
  fn write_to<T: Write>(&self, writer: &mut Writer<T>) -> std::io::Result<()> {
  // signature
@@ -395,7 +430,29 @@ mod tests {
  const_declarations: Vec::new(),
  var_declarations: Vec::new(),
  axioms: Vec::new(),
- functions: Vec::new(),
+ functions: vec![
+ Function::new(
+ "isZero".into(),
+ vec![Parameter::new("x".into(), Type::Int)],
+ Type::Bool,
+ Some(Expr::BinaryOp {
+ op: BinaryOp::Eq,
+ left: Box::new(Expr::Symbol { name: "x".into() }),
+ right: Box::new(Expr::Literal(Literal::Int(0.into()))),
+ }),
+ vec![":inline".into()],
+ ),
+ Function::new(
+ "$BvAnd".into(),
+ vec![
+ Parameter::new("lhs".into(), Type::Bv(32)),
+ Parameter::new("rhs".into(), Type::Bv(32)),
+ ],
+ Type::Bv(32),
+ None,
+ vec![":bvbuiltin \"bvand\"".into()],
+ ),
+ ],
  procedures: vec![Procedure {
  name: "main".to_string(),
  parameters: Vec::new(),
@@ -461,6 +518,13 @@ mod tests {
 
  let expected = String::from(
  "\
+// Functions:
+function {:inline} isZero(x: int) returns (bool) {
+ (x == 0)
+}
+
+function {:bvbuiltin \"bvand\"} $BvAnd(lhs: bv32, rhs: bv32) returns (bv32);
+
 // Procedures:
 procedure main() returns (z: bool)
  ensures (z == true);