From 3d8705013ec6320fb93a708dde7241f07689bd25 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sat, 7 Sep 2024 14:31:17 -0400 Subject: [PATCH] Add support for quantifiers Signed-off-by: Felipe R. Monteiro --- cprover_bindings/src/goto_program/expr.rs | 18 ++ cprover_bindings/src/irep/to_irep.rs | 24 ++ .../codegen_cprover_gotoc/overrides/hooks.rs | 208 ++++++++++++++++++ library/kani_core/src/lib.rs | 38 ++++ rfc/src/rfcs/0010-quantifiers.md | 28 ++- tests/expected/quantifiers/expected | 1 + tests/expected/quantifiers/from_raw_parts.rs | 38 ++++ 7 files changed, 343 insertions(+), 12 deletions(-) create mode 100644 tests/expected/quantifiers/expected create mode 100644 tests/expected/quantifiers/from_raw_parts.rs diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 2a29985cb229..650ca9476c80 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -177,6 +177,14 @@ pub enum ExprValue { Vector { elems: Vec, }, + Forall { + variable: Expr, // symbol + domain: Expr, // where + }, + Exists { + variable: Expr, // symbol + domain: Expr, // where + }, } /// Binary operators. The names are the same as in the Irep representation. @@ -968,6 +976,16 @@ impl Expr { let typ = typ.aggr_tag().unwrap(); expr!(Union { value, field }, typ) } + + pub fn forall_expr(typ: Type, variable: Expr, domain: Expr) -> Expr { + assert!(variable.is_symbol()); + expr!(Forall { variable, domain }, typ) + } + + pub fn exists_expr(typ: Type, variable: Expr, domain: Expr) -> Expr { + assert!(variable.is_symbol()); + expr!(Exists { variable, domain }, typ) + } } /// Constructors for Binary Operations diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index e007652a04a9..036458e5972b 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -379,6 +379,30 @@ impl ToIrep for ExprValue { sub: elems.iter().map(|x| x.to_irep(mm)).collect(), named_sub: linear_map![], }, + ExprValue::Forall { variable, domain } => Irep { + id: IrepId::Forall, + sub: vec![ + Irep { + id: IrepId::Tuple, + sub: vec![variable.to_irep(mm)], + named_sub: linear_map![], + }, + domain.to_irep(mm), + ], + named_sub: linear_map![], + }, + ExprValue::Exists { variable, domain } => Irep { + id: IrepId::Exists, + sub: vec![ + Irep { + id: IrepId::Tuple, + sub: vec![variable.to_irep(mm)], + named_sub: linear_map![], + }, + domain.to_irep(mm), + ], + named_sub: linear_map![], + }, } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 75943b23a392..b2b7670af8d8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -14,16 +14,22 @@ use crate::kani_middle::attributes; use crate::kani_middle::kani_functions::{KaniFunction, KaniHook}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::CIntType; +use cbmc::goto_program::Symbol as GotoSymbol; use cbmc::goto_program::{BuiltinFn, Expr, Stmt, Type}; +use rustc_ast::Closure; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{BasicBlockIdx, Place}; +use stable_mir::ty::RigidTy; +use stable_mir::ty::{ClosureKind, TyKind}; use stable_mir::{CrateDef, ty::Span}; use std::collections::HashMap; use std::rc::Rc; use tracing::debug; +use cbmc::goto_program::ExprValue; + pub trait GotocHook { /// if the hook applies, it means the codegen would do something special to it fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool; @@ -649,6 +655,206 @@ impl GotocHook for LoopInvariantRegister { } } +struct Forall; + +/// __CROVER_forall +impl GotocHook for Forall { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance.def, "KaniExists") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + instance: Instance, + fargs: Vec, + assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + let args_from_instance = instance.args().0; + let loc = gcx.codegen_span_stable(span); + let target = target.unwrap(); + let lower_bound = &fargs[0]; + let upper_bound = &fargs[1]; + let predicate = &fargs[2]; + let mut closure_call_expr: Option = None; + + for arg in args_from_instance.iter() { + let arg_ty = arg.ty().unwrap(); + let kind = arg_ty.kind(); + let arg_kind = kind.rigid().unwrap(); + + match arg_kind { + RigidTy::Closure(def_id, args) => { + let instance_closure = + Instance::resolve_closure(*def_id, args, ClosureKind::Fn) + .expect("failed to normalize and resolve closure during codegen"); + closure_call_expr = Some(gcx.codegen_func_expr(instance_closure, loc)); + } + _ => { + println!("Unexpected type\n"); + } + } + } + + // Extract the identifier from the variable expression + let ident = match lower_bound.value() { + ExprValue::Symbol { identifier } => Some(identifier), + _ => None, + }; + + if let Some(identifier) = ident { + let new_identifier = format!("{}_kani", identifier); + let new_symbol = GotoSymbol::variable( + new_identifier.clone(), + new_identifier.clone(), + lower_bound.typ().clone(), + loc, + ); + println!("Created new symbol with identifier: {:?}", new_identifier); + let new_variable_expr = new_symbol.to_expr(); + + // Create the lower bound comparison: lower_bound <= new_variable_expr + let lower_bound_comparison = lower_bound.clone().le(new_variable_expr.clone()); + + // Create the upper bound comparison: new_variable_expr < upper_bound + let upper_bound_comparison = new_variable_expr.clone().lt(upper_bound.clone()); + + // Combine the comparisons using a logical AND: (lower_bound < new_variable_expr) && (new_variable_expr < upper_bound) + let new_range = lower_bound_comparison.and(upper_bound_comparison); + + // Add the new symbol to the symbol table + gcx.symbol_table.insert(new_symbol); + + let new_predicate = closure_call_expr + .unwrap() + .call(vec![Expr::address_of(predicate.clone()), new_variable_expr.clone()]); + let domain = new_range.implies(new_predicate.clone()); + + Stmt::block( + vec![ + unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(assign_to, loc) + ) + .goto_expr + .assign( + Expr::forall_expr(Type::Bool, new_variable_expr, domain) + .cast_to(Type::CInteger(CIntType::Bool)), + loc, + ), + Stmt::goto(bb_label(target), loc), + ], + loc, + ) + } else { + println!("Variable is not a symbol"); + Stmt::block(vec![Stmt::goto(bb_label(target), loc)], loc) + } + } +} + +struct Exists; + +/// __CROVER_exists +impl GotocHook for Exists { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + matches_function(tcx, instance.def, "KaniExists") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + instance: Instance, + fargs: Vec, + assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + let args_from_instance = instance.args().0; + let loc = gcx.codegen_span_stable(span); + let target = target.unwrap(); + let lower_bound = &fargs[0]; + let upper_bound = &fargs[1]; + let predicate = &fargs[2]; + let mut closure_call_expr: Option = None; + + for arg in args_from_instance.iter() { + let arg_ty = arg.ty().unwrap(); + let kind = arg_ty.kind(); + let arg_kind = kind.rigid().unwrap(); + + match arg_kind { + RigidTy::Closure(def_id, args) => { + let instance_closure = + Instance::resolve_closure(*def_id, args, ClosureKind::Fn) + .expect("failed to normalize and resolve closure during codegen"); + closure_call_expr = Some(gcx.codegen_func_expr(instance_closure, loc)); + } + _ => { + println!("Unexpected type\n"); + } + } + } + + // Extract the identifier from the variable expression + let ident = match lower_bound.value() { + ExprValue::Symbol { identifier } => Some(identifier), + _ => None, + }; + + if let Some(identifier) = ident { + let new_identifier = format!("{}_kani", identifier); + let new_symbol = GotoSymbol::variable( + new_identifier.clone(), + new_identifier.clone(), + lower_bound.typ().clone(), + loc, + ); + println!("Created new symbol with identifier: {:?}", new_identifier); + let new_variable_expr = new_symbol.to_expr(); + + // Create the lower bound comparison: lower_bound <= new_variable_expr + let lower_bound_comparison = lower_bound.clone().le(new_variable_expr.clone()); + + // Create the upper bound comparison: new_variable_expr < upper_bound + let upper_bound_comparison = new_variable_expr.clone().lt(upper_bound.clone()); + + // Combine the comparisons using a logical AND: (lower_bound < new_variable_expr) && (new_variable_expr < upper_bound) + let new_range = lower_bound_comparison.and(upper_bound_comparison); + + // Add the new symbol to the symbol table + gcx.symbol_table.insert(new_symbol); + + let new_predicate = closure_call_expr + .unwrap() + .call(vec![Expr::address_of(predicate.clone()), new_variable_expr.clone()]); + let domain = new_range.implies(new_predicate.clone()); + + Stmt::block( + vec![ + unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(assign_to, loc) + ) + .goto_expr + .assign( + Expr::exists_expr(Type::Bool, new_variable_expr, domain) + .cast_to(Type::CInteger(CIntType::Bool)), + loc, + ), + Stmt::goto(bb_label(target), loc), + ], + loc, + ) + } else { + println!("Variable is not a symbol"); + Stmt::block(vec![Stmt::goto(bb_label(target), loc)], loc) + } + } +} + pub fn fn_hooks() -> GotocHooks { let kani_lib_hooks = [ (KaniHook::Assert, Rc::new(Assert) as Rc), @@ -671,6 +877,8 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(RustAlloc), Rc::new(MemCmp), Rc::new(LoopInvariantRegister), + Rc::new(Forall), + Rc::new(Exists), ], } } diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 551d522ba7e2..40ae9534b531 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -141,6 +141,44 @@ macro_rules! kani_intrinsics { assert!(cond, "{}", msg); } + #[macro_export] + macro_rules! forall { + (|$i:ident in ($lower_bound:expr, $upper_bound:expr)| $predicate:expr) => {{ + let lower_bound: usize = $lower_bound; + let upper_bound: usize = $upper_bound; + let predicate = |$i| $predicate; + kani_forall(lower_bound, upper_bound, predicate) + }}; + } + + #[macro_export] + macro_rules! exists { + (|$i:ident in ($lower_bound:expr, $upper_bound:expr)| $predicate:expr) => {{ + let lower_bound: usize = $lower_bound; + let upper_bound: usize = $upper_bound; + let predicate = |$i| $predicate; + kani_exists(lower_bound, upper_bound, predicate) + }}; + } + + #[inline(never)] + #[rustc_diagnostic_item = "KaniForall"] + pub fn kani_forall(lower_bound: T, upper_bound: T, predicate: F) -> bool + where + F: Fn(T) -> bool, + { + predicate(lower_bound) + } + + #[inline(never)] + #[rustc_diagnostic_item = "KaniExists"] + pub fn kani_exists(lower_bound: T, upper_bound: T, predicate: F) -> bool + where + F: Fn(T) -> bool, + { + predicate(lower_bound) + } + /// Creates a cover property with the specified condition and message. /// /// # Example: diff --git a/rfc/src/rfcs/0010-quantifiers.md b/rfc/src/rfcs/0010-quantifiers.md index 07a5f7548974..892b89b3c722 100644 --- a/rfc/src/rfcs/0010-quantifiers.md +++ b/rfc/src/rfcs/0010-quantifiers.md @@ -1,7 +1,7 @@ - **Feature Name:** Quantifiers - **Feature Request Issue:** [#2546](https://github.com/model-checking/kani/issues/2546) and [#836](https://github.com/model-checking/kani/issues/836) - **RFC PR:** [#](https://github.com/model-checking/kani/pull/) -- **Status:** Unstable +- **Status:** Under Review - **Version:** 1.0 ------------------- @@ -24,11 +24,11 @@ This new feature doesn't introduce any breaking changes to users. It will only a ## User Experience -We propose a syntax inspired by ["Pattern Types"](https://github.com/rust-lang/rust/pull/120131). The syntax of existential (i.e., `kani::exists`) and universal (i.e., `kani::forall`) quantifiers are: +The syntax of existential (i.e., `kani::exists`) and universal (i.e., `kani::forall`) quantifiers are: ```rust -kani::exists(|: [is ] | ) -kani::forall(|: [is ] | ) +kani::exists(|: [in ()] | ) +kani::forall(|: [in ()] | ) ``` If `` is not provided, we assume `` can range over all possible values of the given `` (i.e., syntactic sugar for full range `|: as .. |`). CBMC's SAT backend only supports bounded quantification under **constant** lower and upper bounds (for more details, see the [documentation for quantifiers in CBMC](https://diffblue.github.io/cbmc/contracts-quantifiers.html)). The SMT backend, on the other hand, supports arbitrary Boolean expressions. In any case, `` should not have side effects, as the purpose of quantifiers is to assert a condition over a domain of objects without altering the state. @@ -36,7 +36,6 @@ If `` is not provided, we assume `` can range over all possible Consider the following example adapted from the documentation for the [from_raw_parts](https://doc.rust-lang.org/std/vec/struct.Vec.html#method.from_raw_parts) function: ```rust -use std::ptr; use std::mem; #[kani::proof] @@ -67,7 +66,6 @@ fn main() { Given the `v` vector has non-deterministic values, there are potential arithmetic overflows that might happen in the for loop. So we need to constrain all values of the array. We may also want to check all values of `rebuilt` after the operation. Without quantifiers, we might be tempted to use loops as follows: ```rust -use std::ptr; use std::mem; #[kani::proof] @@ -105,14 +103,17 @@ fn main() { This, however, might unnecessary increase the complexity of the verication process. We can achieve the same effect using quantifiers as shown below. ```rust -use std::ptr; use std::mem; +extern crate kani; +use kani::{kani_forall, kani_exists}; + #[kani::proof] fn main() { let original_v = vec![kani::any::(); 3]; let v = original_v.clone(); - kani::assume(kani::forall(|i: usize is ..v.len() | v[i] < 5)); + let v_len = v.len(); + kani::assume(kani::forall!(|i in (0,v_len) | v[i] < 5)); // Prevent running `v`'s destructor so we are in complete control // of the allocation. @@ -131,7 +132,7 @@ fn main() { // Put everything back together into a Vec let rebuilt = Vec::from_raw_parts(p, len, cap); - assert!(kani::forall(|i: usize is ..len | rebuilt[i] == original_v[i]+1)); + assert!(kani::forall!(|i in (0, len) | rebuilt[i] == original_v[i]+1)); } } ``` @@ -139,14 +140,17 @@ fn main() { The same principle applies if we want to use the existential quantifier. ```rust -use std::ptr; use std::mem; +extern crate kani; +use kani::{kani_forall, kani_exists}; + #[kani::proof] fn main() { let original_v = vec![kani::any::(); 3]; let v = original_v.clone(); - kani::assume(kani::forall(|i: usize is ..v.len() | v[i] < 5)); + let v_len = v.len(); + kani::assume(kani::forall!(|i in (0,v_len) | v[i] < 5)); // Prevent running `v`'s destructor so we are in complete control // of the allocation. @@ -168,7 +172,7 @@ fn main() { // Put everything back together into a Vec let rebuilt = Vec::from_raw_parts(p, len, cap); - assert!(kani::exists(|i: usize is ..len | rebuilt[i] == 0)); + assert!(kani::exists!(| i in (0, len) | rebuilt[i] == 0)); } } ``` diff --git a/tests/expected/quantifiers/expected b/tests/expected/quantifiers/expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/quantifiers/expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/quantifiers/from_raw_parts.rs b/tests/expected/quantifiers/from_raw_parts.rs new file mode 100644 index 000000000000..433106896aa1 --- /dev/null +++ b/tests/expected/quantifiers/from_raw_parts.rs @@ -0,0 +1,38 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use std::mem; + +extern crate kani; +use kani::{kani_forall, kani_exists}; + +#[kani::proof] +fn main() { + let original_v = vec![kani::any::(); 3]; + let v = original_v.clone(); + let v_len = v.len(); + kani::assume(kani::forall!(|i in (0,v_len) | v[i] < 5)); + + // Prevent running `v`'s destructor so we are in complete control + // of the allocation. + let mut v = mem::ManuallyDrop::new(v); + + // Pull out the various important pieces of information about `v` + let p = v.as_mut_ptr(); + let len = v.len(); + let cap = v.capacity(); + + unsafe { + // Overwrite memory + for i in 0..len { + *p.add(i) += 1; + if i == 1 { + *p.add(i) = 0; + } + } + + // Put everything back together into a Vec + let rebuilt = Vec::from_raw_parts(p, len, cap); + assert!(kani::exists!(| i in (0, len) | rebuilt[i] == 0)); + } +}