Skip to content

Commit

Permalink
Address some PR comments
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws committed Jul 24, 2023
1 parent 6475d6c commit fc958b1
Show file tree
Hide file tree
Showing 6 changed files with 120 additions and 24 deletions.
3 changes: 3 additions & 0 deletions Cargo.lock
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,9 @@ checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42"
[[package]]
name = "boogie_ast"
version = "0.30.0"
dependencies = [
"num-bigint",
]

[[package]]
name = "bookrunner"
Expand Down
1 change: 1 addition & 0 deletions boogie_ast/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,3 +11,4 @@ publish = false
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
num-bigint = "0.4.3"
27 changes: 16 additions & 11 deletions boogie_ast/src/boogie_program/mod.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,13 @@
// 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 {}
Expand Down Expand Up @@ -35,13 +40,10 @@ pub enum Literal {
Bool(bool),

/// Bit-vector values, e.g. `5bv8`
Bv {
width: usize,
value: String, // TODO: use bigint
},
Bv { width: usize, value: BigUint },

/// Unbounded integer values, e.g. `1000`
Int(String), // TODO: use bigint
/// Unbounded integer values, e.g. `1000` or `-456789`
Int(BigInt),
}

/// Unary operators
Expand Down Expand Up @@ -149,7 +151,7 @@ pub enum Stmt {
While { condition: Expr, body: Box<Stmt> },
}

