diff --git a/Cargo.lock b/Cargo.lock index 01c577439b62..ae022a612fa5 100644 --- a/Cargo.lock +++ b/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.30.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", diff --git a/boogie_ast/Cargo.toml b/boogie_ast/Cargo.toml new file mode 100644 index 000000000000..ca9f5660e2f8 --- /dev/null +++ b/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" diff --git a/boogie_ast/src/boogie_program/mod.rs b/boogie_ast/src/boogie_program/mod.rs new file mode 100644 index 000000000000..a411d483f260 --- /dev/null +++ b/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, value: Box }, +} + +/// 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 }, + + /// Binary operation + BinaryOp { op: BinaryOp, left: Box, right: Box }, +} + +/// 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 }, + + /// 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 }, + + /// Declaration statement: `var name: type;` + Decl { name: String, typ: Type }, + + /// If statement: `if (condition) { body } else { else_body }` + If { condition: Expr, body: Box, else_body: Option> }, + + /// 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 }, +} + +/// Contract specification +pub struct Contract { + /// Pre-conditions + requires: Vec, + /// Post-conditions + ensures: Vec, + /// Modifies clauses + // TODO: should be symbols and not expressions + modifies: Vec, +} + +/// 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, + return_type: Vec<(String, Type)>, + contract: Option, + body: Stmt, +} + +impl Procedure { + pub fn new( + name: String, + parameters: Vec, + return_type: Vec<(String, Type)>, + contract: Option, + 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, + const_declarations: Vec, + var_declarations: Vec, + axioms: Vec, + functions: Vec, + procedures: Vec, +} + +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); + } +} diff --git a/boogie_ast/src/boogie_program/writer.rs b/boogie_ast/src/boogie_program/writer.rs new file mode 100644 index 000000000000..3b24f2b2225e --- /dev/null +++ b/boogie_ast/src/boogie_program/writer.rs @@ -0,0 +1,484 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! A writer for Boogie programs. +//! Generates a text Boogie program with the following format: +//! ```ignore +//! // 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; + +/// A writer for Boogie programs. +struct Writer<'a, T: Write> { + writer: &'a mut T, + indentation: usize, +} + +impl<'a, T: Write> Writer<'a, T> { + fn new(writer: &'a mut T) -> Self { + Self { writer, indentation: 0 } + } + + fn newline(&mut self) -> std::io::Result<()> { + writeln!(self.writer) + } + + fn increase_indent(&mut self) { + self.indentation += 2; + } + + fn decrease_indent(&mut self) { + self.indentation -= 2; + } + + fn indent(&mut self) -> std::io::Result<()> { + write!(self.writer, "{:width$}", "", width = self.indentation) + } +} + +impl<'a, T: Write> Write for Writer<'a, T> { + fn write(&mut self, buf: &[u8]) -> std::io::Result { + self.writer.write(buf) + } + + fn flush(&mut self) -> std::io::Result<()> { + self.writer.flush() + } +} + +impl BoogieProgram { + pub fn write_to(&self, writer: &mut T) -> std::io::Result<()> { + let mut writer = Writer::new(writer); + + if !self.type_declarations.is_empty() { + writeln!(writer, "// Type declarations:")?; + for _td in &self.type_declarations { + todo!() + } + } + if !self.const_declarations.is_empty() { + writeln!(writer, "// Constant declarations:")?; + for _const_decl in &self.const_declarations { + todo!() + } + } + if !self.var_declarations.is_empty() { + writeln!(writer, "// Variable declarations:")?; + for _var_decl in &self.var_declarations { + todo!() + } + } + if !self.axioms.is_empty() { + writeln!(writer, "// Axioms:")?; + for _a in &self.axioms { + todo!() + } + } + if !self.functions.is_empty() { + writeln!(writer, "// Functions:")?; + for _f in &self.functions { + todo!() + } + } + if !self.procedures.is_empty() { + writeln!(writer, "// Procedures:")?; + for p in &self.procedures { + p.write_to(&mut writer)?; + } + } + Ok(()) + } +} + +impl Procedure { + fn write_to(&self, writer: &mut Writer) -> std::io::Result<()> { + // signature + write!(writer, "procedure {}(", self.name)?; + for (i, param) in self.parameters.iter().enumerate() { + if i > 0 { + write!(writer, ",")?; + } + write!(writer, "{}: ", param.name)?; + param.typ.write_to(writer)?; + } + write!(writer, ") ")?; + if !self.return_type.is_empty() { + write!(writer, "returns (")?; + for (i, (name, typ)) in self.return_type.iter().enumerate() { + if i > 0 { + write!(writer, ",")?; + } + write!(writer, "{name}: ")?; + typ.write_to(writer)?; + } + write!(writer, ")")?; + } + writer.newline()?; + + // contract + if let Some(contract) = &self.contract { + writer.increase_indent(); + contract.write_to(writer)?; + writer.decrease_indent(); + } + writeln!(writer, "{{")?; + writer.increase_indent(); + self.body.write_to(writer)?; + writer.decrease_indent(); + writeln!(writer, "}}")?; + Ok(()) + } +} + +impl Expr { + fn write_to(&self, writer: &mut Writer) -> std::io::Result<()> { + match self { + Expr::Literal(value) => { + value.write_to(writer)?; + } + Expr::Symbol { name } => { + write!(writer, "{name}")?; + } + Expr::UnaryOp { op, operand } => { + op.write_to(writer)?; + write!(writer, "(")?; + operand.write_to(writer)?; + write!(writer, ")")?; + } + Expr::BinaryOp { op, left, right } => { + write!(writer, "(")?; + left.write_to(writer)?; + write!(writer, " ")?; + op.write_to(writer)?; + write!(writer, " ")?; + right.write_to(writer)?; + write!(writer, ")")?; + } + } + Ok(()) + } +} + +impl Stmt { + fn write_to(&self, writer: &mut Writer) -> std::io::Result<()> { + match self { + Stmt::Assignment { target, value } => { + writer.indent()?; + write!(writer, "{} := ", target)?; + value.write_to(writer)?; + writeln!(writer, ";")?; + } + Stmt::Assert { condition } => { + writer.indent()?; + write!(writer, "assert ")?; + condition.write_to(writer)?; + writeln!(writer, ";")?; + } + Stmt::Assume { condition } => { + writer.indent()?; + write!(writer, "assume ")?; + condition.write_to(writer)?; + writeln!(writer, ";")?; + } + Stmt::Block { statements } => { + for s in statements { + s.write_to(writer)?; + } + } + Stmt::Break => { + writer.indent()?; + writeln!(writer, "break;")?; + } + Stmt::Call { symbol, arguments } => { + writer.indent()?; + write!(writer, "{symbol}(")?; + for (i, a) in arguments.iter().enumerate() { + if i > 0 { + write!(writer, ", ")?; + } + a.write_to(writer)?; + } + writeln!(writer, ");")?; + } + Stmt::Decl { name, typ } => { + writer.indent()?; + write!(writer, "var {}: ", name)?; + typ.write_to(writer)?; + writeln!(writer, ";")?; + } + Stmt::If { condition, body, else_body } => { + writer.indent()?; + write!(writer, "if (")?; + condition.write_to(writer)?; + writeln!(writer, ") {{")?; + writer.increase_indent(); + body.write_to(writer)?; + writer.decrease_indent(); + writer.indent()?; + write!(writer, "}}")?; + if let Some(else_body) = else_body { + writeln!(writer, " else {{")?; + writer.increase_indent(); + else_body.write_to(writer)?; + writer.decrease_indent(); + writer.indent()?; + write!(writer, "}}")?; + } + writeln!(writer)?; + } + Stmt::Goto { label } => { + writer.indent()?; + writeln!(writer, "goto {label};")?; + } + Stmt::Label { label } => { + writer.indent()?; + writeln!(writer, "{label}:")?; + } + Stmt::Return => { + writer.indent()?; + writeln!(writer, "return;")?; + } + Stmt::While { condition, body } => { + writer.indent()?; + write!(writer, "while (")?; + condition.write_to(writer)?; + writeln!(writer, ") {{")?; + writer.increase_indent(); + body.write_to(writer)?; + writer.decrease_indent(); + writeln!(writer, "}}")?; + } + } + Ok(()) + } +} + +impl Contract { + fn write_to(&self, writer: &mut Writer) -> std::io::Result<()> { + for r in &self.requires { + writer.indent()?; + write!(writer, "requires ")?; + r.write_to(writer)?; + writeln!(writer, ";")?; + } + for e in &self.ensures { + writer.indent()?; + write!(writer, "ensures ")?; + e.write_to(writer)?; + writeln!(writer, ";")?; + } + for m in &self.modifies { + writer.indent()?; + write!(writer, "modifies ")?; + m.write_to(writer)?; + writeln!(writer, ";")?; + } + Ok(()) + } +} + +impl Type { + fn write_to(&self, writer: &mut Writer) -> std::io::Result<()> { + match self { + Type::Bool => write!(writer, "bool")?, + Type::Bv(size) => write!(writer, "bv{size}")?, + Type::Int => write!(writer, "int")?, + Type::Map { key, value } => { + write!(writer, "[")?; + key.write_to(writer)?; + write!(writer, "]")?; + value.write_to(writer)?; + } + } + Ok(()) + } +} + +impl Literal { + fn write_to(&self, writer: &mut Writer) -> std::io::Result<()> { + match self { + Literal::Bool(value) => { + write!(writer, "{}", value)?; + } + Literal::Bv { width, value } => { + write!(writer, "{value}bv{width}")?; + } + Literal::Int(value) => { + write!(writer, "{}", value)?; + } + } + Ok(()) + } +} + +impl UnaryOp { + fn write_to(&self, writer: &mut Writer) -> std::io::Result<()> { + match self { + UnaryOp::Not => write!(writer, "!")?, + UnaryOp::Neg => write!(writer, "-")?, + } + Ok(()) + } +} + +impl BinaryOp { + fn write_to(&self, writer: &mut Writer) -> std::io::Result<()> { + match self { + BinaryOp::Add => write!(writer, "+")?, + BinaryOp::Sub => write!(writer, "-")?, + BinaryOp::Mul => write!(writer, "*")?, + BinaryOp::Div => write!(writer, "/")?, + BinaryOp::Mod => write!(writer, "%")?, + BinaryOp::And => write!(writer, "&&")?, + BinaryOp::Or => write!(writer, "||")?, + BinaryOp::Eq => write!(writer, "==")?, + BinaryOp::Neq => write!(writer, "!=")?, + BinaryOp::Lt => write!(writer, "<")?, + BinaryOp::Gt => write!(writer, ">")?, + BinaryOp::Lte => write!(writer, "<=")?, + BinaryOp::Gte => write!(writer, ">=")?, + } + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn sample_program() { + let program = BoogieProgram { + type_declarations: Vec::new(), + const_declarations: Vec::new(), + var_declarations: Vec::new(), + axioms: Vec::new(), + functions: Vec::new(), + procedures: vec![Procedure { + name: "main".to_string(), + parameters: Vec::new(), + return_type: vec![("z".to_string(), Type::Bool)], + contract: Some(Contract { + requires: Vec::new(), + ensures: vec![Expr::BinaryOp { + op: BinaryOp::Eq, + left: Box::new(Expr::Symbol { name: "z".to_string() }), + right: Box::new(Expr::Literal(Literal::Bool(true))), + }], + modifies: Vec::new(), + }), + body: Stmt::Block { + statements: vec![ + Stmt::Decl { name: "x".to_string(), typ: Type::Int }, + Stmt::Decl { name: "y".to_string(), typ: Type::Int }, + Stmt::Assignment { + target: "x".to_string(), + value: Expr::Literal(Literal::Int(1.into())), + }, + Stmt::Assignment { + target: "y".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.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.into()))), + }, + }, + Stmt::If { + condition: Expr::BinaryOp { + op: BinaryOp::Lt, + left: Box::new(Expr::Symbol { name: "x".to_string() }), + right: Box::new(Expr::Symbol { name: "y".to_string() }), + }, + body: Box::new(Stmt::Assignment { + target: "z".to_string(), + value: Expr::Literal(Literal::Bool(true)), + }), + else_body: Some(Box::new(Stmt::Assignment { + target: "z".to_string(), + value: Expr::Literal(Literal::Bool(false)), + })), + }, + ], + }, + }], + }; + + let mut v = Vec::new(); + program.write_to(&mut v).unwrap(); + let program_text = String::from_utf8(v).unwrap().to_string(); + + let expected = String::from( + "\ +// Procedures: +procedure main() returns (z: bool) + ensures (z == true); +{ + var x: int; + var y: int; + x := 1; + y := 2; + assert (x == 1); + assert (y == 2); + if ((x < y)) { + z := true; + } else { + z := false; + } +} +", + ); + assert_eq!(program_text, expected); + } +} diff --git a/boogie_ast/src/lib.rs b/boogie_ast/src/lib.rs new file mode 100644 index 000000000000..851b165d5ceb --- /dev/null +++ b/boogie_ast/src/lib.rs @@ -0,0 +1,4 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub mod boogie_program; diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 9fb74d7c1038..275903058314 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -9,6 +9,7 @@ license = "MIT OR Apache-2.0" publish = false [dependencies] +boogie_ast = { path = "../boogie_ast", optional = true } cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true } clap = { version = "4.1.3", features = ["cargo"] } home = "0.5" @@ -28,7 +29,7 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt" # Future proofing: enable backend dependencies using feature. [features] default = ['boogie', 'cprover'] -boogie = ['serde'] +boogie = ['boogie_ast'] cprover = ['cbmc', 'num', 'serde'] write_json_symtab = [] diff --git a/kani-compiler/src/codegen_boogie/compiler_interface.rs b/kani-compiler/src/codegen_boogie/compiler_interface.rs index 3743d001b2af..4cb02c0e4ae2 100644 --- a/kani-compiler/src/codegen_boogie/compiler_interface.rs +++ b/kani-compiler/src/codegen_boogie/compiler_interface.rs @@ -145,7 +145,9 @@ impl BoogieCodegenBackend { for item in &items { match *item { MonoItem::Fn(instance) => { - bcx.declare_function(instance); + if let Some(procedure) = bcx.codegen_function(instance) { + bcx.add_procedure(procedure); + } } MonoItem::Static(_def_id) => {} MonoItem::GlobalAsm(_) => {} // Ignore this. We have already warned about it. @@ -164,6 +166,15 @@ impl BoogieCodegenBackend { "codegen", ); + if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { + let mut pb = boogie_file.to_path_buf(); + pb.set_extension("bpl"); + debug!("Writing Boogie file to {}", pb.display()); + let file = File::create(&pb).unwrap(); + let mut writer = BufWriter::new(file); + bcx.write(&mut writer).unwrap(); + } + (bcx, items) } } diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs index 4ef902f0c36a..fd767743dd63 100644 --- a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs +++ b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs @@ -1,9 +1,27 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use std::io::Write; + use crate::kani_queries::QueryDb; -use rustc_middle::ty::{Instance, TyCtxt}; -use tracing::debug; +use boogie_ast::boogie_program::{BinaryOp, BoogieProgram, Expr, Literal, Procedure, Stmt, Type}; +use rustc_middle::mir::interpret::{ConstValue, Scalar}; +use rustc_middle::mir::traversal::reverse_postorder; +use rustc_middle::mir::{ + BasicBlock, BasicBlockData, BinOp, Constant, ConstantKind, HasLocalDecls, Local, LocalDecls, + Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, +}; +use rustc_middle::span_bug; +use rustc_middle::ty::layout::{ + HasParamEnv, HasTyCtxt, LayoutError, LayoutOf, LayoutOfHelpers, TyAndLayout, +}; +use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy}; +use rustc_span::Span; +use rustc_target::abi::{HasDataLayout, TargetDataLayout}; +use strum::VariantNames; +use tracing::{debug, debug_span, trace}; + +use super::kani_intrinsic::KaniIntrinsic; /// A context that provides the main methods for translating MIR constructs to /// Boogie and stores what has been codegen so far @@ -13,14 +31,352 @@ pub struct BoogieCtx<'tcx> { /// a snapshot of the query values. The queries shouldn't change at this point, /// so we just keep a copy. pub queries: QueryDb, + /// the Boogie program + program: BoogieProgram, + /// Kani intrinsics + pub intrinsics: Vec, } impl<'tcx> BoogieCtx<'tcx> { pub fn new(tcx: TyCtxt<'tcx>, queries: QueryDb) -> BoogieCtx<'tcx> { - BoogieCtx { tcx, queries } + BoogieCtx { + tcx, + queries, + program: BoogieProgram::new(), + intrinsics: KaniIntrinsic::VARIANTS.iter().map(|s| (*s).into()).collect(), + } + } + + /// Codegen a function into a Boogie procedure. + /// Returns `None` if the function is a hook. + pub fn codegen_function(&self, instance: Instance<'tcx>) -> Option { + debug!(?instance, "boogie_codegen_function"); + if self.kani_intrinsic(instance).is_some() { + debug!("skipping kani intrinsic `{instance}`"); + return None; + } + let mut decl = self.codegen_declare_variables(instance); + let body = self.codegen_body(instance); + decl.push(body); + Some(Procedure::new( + self.tcx.symbol_name(instance).name.to_string(), + vec![], + vec![], + None, + Stmt::Block { statements: decl }, + )) + } + + fn codegen_declare_variables(&self, instance: Instance<'tcx>) -> Vec { + let mir = self.tcx.instance_mir(instance.def); + let ldecls = mir.local_decls(); + let decls: Vec = ldecls + .indices() + .enumerate() + .filter_map(|(_idx, lc)| { + let typ = ldecls[lc].ty; + if self.layout_of(typ).is_zst() { + return None; + } + debug!(?lc, ?typ, "codegen_declare_variables"); + let name = format!("{lc:?}"); + let boogie_type = self.codegen_type(typ); + Some(Stmt::Decl { name, typ: boogie_type }) + }) + .collect(); + decls + } + + fn codegen_type(&self, ty: Ty<'tcx>) -> Type { + trace!(typ=?ty, "codegen_type"); + match ty.kind() { + ty::Bool => Type::Bool, + ty::Int(_ity) => Type::Int, // TODO: use Bv + _ => todo!(), + } + } + + fn codegen_body(&self, instance: Instance<'tcx>) -> Stmt { + let mir = self.tcx.instance_mir(instance.def); + let statements: Vec = reverse_postorder(mir) + .map(|(bb, bbd)| self.codegen_block(mir.local_decls(), bb, bbd)) + .collect(); + Stmt::Block { statements } + } + + fn codegen_block( + &self, + local_decls: &LocalDecls<'tcx>, + bb: BasicBlock, + bbd: &BasicBlockData<'tcx>, + ) -> Stmt { + debug!(?bb, ?bbd, "codegen_block"); + // the first statement should be labelled. if there is no statements, then the + // terminator should be labelled. + let statements = match bbd.statements.len() { + 0 => { + let term = bbd.terminator(); + let tcode = self.codegen_terminator(local_decls, term); + vec![tcode] + } + _ => { + let mut statements: Vec = + bbd.statements.iter().map(|stmt| self.codegen_statement(stmt)).collect(); + + let term = self.codegen_terminator(local_decls, bbd.terminator()); + statements.push(term); + statements + } + }; + Stmt::Block { statements } + } + + fn codegen_statement(&self, stmt: &Statement<'tcx>) -> Stmt { + match &stmt.kind { + StatementKind::Assign(box (place, rvalue)) => { + debug!(?place, ?rvalue, "codegen_statement"); + let rv = self.codegen_rvalue(rvalue); + // assignment statement + let asgn = Stmt::Assignment { target: format!("{:?}", place.local), value: rv.1 }; + // add it to other statements generated while creating the rvalue (if any) + add_statement(rv.0, asgn) + } + StatementKind::FakeRead(..) + | StatementKind::SetDiscriminant { .. } + | StatementKind::Deinit(..) + | StatementKind::StorageLive(..) + | StatementKind::StorageDead(..) + | StatementKind::Retag(..) + | StatementKind::PlaceMention(..) + | StatementKind::AscribeUserType(..) + | StatementKind::Coverage(..) + | StatementKind::Intrinsic(..) + | StatementKind::ConstEvalCounter + | StatementKind::Nop => todo!(), + } + } + + /// Codegen an rvalue. Returns the expression for the rvalue and an optional + /// statement for any possible checks instrumented for the rvalue expression + fn codegen_rvalue(&self, rvalue: &Rvalue<'tcx>) -> (Option, Expr) { + debug!(rvalue=?rvalue, "codegen_rvalue"); + match rvalue { + Rvalue::Use(operand) => (None, self.codegen_operand(operand)), + Rvalue::BinaryOp(binop, box (lhs, rhs)) => self.codegen_binary_op(binop, lhs, rhs), + _ => todo!(), + } + } + + fn codegen_binary_op( + &self, + binop: &BinOp, + lhs: &Operand<'tcx>, + rhs: &Operand<'tcx>, + ) -> (Option, Expr) { + let expr = match binop { + BinOp::Eq => Expr::BinaryOp { + op: BinaryOp::Eq, + left: Box::new(self.codegen_operand(lhs)), + right: Box::new(self.codegen_operand(rhs)), + }, + _ => todo!(), + }; + (None, expr) + } + + fn codegen_terminator(&self, local_decls: &LocalDecls<'tcx>, term: &Terminator<'tcx>) -> Stmt { + let _trace_span = debug_span!("CodegenTerminator", statement = ?term.kind).entered(); + debug!("handling terminator {:?}", term); + match &term.kind { + TerminatorKind::Call { func, args, destination, target, .. } => self.codegen_funcall( + local_decls, + func, + args, + destination, + target, + term.source_info.span, + ), + TerminatorKind::Return => Stmt::Return, + _ => todo!(), + } + } + + fn codegen_funcall( + &self, + local_decls: &LocalDecls<'tcx>, + func: &Operand<'tcx>, + args: &[Operand<'tcx>], + destination: &Place<'tcx>, + target: &Option, + span: Span, + ) -> Stmt { + debug!(?func, ?args, ?destination, ?span, "codegen_funcall"); + let fargs = self.codegen_funcall_args(local_decls, args); + let funct = self.operand_ty(local_decls, func); + // TODO: Only Kani intrinsics are handled currently + match &funct.kind() { + ty::FnDef(defid, substs) => { + let instance = + Instance::expect_resolve(self.tcx, ty::ParamEnv::reveal_all(), *defid, substs); + + if let Some(intrinsic) = self.kani_intrinsic(instance) { + return self.codegen_kani_intrinsic( + intrinsic, + instance, + fargs, + *destination, + *target, + Some(span), + ); + } + todo!() + } + _ => todo!(), + } + } + + fn codegen_funcall_args( + &self, + local_decls: &LocalDecls<'tcx>, + args: &[Operand<'tcx>], + ) -> Vec { + debug!(?args, "codegen_funcall_args"); + args.iter() + .filter_map(|o| { + let ty = self.operand_ty(local_decls, o); + // TODO: handle non-primitive types + if ty.is_primitive() { + return Some(self.codegen_operand(o)); + } + // TODO: ignore non-primitive arguments for now (e.g. `msg` + // argument of `kani::assert`) + None + }) + .collect() + } + + fn codegen_operand(&self, o: &Operand<'tcx>) -> Expr { + trace!(operand=?o, "codegen_operand"); + // A MIR operand is either a constant (literal or `const` declaration) + // or a place (being moved or copied for this operation). + // An "operand" in MIR is the argument to an "Rvalue" (and is also used + // by some statements.) + match o { + Operand::Copy(place) | Operand::Move(place) => self.codegen_place(place), + Operand::Constant(c) => self.codegen_constant(c), + } + } + + fn codegen_place(&self, place: &Place<'tcx>) -> Expr { + debug!(place=?place, "codegen_place"); + debug!(place.local=?place.local, "codegen_place"); + debug!(place.projection=?place.projection, "codegen_place"); + self.codegen_local(place.local) } - pub fn declare_function(&mut self, instance: Instance) { - debug!(?instance, "boogie_codegen_declare_function"); + fn codegen_local(&self, local: Local) -> Expr { + // TODO: handle function definitions + Expr::Symbol { name: format!("{local:?}") } + } + + fn codegen_constant(&self, c: &Constant<'tcx>) -> Expr { + trace!(constant=?c, "codegen_constant"); + // TODO: monomorphize + match c.literal { + ConstantKind::Val(val, ty) => self.codegen_constant_value(val, ty), + _ => todo!(), + } + } + + fn codegen_constant_value(&self, val: ConstValue<'tcx>, ty: Ty<'tcx>) -> Expr { + debug!(val=?val, "codegen_constant_value"); + match val { + ConstValue::Scalar(s) => self.codegen_scalar(s, ty), + _ => todo!(), + } + } + + 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(_), 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!(), + } + } + + /// Write the program to the given writer + pub fn write(&self, writer: &mut T) -> std::io::Result<()> { + self.program.write_to(writer)?; + Ok(()) + } + + fn operand_ty(&self, local_decls: &LocalDecls<'tcx>, o: &Operand<'tcx>) -> Ty<'tcx> { + // TODO: monomorphize + o.ty(local_decls, self.tcx) + } +} + +impl<'tcx> LayoutOfHelpers<'tcx> for BoogieCtx<'tcx> { + type LayoutOfResult = TyAndLayout<'tcx>; + + fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: Ty<'tcx>) -> ! { + span_bug!(span, "failed to get layout for `{}`: {}", ty, err) + } +} + +impl<'tcx> HasParamEnv<'tcx> for BoogieCtx<'tcx> { + fn param_env(&self) -> ty::ParamEnv<'tcx> { + ty::ParamEnv::reveal_all() + } +} + +impl<'tcx> HasTyCtxt<'tcx> for BoogieCtx<'tcx> { + fn tcx(&self) -> TyCtxt<'tcx> { + self.tcx + } +} + +impl<'tcx> HasDataLayout for BoogieCtx<'tcx> { + fn data_layout(&self) -> &TargetDataLayout { + self.tcx.data_layout() + } +} + +impl<'tcx> BoogieCtx<'tcx> { + pub fn add_procedure(&mut self, procedure: Procedure) { + self.program.add_procedure(procedure); + } +} + +/// Create a new statement that includes `s1` (if non-empty) and `s2` +fn add_statement(s1: Option, s2: Stmt) -> Stmt { + match s1 { + Some(s1) => match s1 { + Stmt::Block { mut statements } => { + statements.push(s2); + Stmt::Block { statements } + } + _ => Stmt::Block { statements: vec![s1, s2] }, + }, + None => s2, } } diff --git a/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs b/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs new file mode 100644 index 000000000000..1411b88350ed --- /dev/null +++ b/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs @@ -0,0 +1,106 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module is for handling Kani intrinsics, i.e. items whose implementation +//! is defined in the Kani compiler. These items are defined in the `kani` +//! library and are annotated with a `rustc_diagnostic_item`. + +use crate::codegen_boogie::BoogieCtx; + +use boogie_ast::boogie_program::{Expr, Stmt}; +use rustc_middle::mir::{BasicBlock, Place}; +use rustc_middle::ty::Instance; +use rustc_span::Span; +use std::str::FromStr; +use strum::VariantNames; +use strum_macros::{EnumString, EnumVariantNames}; +use tracing::debug; + +// TODO: move this enum up to `kani_middle` +#[derive(Debug, Clone, PartialEq, Eq, EnumString, EnumVariantNames)] +pub enum KaniIntrinsic { + /// Kani assert statement (`kani::assert`) + KaniAssert, + + /// Kani assume statement (`kani::assume`) + KaniAssume, +} + +impl<'tcx> BoogieCtx<'tcx> { + /// If provided function is a Kani intrinsic (e.g. assert, assume, cover), returns it + // TODO: move this function up to `kani_middle` along with the enum + pub fn kani_intrinsic(&self, instance: Instance<'tcx>) -> Option { + let intrinsics = KaniIntrinsic::VARIANTS; + for intrinsic in intrinsics { + let attr_sym = rustc_span::symbol::Symbol::intern(intrinsic); + if let Some(attr_id) = self.tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) { + if instance.def.def_id() == *attr_id { + debug!("matched: {:?} {:?}", attr_id, attr_sym); + return Some(KaniIntrinsic::from_str(intrinsic).unwrap()); + } + } + } + None + } + + pub fn codegen_kani_intrinsic( + &self, + intrinsic: KaniIntrinsic, + instance: Instance<'tcx>, + fargs: Vec, + assign_to: Place<'tcx>, + target: Option, + span: Option, + ) -> Stmt { + match intrinsic { + KaniIntrinsic::KaniAssert => { + self.codegen_kani_assert(instance, fargs, assign_to, target, span) + } + KaniIntrinsic::KaniAssume => { + self.codegen_kani_assume(instance, fargs, assign_to, target, span) + } + } + } + + pub fn codegen_kani_assert( + &self, + _instance: Instance<'tcx>, + mut fargs: Vec, + _assign_to: Place<'tcx>, + _target: Option, + _span: Option, + ) -> Stmt { + // TODO: ignoring the `'static str` argument for now + assert_eq!(fargs.len(), 1); // 2); + let cond = fargs.remove(0); + // TODO: handle message + // TODO: handle location + + Stmt::Block { + statements: vec![ + Stmt::Assert { condition: cond }, + // TODO: handle target + ], + } + } + + pub fn codegen_kani_assume( + &self, + _instance: Instance<'tcx>, + mut fargs: Vec, + _assign_to: Place<'tcx>, + _target: Option, + _span: Option, + ) -> Stmt { + assert_eq!(fargs.len(), 1); + let cond = fargs.remove(0); + // TODO: handle location + + Stmt::Block { + statements: vec![ + Stmt::Assume { condition: cond }, + // TODO: handle target + ], + } + } +} diff --git a/kani-compiler/src/codegen_boogie/context/mod.rs b/kani-compiler/src/codegen_boogie/context/mod.rs index 3164f967c1b9..76a198335ec1 100644 --- a/kani-compiler/src/codegen_boogie/context/mod.rs +++ b/kani-compiler/src/codegen_boogie/context/mod.rs @@ -5,5 +5,6 @@ //! the file level comments for more details. mod boogie_ctx; +mod kani_intrinsic; pub use boogie_ctx::BoogieCtx; diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index f0d43656f55b..130ce2bf6dac 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -30,6 +30,7 @@ ${SCRIPT_DIR}/kani-fmt.sh --check RUSTFLAGS="-D warnings" cargo build-dev # Unit tests +cargo test -p boogie_ast cargo test -p cprover_bindings cargo test -p kani-compiler cargo test -p kani-driver