diff --git a/Cargo.lock b/Cargo.lock index b751dc897b65..1ecfd78e17a4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -108,6 +108,9 @@ checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42" [[package]] name = "boogie_ast" version = "0.30.0" +dependencies = [ + "num-bigint", +] [[package]] name = "bookrunner" diff --git a/boogie_ast/Cargo.toml b/boogie_ast/Cargo.toml index b207b6761d87..4c028ddcbbaa 100644 --- a/boogie_ast/Cargo.toml +++ b/boogie_ast/Cargo.toml @@ -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" diff --git a/boogie_ast/src/boogie_program/mod.rs b/boogie_ast/src/boogie_program/mod.rs index e4366978f0c7..d6dc99c41597 100644 --- a/boogie_ast/src/boogie_program/mod.rs +++ b/boogie_ast/src/boogie_program/mod.rs @@ -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 {} @@ -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 @@ -149,7 +151,7 @@ pub enum Stmt { While { condition: Expr, body: Box }, } -/// Procedure specification +/// Contract specification pub struct Contract { /// Pre-conditions requires: Vec, @@ -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, @@ -182,6 +186,7 @@ impl Procedure { } /// Function definition +/// A function in Boogie is a mathematical function struct Function {} /// A boogie program @@ -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 { diff --git a/boogie_ast/src/boogie_program/writer.rs b/boogie_ast/src/boogie_program/writer.rs index 3ba1db88bf89..55d9c9f329f9 100644 --- a/boogie_ast/src/boogie_program/writer.rs +++ b/boogie_ast/src/boogie_program/writer.rs @@ -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: +//! +//! +//! ... +//! +//! // Constant declarations: +//! +//! +//! ... +//! +//! // Variable declarations: +//! var : ; +//! var : ; +//! ... +//! +//! // Axioms +//! axiom ; +//! axiom ; +//! ... +//! +//! // Functions: +//! function (: , ...) returns (return-var-name: ) +//! { +//! +//! } +//! ... +//! +//! // Procedures: +//! procedure (: , ...) returns (return-var-name: ) +//! requires ; +//! requires ; +//! ... +//! ensures ; +//! ensures ; +//! ... +//! modifies , , ...; +//! { +//! +//! } +//! ... +//! +///! ``` use crate::boogie_program::*; use std::io::Write; @@ -55,13 +98,41 @@ impl BoogieProgram { impl Writable for BoogieProgram { fn write_to(&self, writer: &mut Writer) -> 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(()) } diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs index 4a946f740d8c..18ff49486605 100644 --- a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs +++ b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs @@ -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}; @@ -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!(), } } diff --git a/kani-compiler/src/codegen_boogie/overrides/hooks.rs b/kani-compiler/src/codegen_boogie/overrides/hooks.rs index 5ba2199db518..36b4f00fbd47 100644 --- a/kani-compiler/src/codegen_boogie/overrides/hooks.rs +++ b/kani-compiler/src/codegen_boogie/overrides/hooks.rs @@ -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};