/// Procedure specification
/// Contract specification
pub struct Contract {
/// Pre-conditions
requires: Vec<Expr>,
Expand All @@ -161,6 +163,8 @@ pub struct Contract {
}

/// 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>,
Expand All @@ -182,6 +186,7 @@ impl Procedure {
}

/// Function definition
/// A function in Boogie is a mathematical function
struct Function {}

/// A boogie program
Expand Down Expand Up @@ -236,24 +241,24 @@ impl BoogieProgram {
Stmt::Decl { name: "y".to_string(), typ: Type::Int },
Stmt::Assignment {
target: "x".to_string(),
value: Expr::Literal(Literal::Int("1".to_string())),
value: Expr::Literal(Literal::Int(1.into())),
},
Stmt::Assignment {
target: "y".to_string(),
value: Expr::Literal(Literal::Int("2".to_string())),
value: Expr::Literal(Literal::Int(2.into())),
},
Stmt::Assert {
condition: Expr::BinaryOp {
op: BinaryOp::Eq,
left: Box::new(Expr::Symbol { name: "x".to_string() }),
right: Box::new(Expr::Literal(Literal::Int("1".to_string()))),
right: Box::new(Expr::Literal(Literal::Int(1.into()))),
},
},
Stmt::Assert {
condition: Expr::BinaryOp {
op: BinaryOp::Eq,
left: Box::new(Expr::Symbol { name: "y".to_string() }),
right: Box::new(Expr::Literal(Literal::Int("2".to_string()))),
right: Box::new(Expr::Literal(Literal::Int(2.into()))),
},
},
Stmt::If {
Expand Down
87 changes: 79 additions & 8 deletions boogie_ast/src/boogie_program/writer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,50 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! A writer for Boogie programs.

//! Generates a text Boogie program with the following format:
//! ```
//! // Type declarations:
//! <Type declaration 1>
//! <Type declaration 2>
//! ...
//!
//! // Constant declarations:
//! <Const declaration 1>
//! <Const declaration 2>
//! ...
//!
//! // Variable declarations:
//! var <var-name1>: <type1>;
//! var <var-name2>: <type2>;
//! ...
//!
//! // Axioms
//! axiom <expr1>;
//! axiom <expr2>;
//! ...
//!
//! // Functions:
//! function <function1-name>(<arg1>: <type1>, ...) returns (return-var-name: <return-type>)
//! {
//! <body>
//! }
//! ...
//!
//! // Procedures:
//! procedure <procedure1-name>(<arg1>: <type1>, ...) returns (return-var-name: <return-type>)
//! requires <pre-condition1>;
//! requires <pre-condition2>;
//! ...
//! ensures <post-condition1>;
//! ensures <post-condition2>;
//! ...
//! modifies <var1>, <var2>, ...;
//! {
//! <body>
//! }
//! ...
//!
///! ```
use crate::boogie_program::*;

use std::io::Write;
Expand Down Expand Up @@ -55,13 +98,41 @@ impl BoogieProgram {

impl Writable for BoogieProgram {
fn write_to<T: Write>(&self, writer: &mut Writer<T>) -> std::io::Result<()> {
for _td in &self.type_declarations {}
for _const_decl in &self.const_declarations {}
for _var_decl in &self.var_declarations {}
for _a in &self.axioms {}
for _f in &self.functions {}
for p in &self.procedures {
writer.write(p)?;
if !self.type_declarations.is_empty() {
writeln!(writer.writer, "// Type declarations:")?;
for _td in &self.type_declarations {
todo!()
}
}
if !self.const_declarations.is_empty() {
writeln!(writer.writer, "// Constant declarations:")?;
for _const_decl in &self.const_declarations {
todo!()
}
}
if !self.var_declarations.is_empty() {
writeln!(writer.writer, "// Variable declarations:")?;
for _var_decl in &self.var_declarations {
todo!()
}
}
if !self.axioms.is_empty() {
writeln!(writer.writer, "// Axioms:")?;
for _a in &self.axioms {
todo!()
}
}
if !self.functions.is_empty() {
writeln!(writer.writer, "// Functions:")?;
for _f in &self.functions {
todo!()
}
}
if !self.procedures.is_empty() {
writeln!(writer.writer, "// Procedures:")?;
for p in &self.procedures {
writer.write(p)?;
}
}
Ok(())
}
Expand Down
24 changes: 21 additions & 3 deletions kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use rustc_middle::span_bug;
use rustc_middle::ty::layout::{
HasParamEnv, HasTyCtxt, LayoutError, LayoutOf, LayoutOfHelpers, TyAndLayout,
};
use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy};
use rustc_span::Span;
use rustc_target::abi::{HasDataLayout, TargetDataLayout};
use tracing::{debug, debug_span, trace};
Expand Down Expand Up @@ -281,8 +281,26 @@ impl<'tcx> BoogieCtx<'tcx> {
pub fn codegen_scalar(&self, s: Scalar, ty: Ty<'tcx>) -> Expr {
match (s, ty.kind()) {
(Scalar::Int(_), ty::Bool) => Expr::Literal(Literal::Bool(s.to_bool().unwrap())),
(Scalar::Int(i), ty::Int(_)) => Expr::Literal(Literal::Int(i.to_string())),
(Scalar::Int(i), ty::Uint(_)) => Expr::Literal(Literal::Int(i.to_string())),
(Scalar::Int(_), ty::Int(it)) => match it {
IntTy::I8 => Expr::Literal(Literal::Int(s.to_i8().unwrap().into())),
IntTy::I16 => Expr::Literal(Literal::Int(s.to_i16().unwrap().into())),
IntTy::I32 => Expr::Literal(Literal::Int(s.to_i32().unwrap().into())),
IntTy::I64 => Expr::Literal(Literal::Int(s.to_i64().unwrap().into())),
IntTy::I128 => Expr::Literal(Literal::Int(s.to_i128().unwrap().into())),
IntTy::Isize => {
Expr::Literal(Literal::Int(s.to_target_isize(self).unwrap().into()))
}
},
(Scalar::Int(_), ty::Uint(it)) => match it {
UintTy::U8 => Expr::Literal(Literal::Int(s.to_u8().unwrap().into())),
UintTy::U16 => Expr::Literal(Literal::Int(s.to_u16().unwrap().into())),
UintTy::U32 => Expr::Literal(Literal::Int(s.to_u32().unwrap().into())),
UintTy::U64 => Expr::Literal(Literal::Int(s.to_u64().unwrap().into())),
UintTy::U128 => Expr::Literal(Literal::Int(s.to_u128().unwrap().into())),
UintTy::Usize => {
Expr::Literal(Literal::Int(s.to_target_isize(self).unwrap().into()))
}
},
_ => todo!(),
}
}
Expand Down
2 changes: 0 additions & 2 deletions kani-compiler/src/codegen_boogie/overrides/hooks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,6 @@
//!
//! E.g.: Functions in the Kani library that generate assumptions or symbolic variables.
//!
//! It would be too nasty if we spread around these sort of undocumented hooks in place, so
//! this module addresses this issue.

use crate::codegen_boogie::BoogieCtx;
use boogie_ast::boogie_program::{Expr, Stmt};
Expand Down

0 comments on commit fc958b1

Please sign in to comment.