Create a Boogie AST crate (#2565)

Cargo.lock

@@ -104,6 +104,13 @@ version = "2.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07"
 
+[[package]]
+name = "boogie_ast"
+version = "0.34.0"
+dependencies = [
+ "num-bigint",
+]
+
 [[package]]
 name = "bookrunner"
 version = "0.1.0"
@@ -449,6 +456,7 @@ dependencies = [
 name = "kani-compiler"
 version = "0.41.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);
+ }
+}