[Boogie Backend] Add datatypes to Boogie AST (#2949)

Add datatypes to the Boogie AST. Datatypes can be used to model structs,
tuples, etc.

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

@@ -31,6 +31,11 @@ pub enum Type {
 
     /// Generic type parameter, e.g. `T`
     Parameter { name: String },
+
+    /// A user-defined type, e.g. using `type` or `datatype`
+    /// The arguments to generic type parameters are stored in the
+    /// `type_arguments` field.
+    UserDefined { name: String, type_arguments: Vec<Type> },
 }
 
 impl Type {
@@ -45,6 +50,10 @@ impl Type {
     pub fn map(key: Type, value: Type) -> Self {
         Self::Map { key: Box::new(key), value: Box::new(value) }
     }
+
+    pub fn user_defined(name: String, type_arguments: Vec<Type>) -> Self {
+        Self::UserDefined { name, type_arguments }
+    }
 }
 
 /// Function and procedure parameters
@@ -203,6 +212,37 @@ pub enum Stmt {
     While { condition: Expr, body: Box<Stmt> },
 }
 
+/// 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 {
+    name: String,
+    type_parameters: Vec<String>,
+    constructors: Vec<DataTypeConstructor>,
+}
+
+impl DataType {
+    pub fn new(
+        name: String,
+        type_parameters: Vec<String>,
+        constructors: Vec<DataTypeConstructor>,
+    ) -> Self {
+        Self { name, type_parameters, constructors }
+    }
+}
+
+/// A constructor for a datatype. A constructor has a name and zero or more
+/// parameters.
+pub struct DataTypeConstructor {
+    name: String,
+    parameters: Vec<Parameter>,
+}
+
+impl DataTypeConstructor {
+    pub fn new(name: String, parameters: Vec<Parameter>) -> Self {
+        Self { name, parameters }
+    }
+}
+
 /// Contract specification
 pub struct Contract {
     /// Pre-conditions
@@ -269,6 +309,7 @@ pub struct BoogieProgram {
     const_declarations: Vec<ConstDeclaration>,
     var_declarations: Vec<VarDeclaration>,
     axioms: Vec<Axiom>,
+    datatypes: Vec<DataType>,
     functions: Vec<Function>,
     procedures: Vec<Procedure>,
 }
@@ -280,6 +321,7 @@ impl BoogieProgram {
             const_declarations: Vec::new(),
             var_declarations: Vec::new(),
             axioms: Vec::new(),
+            datatypes: Vec::new(),
             functions: Vec::new(),
             procedures: Vec::new(),
         }
@@ -292,4 +334,8 @@ impl BoogieProgram {
     pub fn add_function(&mut self, function: Function) {
         self.functions.push(function);
     }
+
+    pub fn add_datatype(&mut self, datatype: DataType) {
+        self.datatypes.push(datatype);
+    }
 }

boogie_ast/src/boogie_program/writer.rs

@@ -24,6 +24,10 @@
 //! axiom <expr2>;
 //! ...
 //!
+//! // Datatypes:
+//! datatype <datatype-name> = <constructor1, constructor2, ...>;
+//! ...
+//!
 //! // Functions:
 //! function <function1-name>(<arg1>: <type1>, ...) returns (return-var-name: <return-type>)
 //! {
@@ -118,6 +122,12 @@ impl BoogieProgram {
                 todo!()
             }
         }
+        if !self.datatypes.is_empty() {
+            writeln!(writer, "// Datatypes:")?;
+            for d in &self.datatypes {
+                d.write_to(&mut writer)?;
+            }
+        }
         if !self.functions.is_empty() {
             writeln!(writer, "// Functions:")?;
             for f in &self.functions {
@@ -134,6 +144,50 @@ impl BoogieProgram {
     }
 }
 
+impl DataType {
+    fn write_to<T: Write>(&self, writer: &mut Writer<T>) -> std::io::Result<()> {
+        write!(writer, "datatype {}", self.name)?;
+        if !self.type_parameters.is_empty() {
+            write!(writer, "<")?;
+            for (i, tp) in self.type_parameters.iter().enumerate() {
+                if i > 0 {
+                    write!(writer, ", ")?;
+                }
+                write!(writer, "{tp}")?;
+            }
+            write!(writer, ">")?;
+        }
+        write!(writer, " {{")?;
+        for (i, cons) in self.constructors.iter().enumerate() {
+            if i > 0 {
+                writeln!(writer, ",")?;
+            }
+            cons.write_to(writer)?;
+        }
+        writeln!(writer, " }}")?;
+        writer.newline()?;
+        Ok(())
+    }
+}
+
+impl DataTypeConstructor {
+    fn write_to<T: Write>(&self, writer: &mut Writer<T>) -> std::io::Result<()> {
+        write!(writer, " {}", self.name)?;
+        if !self.parameters.is_empty() {
+            write!(writer, "(")?;
+            for (i, tp) in self.parameters.iter().enumerate() {
+                if i > 0 {
+                    write!(writer, ", ")?;
+                }
+                write!(writer, "{}: ", tp.name)?;
+                tp.typ.write_to(writer)?;
+            }
+            write!(writer, ")")?;
+        }
+        Ok(())
+    }
+}
+
 impl Function {
     fn write_to<T: Write>(&self, writer: &mut Writer<T>) -> std::io::Result<()> {
         // signature
@@ -392,6 +446,13 @@ impl Type {
                 value.write_to(writer)?;
             }
             Type::Parameter { name } => write!(writer, "{name}")?,
+            Type::UserDefined { name, type_arguments } => {
+                write!(writer, "{name}")?;
+                for arg in type_arguments {
+                    write!(writer, " ")?;
+                    arg.write_to(writer)?;
+                }
+            }
         }
         Ok(())
     }
@@ -460,6 +521,17 @@ mod tests {
             const_declarations: Vec::new(),
             var_declarations: Vec::new(),
             axioms: Vec::new(),
+            datatypes: vec![DataType::new(
+                "Pair".into(),
+                vec!["U".into(), "V".into()],
+                vec![DataTypeConstructor::new(
+                    "Pair".into(),
+                    vec![
+                        Parameter::new("fst".into(), Type::parameter("U".into())),
+                        Parameter::new("snd".into(), Type::parameter("V".into())),
+                    ],
+                )],
+            )],
             functions: vec![
                 Function::new(
                     "isZero".into(),
@@ -502,6 +574,13 @@ mod tests {
                     statements: vec![
                         Stmt::Decl { name: "x".to_string(), typ: Type::Int },
                         Stmt::Decl { name: "y".to_string(), typ: Type::Int },
+                        Stmt::Decl {
+                            name: "p".to_string(),
+                            typ: Type::user_defined(
+                                "Pair".to_string(),
+                                vec![Type::Bool, Type::Int],
+                            ),
+                        },
                         Stmt::Assignment {
                             target: "x".to_string(),
                             value: Expr::Literal(Literal::Int(1.into())),
@@ -550,6 +629,9 @@ mod tests {
 
         let expected = String::from(
             "\
+// Datatypes:
+datatype Pair<U, V> { Pair(fst: U, snd: V) }
+
 // Functions:
 function {:inline} isZero(x: int) returns (bool) {
   (x == 0)
@@ -563,6 +645,7 @@ procedure main() returns (z: bool)
 {
   var x: int;
   var y: int;
+  var p: Pair bool int;
   x := 1;
   y := 2;
   assert (x == 1);