[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;