[Boogie Backend] Add an unbounded array API (#2955)

This PR adds an API for creating arrays with non-deterministic content
and length. The array is implemented as a Boogie datatype with a data
field (a Boogie map), and a length field (a bitvector).

The PR also adds a test that demonstrates how the API can be used for
performing unbounded verification.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

boogie_ast/src/boogie_program/mod.rs

@@ -8,6 +8,7 @@ mod writer;
 
 use num_bigint::BigInt;
 use std::ops::Not;
+use std::string::ToString;
 
 struct TypeDeclaration {}
 struct ConstDeclaration {}
@@ -69,6 +70,7 @@ impl Parameter {
 }
 
 /// Literal types
+#[derive(Clone, Debug, PartialEq, Eq)]
 pub enum Literal {
  /// Boolean values: `true`/`false`
  Bool(bool),
@@ -87,6 +89,7 @@ impl Literal {
 }
 
 /// Unary operators
+#[derive(Clone, Debug, PartialEq, Eq)]
 pub enum UnaryOp {
  /// Logical negation
  Not,
@@ -95,6 +98,7 @@ pub enum UnaryOp {
  Neg,
 }
 
+#[derive(Clone, Debug, PartialEq, Eq)]
 pub enum BinaryOp {
  /// Logical AND
  And,
@@ -137,6 +141,7 @@ pub enum BinaryOp {
 }
 
 /// Expr types
+#[derive(Clone, Debug, PartialEq, Eq)]
 pub enum Expr {
  /// Literal (constant)
  Literal(Literal),
@@ -152,6 +157,12 @@ pub enum Expr {
 
  /// Function call
  FunctionCall { symbol: String, arguments: Vec<Expr> },
+
+ /// Field operator for datatypes
+ Field { base: Box<Expr>, field: String },
+
+ /// Select operation for maps
+ Select { base: Box<Expr>, key: Box<Expr> },
 }
 
 impl Expr {
@@ -164,6 +175,12 @@ impl Expr {
  }
 }
 
+impl ToString for Expr {
+ fn to_string(&self) -> String {
+ writer::write_expr(self)
+ }
+}
+
 impl Not for Expr {
  type Output = Self;
 
@@ -184,7 +201,7 @@ pub enum Stmt {
  Assume { condition: Expr },
 
  /// Statement block: `{ statements }`
- Block { statements: Vec<Stmt> },
+ Block { label: Option<String>, statements: Vec<Stmt> },
 
  /// Break statement: `break;`
  /// A `break` in boogie can take a label, but this is probably not needed
@@ -196,22 +213,35 @@ pub enum Stmt {
  /// Declaration statement: `var name: type;`
  Decl { name: String, typ: Type },
 
+ /// Havoc statement: `havoc x;`
+ Havoc { name: String },
+
  /// If statement: `if (condition) { body } else { else_body }`
  If { condition: Expr, body: Box<Stmt>, else_body: Option<Box<Stmt>> },
 
  /// Goto statement: `goto label;`
  Goto { label: String },
 
- /// Label statement: `label:`
- Label { label: String },
-
  /// Return statement: `return;`
  Return,
 
+ /// Skip statement
+ Skip,
+
  /// While statement: `while (condition) { body }`
  While { condition: Expr, body: Box<Stmt> },
 }
 
+impl Stmt {
+ pub fn block(statements: Vec<Stmt>) -> Self {
+ Self::Block { label: None, statements }
+ }
+
+ pub fn labelled_block(label: String, statements: Vec<Stmt>) -> Self {
+ Self::Block { label: Some(label), statements }
+ }
+}
+
 /// A Boogie datatype. A datatype is defined by one or more constructors.
 /// See https://github.com/boogie-org/boogie/pull/685 for more details.
 pub struct DataType {

boogie_ast/src/boogie_program/writer.rs

@@ -310,6 +310,16 @@ impl Expr {
  }
  write!(writer, ")")?;
  }
+ Expr::Field { base, field } => {
+ base.write_to(writer)?;
+ write!(writer, "->{field}")?;
+ }
+ Expr::Select { base, key } => {
+ base.write_to(writer)?;
+ write!(writer, "[(")?;
+ key.write_to(writer)?;
+ write!(writer, ")]")?;
+ }
  }
  Ok(())
  }
@@ -336,7 +346,12 @@ impl Stmt {
  condition.write_to(writer)?;
  writeln!(writer, ";")?;
  }
- Stmt::Block { statements } => {
+ Stmt::Block { label, statements } => {
+ if let Some(label) = label {
+ writer.indent()?;
+ write!(writer, "{label}:")?;
+ writeln!(writer)?;
+ }
  for s in statements {
  s.write_to(writer)?;
  }
@@ -362,6 +377,10 @@ impl Stmt {
  typ.write_to(writer)?;
  writeln!(writer, ";")?;
  }
+ Stmt::Havoc { name } => {
+ writer.indent()?;
+ writeln!(writer, "havoc {}; ", name)?;
+ }
  Stmt::If { condition, body, else_body } => {
  writer.indent()?;
  write!(writer, "if (")?;
@@ -386,14 +405,11 @@ impl Stmt {
  writer.indent()?;
  writeln!(writer, "goto {label};")?;
  }
- Stmt::Label { label } => {
- writer.indent()?;
- writeln!(writer, "{label}:")?;
- }
  Stmt::Return => {
  writer.indent()?;
  writeln!(writer, "return;")?;
  }
+ Stmt::Skip => {}
  Stmt::While { condition, body } => {
  writer.indent()?;
  write!(writer, "while (")?;
@@ -510,6 +526,13 @@ impl BinaryOp {
  }
 }
 
+pub fn write_expr(e: &Expr) -> String {
+ let mut buf = Vec::new();
+ let mut writer = writer::Writer::new(&mut buf);
+ e.write_to(&mut writer).unwrap();
+ String::from_utf8(buf).unwrap()
+}
+
 #[cfg(test)]
 mod tests {
  use super::*;
@@ -571,6 +594,7 @@ mod tests {
  modifies: Vec::new(),
  }),
  body: Stmt::Block {
+ label: Some("label1".into()),
  statements: vec![
  Stmt::Decl { name: "x".to_string(), typ: Type::Int },
  Stmt::Decl { name: "y".to_string(), typ: Type::Int },
@@ -643,6 +667,7 @@ function {:bvbuiltin \"bvand\"} $BvAnd<T>(lhs: T, rhs: T) returns (T);
 procedure main() returns (z: bool)
  ensures (z == true);
 {
+ label1:
  var x: int;
  var y: int;
  var p: Pair bool int;