From a92688f68eaf8f6639f1850e8e2fa3959a8c3535 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sat, 7 Sep 2024 14:31:17 -0400 Subject: [PATCH 01/27] 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 | 206 ++++++++++++++++++ .../src/kani_middle/kani_functions.rs | 4 + 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 ++++ 8 files changed, 345 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 6f140b67ec84..bfae26a10dd7 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. @@ -972,6 +980,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 b9cc6978ea85..90c8189ba1b4 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -377,6 +377,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 e54a1fc4dd9e..ac909b50ec49 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -14,17 +14,21 @@ 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_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; 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; @@ -761,10 +765,212 @@ impl GotocHook for LoopInvariantRegister { } } +struct Forall; + +/// __CROVER_forall +impl GotocHook for Forall { + fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { + unreachable!("{UNEXPECTED_CALL}") + } + + 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 { + unreachable!("{UNEXPECTED_CALL}") + } + + 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), (KaniHook::Assume, Rc::new(Assume)), + (KaniHook::Exists, Rc::new(Exists)), + (KaniHook::Forall, Rc::new(Forall)), (KaniHook::Panic, Rc::new(Panic)), (KaniHook::Check, Rc::new(Check)), (KaniHook::Cover, Rc::new(Cover)), diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 85936041cc38..f1d064ed08eb 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -133,6 +133,10 @@ pub enum KaniHook { Check, #[strum(serialize = "CoverHook")] Cover, + #[strum(serialize = "ExistsHook")] + Exists, + #[strum(serialize = "ForallHook")] + Forall, // TODO: this is temporarily implemented as a hook, but should be implemented as an intrinsic #[strum(serialize = "FloatToIntInRangeHook")] FloatToIntInRange, diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 51b243c9ad33..3c2310666af4 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -200,6 +200,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)] + #[kanitool::fn_marker = "ForallHook"] + pub fn kani_forall(lower_bound: T, upper_bound: T, predicate: F) -> bool + where + F: Fn(T) -> bool, + { + predicate(lower_bound) + } + + #[inline(never)] + #[kanitool::fn_marker = "ExistsHook"] + 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)); + } +} From e8c5e431bbc6967366613d120a567ffb32b97c59 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Sun, 2 Feb 2025 13:55:53 -0500 Subject: [PATCH 02/27] Format code and avoid code duplication Signed-off-by: Felipe R. Monteiro --- .../codegen_cprover_gotoc/overrides/hooks.rs | 243 ++++++------------ tests/expected/quantifiers/from_raw_parts.rs | 4 +- 2 files changed, 83 insertions(+), 164 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index ac909b50ec49..0b703fd3c939 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -15,13 +15,13 @@ 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 cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; 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; +use stable_mir::ty::RigidTy; use stable_mir::{CrateDef, ty::Span}; use std::collections::HashMap; use std::rc::Rc; @@ -766,8 +766,14 @@ impl GotocHook for LoopInvariantRegister { } struct Forall; +struct Exists; + +#[derive(Debug, Clone, Copy)] +enum QuantifierKind { + ForAll, + Exists, +} -/// __CROVER_forall impl GotocHook for Forall { fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { unreachable!("{UNEXPECTED_CALL}") @@ -782,92 +788,10 @@ impl GotocHook for Forall { 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) - } + handle_quantifier(gcx, instance, fargs, assign_to, target, span, QuantifierKind::ForAll) } } -struct Exists; - -/// __CROVER_exists impl GotocHook for Exists { fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { unreachable!("{UNEXPECTED_CALL}") @@ -882,87 +806,82 @@ impl GotocHook for Exists { 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); + handle_quantifier(gcx, instance, fargs, assign_to, target, span, QuantifierKind::Exists) + } +} - // Add the new symbol to the symbol table - gcx.symbol_table.insert(new_symbol); +fn handle_quantifier( + gcx: &mut GotocCtx, + instance: Instance, + fargs: Vec, + assign_to: &Place, + target: Option, + span: Span, + quantifier_kind: QuantifierKind, +) -> Stmt { + 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 closure_call_expr = find_closure_call_expr(&instance, gcx, loc) + .unwrap_or_else(|| unreachable!("Failed to find closure call expression")); + + let new_variable_expr = if let ExprValue::Symbol { identifier } = lower_bound.value() { + let new_identifier = format!("{}_kani", identifier); + let new_symbol = GotoSymbol::variable( + new_identifier.clone(), + new_identifier.clone(), + lower_bound.typ().clone(), + loc, + ); + gcx.symbol_table.insert(new_symbol.clone()); + new_symbol.to_expr() + } else { + unreachable!("Variable is not a symbol"); + }; + + let lower_bound_comparison = lower_bound.clone().le(new_variable_expr.clone()); + let upper_bound_comparison = new_variable_expr.clone().lt(upper_bound.clone()); + let new_range = lower_bound_comparison.and(upper_bound_comparison); + + let new_predicate = closure_call_expr + .call(vec![Expr::address_of(predicate.clone()), new_variable_expr.clone()]); + let domain = new_range.implies(new_predicate.clone()); + + let quantifier_expr = match quantifier_kind { + QuantifierKind::ForAll => Expr::forall_expr(Type::Bool, new_variable_expr, domain), + QuantifierKind::Exists => Expr::exists_expr(Type::Bool, new_variable_expr, domain), + }; + + Stmt::block( + vec![ + unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(assign_to, loc) + ) + .goto_expr + .assign(quantifier_expr.cast_to(Type::CInteger(CIntType::Bool)), loc), + Stmt::goto(bb_label(target), loc), + ], + loc, + ) +} - 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()); +fn find_closure_call_expr(instance: &Instance, gcx: &mut GotocCtx, loc: Location) -> Option { + for arg in instance.args().0.iter() { + let arg_ty = arg.ty()?; + let kind = arg_ty.kind(); + let arg_kind = kind.rigid()?; - 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) + if let RigidTy::Closure(def_id, args) = arg_kind { + let instance_closure = + Instance::resolve_closure(*def_id, args, ClosureKind::Fn).ok()?; + return Some(gcx.codegen_func_expr(instance_closure, loc)); } } + None } pub fn fn_hooks() -> GotocHooks { diff --git a/tests/expected/quantifiers/from_raw_parts.rs b/tests/expected/quantifiers/from_raw_parts.rs index 433106896aa1..30c74f90ee64 100644 --- a/tests/expected/quantifiers/from_raw_parts.rs +++ b/tests/expected/quantifiers/from_raw_parts.rs @@ -4,7 +4,7 @@ use std::mem; extern crate kani; -use kani::{kani_forall, kani_exists}; +use kani::{kani_exists, kani_forall}; #[kani::proof] fn main() { @@ -27,7 +27,7 @@ fn main() { for i in 0..len { *p.add(i) += 1; if i == 1 { - *p.add(i) = 0; + *p.add(i) = 0; } } From 0be406acdb4b04b3d727064420ab6f49b0f3a83e Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 7 Apr 2025 06:21:21 +0000 Subject: [PATCH 03/27] Inlining function calls in quantifier expressions --- cprover_bindings/src/goto_program/symbol.rs | 4 + .../src/goto_program/symbol_table.rs | 32 +- .../codegen_cprover_gotoc/codegen/function.rs | 21 +- .../compiler_interface.rs | 2 + .../codegen_cprover_gotoc/context/goto_ctx.rs | 412 +++++++++++++++++- .../codegen_cprover_gotoc/overrides/hooks.rs | 43 +- library/kani_core/src/lib.rs | 16 +- tests/kani/Quantifiers/even.rs | 12 + tests/kani/Quantifiers/no_array.rs | 44 ++ 9 files changed, 555 insertions(+), 31 deletions(-) create mode 100644 tests/kani/Quantifiers/even.rs create mode 100644 tests/kani/Quantifiers/no_array.rs diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index 5c86dd04909a..bb40ed9ed9d9 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -172,6 +172,10 @@ impl Symbol { } } + pub fn update(&mut self, value: SymbolValues) { + self.value = value; + } + /// Add this contract to the symbol (symbol must be a function) or fold the /// conditions into an existing contract. pub fn attach_contract(&mut self, contract: FunctionContract) { diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index 97567670dee0..e0dc2c689108 100644 --- a/cprover_bindings/src/goto_program/symbol_table.rs +++ b/cprover_bindings/src/goto_program/symbol_table.rs @@ -10,13 +10,18 @@ use std::collections::BTreeMap; #[derive(Clone, Debug)] pub struct SymbolTable { symbol_table: BTreeMap, + parameters_map: BTreeMap>, machine_model: MachineModel, } /// Constructors impl SymbolTable { pub fn new(machine_model: MachineModel) -> SymbolTable { - let mut symtab = SymbolTable { machine_model, symbol_table: BTreeMap::new() }; + let mut symtab = SymbolTable { + machine_model, + symbol_table: BTreeMap::new(), + parameters_map: BTreeMap::new(), + }; env::machine_model_symbols(symtab.machine_model()) .into_iter() .for_each(|s| symtab.insert(s)); @@ -54,6 +59,19 @@ impl SymbolTable { self.symbol_table.insert(symbol.name, symbol); } + /// Inserts a parameter into the parameters map for a given function symbol. + /// If the function does not exist in the parameters map, it initializes it with an empty vector. + pub fn insert_parameter, P: Into>( + &mut self, + function_name: T, + parameter: P, + ) { + let function_name = function_name.into(); + let parameter = parameter.into(); + + self.parameters_map.entry(function_name).or_insert_with(Vec::new).push(parameter); + } + /// Validates the previous value of the symbol using the validator function, then replaces it. /// Useful to replace declarations with the actual definition. pub fn replace) -> bool>( @@ -102,6 +120,10 @@ impl SymbolTable { self.symbol_table.iter() } + pub fn iter_mut(&mut self) -> std::collections::btree_map::IterMut<'_, InternedString, Symbol> { + self.symbol_table.iter_mut() + } + pub fn lookup>(&self, name: T) -> Option<&Symbol> { let name = name.into(); self.symbol_table.get(&name) @@ -112,6 +134,14 @@ impl SymbolTable { self.symbol_table.get_mut(&name) } + pub fn lookup_parameters>( + &self, + name: T, + ) -> Option<&Vec> { + let name = name.into(); + self.parameters_map.get(&name) + } + pub fn machine_model(&self) -> &MachineModel { &self.machine_model } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index dd6909483694..89f2ad157ede 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -6,6 +6,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder; use cbmc::InternString; +use cbmc::InternedString; use cbmc::goto_program::{Expr, Stmt, Symbol}; use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; @@ -20,7 +21,7 @@ impl GotocCtx<'_> { /// - Index 0 represents the return value. /// - Indices [1, N] represent the function parameters where N is the number of parameters. /// - Indices that are greater than N represent local variables. - fn codegen_declare_variables(&mut self, body: &Body) { + fn codegen_declare_variables(&mut self, body: &Body, function_name: InternedString) { let ldecls = body.local_decls(); let num_args = body.arg_locals().len(); for (lc, ldata) in ldecls { @@ -35,13 +36,21 @@ impl GotocCtx<'_> { let loc = self.codegen_span_stable(ldata.span); // Indices [1, N] represent the function parameters where N is the number of parameters. // Except that ZST fields are not included as parameters. - let sym = - Symbol::variable(name, base_name, var_type, self.codegen_span_stable(ldata.span)) - .with_is_hidden(!self.is_user_variable(&lc)) - .with_is_parameter((lc > 0 && lc <= num_args) && !self.is_zst_stable(ldata.ty)); + let sym = Symbol::variable( + name.clone(), + base_name, + var_type, + self.codegen_span_stable(ldata.span), + ) + .with_is_hidden(!self.is_user_variable(&lc)) + .with_is_parameter((lc > 0 && lc <= num_args) && !self.is_zst_stable(ldata.ty)); let sym_e = sym.to_expr(); self.symbol_table.insert(sym); + if lc > 0 && lc <= num_args { + self.symbol_table.insert_parameter(function_name, name); + } + // Index 0 represents the return value, which does not need to be // declared in the first block if lc < 1 || lc > body.arg_locals().len() { @@ -64,7 +73,7 @@ impl GotocCtx<'_> { self.set_current_fn(instance, &body); self.print_instance(instance, &body); self.codegen_function_prelude(&body); - self.codegen_declare_variables(&body); + self.codegen_declare_variables(&body, name.clone().into()); // Get the order from internal body for now. reverse_postorder(&body).for_each(|bb| self.codegen_block(bb, &body.blocks[bb])); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 8ed90b2c975e..ee7d83fcd7d1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -198,6 +198,8 @@ impl GotocCodegenBackend { None }; + gcx.handle_quantifiers(); + // No output should be generated if user selected no_codegen. if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { let pretty = self.queries.lock().unwrap().args().output_pretty_json; diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 79410bd3373e..43657c8b6c1a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -22,7 +22,8 @@ use crate::codegen_cprover_gotoc::utils::full_crate_name; use crate::kani_middle::transform::BodyTransformation; use crate::kani_queries::QueryDb; use cbmc::goto_program::{ - DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, SymbolValues, Type, + CIntType, DatatypeComponent, Expr, ExprValue, Location, Stmt, StmtBody, Symbol, SymbolTable, + SymbolValues, Type, }; use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; @@ -40,6 +41,7 @@ use rustc_target::callconv::FnAbi; use stable_mir::mir::Body; use stable_mir::mir::mono::Instance; use stable_mir::ty::Allocation; +use std::collections::{BTreeMap, HashSet}; use std::fmt::Debug; pub struct GotocCtx<'tcx> { @@ -304,6 +306,414 @@ impl<'tcx> GotocCtx<'tcx> { } } +/// Quantifiers Related +impl GotocCtx<'_> { + /// Find all quantifier expressions and recursively inline functions in the quantifier bodies. + pub fn handle_quantifiers(&mut self) { + // Store the found quantifiers and the inlined results. + let mut to_modify: BTreeMap = BTreeMap::new(); + for (key, symbol) in self.symbol_table.iter() { + match &symbol.value { + SymbolValues::Stmt(stmt) => { + let new_stmt_val = SymbolValues::Stmt(self.handle_quantifiers_in_stmt(stmt)); + to_modify.insert(key.clone(), new_stmt_val); + } + _ => (), + } + } + + // Update the found quantifiers with the inlined results. + for (key, symbol_value) in to_modify { + self.symbol_table.lookup_mut(key).unwrap().update(symbol_value); + } + } + + /// Find all quantifier expressions in `stmt` and recursively inline functions. + fn handle_quantifiers_in_stmt(&self, stmt: &Stmt) -> Stmt { + match &stmt.body() { + // According to the hook handling for quantifiers, quantifier expressions must be of form + // lhs = typecast(qex, c_bool) + // where qex is either a forall-expression or an exists-expression. + StmtBody::Assign { lhs, rhs } => { + let new_rhs = match &rhs.value() { + ExprValue::Typecast(quantified_expr) => match &quantified_expr.value() { + ExprValue::Forall { variable, domain } => { + // We store the function symbols we have inlined to avoid recursion. + let mut visited_func_symbols: HashSet = HashSet::new(); + // We count the number of function that we have inlined, and use the count to + // make inlined labeled unique. + let mut suffix_count: u16 = 0; + + let end_stmt = Stmt::code_expression( + self.inline_function_calls_in_expr( + domain, + &mut visited_func_symbols, + &mut suffix_count, + ) + .unwrap(), + domain.location().clone(), + ); + + // Make the result a statement expression. + let res = Expr::forall_expr( + Type::Bool, + variable.clone(), + Expr::statement_expression( + vec![Stmt::skip(domain.location().clone()), end_stmt], + Type::Bool, + domain.location().clone(), + ), + ); + res.cast_to(Type::CInteger(CIntType::Bool)) + } + ExprValue::Exists { variable, domain } => { + // We store the function symbols we have inlined to avoid recursion. + let mut visited_func_symbols: HashSet = HashSet::new(); + // We count the number of function that we have inlined, and use the count to + // make inlined labeled unique. + let mut suffix_count = 0; + + let end_stmt = Stmt::code_expression( + self.inline_function_calls_in_expr( + domain, + &mut visited_func_symbols, + &mut suffix_count, + ) + .unwrap(), + domain.location().clone(), + ); + + // Make the result a statement expression. + let res = Expr::exists_expr( + Type::Bool, + variable.clone(), + Expr::statement_expression( + vec![Stmt::skip(domain.location().clone()), end_stmt], + Type::Bool, + domain.location().clone(), + ), + ); + res.cast_to(Type::CInteger(CIntType::Bool)) + } + _ => rhs.clone(), + }, + _ => rhs.clone(), + }; + Stmt::assign(lhs.clone(), new_rhs, stmt.location().clone()) + } + // Recursively find quantifier expressions. + StmtBody::Block(stmts) => Stmt::block( + stmts.iter().map(|stmt| self.handle_quantifiers_in_stmt(stmt)).collect(), + stmt.location().clone(), + ), + StmtBody::Label { label, body } => { + self.handle_quantifiers_in_stmt(body).with_label(*label) + } + _ => stmt.clone(), + } + } + + /// Count and return the number of return statements in `stmt`. + fn count_return_stmts(&self, stmt: &Stmt) -> usize { + match stmt.body() { + StmtBody::Return(_) => 1, + StmtBody::Block(stmts) => stmts.iter().map(|s| self.count_return_stmts(s)).sum(), + StmtBody::Label { label: _, body } => self.count_return_stmts(body), + _ => 0, + } + } + + /// Rewrite return statements in `stmt` with a goto statement to `end_label`. + /// It also stores the return symbol in `return_symbol`. + fn rewrite_return_stmt_with_goto( + &self, + stmt: &Stmt, + return_symbol: &mut Option, + end_label: &InternedString, + ) -> Stmt { + match stmt.body() { + StmtBody::Return(Some(expr)) => { + if let ExprValue::Symbol { ref identifier } = expr.value() { + *return_symbol = + Some(Expr::symbol_expression(identifier.clone(), expr.typ().clone())); + Stmt::goto(*end_label, stmt.location().clone()) + } else { + panic!("Expected symbol expression in return statement"); + } + } + StmtBody::Block(stmts) => Stmt::block( + stmts + .iter() + .map(|s| self.rewrite_return_stmt_with_goto(s, return_symbol, end_label)) + .collect(), + stmt.location().clone(), + ), + StmtBody::Label { label, body } => self + .rewrite_return_stmt_with_goto(body, return_symbol, end_label) + .with_label(*label), + _ => stmt.clone(), + } + } + + /// Append a given suffix to all labels and goto destinations in `stmt`. + fn append_suffix_to_stmt(&self, stmt: &Stmt, suffix: &str) -> Stmt { + match stmt.body() { + StmtBody::Label { label, body } => { + let new_label = format!("{}{}", label, suffix); + self.append_suffix_to_stmt(body, suffix).with_label(new_label) + } + StmtBody::Goto { dest, .. } => { + let new_target = format!("{}{}", dest, suffix); + Stmt::goto(new_target, stmt.location().clone()) + } + StmtBody::Block(stmts) => Stmt::block( + stmts.iter().map(|s| self.append_suffix_to_stmt(s, suffix)).collect(), + stmt.location().clone(), + ), + StmtBody::Ifthenelse { i, t, e } => Stmt::if_then_else( + i.clone(), + self.append_suffix_to_stmt(t, suffix), + e.clone().map(|s| self.append_suffix_to_stmt(&s, suffix)), + stmt.location().clone(), + ), + StmtBody::While { .. } | StmtBody::For { .. } | StmtBody::Switch { .. } => { + unimplemented!() + } + _ => stmt.clone(), + } + } + + /// Recursively inline all function calls in `expr`. + /// `visited_func_symbols` contain all function symbols in the stack. + /// `suffix_count` is used to make inlined labels unique. + fn inline_function_calls_in_expr( + &self, + expr: &Expr, + visited_func_symbols: &mut HashSet, + suffix_count: &mut u16, + ) -> Option { + match &expr.value() { + // For function call expression, we find the function symbol and function body from the + // symbol table for inlining. + ExprValue::FunctionCall { function, arguments } => { + if let ExprValue::Symbol { identifier } = &function.value() { + // Check if the function symbol exists in the symbol table + if let Some(function_body) = + self.symbol_table.lookup(*identifier).and_then(|sym| match &sym.value { + SymbolValues::Stmt(stmt) => Some(stmt), + _ => None, + }) + { + // For function calls to foo(args) where the definition of foo is + // fn foo(params) { + // body; + // return res; + // } + // The inlining result will be a statement expression + // { + // DECL params + // ASSIGN params = args + // inline(body) + // GOTO end_label + // end_label: + // EXPRESSION res + // } + // where res is the end expression of the statement expression. + + // Keep suffix unique in difference inlining. + *suffix_count += 1; + + // Use call stacks to avoid recursion. + assert!( + !visited_func_symbols.contains(identifier), + "Detected recursions in the usage of quantifiers." + ); + visited_func_symbols.insert(*identifier); + + let inlined_body: &Stmt = function_body; + let mut stmts_of_inlined_body: Vec = + inlined_body.get_stmts().unwrap().clone(); + + // Substitute parameters with arguments in the function body. + if let Some(parameters) = self.symbol_table.lookup_parameters(*identifier) { + assert!( + parameters.len() == arguments.len(), + "Mismatch between parameters and arguments for function {}: parameters = {}, arguments = {}", + identifier, + parameters.len(), + arguments.len() + ); + + // Create decl statements of parameters. + let mut param_decls: Vec = parameters + .iter() + .zip(arguments.iter()) + .map(|(param, arg)| { + Stmt::decl( + Expr::symbol_expression(param.clone(), arg.typ().clone()), + None, + arg.location().clone(), + ) + }) + .collect(); + + // Create assignment statements from arguments to parameters. + let mut param_assigs: Vec = parameters + .iter() + .zip(arguments.iter()) + .map(|(param, arg)| { + Stmt::assign( + Expr::symbol_expression(param.clone(), arg.typ().clone()), + arg.clone(), + arg.location().clone(), + ) + }) + .collect(); + + // Prepend the assignments to stmts_of_inlined_body + param_decls.append(&mut param_assigs); + param_decls.append(&mut stmts_of_inlined_body); + stmts_of_inlined_body = param_decls; + } + + let count_return: usize = stmts_of_inlined_body + .clone() + .iter() + .map(|stmt: &Stmt| self.count_return_stmts(stmt)) + .sum(); + // The function is a void function, we safely ignore it. + if count_return == 0 { + return None; + } + // For simplicity, we currently only handle cases with one return statement. + assert_eq!(count_return, 1); + + // Make labels in the inlined body unique. + let suffix = format!("_{}", suffix_count); + stmts_of_inlined_body = stmts_of_inlined_body + .iter() + .map(|stmt| self.append_suffix_to_stmt(stmt, &suffix)) + .collect(); + + // Replace all return stmts with symbol expressions. + let end_label: InternedString = + format!("KANI_quantifier_end{suffix}").into(); + let mut end_stmt = None; + stmts_of_inlined_body = stmts_of_inlined_body + .iter() + .map(|stmt| { + self.rewrite_return_stmt_with_goto(stmt, &mut end_stmt, &end_label) + }) + .collect(); + stmts_of_inlined_body + .push(Stmt::skip(expr.location().clone()).with_label(end_label)); + stmts_of_inlined_body.push(Stmt::code_expression( + end_stmt.unwrap(), + expr.location().clone(), + )); + + // Recursively inline function calls in the function body. + let res = self.inline_function_calls_in_expr( + &Expr::statement_expression( + stmts_of_inlined_body, + expr.typ().clone(), + expr.location().clone(), + ), + visited_func_symbols, + suffix_count, + ); + + visited_func_symbols.remove(identifier); + + return res; + } else { + unreachable!() + } + } + } + // Recursively inline function calls in ops. + ExprValue::BinOp { op, lhs, rhs } => { + return Some( + self.inline_function_calls_in_expr(lhs, visited_func_symbols, suffix_count) + .unwrap() + .binop( + *op, + self.inline_function_calls_in_expr( + rhs, + visited_func_symbols, + suffix_count, + ) + .unwrap(), + ), + ); + } + ExprValue::StatementExpression { statements, location: _ } => { + let inlined_stmts: Vec = statements + .iter() + .filter_map(|stmt| { + self.inline_function_calls_in_stmt(stmt, visited_func_symbols, suffix_count) + }) + .collect(); + return Some(Expr::statement_expression( + inlined_stmts, + expr.typ().clone(), + expr.location().clone(), + )); + } + _ => {} + } + Some(expr.clone()) + } + + /// Recursively inline all function calls in `stmt`. + /// `visited_func_symbols` contain all function symbols in the stack. + /// `suffix_count` is used to make inlined labels unique. + fn inline_function_calls_in_stmt( + &self, + stmt: &Stmt, + visited_func_symbols: &mut HashSet, + suffix_count: &mut u16, + ) -> Option { + match stmt.body() { + StmtBody::Expression(expr) => { + match self.inline_function_calls_in_expr(expr, visited_func_symbols, suffix_count) { + None => None, + Some(inlined_expr) => { + Some(Stmt::code_expression(inlined_expr, expr.location().clone())) + } + } + } + StmtBody::Assign { lhs, rhs } => { + match self.inline_function_calls_in_expr(rhs, visited_func_symbols, suffix_count) { + None => None, + Some(inlined_rhs) => { + Some(Stmt::assign(lhs.clone(), inlined_rhs, stmt.location().clone())) + } + } + } + StmtBody::Block(stmts) => { + let inlined_block = stmts + .iter() + .filter_map(|s| { + self.inline_function_calls_in_stmt(s, visited_func_symbols, suffix_count) + }) + .collect(); + Some(Stmt::block(inlined_block, stmt.location().clone())) + } + StmtBody::Label { label, body } => { + match self.inline_function_calls_in_stmt(body, visited_func_symbols, suffix_count) { + None => Some(Stmt::skip(stmt.location().clone()).with_label(label.clone())), + Some(inlined_body) => Some(inlined_body.with_label(label.clone())), + } + } + StmtBody::While { .. } | StmtBody::For { .. } | StmtBody::Switch { .. } => { + unimplemented!() + } + _ => Some(stmt.clone()), + } + } +} + /// Mutators impl GotocCtx<'_> { pub fn set_current_fn(&mut self, instance: Instance, body: &Body) { diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 0b703fd3c939..8a2ed9e938cb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -27,8 +27,6 @@ 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; @@ -823,32 +821,39 @@ fn handle_quantifier( let target = target.unwrap(); let lower_bound = &fargs[0]; let upper_bound = &fargs[1]; - let predicate = &fargs[2]; - let closure_call_expr = find_closure_call_expr(&instance, gcx, loc) .unwrap_or_else(|| unreachable!("Failed to find closure call expression")); - let new_variable_expr = if let ExprValue::Symbol { identifier } = lower_bound.value() { - let new_identifier = format!("{}_kani", identifier); - let new_symbol = GotoSymbol::variable( - new_identifier.clone(), - new_identifier.clone(), - lower_bound.typ().clone(), - loc, - ); + let predicate = if fargs.len() == 3 { + Expr::address_of(fargs[2].clone()) + } else { + Expr::symbol_expression( + "dummy", + closure_call_expr.typ().parameters().unwrap().first().unwrap().typ().clone(), + ) + }; + + // Quantified variable. + let base_name = format!("kani_quantified_var"); + let mut counter = 0; + let mut unique_name = format!("{}_{}", base_name, counter); + // Ensure the name is not already in the symbol table + while gcx.symbol_table.lookup(&unique_name).is_some() { + counter += 1; + unique_name = format!("{}_{}", base_name, counter); + } + let new_variable_expr = { + let new_symbol = + GotoSymbol::variable(unique_name.clone(), unique_name, lower_bound.typ().clone(), loc); gcx.symbol_table.insert(new_symbol.clone()); new_symbol.to_expr() - } else { - unreachable!("Variable is not a symbol"); }; let lower_bound_comparison = lower_bound.clone().le(new_variable_expr.clone()); let upper_bound_comparison = new_variable_expr.clone().lt(upper_bound.clone()); - let new_range = lower_bound_comparison.and(upper_bound_comparison); - - let new_predicate = closure_call_expr - .call(vec![Expr::address_of(predicate.clone()), new_variable_expr.clone()]); - let domain = new_range.implies(new_predicate.clone()); + let range = lower_bound_comparison.and(upper_bound_comparison); + let domain = + range.implies(closure_call_expr.call(vec![predicate.clone(), new_variable_expr.clone()])); let quantifier_expr = match quantifier_kind { QuantifierKind::ForAll => Expr::forall_expr(Type::Bool, new_variable_expr, domain), diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 3c2310666af4..82ee0adc3d54 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -203,21 +203,29 @@ macro_rules! kani_intrinsics { #[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 lower_bound: isize = $lower_bound; + let upper_bound: isize = $upper_bound; let predicate = |$i| $predicate; kani_forall(lower_bound, upper_bound, predicate) }}; + (|$i:ident | $predicate:expr) => {{ + let predicate = |$i| $predicate; + kani_forall(isize::MIN, isize::MAX, 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 lower_bound: isize = $lower_bound; + let upper_bound: isize = $upper_bound; let predicate = |$i| $predicate; kani_exists(lower_bound, upper_bound, predicate) }}; + (|$i:ident | $predicate:expr) => {{ + let predicate = |$i| $predicate; + kani_exists(isize::MIN, isize::MAX, predicate) + }}; } #[inline(never)] diff --git a/tests/kani/Quantifiers/even.rs b/tests/kani/Quantifiers/even.rs new file mode 100644 index 000000000000..ab703148234b --- /dev/null +++ b/tests/kani/Quantifiers/even.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::kani_exists; + +#[kani::proof] +fn quantifier_even_harness() { + let j: isize = kani::any(); + kani::assume(j % 2 == 0); + kani::assert(kani::exists!(|i in (-1000, 1000)| i + i == j), ""); +} diff --git a/tests/kani/Quantifiers/no_array.rs b/tests/kani/Quantifiers/no_array.rs new file mode 100644 index 000000000000..1171058e4054 --- /dev/null +++ b/tests/kani/Quantifiers/no_array.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::{kani_exists, kani_forall}; + +#[kani::proof] +fn forall_assert_harness() { + let j = kani::any(); + kani::assume(j > 5); + kani::assert(kani::forall!(|i in (2,5)| i < j ), ""); +} + +#[kani::proof] +fn forall_assume_harness() { + let j = kani::any(); + kani::assume(kani::forall!(|i in (2,5)| i < j)); + kani::assert(j > 4, ""); +} + +fn comp(x: isize, y: isize) -> bool { + x > y +} + +#[kani::proof] +fn forall_function_harness() { + let j = kani::any(); + kani::assume(j > 5); + kani::assert(kani::forall!(|i in (2,5)| comp(j, i) ), ""); +} + +#[kani::proof] +fn exists_assert_harness() { + let j = kani::any(); + kani::assume(j > 2); + kani::assert(kani::exists!(|i in (2,5)| i < j ), ""); +} + +#[kani::proof] +fn exists_function_harness() { + let j = kani::any(); + kani::assume(j > 2); + kani::assert(kani::exists!(|i in (2,5)| comp(j, i) ), ""); +} From f838e91896897dfb624ef8ca78a71c332de55f98 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 14:44:32 +0000 Subject: [PATCH 04/27] Fix ranged existential quantification --- .../codegen_cprover_gotoc/overrides/hooks.rs | 17 +++++++++++++---- library/kani_core/src/lib.rs | 12 ++++++------ 2 files changed, 19 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 8a2ed9e938cb..544438cd83ba 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -852,12 +852,21 @@ fn handle_quantifier( let lower_bound_comparison = lower_bound.clone().le(new_variable_expr.clone()); let upper_bound_comparison = new_variable_expr.clone().lt(upper_bound.clone()); let range = lower_bound_comparison.and(upper_bound_comparison); - let domain = - range.implies(closure_call_expr.call(vec![predicate.clone(), new_variable_expr.clone()])); let quantifier_expr = match quantifier_kind { - QuantifierKind::ForAll => Expr::forall_expr(Type::Bool, new_variable_expr, domain), - QuantifierKind::Exists => Expr::exists_expr(Type::Bool, new_variable_expr, domain), + QuantifierKind::ForAll => { + let domain = range.implies( + closure_call_expr.call(vec![predicate.clone(), new_variable_expr.clone()]), + ); + Expr::forall_expr(Type::Bool, new_variable_expr, domain) + } + QuantifierKind::Exists => { + let domain = range + .clone() + .and(closure_call_expr.call(vec![predicate.clone(), new_variable_expr.clone()])) + .and(range.not().implies(Expr::bool_false())); + Expr::exists_expr(Type::Bool, new_variable_expr, domain) + } }; Stmt::block( diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 82ee0adc3d54..597defac53f3 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -203,28 +203,28 @@ macro_rules! kani_intrinsics { #[macro_export] macro_rules! forall { (|$i:ident in ($lower_bound:expr, $upper_bound:expr)| $predicate:expr) => {{ - let lower_bound: isize = $lower_bound; - let upper_bound: isize = $upper_bound; + let lower_bound: usize = $lower_bound; + let upper_bound: usize = $upper_bound; let predicate = |$i| $predicate; kani_forall(lower_bound, upper_bound, predicate) }}; (|$i:ident | $predicate:expr) => {{ let predicate = |$i| $predicate; - kani_forall(isize::MIN, isize::MAX, predicate) + kani_forall(usize::MIN, usize::MAX, predicate) }}; } #[macro_export] macro_rules! exists { (|$i:ident in ($lower_bound:expr, $upper_bound:expr)| $predicate:expr) => {{ - let lower_bound: isize = $lower_bound; - let upper_bound: isize = $upper_bound; + let lower_bound: usize = $lower_bound; + let upper_bound: usize = $upper_bound; let predicate = |$i| $predicate; kani_exists(lower_bound, upper_bound, predicate) }}; (|$i:ident | $predicate:expr) => {{ let predicate = |$i| $predicate; - kani_exists(isize::MIN, isize::MAX, predicate) + kani_exists(usize::MIN, usize::MAX, predicate) }}; } From 6d0017b4594360cf0a2ead01f6bf19fb803819f1 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 14:45:29 +0000 Subject: [PATCH 05/27] Add support of switch in quantifier expression --- .../codegen_cprover_gotoc/context/goto_ctx.rs | 70 +++++++++++++++---- 1 file changed, 58 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 43657c8b6c1a..07a5aff4c178 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -22,8 +22,8 @@ use crate::codegen_cprover_gotoc::utils::full_crate_name; use crate::kani_middle::transform::BodyTransformation; use crate::kani_queries::QueryDb; use cbmc::goto_program::{ - CIntType, DatatypeComponent, Expr, ExprValue, Location, Stmt, StmtBody, Symbol, SymbolTable, - SymbolValues, Type, + CIntType, DatatypeComponent, Expr, ExprValue, Location, Stmt, StmtBody, SwitchCase, Symbol, + SymbolTable, SymbolValues, Type, }; use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; @@ -476,7 +476,24 @@ impl GotocCtx<'_> { e.clone().map(|s| self.append_suffix_to_stmt(&s, suffix)), stmt.location().clone(), ), - StmtBody::While { .. } | StmtBody::For { .. } | StmtBody::Switch { .. } => { + StmtBody::Switch { control, cases, default } => { + // Append the suffix to each case + let new_cases: Vec<_> = cases + .iter() + .map(|case| { + let new_body = self.append_suffix_to_stmt(case.body(), suffix); + SwitchCase::new(case.case().clone(), new_body) + }) + .collect(); + + // Append the suffix to the default case, if it exists + let new_default = + default.as_ref().map(|stmt| self.append_suffix_to_stmt(stmt, suffix)); + + // Construct the new switch statement + Stmt::switch(control.clone(), new_cases, new_default, stmt.location().clone()) + } + StmtBody::While { .. } | StmtBody::For { .. } => { unimplemented!() } _ => stmt.clone(), @@ -504,6 +521,8 @@ impl GotocCtx<'_> { _ => None, }) { + println!("{:?}", function_body.location()); + println!("{:?}\n", function_body); // For function calls to foo(args) where the definition of foo is // fn foo(params) { // body; @@ -536,14 +555,6 @@ impl GotocCtx<'_> { // Substitute parameters with arguments in the function body. if let Some(parameters) = self.symbol_table.lookup_parameters(*identifier) { - assert!( - parameters.len() == arguments.len(), - "Mismatch between parameters and arguments for function {}: parameters = {}, arguments = {}", - identifier, - parameters.len(), - arguments.len() - ); - // Create decl statements of parameters. let mut param_decls: Vec = parameters .iter() @@ -706,7 +717,42 @@ impl GotocCtx<'_> { Some(inlined_body) => Some(inlined_body.with_label(label.clone())), } } - StmtBody::While { .. } | StmtBody::For { .. } | StmtBody::Switch { .. } => { + StmtBody::Switch { control, cases, default } => { + // Inline function calls in the discriminant expression + let inlined_control = self + .inline_function_calls_in_expr(control, visited_func_symbols, suffix_count) + .unwrap_or_else(|| control.clone()); + + // Inline function calls in each case + let inlined_cases: Vec<_> = cases + .iter() + .map(|sc| { + let inlined_stmt = self + .inline_function_calls_in_stmt( + sc.body(), + visited_func_symbols, + suffix_count, + ) + .unwrap_or_else(|| sc.body().clone()); + SwitchCase::new(sc.case().clone(), inlined_stmt) + }) + .collect(); + + // Inline function calls in the default case, if it exists + let inlined_default = default.as_ref().map(|stmt| { + self.inline_function_calls_in_stmt(stmt, visited_func_symbols, suffix_count) + .unwrap_or_else(|| stmt.clone()) + }); + + // Construct the new switch statement + Some(Stmt::switch( + inlined_control, + inlined_cases, + inlined_default, + stmt.location().clone(), + )) + } + StmtBody::While { .. } | StmtBody::For { .. } => { unimplemented!() } _ => Some(stmt.clone()), From df78d91d8c5892b14849ee31fe94a0a28728652e Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 14:46:10 +0000 Subject: [PATCH 06/27] Remove debug leftover --- kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 07a5aff4c178..99c10ac5814b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -521,8 +521,6 @@ impl GotocCtx<'_> { _ => None, }) { - println!("{:?}", function_body.location()); - println!("{:?}\n", function_body); // For function calls to foo(args) where the definition of foo is // fn foo(params) { // body; From d463882592b5770a541131381a3e59541f8b466a Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 15:02:38 +0000 Subject: [PATCH 07/27] Make tests depending on new CBMC fixme --- .../Quantifiers/{even.rs => even_fixme.rs} | 2 +- tests/kani/Quantifiers/no_array.rs | 18 ------- tests/kani/Quantifiers/no_array_fixme.rs | 51 +++++++++++++++++++ 3 files changed, 52 insertions(+), 19 deletions(-) rename tests/kani/Quantifiers/{even.rs => even_fixme.rs} (83%) create mode 100644 tests/kani/Quantifiers/no_array_fixme.rs diff --git a/tests/kani/Quantifiers/even.rs b/tests/kani/Quantifiers/even_fixme.rs similarity index 83% rename from tests/kani/Quantifiers/even.rs rename to tests/kani/Quantifiers/even_fixme.rs index ab703148234b..7aac6214b322 100644 --- a/tests/kani/Quantifiers/even.rs +++ b/tests/kani/Quantifiers/even_fixme.rs @@ -7,6 +7,6 @@ use kani::kani_exists; #[kani::proof] fn quantifier_even_harness() { let j: isize = kani::any(); - kani::assume(j % 2 == 0); + kani::assume(j % 2 == 0 && j < 2000 && j > -2000); kani::assert(kani::exists!(|i in (-1000, 1000)| i + i == j), ""); } diff --git a/tests/kani/Quantifiers/no_array.rs b/tests/kani/Quantifiers/no_array.rs index 1171058e4054..1992b995ceef 100644 --- a/tests/kani/Quantifiers/no_array.rs +++ b/tests/kani/Quantifiers/no_array.rs @@ -18,27 +18,9 @@ fn forall_assume_harness() { kani::assert(j > 4, ""); } -fn comp(x: isize, y: isize) -> bool { - x > y -} - -#[kani::proof] -fn forall_function_harness() { - let j = kani::any(); - kani::assume(j > 5); - kani::assert(kani::forall!(|i in (2,5)| comp(j, i) ), ""); -} - #[kani::proof] fn exists_assert_harness() { let j = kani::any(); kani::assume(j > 2); kani::assert(kani::exists!(|i in (2,5)| i < j ), ""); } - -#[kani::proof] -fn exists_function_harness() { - let j = kani::any(); - kani::assume(j > 2); - kani::assert(kani::exists!(|i in (2,5)| comp(j, i) ), ""); -} diff --git a/tests/kani/Quantifiers/no_array_fixme.rs b/tests/kani/Quantifiers/no_array_fixme.rs new file mode 100644 index 000000000000..41dd63bfe24d --- /dev/null +++ b/tests/kani/Quantifiers/no_array_fixme.rs @@ -0,0 +1,51 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::{kani_exists, kani_forall}; + +#[kani::proof] +fn forall_assert_harness() { + let j = kani::any(); + kani::assume(j > 5); + kani::assert(kani::forall!(|i in (2,5)| i < j ), ""); +} + +#[kani::proof] +fn forall_assume_harness() { + let j = kani::any(); + kani::assume(kani::forall!(|i in (2,5)| i < j)); + kani::assert(j > 4, ""); +} + +fn comp(x: isize, y: isize) -> bool { + x > y +} + +#[kani::proof] +fn forall_function_harness() { + let j = kani::any(); + kani::assume(j > 5); + kani::assert(kani::forall!(|i in (2,5)| comp(j, i) ), ""); +} + +#[kani::proof] +fn exists_assert_harness() { + let j = kani::any(); + kani::assume(j > 2); + kani::assert(kani::exists!(|i in (2,5)| i < j ), ""); +} + +#[kani::proof] +fn exists_assume_harness() { + let j = kani::any(); + kani::assume(kani::exists!(|i in (2,4)| i == j)); + kani::assert(j == 3 || j == 2, ""); +} + +#[kani::proof] +fn exists_function_harness() { + let j = kani::any(); + kani::assume(j > 2); + kani::assert(kani::exists!(|i in (2,5)| comp(j, i) ), ""); +} From bf9eb976d27006677f71ea4639eb9e60963fea86 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 15:10:00 +0000 Subject: [PATCH 08/27] Fix clippy --- cprover_bindings/src/goto_program/symbol_table.rs | 2 +- .../quantifiers/{from_raw_parts.rs => from_raw_parts_fixme.rs} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename tests/expected/quantifiers/{from_raw_parts.rs => from_raw_parts_fixme.rs} (100%) diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index e0dc2c689108..b66eb581e3cb 100644 --- a/cprover_bindings/src/goto_program/symbol_table.rs +++ b/cprover_bindings/src/goto_program/symbol_table.rs @@ -69,7 +69,7 @@ impl SymbolTable { let function_name = function_name.into(); let parameter = parameter.into(); - self.parameters_map.entry(function_name).or_insert_with(Vec::new).push(parameter); + self.parameters_map.entry(function_name).or_default().push(parameter); } /// Validates the previous value of the symbol using the validator function, then replaces it. diff --git a/tests/expected/quantifiers/from_raw_parts.rs b/tests/expected/quantifiers/from_raw_parts_fixme.rs similarity index 100% rename from tests/expected/quantifiers/from_raw_parts.rs rename to tests/expected/quantifiers/from_raw_parts_fixme.rs From f21041dc30b2f1d06d2ac34805a94e92813e456b Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 15:25:52 +0000 Subject: [PATCH 09/27] Fix clippy --- .../codegen_cprover_gotoc/context/goto_ctx.rs | 123 ++++++++---------- .../codegen_cprover_gotoc/overrides/hooks.rs | 2 +- 2 files changed, 55 insertions(+), 70 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 99c10ac5814b..7d1fce8b246a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -313,12 +313,9 @@ impl GotocCtx<'_> { // Store the found quantifiers and the inlined results. let mut to_modify: BTreeMap = BTreeMap::new(); for (key, symbol) in self.symbol_table.iter() { - match &symbol.value { - SymbolValues::Stmt(stmt) => { - let new_stmt_val = SymbolValues::Stmt(self.handle_quantifiers_in_stmt(stmt)); - to_modify.insert(key.clone(), new_stmt_val); - } - _ => (), + if let SymbolValues::Stmt(stmt) = &symbol.value { + let new_stmt_val = SymbolValues::Stmt(self.handle_quantifiers_in_stmt(stmt)); + to_modify.insert(*key, new_stmt_val); } } @@ -351,7 +348,7 @@ impl GotocCtx<'_> { &mut suffix_count, ) .unwrap(), - domain.location().clone(), + *domain.location(), ); // Make the result a statement expression. @@ -359,9 +356,9 @@ impl GotocCtx<'_> { Type::Bool, variable.clone(), Expr::statement_expression( - vec![Stmt::skip(domain.location().clone()), end_stmt], + vec![Stmt::skip(*domain.location()), end_stmt], Type::Bool, - domain.location().clone(), + *domain.location(), ), ); res.cast_to(Type::CInteger(CIntType::Bool)) @@ -380,7 +377,7 @@ impl GotocCtx<'_> { &mut suffix_count, ) .unwrap(), - domain.location().clone(), + *domain.location(), ); // Make the result a statement expression. @@ -388,9 +385,9 @@ impl GotocCtx<'_> { Type::Bool, variable.clone(), Expr::statement_expression( - vec![Stmt::skip(domain.location().clone()), end_stmt], + vec![Stmt::skip(*domain.location()), end_stmt], Type::Bool, - domain.location().clone(), + *domain.location(), ), ); res.cast_to(Type::CInteger(CIntType::Bool)) @@ -399,12 +396,12 @@ impl GotocCtx<'_> { }, _ => rhs.clone(), }; - Stmt::assign(lhs.clone(), new_rhs, stmt.location().clone()) + Stmt::assign(lhs.clone(), new_rhs, *stmt.location()) } // Recursively find quantifier expressions. StmtBody::Block(stmts) => Stmt::block( stmts.iter().map(|stmt| self.handle_quantifiers_in_stmt(stmt)).collect(), - stmt.location().clone(), + *stmt.location(), ), StmtBody::Label { label, body } => { self.handle_quantifiers_in_stmt(body).with_label(*label) @@ -414,11 +411,11 @@ impl GotocCtx<'_> { } /// Count and return the number of return statements in `stmt`. - fn count_return_stmts(&self, stmt: &Stmt) -> usize { + fn count_return_stmts(stmt: &Stmt) -> usize { match stmt.body() { StmtBody::Return(_) => 1, - StmtBody::Block(stmts) => stmts.iter().map(|s| self.count_return_stmts(s)).sum(), - StmtBody::Label { label: _, body } => self.count_return_stmts(body), + StmtBody::Block(stmts) => stmts.iter().map(|s| Self::count_return_stmts(s)).sum(), + StmtBody::Label { label: _, body } => Self::count_return_stmts(body), _ => 0, } } @@ -426,7 +423,6 @@ impl GotocCtx<'_> { /// Rewrite return statements in `stmt` with a goto statement to `end_label`. /// It also stores the return symbol in `return_symbol`. fn rewrite_return_stmt_with_goto( - &self, stmt: &Stmt, return_symbol: &mut Option, end_label: &InternedString, @@ -436,7 +432,7 @@ impl GotocCtx<'_> { if let ExprValue::Symbol { ref identifier } = expr.value() { *return_symbol = Some(Expr::symbol_expression(identifier.clone(), expr.typ().clone())); - Stmt::goto(*end_label, stmt.location().clone()) + Stmt::goto(*end_label, *stmt.location()) } else { panic!("Expected symbol expression in return statement"); } @@ -444,54 +440,55 @@ impl GotocCtx<'_> { StmtBody::Block(stmts) => Stmt::block( stmts .iter() - .map(|s| self.rewrite_return_stmt_with_goto(s, return_symbol, end_label)) + .map(|s| Self::rewrite_return_stmt_with_goto(s, return_symbol, end_label)) .collect(), - stmt.location().clone(), + *stmt.location(), ), - StmtBody::Label { label, body } => self - .rewrite_return_stmt_with_goto(body, return_symbol, end_label) - .with_label(*label), + StmtBody::Label { label, body } => { + Self::rewrite_return_stmt_with_goto(body, return_symbol, end_label) + .with_label(*label) + } _ => stmt.clone(), } } /// Append a given suffix to all labels and goto destinations in `stmt`. - fn append_suffix_to_stmt(&self, stmt: &Stmt, suffix: &str) -> Stmt { + fn append_suffix_to_stmt(stmt: &Stmt, suffix: &str) -> Stmt { match stmt.body() { StmtBody::Label { label, body } => { let new_label = format!("{}{}", label, suffix); - self.append_suffix_to_stmt(body, suffix).with_label(new_label) + Self::append_suffix_to_stmt(body, suffix).with_label(new_label) } StmtBody::Goto { dest, .. } => { let new_target = format!("{}{}", dest, suffix); - Stmt::goto(new_target, stmt.location().clone()) + Stmt::goto(new_target, *stmt.location()) } StmtBody::Block(stmts) => Stmt::block( - stmts.iter().map(|s| self.append_suffix_to_stmt(s, suffix)).collect(), - stmt.location().clone(), + stmts.iter().map(|s| Self::append_suffix_to_stmt(s, suffix)).collect(), + *stmt.location(), ), StmtBody::Ifthenelse { i, t, e } => Stmt::if_then_else( i.clone(), - self.append_suffix_to_stmt(t, suffix), - e.clone().map(|s| self.append_suffix_to_stmt(&s, suffix)), - stmt.location().clone(), + Self::append_suffix_to_stmt(t, suffix), + e.clone().map(|s| Self::append_suffix_to_stmt(&s, suffix)), + *stmt.location(), ), StmtBody::Switch { control, cases, default } => { // Append the suffix to each case let new_cases: Vec<_> = cases .iter() .map(|case| { - let new_body = self.append_suffix_to_stmt(case.body(), suffix); + let new_body = Self::append_suffix_to_stmt(case.body(), suffix); SwitchCase::new(case.case().clone(), new_body) }) .collect(); // Append the suffix to the default case, if it exists let new_default = - default.as_ref().map(|stmt| self.append_suffix_to_stmt(stmt, suffix)); + default.as_ref().map(|stmt| Self::append_suffix_to_stmt(stmt, suffix)); // Construct the new switch statement - Stmt::switch(control.clone(), new_cases, new_default, stmt.location().clone()) + Stmt::switch(control.clone(), new_cases, new_default, *stmt.location()) } StmtBody::While { .. } | StmtBody::For { .. } => { unimplemented!() @@ -559,9 +556,9 @@ impl GotocCtx<'_> { .zip(arguments.iter()) .map(|(param, arg)| { Stmt::decl( - Expr::symbol_expression(param.clone(), arg.typ().clone()), + Expr::symbol_expression(*param, arg.typ().clone()), None, - arg.location().clone(), + *arg.location(), ) }) .collect(); @@ -572,9 +569,9 @@ impl GotocCtx<'_> { .zip(arguments.iter()) .map(|(param, arg)| { Stmt::assign( - Expr::symbol_expression(param.clone(), arg.typ().clone()), + Expr::symbol_expression(*param, arg.typ().clone()), arg.clone(), - arg.location().clone(), + *arg.location(), ) }) .collect(); @@ -588,7 +585,7 @@ impl GotocCtx<'_> { let count_return: usize = stmts_of_inlined_body .clone() .iter() - .map(|stmt: &Stmt| self.count_return_stmts(stmt)) + .map(|stmt: &Stmt| Self::count_return_stmts(stmt)) .sum(); // The function is a void function, we safely ignore it. if count_return == 0 { @@ -601,7 +598,7 @@ impl GotocCtx<'_> { let suffix = format!("_{}", suffix_count); stmts_of_inlined_body = stmts_of_inlined_body .iter() - .map(|stmt| self.append_suffix_to_stmt(stmt, &suffix)) + .map(|stmt| Self::append_suffix_to_stmt(stmt, &suffix)) .collect(); // Replace all return stmts with symbol expressions. @@ -611,22 +608,20 @@ impl GotocCtx<'_> { stmts_of_inlined_body = stmts_of_inlined_body .iter() .map(|stmt| { - self.rewrite_return_stmt_with_goto(stmt, &mut end_stmt, &end_label) + Self::rewrite_return_stmt_with_goto(stmt, &mut end_stmt, &end_label) }) .collect(); stmts_of_inlined_body - .push(Stmt::skip(expr.location().clone()).with_label(end_label)); - stmts_of_inlined_body.push(Stmt::code_expression( - end_stmt.unwrap(), - expr.location().clone(), - )); + .push(Stmt::skip(*expr.location()).with_label(end_label)); + stmts_of_inlined_body + .push(Stmt::code_expression(end_stmt.unwrap(), *expr.location())); // Recursively inline function calls in the function body. let res = self.inline_function_calls_in_expr( &Expr::statement_expression( stmts_of_inlined_body, expr.typ().clone(), - expr.location().clone(), + *expr.location(), ), visited_func_symbols, suffix_count, @@ -666,7 +661,7 @@ impl GotocCtx<'_> { return Some(Expr::statement_expression( inlined_stmts, expr.typ().clone(), - expr.location().clone(), + *expr.location(), )); } _ => {} @@ -684,22 +679,12 @@ impl GotocCtx<'_> { suffix_count: &mut u16, ) -> Option { match stmt.body() { - StmtBody::Expression(expr) => { - match self.inline_function_calls_in_expr(expr, visited_func_symbols, suffix_count) { - None => None, - Some(inlined_expr) => { - Some(Stmt::code_expression(inlined_expr, expr.location().clone())) - } - } - } - StmtBody::Assign { lhs, rhs } => { - match self.inline_function_calls_in_expr(rhs, visited_func_symbols, suffix_count) { - None => None, - Some(inlined_rhs) => { - Some(Stmt::assign(lhs.clone(), inlined_rhs, stmt.location().clone())) - } - } - } + StmtBody::Expression(expr) => self + .inline_function_calls_in_expr(expr, visited_func_symbols, suffix_count) + .map(|inlined_expr| Stmt::code_expression(inlined_expr, *expr.location())), + StmtBody::Assign { lhs, rhs } => self + .inline_function_calls_in_expr(rhs, visited_func_symbols, suffix_count) + .map(|inlined_rhs| Stmt::assign(lhs.clone(), inlined_rhs, *stmt.location())), StmtBody::Block(stmts) => { let inlined_block = stmts .iter() @@ -707,12 +692,12 @@ impl GotocCtx<'_> { self.inline_function_calls_in_stmt(s, visited_func_symbols, suffix_count) }) .collect(); - Some(Stmt::block(inlined_block, stmt.location().clone())) + Some(Stmt::block(inlined_block, *stmt.location())) } StmtBody::Label { label, body } => { match self.inline_function_calls_in_stmt(body, visited_func_symbols, suffix_count) { - None => Some(Stmt::skip(stmt.location().clone()).with_label(label.clone())), - Some(inlined_body) => Some(inlined_body.with_label(label.clone())), + None => Some(Stmt::skip(*stmt.location()).with_label(*label)), + Some(inlined_body) => Some(inlined_body.with_label(*label)), } } StmtBody::Switch { control, cases, default } => { @@ -747,7 +732,7 @@ impl GotocCtx<'_> { inlined_control, inlined_cases, inlined_default, - stmt.location().clone(), + *stmt.location(), )) } StmtBody::While { .. } | StmtBody::For { .. } => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 544438cd83ba..ce4bad2b2930 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -834,7 +834,7 @@ fn handle_quantifier( }; // Quantified variable. - let base_name = format!("kani_quantified_var"); + let base_name = "kani_quantified_var".to_string(); let mut counter = 0; let mut unique_name = format!("{}_{}", base_name, counter); // Ensure the name is not already in the symbol table From 49c22c90db920f8ef63b9cb7e7550289c080c18d Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 15:50:17 +0000 Subject: [PATCH 10/27] Fix clippy --- kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 7d1fce8b246a..7951fa95df25 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -414,7 +414,7 @@ impl GotocCtx<'_> { fn count_return_stmts(stmt: &Stmt) -> usize { match stmt.body() { StmtBody::Return(_) => 1, - StmtBody::Block(stmts) => stmts.iter().map(|s| Self::count_return_stmts(s)).sum(), + StmtBody::Block(stmts) => stmts.iter().map(Self::count_return_stmts).sum(), StmtBody::Label { label: _, body } => Self::count_return_stmts(body), _ => 0, } @@ -430,8 +430,7 @@ impl GotocCtx<'_> { match stmt.body() { StmtBody::Return(Some(expr)) => { if let ExprValue::Symbol { ref identifier } = expr.value() { - *return_symbol = - Some(Expr::symbol_expression(identifier.clone(), expr.typ().clone())); + *return_symbol = Some(Expr::symbol_expression(*identifier, expr.typ().clone())); Stmt::goto(*end_label, *stmt.location()) } else { panic!("Expected symbol expression in return statement"); From 82102091d65c21e1059c4d004c45f0c70508526b Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 15:52:19 +0000 Subject: [PATCH 11/27] Make universal quantification complete --- kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index ce4bad2b2930..5e41872b816e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -855,8 +855,10 @@ fn handle_quantifier( let quantifier_expr = match quantifier_kind { QuantifierKind::ForAll => { - let domain = range.implies( - closure_call_expr.call(vec![predicate.clone(), new_variable_expr.clone()]), + let domain = range.clone().implies( + closure_call_expr + .call(vec![predicate.clone(), new_variable_expr.clone()]) + .and(range.not().implies(Expr::bool_true())), ); Expr::forall_expr(Type::Bool, new_variable_expr, domain) } From e27664204f52383e2f4431e5ef299fef50a2dafc Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 11 Apr 2025 16:06:17 +0000 Subject: [PATCH 12/27] Make universal quantification complete --- .../src/codegen_cprover_gotoc/overrides/hooks.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 5e41872b816e..6b15fd53ecad 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -855,11 +855,10 @@ fn handle_quantifier( let quantifier_expr = match quantifier_kind { QuantifierKind::ForAll => { - let domain = range.clone().implies( - closure_call_expr - .call(vec![predicate.clone(), new_variable_expr.clone()]) - .and(range.not().implies(Expr::bool_true())), - ); + let domain = range + .clone() + .implies(closure_call_expr.call(vec![predicate.clone(), new_variable_expr.clone()])) + .and(range.not().implies(Expr::bool_true())); Expr::forall_expr(Type::Bool, new_variable_expr, domain) } QuantifierKind::Exists => { From 5a60da90c1fcd9ec9755bf43bd151e0824a6f265 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 15 Apr 2025 05:52:05 +0000 Subject: [PATCH 13/27] Add tests for quantifier expression with array indexing --- tests/expected/quantifiers/expected | 1 - .../quantifiers/from_raw_parts_fixme.rs | 38 ------------------- tests/kani/Quantifiers/slice_fixme.rs | 28 ++++++++++++++ 3 files changed, 28 insertions(+), 39 deletions(-) delete mode 100644 tests/expected/quantifiers/expected delete mode 100644 tests/expected/quantifiers/from_raw_parts_fixme.rs create mode 100644 tests/kani/Quantifiers/slice_fixme.rs diff --git a/tests/expected/quantifiers/expected b/tests/expected/quantifiers/expected deleted file mode 100644 index 34c886c358cb..000000000000 --- a/tests/expected/quantifiers/expected +++ /dev/null @@ -1 +0,0 @@ -VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/quantifiers/from_raw_parts_fixme.rs b/tests/expected/quantifiers/from_raw_parts_fixme.rs deleted file mode 100644 index 30c74f90ee64..000000000000 --- a/tests/expected/quantifiers/from_raw_parts_fixme.rs +++ /dev/null @@ -1,38 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::mem; - -extern crate kani; -use kani::{kani_exists, kani_forall}; - -#[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)); - } -} diff --git a/tests/kani/Quantifiers/slice_fixme.rs b/tests/kani/Quantifiers/slice_fixme.rs new file mode 100644 index 000000000000..8bb9ac91114b --- /dev/null +++ b/tests/kani/Quantifiers/slice_fixme.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::kani_forall; + +#[kani::proof] +fn vec_assert_forall_harness() { + let v = vec![10 as u8; 128]; + let ptr = v.as_ptr(); + unsafe { + kani::assert(kani::forall!(|i in (0,128)| *ptr.wrapping_byte_offset(i as isize) == 10), ""); + } +} + +#[kani::proof] +fn slice_assume_forall_harness() { + let arr: [u8; 8] = kani::any(); + let bytes = kani::slice::any_slice_of_array(&arr); + let ptr = bytes.as_ptr(); + kani::assume(bytes.len() > 0); + unsafe { + kani::assume( + kani::forall!(|i in (0,bytes.len())| *ptr.wrapping_byte_offset(i as isize) < 8), + ); + } + kani::assert(bytes[0] < 8, ""); +} From 8c242b8e1e50018f1dc0437031dd0507466a20e2 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 15 Apr 2025 06:09:27 +0000 Subject: [PATCH 14/27] Add fixme info --- tests/kani/Quantifiers/from_raw_part_fixme.rs | 48 +++++++++++++++++++ tests/kani/Quantifiers/no_array_fixme.rs | 2 + tests/kani/Quantifiers/slice_fixme.rs | 2 + 3 files changed, 52 insertions(+) create mode 100644 tests/kani/Quantifiers/from_raw_part_fixme.rs diff --git a/tests/kani/Quantifiers/from_raw_part_fixme.rs b/tests/kani/Quantifiers/from_raw_part_fixme.rs new file mode 100644 index 000000000000..1310f411e23a --- /dev/null +++ b/tests/kani/Quantifiers/from_raw_part_fixme.rs @@ -0,0 +1,48 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! FIXME: + +use std::mem; + +extern crate kani; +use kani::{kani_exists, kani_forall}; + +#[kani::proof] +fn main() { + let original_v = vec![kani::any::(); 3]; + let v = original_v.clone(); + let v_len = v.len(); + let v_ptr = v.as_ptr(); + unsafe { + kani::assume( + kani::forall!(|i in (0,v_len) | *v_ptr.wrapping_byte_offset(4*i as isize) < 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); + let rebuilt_ptr = v.as_ptr(); + assert!( + kani::exists!(| i in (0, len) | *rebuilt_ptr.wrapping_byte_offset(4*i as isize) == 0) + ); + } +} diff --git a/tests/kani/Quantifiers/no_array_fixme.rs b/tests/kani/Quantifiers/no_array_fixme.rs index 41dd63bfe24d..3d4e0748aae7 100644 --- a/tests/kani/Quantifiers/no_array_fixme.rs +++ b/tests/kani/Quantifiers/no_array_fixme.rs @@ -1,6 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! FIXME: + extern crate kani; use kani::{kani_exists, kani_forall}; diff --git a/tests/kani/Quantifiers/slice_fixme.rs b/tests/kani/Quantifiers/slice_fixme.rs index 8bb9ac91114b..149f80bfee48 100644 --- a/tests/kani/Quantifiers/slice_fixme.rs +++ b/tests/kani/Quantifiers/slice_fixme.rs @@ -1,6 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! FIXME: + extern crate kani; use kani::kani_forall; From 40195bcea3d6c1f3da459ffb14a7475e1d91437a Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 15 Apr 2025 06:19:07 +0000 Subject: [PATCH 15/27] Update RFC with function inlining --- rfc/src/rfcs/0010-quantifiers.md | 48 ++++++++++++++++++++++++++------ 1 file changed, 39 insertions(+), 9 deletions(-) diff --git a/rfc/src/rfcs/0010-quantifiers.md b/rfc/src/rfcs/0010-quantifiers.md index 892b89b3c722..cf0ad48dfd0d 100644 --- a/rfc/src/rfcs/0010-quantifiers.md +++ b/rfc/src/rfcs/0010-quantifiers.md @@ -20,7 +20,7 @@ There are two primary quantifiers: the existential quantifier (∃) and the univ Rather than exhaustively listing all elements in a domain, quantifiers enable users to make statements about the entire domain at once. This compact representation is crucial when dealing with large or unbounded inputs. Quantifiers also facilitate abstraction and generalization of properties. Instead of specifying properties for specific instances, quantified properties can capture general patterns and behaviors that hold across different objects in a domain. Additionally, by replacing loops in the specification with quantifiers, Kani can encode the properties more efficiently within the specified bounds, making the verification process more manageable and computationally feasible. -This new feature doesn't introduce any breaking changes to users. It will only allow them to write properites using the existential (∃) and universal (∀) quantifiers. +This new feature doesn't introduce any breaking changes to users. It will only allow them to write properties using the existential (∃) and universal (∀) quantifiers. ## User Experience @@ -100,7 +100,7 @@ fn main() { } ``` -This, however, might unnecessary increase the complexity of the verication process. We can achieve the same effect using quantifiers as shown below. +This, however, might unnecessary increase the complexity of the verification process. We can achieve the same effect using quantifiers as shown below. ```rust use std::mem; @@ -110,10 +110,16 @@ use kani::{kani_forall, kani_exists}; #[kani::proof] fn main() { - let original_v = vec![kani::any::(); 3]; + 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)); + let v_ptr = v.as_ptr(); + let original_v_ptr = original_v.as_ptr(); + unsafe { + kani::assume( + kani::forall!(|i in (0,v_len) | *v_ptr.wrapping_byte_offset(4*i as isize) < 5), + ); + } // Prevent running `v`'s destructor so we are in complete control // of the allocation. @@ -128,11 +134,17 @@ fn main() { // 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::forall!(|i in (0, len) | rebuilt[i] == original_v[i]+1)); + let rebuilt_ptr = v.as_ptr(); + assert!( + kani::exists!(| i in (0, len) | *rebuilt_ptr.wrapping_byte_offset(4*i as isize) == original_v_ptr.wrapping_byte_offset(4*i as isize) + 1) + ); } } ``` @@ -147,10 +159,15 @@ use kani::{kani_forall, kani_exists}; #[kani::proof] fn main() { - let original_v = vec![kani::any::(); 3]; + 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)); + let v_ptr = v.as_ptr(); + unsafe { + kani::assume( + kani::forall!(|i in (0,v_len) | *v_ptr.wrapping_byte_offset(4*i as isize) < 5), + ); + } // Prevent running `v`'s destructor so we are in complete control // of the allocation. @@ -166,13 +183,16 @@ fn main() { for i in 0..len { *p.add(i) += 1; if i == 1 { - *p.add(i) = 0; + *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)); + let rebuilt_ptr = v.as_ptr(); + assert!( + kani::exists!(| i in (0, len) | *rebuilt_ptr.wrapping_byte_offset(4*i as isize) == 0) + ); } } ``` @@ -185,6 +205,16 @@ The usage of quantifiers should be valid in any part of the Rust code analysed b Kani should have the same support that CBMC has for quantifiers. For more details, see [Quantifiers](https://github.com/diffblue/cbmc/blob/0a69a64e4481473d62496f9975730d24f194884a/doc/cprover-manual/contracts-quantifiers.md). +The implementation of quantifiers in Kani will be based on the following principle: +- **Single expression without function calls**: CBMC's quantifiers only support + single expressions without function calls. This means that the CBMC expressions generated + from the quantifiers in Kani should be limited to a single expression without any + function calls. + +To achieve this, we will need to implement the function inlining pass in Kani. This + pass will inline all function calls in quantifiers before they are codegened to CBMC + expressions. This will ensure that the generated expressions are compliant with CBMC's + quantifier support. ## Open questions From fac313fb4b02424d2b742e52cdc95f3a6c5b8d49 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 22 Apr 2025 15:41:13 +0000 Subject: [PATCH 16/27] Make even test non fixme --- tests/kani/Quantifiers/{even_fixme.rs => even.rs} | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) rename tests/kani/Quantifiers/{even_fixme.rs => even.rs} (51%) diff --git a/tests/kani/Quantifiers/even_fixme.rs b/tests/kani/Quantifiers/even.rs similarity index 51% rename from tests/kani/Quantifiers/even_fixme.rs rename to tests/kani/Quantifiers/even.rs index 7aac6214b322..32b554d77162 100644 --- a/tests/kani/Quantifiers/even_fixme.rs +++ b/tests/kani/Quantifiers/even.rs @@ -6,7 +6,7 @@ use kani::kani_exists; #[kani::proof] fn quantifier_even_harness() { - let j: isize = kani::any(); - kani::assume(j % 2 == 0 && j < 2000 && j > -2000); - kani::assert(kani::exists!(|i in (-1000, 1000)| i + i == j), ""); + let j: usize = kani::any(); + kani::assume(j % 2 == 0 && j < 2000); + kani::assert(kani::exists!(|i in (0, 1000)| i + i == j), ""); } From 131d5038a040f1b6ade42a92f4b34662ae48af02 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 22 Apr 2025 15:55:15 +0000 Subject: [PATCH 17/27] Update array tests --- .../{slice_fixme.rs => array_fixme.rs} | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) rename tests/kani/Quantifiers/{slice_fixme.rs => array_fixme.rs} (54%) diff --git a/tests/kani/Quantifiers/slice_fixme.rs b/tests/kani/Quantifiers/array_fixme.rs similarity index 54% rename from tests/kani/Quantifiers/slice_fixme.rs rename to tests/kani/Quantifiers/array_fixme.rs index 149f80bfee48..31b11d0841de 100644 --- a/tests/kani/Quantifiers/slice_fixme.rs +++ b/tests/kani/Quantifiers/array_fixme.rs @@ -18,13 +18,21 @@ fn vec_assert_forall_harness() { #[kani::proof] fn slice_assume_forall_harness() { let arr: [u8; 8] = kani::any(); - let bytes = kani::slice::any_slice_of_array(&arr); - let ptr = bytes.as_ptr(); - kani::assume(bytes.len() > 0); + let ptr = arr.as_ptr(); + unsafe { + kani::assume(kani::forall!(|i in (0,arr.len())| *ptr.wrapping_byte_offset(i as isize) < 8)); + } + kani::assert(arr[0] < 8, ""); +} + +#[kani::proof] +fn slice_assume_sorted_harness() { + let arr: [u8; 12] = kani::any(); + let ptr = arr.as_ptr(); unsafe { kani::assume( - kani::forall!(|i in (0,bytes.len())| *ptr.wrapping_byte_offset(i as isize) < 8), + kani::forall!(|i in (0,arr.len()-1)| *ptr.wrapping_byte_offset(i as isize) < *ptr.wrapping_byte_offset((i+1) as isize)), ); } - kani::assert(bytes[0] < 8, ""); + kani::assert(arr[0] < arr[1], ""); } From 3bf250b568d955a3c438684c5dcf97be6d4ebdd2 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 22 Apr 2025 16:01:32 +0000 Subject: [PATCH 18/27] Add tests with quantifiers in contracts --- tests/kani/Quantifiers/contracts_fixme.rs | 50 +++++++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 tests/kani/Quantifiers/contracts_fixme.rs diff --git a/tests/kani/Quantifiers/contracts_fixme.rs b/tests/kani/Quantifiers/contracts_fixme.rs new file mode 100644 index 000000000000..09f558281450 --- /dev/null +++ b/tests/kani/Quantifiers/contracts_fixme.rs @@ -0,0 +1,50 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! FIXME: + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] +extern crate kani; +use kani::kani_forall; + +#[kani::requires(i==0)] +#[kani::ensures(|ret| { + unsafe{ + let ptr = arr.as_ptr(); kani::forall!(| k in (0, 8)| *ptr.wrapping_byte_offset(k as isize) == 0)}})] +#[kani::modifies(arr)] +pub fn set_zero(arr: &mut [u8; 8], mut i: usize) -> usize { + while i < 8 { + arr[i] = 0; + i = i + 1; + } + i +} + +#[kani::proof_for_contract(set_zero)] +fn set_zero_harness() { + let mut arr: [u8; 8] = kani::any(); + let i: usize = 0; + let _j = set_zero(&mut arr, i); +} + +#[kani::ensures(|ret| { + unsafe{ + let ptr_x = xs.as_ptr(); + let ptr_y = ys.as_ptr(); kani::forall!(| k in (0, 8)| *ptr_x.wrapping_byte_offset(k as isize) == *ptr_y.wrapping_byte_offset(k as isize))}})] +#[kani::modifies(ys)] +pub fn copy(xs: &mut [u8; 8], ys: &mut [u8; 8]) { + let mut i = 0; + while i < 8 { + ys[i] = xs[i]; + i = i + 1; + } +} + +#[kani::proof_for_contract(copy)] +fn copy_harness() { + let mut xs: [u8; 8] = kani::any(); + let mut ys: [u8; 8] = kani::any(); + copy(&mut xs, &mut ys); +} From acee4efa9f1d9386d6589398e231a579db742ff2 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 22 Apr 2025 16:35:50 +0000 Subject: [PATCH 19/27] Add document for quantifiers --- .../src/reference/experimental/quantifiers.md | 62 +++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 docs/src/reference/experimental/quantifiers.md diff --git a/docs/src/reference/experimental/quantifiers.md b/docs/src/reference/experimental/quantifiers.md new file mode 100644 index 000000000000..7af96eea39ad --- /dev/null +++ b/docs/src/reference/experimental/quantifiers.md @@ -0,0 +1,62 @@ +# Quantifiers in Kani + +Quantifiers are a powerful feature in formal verification that allow you to express properties over a range of values. Kani provides experimental support for quantifiers, enabling users to write concise and expressive specifications for their programs. + +## Supported Quantifiers + +Kani currently supports the following quantifiers: + +1. **Universal Quantifier**: + - Ensures that a property holds for all values in a given range. + - Syntax: `kani::forall!(|variable in range| condition)` + - Example: + +```rust +extern crate kani; +use kani::kani_forall; +#[kani::proof] +fn test_forall() { + let v = vec![10; 10]; + kani::assert(kani::forall!(|i in 0..10| v[i] == 10)); +} +``` + +2. **Existential Quantifier**: + - Ensures that there exists at least one value in a given range for which a property holds. + - Syntax: `kani::exists!(|variable in range| condition)` + - Example: + +```rust +extern crate kani; +use kani::kani_exists; +#[kani::proof] +fn test_exists() { + let v = vec![1, 2, 3, 4, 5]; + kani::assert(kani::exists!(|i in 0..v.len()| v[i] == 3)); +} +``` + +### Limitations + +#### Array Indexing + +The performance of quantifiers can be affected by the depth of call stacks in the quantified expressions. If the call stack is too deep, Kani may not be able to evaluate the quantifier effectively, leading to potential timeouts or running out of memory. Actually, array indexing in Rust leads to a deep call stack, which can cause issues with quantifiers. To mitigate this, consider using *unsafe* pointer dereferencing instead of array indexing when working with quantifiers. For example: + +```rust +extern crate kani; +use kani::kani_forall; + +#[kani::proof] +fn vec_assert_forall_harness() { + let v = vec![10 as u8; 128]; + let ptr = v.as_ptr(); + unsafe { + kani::assert(kani::forall!(|i in (0,128)| *ptr.wrapping_byte_offset(i as isize) == 10), ""); + } +} +``` + +#### Types of Quantified Variables + +We now assume that all quantified variables are of type `usize`. This means that the range specified in the quantifier must be compatible with `usize`. + We plan to support other types in the future, but for now, ensure that your quantifiers use `usize` ranges. From e336cadddd4dd22399fdecb493b9139524bf4934 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 24 Apr 2025 15:00:53 +0000 Subject: [PATCH 20/27] Fix format --- tests/kani/Quantifiers/contracts_fixme.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/kani/Quantifiers/contracts_fixme.rs b/tests/kani/Quantifiers/contracts_fixme.rs index 09f558281450..10cfc8f82d56 100644 --- a/tests/kani/Quantifiers/contracts_fixme.rs +++ b/tests/kani/Quantifiers/contracts_fixme.rs @@ -31,10 +31,10 @@ fn set_zero_harness() { #[kani::ensures(|ret| { unsafe{ - let ptr_x = xs.as_ptr(); + let ptr_x = xs.as_ptr(); let ptr_y = ys.as_ptr(); kani::forall!(| k in (0, 8)| *ptr_x.wrapping_byte_offset(k as isize) == *ptr_y.wrapping_byte_offset(k as isize))}})] #[kani::modifies(ys)] -pub fn copy(xs: &mut [u8; 8], ys: &mut [u8; 8]) { +pub fn copy(xs: &mut [u8; 8], ys: &mut [u8; 8]) { let mut i = 0; while i < 8 { ys[i] = xs[i]; From a3549ec6cb90f6ccc5bbd07d9daed1e59df61dcc Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 24 Apr 2025 16:10:22 +0000 Subject: [PATCH 21/27] Fix clippy --- kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs | 6 +++--- kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 7951fa95df25..8dde51d755ce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -455,11 +455,11 @@ impl GotocCtx<'_> { fn append_suffix_to_stmt(stmt: &Stmt, suffix: &str) -> Stmt { match stmt.body() { StmtBody::Label { label, body } => { - let new_label = format!("{}{}", label, suffix); + let new_label = format!("{label}{suffix}"); Self::append_suffix_to_stmt(body, suffix).with_label(new_label) } StmtBody::Goto { dest, .. } => { - let new_target = format!("{}{}", dest, suffix); + let new_target = format!("{dest}{suffix}"); Stmt::goto(new_target, *stmt.location()) } StmtBody::Block(stmts) => Stmt::block( @@ -594,7 +594,7 @@ impl GotocCtx<'_> { assert_eq!(count_return, 1); // Make labels in the inlined body unique. - let suffix = format!("_{}", suffix_count); + let suffix = format!("_{suffix_count}"); stmts_of_inlined_body = stmts_of_inlined_body .iter() .map(|stmt| Self::append_suffix_to_stmt(stmt, &suffix)) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 6b15fd53ecad..3a30e397f52b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -836,11 +836,11 @@ fn handle_quantifier( // Quantified variable. let base_name = "kani_quantified_var".to_string(); let mut counter = 0; - let mut unique_name = format!("{}_{}", base_name, counter); + let mut unique_name = format!("{base_name}_{counter}"); // Ensure the name is not already in the symbol table while gcx.symbol_table.lookup(&unique_name).is_some() { counter += 1; - unique_name = format!("{}_{}", base_name, counter); + unique_name = format!("{base_name}_{counter}"); } let new_variable_expr = { let new_symbol = From 41b4755326b0f5ba577d118d7b5a23b3d07d4c01 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Apr 2025 13:19:35 +0000 Subject: [PATCH 22/27] Update tests --- .../Quantifiers/{array_fixme.rs => array.rs} | 2 - .../{contracts_fixme.rs => contracts.rs} | 2 - tests/kani/Quantifiers/no_array.rs | 25 +++++++++ tests/kani/Quantifiers/no_array_fixme.rs | 53 ------------------- 4 files changed, 25 insertions(+), 57 deletions(-) rename tests/kani/Quantifiers/{array_fixme.rs => array.rs} (93%) rename tests/kani/Quantifiers/{contracts_fixme.rs => contracts.rs} (95%) delete mode 100644 tests/kani/Quantifiers/no_array_fixme.rs diff --git a/tests/kani/Quantifiers/array_fixme.rs b/tests/kani/Quantifiers/array.rs similarity index 93% rename from tests/kani/Quantifiers/array_fixme.rs rename to tests/kani/Quantifiers/array.rs index 31b11d0841de..1a127ab78888 100644 --- a/tests/kani/Quantifiers/array_fixme.rs +++ b/tests/kani/Quantifiers/array.rs @@ -1,8 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! FIXME: - extern crate kani; use kani::kani_forall; diff --git a/tests/kani/Quantifiers/contracts_fixme.rs b/tests/kani/Quantifiers/contracts.rs similarity index 95% rename from tests/kani/Quantifiers/contracts_fixme.rs rename to tests/kani/Quantifiers/contracts.rs index 10cfc8f82d56..6e3621297048 100644 --- a/tests/kani/Quantifiers/contracts_fixme.rs +++ b/tests/kani/Quantifiers/contracts.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -//! FIXME: - #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] extern crate kani; diff --git a/tests/kani/Quantifiers/no_array.rs b/tests/kani/Quantifiers/no_array.rs index 1992b995ceef..bebd5044c7fa 100644 --- a/tests/kani/Quantifiers/no_array.rs +++ b/tests/kani/Quantifiers/no_array.rs @@ -18,9 +18,34 @@ fn forall_assume_harness() { kani::assert(j > 4, ""); } +fn comp(x: usize, y: usize) -> bool { + x > y +} + +#[kani::proof] +fn forall_function_harness() { + let j = kani::any(); + kani::assume(j > 5); + kani::assert(kani::forall!(|i in (2,5)| comp(j, i) ), ""); +} + #[kani::proof] fn exists_assert_harness() { let j = kani::any(); kani::assume(j > 2); kani::assert(kani::exists!(|i in (2,5)| i < j ), ""); } + +#[kani::proof] +fn exists_assume_harness() { + let j = kani::any(); + kani::assume(kani::exists!(|i in (2,4)| i == j)); + kani::assert(j == 3 || j == 2, ""); +} + +#[kani::proof] +fn exists_function_harness() { + let j = kani::any(); + kani::assume(j > 2); + kani::assert(kani::exists!(|i in (2,5)| comp(j, i) ), ""); +} diff --git a/tests/kani/Quantifiers/no_array_fixme.rs b/tests/kani/Quantifiers/no_array_fixme.rs deleted file mode 100644 index 3d4e0748aae7..000000000000 --- a/tests/kani/Quantifiers/no_array_fixme.rs +++ /dev/null @@ -1,53 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! FIXME: - -extern crate kani; -use kani::{kani_exists, kani_forall}; - -#[kani::proof] -fn forall_assert_harness() { - let j = kani::any(); - kani::assume(j > 5); - kani::assert(kani::forall!(|i in (2,5)| i < j ), ""); -} - -#[kani::proof] -fn forall_assume_harness() { - let j = kani::any(); - kani::assume(kani::forall!(|i in (2,5)| i < j)); - kani::assert(j > 4, ""); -} - -fn comp(x: isize, y: isize) -> bool { - x > y -} - -#[kani::proof] -fn forall_function_harness() { - let j = kani::any(); - kani::assume(j > 5); - kani::assert(kani::forall!(|i in (2,5)| comp(j, i) ), ""); -} - -#[kani::proof] -fn exists_assert_harness() { - let j = kani::any(); - kani::assume(j > 2); - kani::assert(kani::exists!(|i in (2,5)| i < j ), ""); -} - -#[kani::proof] -fn exists_assume_harness() { - let j = kani::any(); - kani::assume(kani::exists!(|i in (2,4)| i == j)); - kani::assert(j == 3 || j == 2, ""); -} - -#[kani::proof] -fn exists_function_harness() { - let j = kani::any(); - kani::assume(j > 2); - kani::assert(kani::exists!(|i in (2,5)| comp(j, i) ), ""); -} From 6d795e9d023b8ffed426acea5635840ccf7697ca Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 30 Apr 2025 05:06:13 +0000 Subject: [PATCH 23/27] Add expected tests --- .../assert_with_exists_fail.expected | 4 +++ .../quantifiers/assert_with_exists_fail.rs | 12 ++++++++ .../assert_with_exists_pass.expected | 4 +++ .../quantifiers/assert_with_exists_pass.rs | 12 ++++++++ .../assert_with_forall_fail.expected | 5 ++++ .../quantifiers/assert_with_forall_fail.rs | 12 ++++++++ .../assert_with_forall_pass.expected | 4 +++ .../quantifiers/assert_with_forall_pass.rs | 12 ++++++++ .../assume_with_exists_fail.expected | 4 +++ .../quantifiers/assume_with_exists_fail.rs | 12 ++++++++ .../quantifiers/contracts_fail.expected | 7 +++++ tests/expected/quantifiers/contracts_fail.rs | 29 +++++++++++++++++++ 12 files changed, 117 insertions(+) create mode 100644 tests/expected/quantifiers/assert_with_exists_fail.expected create mode 100644 tests/expected/quantifiers/assert_with_exists_fail.rs create mode 100644 tests/expected/quantifiers/assert_with_exists_pass.expected create mode 100644 tests/expected/quantifiers/assert_with_exists_pass.rs create mode 100644 tests/expected/quantifiers/assert_with_forall_fail.expected create mode 100644 tests/expected/quantifiers/assert_with_forall_fail.rs create mode 100644 tests/expected/quantifiers/assert_with_forall_pass.expected create mode 100644 tests/expected/quantifiers/assert_with_forall_pass.rs create mode 100644 tests/expected/quantifiers/assume_with_exists_fail.expected create mode 100644 tests/expected/quantifiers/assume_with_exists_fail.rs create mode 100644 tests/expected/quantifiers/contracts_fail.expected create mode 100644 tests/expected/quantifiers/contracts_fail.rs diff --git a/tests/expected/quantifiers/assert_with_exists_fail.expected b/tests/expected/quantifiers/assert_with_exists_fail.expected new file mode 100644 index 000000000000..7c93e835e724 --- /dev/null +++ b/tests/expected/quantifiers/assert_with_exists_fail.expected @@ -0,0 +1,4 @@ +- Status: FAILURE\ +- Description: "assertion with exists"\ + +VERIFICATION:- FAILED diff --git a/tests/expected/quantifiers/assert_with_exists_fail.rs b/tests/expected/quantifiers/assert_with_exists_fail.rs new file mode 100644 index 000000000000..71b3a5df3728 --- /dev/null +++ b/tests/expected/quantifiers/assert_with_exists_fail.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::kani_exists; + +#[kani::proof] +fn exists_assert_harness() { + let j = kani::any(); + kani::assume(j > 1); + kani::assert(kani::exists!(|i in (3,5)| i < j ), "assertion with exists"); +} diff --git a/tests/expected/quantifiers/assert_with_exists_pass.expected b/tests/expected/quantifiers/assert_with_exists_pass.expected new file mode 100644 index 000000000000..33abfd607aaa --- /dev/null +++ b/tests/expected/quantifiers/assert_with_exists_pass.expected @@ -0,0 +1,4 @@ +- Status: SUCCESS\ +- Description: "assertion with exists"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/quantifiers/assert_with_exists_pass.rs b/tests/expected/quantifiers/assert_with_exists_pass.rs new file mode 100644 index 000000000000..cb79ea26fb30 --- /dev/null +++ b/tests/expected/quantifiers/assert_with_exists_pass.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::kani_exists; + +#[kani::proof] +fn exists_assert_harness() { + let j = kani::any(); + kani::assume(j > 2); + kani::assert(kani::exists!(|i in (2,5)| i < j ), "assertion with exists"); +} diff --git a/tests/expected/quantifiers/assert_with_forall_fail.expected b/tests/expected/quantifiers/assert_with_forall_fail.expected new file mode 100644 index 000000000000..d8eaf5db2b9a --- /dev/null +++ b/tests/expected/quantifiers/assert_with_forall_fail.expected @@ -0,0 +1,5 @@ +- Status: FAILURE\ +- Description: "assertion with forall"\ + +VERIFICATION:- FAILED + diff --git a/tests/expected/quantifiers/assert_with_forall_fail.rs b/tests/expected/quantifiers/assert_with_forall_fail.rs new file mode 100644 index 000000000000..279cba423fbe --- /dev/null +++ b/tests/expected/quantifiers/assert_with_forall_fail.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::kani_forall; + +#[kani::proof] +fn forall_assert_harness() { + let j = kani::any(); + kani::assume(j > 3); + kani::assert(kani::forall!(|i in (2,5)| i < j ), "assertion with forall"); +} diff --git a/tests/expected/quantifiers/assert_with_forall_pass.expected b/tests/expected/quantifiers/assert_with_forall_pass.expected new file mode 100644 index 000000000000..d6f419825425 --- /dev/null +++ b/tests/expected/quantifiers/assert_with_forall_pass.expected @@ -0,0 +1,4 @@ +- Status: SUCCESS\ +- Description: "assertion with forall"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/quantifiers/assert_with_forall_pass.rs b/tests/expected/quantifiers/assert_with_forall_pass.rs new file mode 100644 index 000000000000..62a4e031f3a6 --- /dev/null +++ b/tests/expected/quantifiers/assert_with_forall_pass.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::kani_forall; + +#[kani::proof] +fn forall_assert_harness() { + let j = kani::any(); + kani::assume(j > 5); + kani::assert(kani::forall!(|i in (2,5)| i < j ), "assertion with forall"); +} diff --git a/tests/expected/quantifiers/assume_with_exists_fail.expected b/tests/expected/quantifiers/assume_with_exists_fail.expected new file mode 100644 index 000000000000..794397c227e8 --- /dev/null +++ b/tests/expected/quantifiers/assume_with_exists_fail.expected @@ -0,0 +1,4 @@ +- Status: FAILURE\ +- Description: "assume with exists"\ + +VERIFICATION:- FAILED diff --git a/tests/expected/quantifiers/assume_with_exists_fail.rs b/tests/expected/quantifiers/assume_with_exists_fail.rs new file mode 100644 index 000000000000..073c150ed5a9 --- /dev/null +++ b/tests/expected/quantifiers/assume_with_exists_fail.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +extern crate kani; +use kani::kani_exists; + +#[kani::proof] +fn exists_assume_harness() { + let j = kani::any(); + kani::assume(kani::exists!(|i in (2,4)| i == j)); + kani::assert(j == 3, "assume with exists"); +} \ No newline at end of file diff --git a/tests/expected/quantifiers/contracts_fail.expected b/tests/expected/quantifiers/contracts_fail.expected new file mode 100644 index 000000000000..64ddeaacd782 --- /dev/null +++ b/tests/expected/quantifiers/contracts_fail.expected @@ -0,0 +1,7 @@ +- Status: FAILURE\ +- Description: "|ret| +{ + unsafe{ + let ptr_x = xs.as_ptr(); let ptr_y = ys.as_ptr();\ + +VERIFICATION:- FAILED diff --git a/tests/expected/quantifiers/contracts_fail.rs b/tests/expected/quantifiers/contracts_fail.rs new file mode 100644 index 000000000000..33e74668c85f --- /dev/null +++ b/tests/expected/quantifiers/contracts_fail.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] +extern crate kani; +use kani::kani_forall; + +/// Copy only first 7 elements and left the last one unchanged. +#[kani::ensures(|ret| { unsafe{ + let ptr_x = xs.as_ptr(); + let ptr_y = ys.as_ptr(); + kani::forall!(| k in (0, 8)| *ptr_x.wrapping_byte_offset(k as isize) == *ptr_y.wrapping_byte_offset(k as isize))}})] +#[kani::modifies(ys)] +pub fn copy(xs: &mut [u8; 8], ys: &mut [u8; 8]) { + let mut i = 0; + while i < 7 { + ys[i] = xs[i]; + i = i + 1; + } +} + +#[kani::proof_for_contract(copy)] +fn copy_harness() { + let mut xs: [u8; 8] = kani::any(); + let mut ys: [u8; 8] = kani::any(); + copy(&mut xs, &mut ys); +} From 71d1a924b36a6b74763509e74282a10ef042597d Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 30 Apr 2025 05:09:48 +0000 Subject: [PATCH 24/27] Fix format --- tests/expected/quantifiers/assume_with_exists_fail.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/quantifiers/assume_with_exists_fail.rs b/tests/expected/quantifiers/assume_with_exists_fail.rs index 073c150ed5a9..c591e1ed8626 100644 --- a/tests/expected/quantifiers/assume_with_exists_fail.rs +++ b/tests/expected/quantifiers/assume_with_exists_fail.rs @@ -9,4 +9,4 @@ fn exists_assume_harness() { let j = kani::any(); kani::assume(kani::exists!(|i in (2,4)| i == j)); kani::assert(j == 3, "assume with exists"); -} \ No newline at end of file +} From abb3e8e28ecb737da3b65ac90670750ec0adf19d Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 1 May 2025 06:10:18 +0000 Subject: [PATCH 25/27] Address Carolyn's comments --- docs/src/SUMMARY.md | 1 + .../codegen_cprover_gotoc/codegen/function.rs | 2 ++ .../codegen_cprover_gotoc/context/goto_ctx.rs | 19 +++++++++++++++++++ .../codegen_cprover_gotoc/overrides/hooks.rs | 9 +-------- .../quantifiers/contracts_fail.expected | 6 +++++- tests/expected/quantifiers/contracts_fail.rs | 2 -- tests/kani/Quantifiers/contracts.rs | 2 -- 7 files changed, 28 insertions(+), 13 deletions(-) diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 0b618c577021..9d7553a668d7 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -25,6 +25,7 @@ - [Contracts](./reference/experimental/contracts.md) - [Loop Contracts](./reference/experimental/loop-contracts.md) - [Concrete Playback](./reference/experimental/concrete-playback.md) + - [Quantifiers](./reference/experimental/quantifiers.md) - [Application](./application.md) - [Comparison with other tools](./tool-comparison.md) - [Where to start on real code](./tutorial-real-code.md) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 89f2ad157ede..de17c4b33879 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -47,6 +47,8 @@ impl GotocCtx<'_> { let sym_e = sym.to_expr(); self.symbol_table.insert(sym); + // Store the parameter symbols of the function, which will be used for function + // inlining. if lc > 0 && lc <= num_args { self.symbol_table.insert_parameter(function_name, name); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 8dde51d755ce..e3073f87ba6b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -309,6 +309,9 @@ impl<'tcx> GotocCtx<'tcx> { /// Quantifiers Related impl GotocCtx<'_> { /// Find all quantifier expressions and recursively inline functions in the quantifier bodies. + /// We inline all the function calls in quantifier expressions because CBMC accept only + /// statement expressiont without function calls in quantifier expressions: + /// see https://github.com/diffblue/cbmc/pull/8605 for detail. pub fn handle_quantifiers(&mut self) { // Store the found quantifiers and the inlined results. let mut to_modify: BTreeMap = BTreeMap::new(); @@ -422,6 +425,22 @@ impl GotocCtx<'_> { /// Rewrite return statements in `stmt` with a goto statement to `end_label`. /// It also stores the return symbol in `return_symbol`. + /// When inlining the function body of some function foo + /// fn foo(params) { + /// body; + /// return res; // ** rewrite this statement + /// } + /// with the statement expression + /// { + /// DECL params + /// ASSIGN params = args + /// inline(body) + /// GOTO end_label // ** to this statement + /// end_label: + /// EXPRESSION res + /// }, + /// this function rewrites all return statements + /// into a goto statement to `end_label` fn rewrite_return_stmt_with_goto( stmt: &Stmt, return_symbol: &mut Option, diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 3a30e397f52b..cf614116a0c2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -824,14 +824,7 @@ fn handle_quantifier( let closure_call_expr = find_closure_call_expr(&instance, gcx, loc) .unwrap_or_else(|| unreachable!("Failed to find closure call expression")); - let predicate = if fargs.len() == 3 { - Expr::address_of(fargs[2].clone()) - } else { - Expr::symbol_expression( - "dummy", - closure_call_expr.typ().parameters().unwrap().first().unwrap().typ().clone(), - ) - }; + let predicate = Expr::address_of(fargs[2].clone()); // Quantified variable. let base_name = "kani_quantified_var".to_string(); diff --git a/tests/expected/quantifiers/contracts_fail.expected b/tests/expected/quantifiers/contracts_fail.expected index 64ddeaacd782..1d67c28486c1 100644 --- a/tests/expected/quantifiers/contracts_fail.expected +++ b/tests/expected/quantifiers/contracts_fail.expected @@ -2,6 +2,10 @@ - Description: "|ret| { unsafe{ - let ptr_x = xs.as_ptr(); let ptr_y = ys.as_ptr();\ + let ptr_x = xs.as_ptr(); let ptr_y = ys.as_ptr(); + kani::forall!(| k in (0, 8)| *ptr_x.wrapping_byte_offset(k as isize) + == *ptr_y.wrapping_byte_offset(k as isize)) + } +}" VERIFICATION:- FAILED diff --git a/tests/expected/quantifiers/contracts_fail.rs b/tests/expected/quantifiers/contracts_fail.rs index 33e74668c85f..13b16f513fc6 100644 --- a/tests/expected/quantifiers/contracts_fail.rs +++ b/tests/expected/quantifiers/contracts_fail.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#![feature(proc_macro_hygiene)] -#![feature(stmt_expr_attributes)] extern crate kani; use kani::kani_forall; diff --git a/tests/kani/Quantifiers/contracts.rs b/tests/kani/Quantifiers/contracts.rs index 6e3621297048..fc2da350892e 100644 --- a/tests/kani/Quantifiers/contracts.rs +++ b/tests/kani/Quantifiers/contracts.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -#![feature(proc_macro_hygiene)] -#![feature(stmt_expr_attributes)] extern crate kani; use kani::kani_forall; From c8ea72f9ea0154b1d6c1e71378350492389e1fec Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 1 May 2025 06:30:23 +0000 Subject: [PATCH 26/27] Remove the need of import quantifiers --- .../src/reference/experimental/quantifiers.md | 6 --- library/kani_core/src/lib.rs | 44 +++++++++---------- rfc/src/rfcs/0010-quantifiers.md | 10 +---- .../quantifiers/assert_with_exists_fail.rs | 3 -- .../quantifiers/assert_with_exists_pass.rs | 3 -- .../quantifiers/assert_with_forall_fail.rs | 3 -- .../quantifiers/assert_with_forall_pass.rs | 3 -- .../quantifiers/assume_with_exists_fail.rs | 3 -- tests/expected/quantifiers/contracts_fail.rs | 3 -- tests/kani/Quantifiers/array.rs | 3 -- tests/kani/Quantifiers/contracts.rs | 3 -- tests/kani/Quantifiers/even.rs | 3 -- tests/kani/Quantifiers/from_raw_part_fixme.rs | 3 -- tests/kani/Quantifiers/no_array.rs | 3 -- 14 files changed, 24 insertions(+), 69 deletions(-) diff --git a/docs/src/reference/experimental/quantifiers.md b/docs/src/reference/experimental/quantifiers.md index 7af96eea39ad..c62a70f2c7b3 100644 --- a/docs/src/reference/experimental/quantifiers.md +++ b/docs/src/reference/experimental/quantifiers.md @@ -12,8 +12,6 @@ Kani currently supports the following quantifiers: - Example: ```rust -extern crate kani; -use kani::kani_forall; #[kani::proof] fn test_forall() { let v = vec![10; 10]; @@ -27,8 +25,6 @@ fn test_forall() { - Example: ```rust -extern crate kani; -use kani::kani_exists; #[kani::proof] fn test_exists() { let v = vec![1, 2, 3, 4, 5]; @@ -43,8 +39,6 @@ fn test_exists() { The performance of quantifiers can be affected by the depth of call stacks in the quantified expressions. If the call stack is too deep, Kani may not be able to evaluate the quantifier effectively, leading to potential timeouts or running out of memory. Actually, array indexing in Rust leads to a deep call stack, which can cause issues with quantifiers. To mitigate this, consider using *unsafe* pointer dereferencing instead of array indexing when working with quantifiers. For example: ```rust -extern crate kani; -use kani::kani_forall; #[kani::proof] fn vec_assert_forall_harness() { diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index b4602ce94c46..755f6960e955 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -207,17 +207,35 @@ macro_rules! kani_intrinsics { assert!(cond, "{}", msg); } + #[inline(never)] + #[kanitool::fn_marker = "ForallHook"] + pub fn kani_forall(lower_bound: T, upper_bound: T, predicate: F) -> bool + where + F: Fn(T) -> bool, + { + predicate(lower_bound) + } + + #[inline(never)] + #[kanitool::fn_marker = "ExistsHook"] + pub fn kani_exists(lower_bound: T, upper_bound: T, predicate: F) -> bool + where + F: Fn(T) -> bool, + { + predicate(lower_bound) + } + #[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) + kani::kani_forall(lower_bound, upper_bound, predicate) }}; (|$i:ident | $predicate:expr) => {{ let predicate = |$i| $predicate; - kani_forall(usize::MIN, usize::MAX, predicate) + kani::kani_forall(usize::MIN, usize::MAX, predicate) }}; } @@ -227,32 +245,14 @@ macro_rules! kani_intrinsics { let lower_bound: usize = $lower_bound; let upper_bound: usize = $upper_bound; let predicate = |$i| $predicate; - kani_exists(lower_bound, upper_bound, predicate) + kani::kani_exists(lower_bound, upper_bound, predicate) }}; (|$i:ident | $predicate:expr) => {{ let predicate = |$i| $predicate; - kani_exists(usize::MIN, usize::MAX, predicate) + kani::kani_exists(usize::MIN, usize::MAX, predicate) }}; } - #[inline(never)] - #[kanitool::fn_marker = "ForallHook"] - pub fn kani_forall(lower_bound: T, upper_bound: T, predicate: F) -> bool - where - F: Fn(T) -> bool, - { - predicate(lower_bound) - } - - #[inline(never)] - #[kanitool::fn_marker = "ExistsHook"] - 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 cf0ad48dfd0d..9127834a4887 100644 --- a/rfc/src/rfcs/0010-quantifiers.md +++ b/rfc/src/rfcs/0010-quantifiers.md @@ -105,9 +105,6 @@ This, however, might unnecessary increase the complexity of the verification pro ```rust use std::mem; -extern crate kani; -use kani::{kani_forall, kani_exists}; - #[kani::proof] fn main() { let original_v = vec![kani::any::(); 3]; @@ -154,9 +151,6 @@ The same principle applies if we want to use the existential quantifier. ```rust use std::mem; -extern crate kani; -use kani::{kani_forall, kani_exists}; - #[kani::proof] fn main() { let original_v = vec![kani::any::(); 3]; @@ -206,6 +200,7 @@ The usage of quantifiers should be valid in any part of the Rust code analysed b Kani should have the same support that CBMC has for quantifiers. For more details, see [Quantifiers](https://github.com/diffblue/cbmc/blob/0a69a64e4481473d62496f9975730d24f194884a/doc/cprover-manual/contracts-quantifiers.md). The implementation of quantifiers in Kani will be based on the following principle: + - **Single expression without function calls**: CBMC's quantifiers only support single expressions without function calls. This means that the CBMC expressions generated from the quantifiers in Kani should be limited to a single expression without any @@ -226,8 +221,7 @@ To achieve this, we will need to implement the function inlining pass in Kani. T interface is familiar to developers, but the code generation is tricky, as CBMC level quantifiers only allow certain kinds of expressions. This necessitates a rewrite of the `Fn` closure to a compliant expression. - - Which kind of expressions should be accepted as a "compliant expression"? - + - Which kind of expressions should be accepted as a "compliant expression"? ## Future possibilities diff --git a/tests/expected/quantifiers/assert_with_exists_fail.rs b/tests/expected/quantifiers/assert_with_exists_fail.rs index 71b3a5df3728..3e2c6cdb3781 100644 --- a/tests/expected/quantifiers/assert_with_exists_fail.rs +++ b/tests/expected/quantifiers/assert_with_exists_fail.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern crate kani; -use kani::kani_exists; - #[kani::proof] fn exists_assert_harness() { let j = kani::any(); diff --git a/tests/expected/quantifiers/assert_with_exists_pass.rs b/tests/expected/quantifiers/assert_with_exists_pass.rs index cb79ea26fb30..7d43d6117729 100644 --- a/tests/expected/quantifiers/assert_with_exists_pass.rs +++ b/tests/expected/quantifiers/assert_with_exists_pass.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern crate kani; -use kani::kani_exists; - #[kani::proof] fn exists_assert_harness() { let j = kani::any(); diff --git a/tests/expected/quantifiers/assert_with_forall_fail.rs b/tests/expected/quantifiers/assert_with_forall_fail.rs index 279cba423fbe..c9bb7bbf62dd 100644 --- a/tests/expected/quantifiers/assert_with_forall_fail.rs +++ b/tests/expected/quantifiers/assert_with_forall_fail.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern crate kani; -use kani::kani_forall; - #[kani::proof] fn forall_assert_harness() { let j = kani::any(); diff --git a/tests/expected/quantifiers/assert_with_forall_pass.rs b/tests/expected/quantifiers/assert_with_forall_pass.rs index 62a4e031f3a6..5ebf73e7c0ee 100644 --- a/tests/expected/quantifiers/assert_with_forall_pass.rs +++ b/tests/expected/quantifiers/assert_with_forall_pass.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern crate kani; -use kani::kani_forall; - #[kani::proof] fn forall_assert_harness() { let j = kani::any(); diff --git a/tests/expected/quantifiers/assume_with_exists_fail.rs b/tests/expected/quantifiers/assume_with_exists_fail.rs index c591e1ed8626..f6df36a6942d 100644 --- a/tests/expected/quantifiers/assume_with_exists_fail.rs +++ b/tests/expected/quantifiers/assume_with_exists_fail.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern crate kani; -use kani::kani_exists; - #[kani::proof] fn exists_assume_harness() { let j = kani::any(); diff --git a/tests/expected/quantifiers/contracts_fail.rs b/tests/expected/quantifiers/contracts_fail.rs index 13b16f513fc6..a1b87ebc8633 100644 --- a/tests/expected/quantifiers/contracts_fail.rs +++ b/tests/expected/quantifiers/contracts_fail.rs @@ -2,9 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -extern crate kani; -use kani::kani_forall; - /// Copy only first 7 elements and left the last one unchanged. #[kani::ensures(|ret| { unsafe{ let ptr_x = xs.as_ptr(); diff --git a/tests/kani/Quantifiers/array.rs b/tests/kani/Quantifiers/array.rs index 1a127ab78888..b59eccd614fb 100644 --- a/tests/kani/Quantifiers/array.rs +++ b/tests/kani/Quantifiers/array.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern crate kani; -use kani::kani_forall; - #[kani::proof] fn vec_assert_forall_harness() { let v = vec![10 as u8; 128]; diff --git a/tests/kani/Quantifiers/contracts.rs b/tests/kani/Quantifiers/contracts.rs index fc2da350892e..d8e36c194774 100644 --- a/tests/kani/Quantifiers/contracts.rs +++ b/tests/kani/Quantifiers/contracts.rs @@ -2,9 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -extern crate kani; -use kani::kani_forall; - #[kani::requires(i==0)] #[kani::ensures(|ret| { unsafe{ diff --git a/tests/kani/Quantifiers/even.rs b/tests/kani/Quantifiers/even.rs index 32b554d77162..e7f74440d85a 100644 --- a/tests/kani/Quantifiers/even.rs +++ b/tests/kani/Quantifiers/even.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern crate kani; -use kani::kani_exists; - #[kani::proof] fn quantifier_even_harness() { let j: usize = kani::any(); diff --git a/tests/kani/Quantifiers/from_raw_part_fixme.rs b/tests/kani/Quantifiers/from_raw_part_fixme.rs index 1310f411e23a..2f06161847bf 100644 --- a/tests/kani/Quantifiers/from_raw_part_fixme.rs +++ b/tests/kani/Quantifiers/from_raw_part_fixme.rs @@ -5,9 +5,6 @@ use std::mem; -extern crate kani; -use kani::{kani_exists, kani_forall}; - #[kani::proof] fn main() { let original_v = vec![kani::any::(); 3]; diff --git a/tests/kani/Quantifiers/no_array.rs b/tests/kani/Quantifiers/no_array.rs index bebd5044c7fa..9681e4ccf0fa 100644 --- a/tests/kani/Quantifiers/no_array.rs +++ b/tests/kani/Quantifiers/no_array.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -extern crate kani; -use kani::{kani_exists, kani_forall}; - #[kani::proof] fn forall_assert_harness() { let j = kani::any(); From 445b80922a8489a59f329125483e5cd668c8bbc5 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 7 May 2025 16:33:55 +0000 Subject: [PATCH 27/27] Make quantifier functions hidden --- library/kani_core/src/lib.rs | 44 ++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 755f6960e955..b0c27436227f 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -207,35 +207,17 @@ macro_rules! kani_intrinsics { assert!(cond, "{}", msg); } - #[inline(never)] - #[kanitool::fn_marker = "ForallHook"] - pub fn kani_forall(lower_bound: T, upper_bound: T, predicate: F) -> bool - where - F: Fn(T) -> bool, - { - predicate(lower_bound) - } - - #[inline(never)] - #[kanitool::fn_marker = "ExistsHook"] - pub fn kani_exists(lower_bound: T, upper_bound: T, predicate: F) -> bool - where - F: Fn(T) -> bool, - { - predicate(lower_bound) - } - #[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::kani_forall(lower_bound, upper_bound, predicate) + kani::internal::kani_forall(lower_bound, upper_bound, predicate) }}; (|$i:ident | $predicate:expr) => {{ let predicate = |$i| $predicate; - kani::kani_forall(usize::MIN, usize::MAX, predicate) + kani::internal::kani_forall(usize::MIN, usize::MAX, predicate) }}; } @@ -245,11 +227,11 @@ macro_rules! kani_intrinsics { let lower_bound: usize = $lower_bound; let upper_bound: usize = $upper_bound; let predicate = |$i| $predicate; - kani::kani_exists(lower_bound, upper_bound, predicate) + kani::internal::kani_exists(lower_bound, upper_bound, predicate) }}; (|$i:ident | $predicate:expr) => {{ let predicate = |$i| $predicate; - kani::kani_exists(usize::MIN, usize::MAX, predicate) + kani::internal::kani_exists(usize::MIN, usize::MAX, predicate) }}; } @@ -657,6 +639,24 @@ macro_rules! kani_intrinsics { pub(crate) const fn check(cond: bool, msg: &'static str) { assert!(cond, "{}", msg); } + + #[inline(never)] + #[kanitool::fn_marker = "ForallHook"] + pub fn kani_forall(lower_bound: T, upper_bound: T, predicate: F) -> bool + where + F: Fn(T) -> bool, + { + predicate(lower_bound) + } + + #[inline(never)] + #[kanitool::fn_marker = "ExistsHook"] + pub fn kani_exists(lower_bound: T, upper_bound: T, predicate: F) -> bool + where + F: Fn(T) -> bool, + { + predicate(lower_bound) + } } }; }