Add support for quantifiers

cprover_bindings/src/goto_program/expr.rs

@@ -177,6 +177,14 @@ pub enum ExprValue {
     Vector {
         elems: Vec<Expr>,
     },
+    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

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![],
+            },
         }
     }
 }

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::{BuiltinFn, Expr, Stmt, Type};
+use cbmc::goto_program::Symbol as GotoSymbol;
+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::ClosureKind;
 use stable_mir::ty::RigidTy;
 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,131 @@ impl GotocHook for LoopInvariantRegister {
     }
 }
 
+struct Forall;
+struct Exists;
+
+#[derive(Debug, Clone, Copy)]
+enum QuantifierKind {
+    ForAll,
+    Exists,
+}
+
+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<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        handle_quantifier(gcx, instance, fargs, assign_to, target, span, QuantifierKind::ForAll)
+    }
+}
+
+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<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        handle_quantifier(gcx, instance, fargs, assign_to, target, span, QuantifierKind::Exists)
+    }
+}
+
+fn handle_quantifier(
+    gcx: &mut GotocCtx,
+    instance: Instance,
+    fargs: Vec<Expr>,
+    assign_to: &Place,
+    target: Option<BasicBlockIdx>,
+    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,
+    )
+}
+
+fn find_closure_call_expr(instance: &Instance, gcx: &mut GotocCtx, loc: Location) -> Option<Expr> {
+    for arg in instance.args().0.iter() {
+        let arg_ty = arg.ty()?;
+        let kind = arg_ty.kind();
+        let arg_kind = kind.rigid()?;
+
+        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 {
     let kani_lib_hooks = [
         (KaniHook::Assert, Rc::new(Assert) as Rc<dyn GotocHook>),
         (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)),

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,

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<T, F>(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<T, F>(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:

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,19 +24,18 @@ 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(|<var>: <type> [is <range-expr>] | <boolean-expression>)
-kani::forall(|<var>: <type> [is <range-expr>] | <boolean-expression>)
+kani::exists(|<var>: <type> [in (<range-expr>)] | <boolean-expression>)
+kani::forall(|<var>: <type> [in (<range-expr>)] | <boolean-expression>)
 ```
 
 If `<range-expr>` is not provided, we assume `<var>` can range over all possible values of the given `<type>` (i.e., syntactic sugar for full range `|<var>: <type> 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, `<boolean-expression>` should not have side effects, as the purpose of quantifiers is to assert a condition over a domain of objects without altering the state.
 
 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::<usize>(); 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,22 +132,25 @@ 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));
     }
 }
 ```
 
 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::<usize>(); 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));
     }
 }
 ```

tests/expected/quantifiers/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL