From bbc70a5e7fea1c0a00e1b1bd421d3d461ad6d44b Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 15 Dec 2023 16:36:00 -0800 Subject: [PATCH] [Boogie Backend] Add datatypes to Boogie AST --- boogie_ast/src/boogie_program/mod.rs | 46 ++++++++++++++ boogie_ast/src/boogie_program/writer.rs | 83 +++++++++++++++++++++++++ 2 files changed, 129 insertions(+) diff --git a/boogie_ast/src/boogie_program/mod.rs b/boogie_ast/src/boogie_program/mod.rs index 14b0855d958a..db46c9491ae0 100644 --- a/boogie_ast/src/boogie_program/mod.rs +++ b/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 }, } 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) -> Self { + Self::UserDefined { name, type_arguments } + } } /// Function and procedure parameters @@ -203,6 +212,37 @@ pub enum Stmt { While { condition: Expr, body: Box }, } +/// 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, + constructors: Vec, +} + +impl DataType { + pub fn new( + name: String, + type_parameters: Vec, + constructors: Vec, + ) -> 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, +} + +impl DataTypeConstructor { + pub fn new(name: String, parameters: Vec) -> Self { + Self { name, parameters } + } +} + /// Contract specification pub struct Contract { /// Pre-conditions @@ -269,6 +309,7 @@ pub struct BoogieProgram { const_declarations: Vec, var_declarations: Vec, axioms: Vec, + datatypes: Vec, functions: Vec, procedures: Vec, } @@ -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); + } } diff --git a/boogie_ast/src/boogie_program/writer.rs b/boogie_ast/src/boogie_program/writer.rs index 2cf18b193d2f..af0699612486 100644 --- a/boogie_ast/src/boogie_program/writer.rs +++ b/boogie_ast/src/boogie_program/writer.rs @@ -24,6 +24,10 @@ //! axiom ; //! ... //! +//! // Datatypes: +//! datatype = ; +//! ... +//! //! // Functions: //! function (: , ...) returns (return-var-name: ) //! { @@ -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(&self, writer: &mut Writer) -> 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(&self, writer: &mut Writer) -> 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(&self, writer: &mut Writer) -> 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 { 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);