Create a Boogie AST crate (#2565)

Cargo.lock

@@ -105,6 +105,13 @@ version = "2.3.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42"
 
+[[package]]
+name = "boogie_ast"
+version = "0.34.0"
+dependencies = [
+ "num-bigint",
+]
+
 [[package]]
 name = "bookrunner"
 version = "0.1.0"
@@ -496,6 +503,7 @@ dependencies = [
 name = "kani-compiler"
 version = "0.34.0"
 dependencies = [
+ "boogie_ast",
  "clap",
  "cprover_bindings",
  "home",

boogie_ast/Cargo.toml

@@ -0,0 +1,14 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "boogie_ast"
+version = "0.34.0"
+edition = "2021"
+license = "MIT OR Apache-2.0"
+publish = false
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+num-bigint = "0.4.3"

boogie_ast/src/boogie_program/mod.rs

@@ -0,0 +1,218 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! A module that defines the AST of a Boogie program and provides methods for
+//! creating nodes of the AST.
+
+mod writer;
+
+use num_bigint::{BigInt, BigUint};
+
+struct TypeDeclaration {}
+struct ConstDeclaration {}
+struct VarDeclaration {}
+struct Axiom {}
+
+/// Boogie types
+pub enum Type {
+    /// Boolean
+    Bool,
+
+    /// Bit-vector of a given width, e.g. `bv32`
+    Bv(usize),
+
+    /// Unbounded integer
+    Int,
+
+    /// Map type, e.g. `[int]bool`
+    Map { key: Box<Type>, value: Box<Type> },
+}
+
+/// Function and procedure parameters
+pub struct Parameter {
+    name: String,
+    typ: Type,
+}
+
+/// Literal types
+pub enum Literal {
+    /// Boolean values: `true`/`false`
+    Bool(bool),
+
+    /// Bit-vector values, e.g. `5bv8`
+    Bv { width: usize, value: BigUint },
+
+    /// Unbounded integer values, e.g. `1000` or `-456789`
+    Int(BigInt),
+}
+
+/// Unary operators
+pub enum UnaryOp {
+    /// Logical negation
+    Not,
+
+    /// Arithmetic negative
+    Neg,
+}
+
+pub enum BinaryOp {
+    /// Logical AND
+    And,
+
+    /// Logical OR
+    Or,
+
+    /// Equality
+    Eq,
+
+    /// Inequality
+    Neq,
+
+    /// Less than
+    Lt,
+
+    /// Less than or equal
+    Lte,
+
+    /// Greater than
+    Gt,
+
+    /// Greater than or equal
+    Gte,
+
+    /// Addition
+    Add,
+
+    /// Subtraction
+    Sub,
+
+    /// Multiplication
+    Mul,
+
+    /// Division
+    Div,
+
+    /// Modulo
+    Mod,
+}
+
+/// Expr types
+pub enum Expr {
+    /// Literal (constant)
+    Literal(Literal),
+
+    /// Variable
+    Symbol { name: String },
+
+    /// Unary operation
+    UnaryOp { op: UnaryOp, operand: Box<Expr> },
+
+    /// Binary operation
+    BinaryOp { op: BinaryOp, left: Box<Expr>, right: Box<Expr> },
+}
+
+/// Statement types
+pub enum Stmt {
+    /// Assignment statement: `target := value;`
+    Assignment { target: String, value: Expr },
+
+    /// Assert statement: `assert condition;`
+    Assert { condition: Expr },
+
+    /// Assume statement: `assume condition;`
+    Assume { condition: Expr },
+
+    /// Statement block: `{ statements }`
+    Block { statements: Vec<Stmt> },
+
+    /// Break statement: `break;`
+    /// A `break` in boogie can take a label, but this is probably not needed
+    Break,
+
+    /// Procedure call: `symbol(arguments);`
+    Call { symbol: String, arguments: Vec<Expr> },
+
+    /// Declaration statement: `var name: type;`
+    Decl { name: String, typ: Type },
+
+    /// 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,
+
+    /// While statement: `while (condition) { body }`
+    While { condition: Expr, body: Box<Stmt> },
+}
+
+/// Contract specification
+pub struct Contract {
+    /// Pre-conditions
+    requires: Vec<Expr>,
+    /// Post-conditions
+    ensures: Vec<Expr>,
+    /// Modifies clauses
+    // TODO: should be symbols and not expressions
+    modifies: Vec<Expr>,
+}
+
+/// Procedure definition
+/// A procedure is a function that has a contract specification and that can
+/// have side effects
+pub struct Procedure {
+    name: String,
+    parameters: Vec<Parameter>,
+    return_type: Vec<(String, Type)>,
+    contract: Option<Contract>,
+    body: Stmt,
+}
+
+impl Procedure {
+    pub fn new(
+        name: String,
+        parameters: Vec<Parameter>,
+        return_type: Vec<(String, Type)>,
+        contract: Option<Contract>,
+        body: Stmt,
+    ) -> Self {
+        Procedure { name, parameters, return_type, contract, body }
+    }
+}
+
+/// Function definition
+/// A function in Boogie is a mathematical function (deterministic, has no side
+/// effects, and whose body is an expression)
+struct Function {}
+
+/// A boogie program
+pub struct BoogieProgram {
+    type_declarations: Vec<TypeDeclaration>,
+    const_declarations: Vec<ConstDeclaration>,
+    var_declarations: Vec<VarDeclaration>,
+    axioms: Vec<Axiom>,
+    functions: Vec<Function>,
+    procedures: Vec<Procedure>,
+}
+
+impl BoogieProgram {
+    pub fn new() -> Self {
+        BoogieProgram {
+            type_declarations: Vec::new(),
+            const_declarations: Vec::new(),
+            var_declarations: Vec::new(),
+            axioms: Vec::new(),
+            functions: Vec::new(),
+            procedures: Vec::new(),
+        }
+    }
+
+    pub fn add_procedure(&mut self, procedure: Procedure) {
+        self.procedures.push(procedure);
+    }
+}