From 8ea0e00bc5ed446e0ab38bdb6a57beb26a0a3eb3 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Mon, 18 Dec 2023 17:49:13 -0800 Subject: [PATCH] [Boogie Backend] Add an unbounded array API (#2955) This PR adds an API for creating arrays with non-deterministic content and length. The array is implemented as a Boogie datatype with a data field (a Boogie map), and a length field (a bitvector). The PR also adds a test that demonstrates how the API can be used for performing unbounded verification. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- boogie_ast/src/boogie_program/mod.rs | 38 +++- boogie_ast/src/boogie_program/writer.rs | 35 +++- .../src/codegen_boogie/context/boogie_ctx.rs | 175 +++++++++++++++--- .../codegen_boogie/context/kani_intrinsic.rs | 174 +++++++++++++++-- library/kani/src/array.rs | 72 +++++++ library/kani/src/lib.rs | 1 + .../unbounded_array_copy/config.yml | 4 + .../unbounded_array_copy/expected | 50 +++++ .../gen_boogie_and_dump.sh | 13 ++ .../unbounded_array_copy/test.rs | 31 ++++ 10 files changed, 545 insertions(+), 48 deletions(-) create mode 100644 library/kani/src/array.rs create mode 100644 tests/script-based-boogie/unbounded_array_copy/config.yml create mode 100644 tests/script-based-boogie/unbounded_array_copy/expected create mode 100755 tests/script-based-boogie/unbounded_array_copy/gen_boogie_and_dump.sh create mode 100644 tests/script-based-boogie/unbounded_array_copy/test.rs diff --git a/boogie_ast/src/boogie_program/mod.rs b/boogie_ast/src/boogie_program/mod.rs index db46c9491ae0..fc9fc85c6d10 100644 --- a/boogie_ast/src/boogie_program/mod.rs +++ b/boogie_ast/src/boogie_program/mod.rs @@ -8,6 +8,7 @@ mod writer; use num_bigint::BigInt; use std::ops::Not; +use std::string::ToString; struct TypeDeclaration {} struct ConstDeclaration {} @@ -69,6 +70,7 @@ impl Parameter { } /// Literal types +#[derive(Clone, Debug, PartialEq, Eq)] pub enum Literal { /// Boolean values: `true`/`false` Bool(bool), @@ -87,6 +89,7 @@ impl Literal { } /// Unary operators +#[derive(Clone, Debug, PartialEq, Eq)] pub enum UnaryOp { /// Logical negation Not, @@ -95,6 +98,7 @@ pub enum UnaryOp { Neg, } +#[derive(Clone, Debug, PartialEq, Eq)] pub enum BinaryOp { /// Logical AND And, @@ -137,6 +141,7 @@ pub enum BinaryOp { } /// Expr types +#[derive(Clone, Debug, PartialEq, Eq)] pub enum Expr { /// Literal (constant) Literal(Literal), @@ -152,6 +157,12 @@ pub enum Expr { /// Function call FunctionCall { symbol: String, arguments: Vec }, + + /// Field operator for datatypes + Field { base: Box, field: String }, + + /// Select operation for maps + Select { base: Box, key: Box }, } impl Expr { @@ -164,6 +175,12 @@ impl Expr { } } +impl ToString for Expr { + fn to_string(&self) -> String { + writer::write_expr(self) + } +} + impl Not for Expr { type Output = Self; @@ -184,7 +201,7 @@ pub enum Stmt { Assume { condition: Expr }, /// Statement block: `{ statements }` - Block { statements: Vec }, + Block { label: Option, statements: Vec }, /// Break statement: `break;` /// A `break` in boogie can take a label, but this is probably not needed @@ -196,22 +213,35 @@ pub enum Stmt { /// Declaration statement: `var name: type;` Decl { name: String, typ: Type }, + /// Havoc statement: `havoc x;` + Havoc { name: String }, + /// 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, + /// Skip statement + Skip, + /// While statement: `while (condition) { body }` While { condition: Expr, body: Box }, } +impl Stmt { + pub fn block(statements: Vec) -> Self { + Self::Block { label: None, statements } + } + + pub fn labelled_block(label: String, statements: Vec) -> Self { + Self::Block { label: Some(label), statements } + } +} + /// A Boogie datatype. A datatype is defined by one or more constructors. /// See https://github.com/boogie-org/boogie/pull/685 for more details. pub struct DataType { diff --git a/boogie_ast/src/boogie_program/writer.rs b/boogie_ast/src/boogie_program/writer.rs index af0699612486..5464aa0eabc1 100644 --- a/boogie_ast/src/boogie_program/writer.rs +++ b/boogie_ast/src/boogie_program/writer.rs @@ -310,6 +310,16 @@ impl Expr { } write!(writer, ")")?; } + Expr::Field { base, field } => { + base.write_to(writer)?; + write!(writer, "->{field}")?; + } + Expr::Select { base, key } => { + base.write_to(writer)?; + write!(writer, "[(")?; + key.write_to(writer)?; + write!(writer, ")]")?; + } } Ok(()) } @@ -336,7 +346,12 @@ impl Stmt { condition.write_to(writer)?; writeln!(writer, ";")?; } - Stmt::Block { statements } => { + Stmt::Block { label, statements } => { + if let Some(label) = label { + writer.indent()?; + write!(writer, "{label}:")?; + writeln!(writer)?; + } for s in statements { s.write_to(writer)?; } @@ -362,6 +377,10 @@ impl Stmt { typ.write_to(writer)?; writeln!(writer, ";")?; } + Stmt::Havoc { name } => { + writer.indent()?; + writeln!(writer, "havoc {}; ", name)?; + } Stmt::If { condition, body, else_body } => { writer.indent()?; write!(writer, "if (")?; @@ -386,14 +405,11 @@ impl Stmt { writer.indent()?; writeln!(writer, "goto {label};")?; } - Stmt::Label { label } => { - writer.indent()?; - writeln!(writer, "{label}:")?; - } Stmt::Return => { writer.indent()?; writeln!(writer, "return;")?; } + Stmt::Skip => {} Stmt::While { condition, body } => { writer.indent()?; write!(writer, "while (")?; @@ -510,6 +526,13 @@ impl BinaryOp { } } +pub fn write_expr(e: &Expr) -> String { + let mut buf = Vec::new(); + let mut writer = writer::Writer::new(&mut buf); + e.write_to(&mut writer).unwrap(); + String::from_utf8(buf).unwrap() +} + #[cfg(test)] mod tests { use super::*; @@ -571,6 +594,7 @@ mod tests { modifies: Vec::new(), }), body: Stmt::Block { + label: Some("label1".into()), statements: vec![ Stmt::Decl { name: "x".to_string(), typ: Type::Int }, Stmt::Decl { name: "y".to_string(), typ: Type::Int }, @@ -643,6 +667,7 @@ function {:bvbuiltin \"bvand\"} $BvAnd(lhs: T, rhs: T) returns (T); procedure main() returns (z: bool) ensures (z == true); { + label1: var x: int; var y: int; var p: Pair bool int; diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs index 0a19cc8cd950..103d5e14c59d 100644 --- a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs +++ b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs @@ -1,25 +1,27 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use itertools::Itertools; use std::io::Write; use crate::kani_queries::QueryDb; use boogie_ast::boogie_program::{ - BinaryOp, BoogieProgram, Expr, Literal, Procedure, Stmt, Type, UnaryOp, + BinaryOp, BoogieProgram, DataType, DataTypeConstructor, Expr, Literal, Parameter, Procedure, + Stmt, Type, UnaryOp, }; use rustc_data_structures::fx::FxHashMap; use rustc_middle::mir::interpret::Scalar; use rustc_middle::mir::traversal::reverse_postorder; use rustc_middle::mir::{ BasicBlock, BasicBlockData, BinOp, Body, Const as mirConst, ConstOperand, ConstValue, - HasLocalDecls, Local, Operand, Place, Rvalue, Statement, StatementKind, Terminator, - TerminatorKind, UnOp, VarDebugInfoContents, + HasLocalDecls, Local, Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, + SwitchTargets, Terminator, TerminatorKind, UnOp, VarDebugInfoContents, }; 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_middle::ty::{self, Instance, IntTy, List, Ty, TyCtxt, UintTy}; use rustc_span::Span; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use std::collections::hash_map::Entry; @@ -29,6 +31,8 @@ use tracing::{debug, debug_span, trace}; use super::kani_intrinsic::get_kani_intrinsic; use super::smt_builtins::{smt_builtin_binop, SmtBvBuiltin}; +const UNBOUNDED_ARRAY: &str = "$Array"; + /// A context that provides the main methods for translating MIR constructs to /// Boogie and stores what has been codegen so far pub struct BoogieCtx<'tcx> { @@ -60,6 +64,22 @@ impl<'tcx> BoogieCtx<'tcx> { bv_builtin.is_predicate(), )); } + + // Add unbounded array + let name = String::from(UNBOUNDED_ARRAY); + let constructor = DataTypeConstructor::new( + name.clone(), + vec![ + Parameter::new( + String::from("data"), + Type::map(Type::Bv(64), Type::parameter(String::from("T"))), + ), + Parameter::new(String::from("len"), Type::Bv(64)), + ], + ); + let unbounded_array_data_type = + DataType::new(name.clone(), vec![String::from("T")], vec![constructor]); + program.add_datatype(unbounded_array_data_type); } /// Codegen a function into a Boogie procedure. @@ -70,7 +90,7 @@ impl<'tcx> BoogieCtx<'tcx> { debug!("skipping kani intrinsic `{instance}`"); return None; } - let fcx = FunctionCtx::new(self, instance); + let mut fcx = FunctionCtx::new(self, instance); let mut decl = fcx.codegen_declare_variables(); let body = fcx.codegen_body(); decl.push(body); @@ -79,7 +99,7 @@ impl<'tcx> BoogieCtx<'tcx> { vec![], vec![], None, - Stmt::Block { statements: decl }, + Stmt::block(decl), )) } @@ -100,6 +120,14 @@ pub(crate) struct FunctionCtx<'a, 'tcx> { mir: &'a Body<'tcx>, /// Maps from local to the name of the corresponding Boogie variable. local_names: FxHashMap, + /// A map to keep track of the source of each borrow. This is an ugly hack + /// that only works in very special cases, more specifically where an + /// explicit variable is borrowed, e.g. + /// ``` + /// let b = &mut x; + /// ```` + /// In this case, the map will contain an entry that maps `b` to `x` + pub(crate) ref_to_expr: FxHashMap, Expr>, } impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { @@ -135,7 +163,7 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { }; local_names.insert(local, name); } - Self { bcx, instance, mir, local_names } + Self { bcx, instance, mir, local_names, ref_to_expr: FxHashMap::default() } } fn codegen_declare_variables(&self) -> Vec { @@ -154,6 +182,12 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { } debug!(?lc, ?typ, "codegen_declare_variables"); let name = self.local_name(lc).clone(); + // skip the declaration of mutable references (e.g. `let mut _9: &mut i32;`) + if let ty::Ref(_, _, m) = typ.kind() { + if m.is_mut() { + return None; + } + } let boogie_type = self.codegen_type(typ); Some(Stmt::Decl { name, typ: boogie_type }) }) @@ -167,17 +201,52 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { ty::Bool => Type::Bool, ty::Int(ity) => Type::Bv(ity.bit_width().unwrap_or(64).try_into().unwrap()), ty::Uint(uty) => Type::Bv(uty.bit_width().unwrap_or(64).try_into().unwrap()), + ty::Tuple(types) => { + // TODO: Only handles first element of tuple for now (e.g. + // ignores overflow field of an addition and only takes the + // result field) + self.codegen_type(types.iter().next().unwrap()) + } + ty::Adt(def, args) => { + let name = format!("{def:?}"); + if name == "kani::array::Array" { + let fields = def.all_fields(); + //let mut field_types: Vec = fields.filter_map(|f| { + // let typ = f.ty(self.tcx(), args); + // self.layout_of(typ).is_zst().then(|| self.codegen_type(typ)) + //}).collect(); + //assert_eq!(field_types.len(), 1); + //let typ = field_types.pop().unwrap(); + let phantom_data_field = fields + .filter(|f| self.layout_of(f.ty(self.tcx(), args)).is_zst()) + .exactly_one() + .unwrap_or_else(|_| panic!()); + let phantom_data_type = phantom_data_field.ty(self.tcx(), args); + assert!(phantom_data_type.is_phantom_data()); + let field_type = args.types().exactly_one().unwrap_or_else(|_| panic!()); + let typ = self.codegen_type(field_type); + Type::user_defined(String::from(UNBOUNDED_ARRAY), vec![typ]) + } else { + todo!() + } + } + ty::Ref(_r, ty, m) => { + if m.is_not() { + return self.codegen_type(*ty); + } + todo!() + } _ => todo!(), } } - fn codegen_body(&self) -> Stmt { + fn codegen_body(&mut self) -> Stmt { let statements: Vec = reverse_postorder(self.mir).map(|(bb, bbd)| self.codegen_block(bb, bbd)).collect(); - Stmt::Block { statements } + Stmt::block(statements) } - fn codegen_block(&self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) -> Stmt { + fn codegen_block(&mut self, 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. @@ -196,19 +265,34 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { statements } }; - Stmt::Block { statements } + Stmt::labelled_block(format!("{bb:?}"), statements) } - fn codegen_statement(&self, stmt: &Statement<'tcx>) -> Stmt { + fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt { match &stmt.kind { StatementKind::Assign(box (place, rvalue)) => { debug!(?place, ?rvalue, "codegen_statement"); - let rv = self.codegen_rvalue(rvalue); let place_name = self.local_name(place.local).clone(); - // assignment statement - let asgn = Stmt::Assignment { target: place_name, value: rv.1 }; - // add it to other statements generated while creating the rvalue (if any) - add_statement(rv.0, asgn) + if let Rvalue::Ref(_, _, rhs) = rvalue { + let expr = self.codegen_place(rhs); + self.ref_to_expr.insert(*place, expr); + Stmt::Skip + } else if is_deref(place) { + // lookup the place itself + debug!(?self.ref_to_expr, ?place, ?place.local, "codegen_statement_assign_deref"); + let empty_projection = List::empty(); + let place = Place { local: place.local, projection: empty_projection }; + let expr = self.ref_to_expr.get(&place).unwrap(); + let rv = self.codegen_rvalue(rvalue); + let asgn = Stmt::Assignment { target: expr.to_string(), value: rv.1 }; + add_statement(rv.0, asgn) + } else { + let rv = self.codegen_rvalue(rvalue); + // assignment statement + let asgn = Stmt::Assignment { target: place_name, value: rv.1 }; + // add it to other statements generated while creating the rvalue (if any) + add_statement(rv.0, asgn) + } } StatementKind::FakeRead(..) | StatementKind::SetDiscriminant { .. } @@ -233,6 +317,10 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { Rvalue::Use(operand) => (None, self.codegen_operand(operand)), Rvalue::UnaryOp(op, operand) => self.codegen_unary_op(op, operand), Rvalue::BinaryOp(binop, box (lhs, rhs)) => self.codegen_binary_op(binop, lhs, rhs), + Rvalue::CheckedBinaryOp(binop, box (ref e1, ref e2)) => { + // TODO: handle overflow check + self.codegen_binary_op(binop, e1, e2) + } _ => todo!(), } } @@ -318,20 +406,23 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { (None, expr) } - fn codegen_terminator(&self, term: &Terminator<'tcx>) -> Stmt { + fn codegen_terminator(&mut self, 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(func, args, destination, target, term.source_info.span) } + TerminatorKind::Goto { target } => Stmt::Goto { label: format!("{target:?}") }, TerminatorKind::Return => Stmt::Return, + TerminatorKind::SwitchInt { discr, targets } => self.codegen_switch_int(discr, targets), + TerminatorKind::Assert { .. } => Stmt::Skip, // TODO: ignore injection assertions for now _ => todo!(), } } fn codegen_funcall( - &self, + &mut self, func: &Operand<'tcx>, args: &[Operand<'tcx>], destination: &Place<'tcx>, @@ -367,6 +458,32 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { } } + fn codegen_switch_int(&self, discr: &Operand<'tcx>, targets: &SwitchTargets) -> Stmt { + debug!(discr=?discr, targets=?targets, "codegen_switch_int"); + let op = self.codegen_operand(discr); + if targets.all_targets().len() == 2 { + let then = targets.iter().next().unwrap(); + let right = match self.operand_ty(discr).kind() { + ty::Bool => Literal::Bool(then.0 != 0), + ty::Uint(_) => Literal::bv(128, then.0.into()), + _ => unreachable!(), + }; + // model as an if + return Stmt::If { + condition: Expr::BinaryOp { + op: BinaryOp::Eq, + left: Box::new(op), + right: Box::new(Expr::Literal(right)), + }, + body: Box::new(Stmt::Goto { label: format!("{:?}", then.1) }), + else_body: Some(Box::new(Stmt::Goto { + label: format!("{:?}", targets.otherwise()), + })), + }; + } + todo!() + } + fn codegen_funcall_args(&self, args: &[Operand<'tcx>]) -> Vec { debug!(?args, "codegen_funcall_args"); args.iter() @@ -395,10 +512,14 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { } } - fn codegen_place(&self, place: &Place<'tcx>) -> Expr { + pub(crate) 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"); + if let Some(expr) = self.ref_to_expr.get(place) { + return expr.clone(); + } + //let local_ty = self.mir.local_decls()[place.local].ty; self.codegen_local(place.local) } @@ -494,12 +615,20 @@ impl<'a, 'tcx> HasDataLayout for FunctionCtx<'a, 'tcx> { fn add_statement(s1: Option, s2: Stmt) -> Stmt { match s1 { Some(s1) => match s1 { - Stmt::Block { mut statements } => { + Stmt::Block { label, mut statements } => { statements.push(s2); - Stmt::Block { statements } + Stmt::Block { label, statements } } - _ => Stmt::Block { statements: vec![s1, s2] }, + _ => Stmt::block(vec![s1, s2]), }, None => s2, } } + +fn is_deref(p: &Place<'_>) -> bool { + let proj = p.projection; + if proj.len() == 1 && proj.iter().next().unwrap() == ProjectionElem::Deref { + return true; + } + false +} diff --git a/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs b/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs index 4a7afbae3699..addbeb942f81 100644 --- a/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs +++ b/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs @@ -7,7 +7,7 @@ use super::boogie_ctx::FunctionCtx; -use boogie_ast::boogie_program::Stmt; +use boogie_ast::boogie_program::{Expr, Stmt}; use rustc_middle::mir::{BasicBlock, Operand, Place}; use rustc_middle::ty::{Instance, TyCtxt}; use rustc_span::Span; @@ -18,12 +18,25 @@ use tracing::debug; // TODO: move this enum up to `kani_middle` #[derive(Debug, Clone, PartialEq, Eq, EnumString, EnumVariantNames)] +#[allow(clippy::enum_variant_names)] pub enum KaniIntrinsic { /// Kani assert statement (`kani::assert`) KaniAssert, /// Kani assume statement (`kani::assume`) KaniAssume, + + /// Kani unbounded array (`kani::array::any_array`) + KaniAnyArray, + + /// `kani::array::Array::len` + KaniAnyArrayLen, + + /// `Index for kani::array::Array` + KaniAnyArrayIndex, + + /// `IndexMut for kani::array::Array` + KaniAnyArrayIndexMut, } /// If provided function is a Kani intrinsic (e.g. assert, assume, cover), returns it @@ -46,7 +59,7 @@ pub fn get_kani_intrinsic<'tcx>( impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { pub fn codegen_kani_intrinsic( - &self, + &mut self, intrinsic: KaniIntrinsic, instance: Instance<'tcx>, args: &[Operand<'tcx>], @@ -61,10 +74,22 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { KaniIntrinsic::KaniAssume => { self.codegen_kani_assume(instance, args, assign_to, target, span) } + KaniIntrinsic::KaniAnyArray => { + self.codegen_kani_any_array(instance, args, assign_to, target, span) + } + KaniIntrinsic::KaniAnyArrayLen => { + self.codegen_kani_any_array_len(instance, args, assign_to, target, span) + } + KaniIntrinsic::KaniAnyArrayIndex => { + self.codegen_kani_any_array_index(instance, args, assign_to, target, span) + } + KaniIntrinsic::KaniAnyArrayIndexMut => { + self.codegen_kani_any_array_index_mut(instance, args, assign_to, target, span) + } } } - pub fn codegen_kani_assert( + fn codegen_kani_assert( &self, _instance: Instance<'tcx>, args: &[Operand<'tcx>], @@ -78,15 +103,13 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { // TODO: handle message // TODO: handle location - Stmt::Block { - statements: vec![ - Stmt::Assert { condition: cond }, - // TODO: handle target - ], - } + Stmt::block(vec![ + Stmt::Assert { condition: cond }, + // TODO: handle target + ]) } - pub fn codegen_kani_assume( + fn codegen_kani_assume( &self, _instance: Instance<'tcx>, args: &[Operand<'tcx>], @@ -98,11 +121,130 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> { let cond = self.codegen_operand(&args[0]); // TODO: handle location - Stmt::Block { - statements: vec![ - Stmt::Assume { condition: cond }, - // TODO: handle target - ], - } + Stmt::block(vec![ + Stmt::Assume { condition: cond }, + // TODO: handle target + ]) + } + + fn codegen_kani_any_raw( + &self, + _instance: Instance<'tcx>, + args: &[Operand<'tcx>], + assign_to: Place<'tcx>, + target: Option, + _span: Option, + ) -> Stmt { + assert!(args.is_empty()); + + let place = self.codegen_place(&assign_to); + + let symbol = if let Expr::Symbol { name } = place { + name + } else { + panic!("expecting place to be a symbol and not {place:?}.") + }; + + Stmt::block(vec![ + Stmt::Havoc { name: symbol }, + Stmt::Goto { label: format!("{:?}", target.unwrap()) }, + ]) + } + + fn codegen_kani_any_array( + &self, + instance: Instance<'tcx>, + args: &[Operand<'tcx>], + assign_to: Place<'tcx>, + target: Option, + span: Option, + ) -> Stmt { + assert!(args.is_empty()); + + self.codegen_kani_any_raw(instance, args, assign_to, target, span) + } + + fn codegen_kani_any_array_len( + &self, + _instance: Instance<'tcx>, + args: &[Operand<'tcx>], + assign_to: Place<'tcx>, + _target: Option, + _span: Option, + ) -> Stmt { + assert_eq!(args.len(), 1); + debug!(?args, "codegen_kani_any_array_len"); + + let self_ref = &args[0]; + let expr = self + .operand_to_expr(self_ref) + .expect("expecting operand to be a ref to an existing expression"); + let len = Expr::Field { base: Box::new(expr.clone()), field: String::from("len") }; + + let place = self.codegen_place(&assign_to); + + let Expr::Symbol { name } = place else { panic!("expecting place to be a symbol") }; + + Stmt::Assignment { target: name, value: len } + } + + fn codegen_kani_any_array_index( + &self, + _instance: Instance<'tcx>, + args: &[Operand<'tcx>], + assign_to: Place<'tcx>, + _target: Option, + _span: Option, + ) -> Stmt { + assert_eq!(args.len(), 2); + debug!(?args, "codegen_kani_any_array_index"); + + let self_ref = &args[0]; + let expr = self + .operand_to_expr(self_ref) + .expect("expecting operand to be a ref to an existing expression"); + let map = Expr::Field { base: Box::new(expr.clone()), field: String::from("data") }; + + let index = self.codegen_operand(&args[1]); + let index_expr = Expr::Select { base: Box::new(map), key: Box::new(index) }; + + let place = self.codegen_place(&assign_to); + + let Expr::Symbol { name } = place else { panic!("expecting place to be a symbol") }; + + Stmt::Assignment { target: name, value: index_expr } + } + + fn codegen_kani_any_array_index_mut( + &mut self, + _instance: Instance<'tcx>, + args: &[Operand<'tcx>], + assign_to: Place<'tcx>, + _target: Option, + _span: Option, + ) -> Stmt { + assert_eq!(args.len(), 2); + debug!(?args, "codegen_kani_any_array_index_mut"); + + let mut_self_ref = &args[0]; + let expr = self + .operand_to_expr(mut_self_ref) + .expect("expecting operand to be a ref to an existing expression"); + let map = Expr::Field { base: Box::new(expr.clone()), field: String::from("data") }; + + let index = self.codegen_operand(&args[1]); + + // TODO: change `Stmt::Assignment` to be in terms of a symbol not a + // string to avoid the hacky code below + let index_expr = Expr::Select { base: Box::new(map), key: Box::new(index) }; + self.ref_to_expr.insert(assign_to, index_expr); + Stmt::Skip + } + + fn operand_to_expr(&self, operand: &Operand<'tcx>) -> Option<&Expr> { + let Operand::Move(place) = operand else { + return None; + }; + self.ref_to_expr.get(place) } } diff --git a/library/kani/src/array.rs b/library/kani/src/array.rs new file mode 100644 index 000000000000..52b758c85399 --- /dev/null +++ b/library/kani/src/array.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use crate::Arbitrary; +use std::marker::PhantomData; +use std::ops::{Index, IndexMut}; + +/// Create an array with non-deterministic content and a non-deterministic +/// length. This API currently works with the Boogie backend only. +/// +/// # Example: +/// +/// ``` +/// let arr = kani::array::any_array::(); +/// if arr.len() > 2 { +/// kani::assume(arr[0] == 0); +/// kani::assume(arr[1] == arr[0]); +/// assert!(arr[1] == 0); +/// } +/// ``` +#[inline(never)] +#[rustc_diagnostic_item = "KaniAnyArray"] +pub fn any_array() -> Array +where + T: Arbitrary, +{ + #[allow(clippy::empty_loop)] + loop {} +} + +/// An array-like data structure that is intended for unbounded verification +pub struct Array { + _p: PhantomData, + len: usize, +} + +impl Array +where + T: Arbitrary, +{ + /// Get the length of the array + #[inline(never)] + #[rustc_diagnostic_item = "KaniAnyArrayLen"] + pub fn len(&self) -> usize { + self.len + } + + /// Whether the array is empty + pub fn is_empty(&self) -> bool { + self.len == 0 + } +} + +impl Index for Array { + type Output = T; + + #[inline(never)] + #[rustc_diagnostic_item = "KaniAnyArrayIndex"] + fn index(&self, _index: usize) -> &Self::Output { + #[allow(clippy::empty_loop)] + loop {} + } +} + +impl IndexMut for Array { + #[inline(never)] + #[rustc_diagnostic_item = "KaniAnyArrayIndexMut"] + fn index_mut(&mut self, _index: usize) -> &mut Self::Output { + #[allow(clippy::empty_loop)] + loop {} + } +} diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index d2959e548417..b6196fab6ff0 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -18,6 +18,7 @@ #![allow(internal_features)] pub mod arbitrary; +pub mod array; #[cfg(feature = "concrete_playback")] mod concrete_playback; pub mod futures; diff --git a/tests/script-based-boogie/unbounded_array_copy/config.yml b/tests/script-based-boogie/unbounded_array_copy/config.yml new file mode 100644 index 000000000000..2e9f6c922a1e --- /dev/null +++ b/tests/script-based-boogie/unbounded_array_copy/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: gen_boogie_and_dump.sh +expected: expected diff --git a/tests/script-based-boogie/unbounded_array_copy/expected b/tests/script-based-boogie/unbounded_array_copy/expected new file mode 100644 index 000000000000..8f88ea082959 --- /dev/null +++ b/tests/script-based-boogie/unbounded_array_copy/expected @@ -0,0 +1,50 @@ +// Datatypes: +datatype $Array { $Array(data: [bv64]T, len: bv64) } + +// Functions: +function {:bvbuiltin "bvult"} $BvUnsignedLessThan(lhs: T, rhs: T) returns (bool); + +function {:bvbuiltin "bvslt"} $BvSignedLessThan(lhs: T, rhs: T) returns (bool); + +function {:bvbuiltin "bvugt"} $BvUnsignedGreaterThan(lhs: T, rhs: T) returns (bool); + +function {:bvbuiltin "bvsgt"} $BvSignedGreaterThan(lhs: T, rhs: T) returns (bool); + +function {:bvbuiltin "bvadd"} $BvAdd(lhs: T, rhs: T) returns (T); + +function {:bvbuiltin "bvor"} $BvOr(lhs: T, rhs: T) returns (T); + +function {:bvbuiltin "bvand"} $BvAnd(lhs: T, rhs: T) returns (T); + +function {:bvbuiltin "bvshl"} $BvShl(lhs: T, rhs: T) returns (T); + +function {:bvbuiltin "bvlshr"} $BvShr(lhs: T, rhs: T) returns (T); + +// Procedures: +procedure +{ + var src: $Array bv32; + var dst: $Array bv32; + var src_len: bv64; + var dst_len: bv64; + var i: bv64; + bb + havoc src; + goto bb + havoc dst; + src_len := src->len; + dst_len := dst->len; + i := 0bv64; + := $BvUnsignedLessThan( + if (\ + goto bb\ + } else {\ + goto bb\ + } + i := 0bv64; + return; + := dst->data[ + := src->data[ + assert + := $BvAdd( +} diff --git a/tests/script-based-boogie/unbounded_array_copy/gen_boogie_and_dump.sh b/tests/script-based-boogie/unbounded_array_copy/gen_boogie_and_dump.sh new file mode 100755 index 000000000000..0233ad780871 --- /dev/null +++ b/tests/script-based-boogie/unbounded_array_copy/gen_boogie_and_dump.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set +e + +# Delete any leftover Boogie files +rm *.bpl + +echo "[TEST] Run verification..." +kani -Zboogie test.rs + +cat *.bpl diff --git a/tests/script-based-boogie/unbounded_array_copy/test.rs b/tests/script-based-boogie/unbounded_array_copy/test.rs new file mode 100644 index 000000000000..adce37e1adc4 --- /dev/null +++ b/tests/script-based-boogie/unbounded_array_copy/test.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! A test that demonstrates unbounded verification of array-based programs. +//! The test uses `any_array` which creates arrays with non-deterministic +//! content and length. +//! The `src` array is copied into the `dst` array up to the minimum length of +//! the two arrays. + +#[kani::proof] +fn copy() { + let src = kani::array::any_array::(); + let mut dst = kani::array::any_array::(); + let src_len: usize = src.len(); + let dst_len: usize = dst.len(); + + // copy as many elements as possible of `src` to `dst` + let mut i: usize = 0; + // Loop invariant: forall j: usize :: j < i => dst[j] == src[j]) + while i < src_len && i < dst_len { + dst[i] = src[i]; + i = i + 1; + } + + // check that the data was copied + i = 0; + while i < src_len && i < dst_len { + kani::assert(dst[i] == src[i], "element doesn't have the correct value"); + i = i + 1; + } +}