Add support for quantifiers

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

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.
@@ -968,6 +976,12 @@ 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!(typ.is_c_bool());
+        assert!(variable.is_symbol());
+        expr!(Forall { variable, domain }, typ)
+    }
 }
 
 /// Constructors for Binary Operations

cprover_bindings/src/goto_program/stmt.rs

@@ -261,6 +261,13 @@ impl Stmt {
         stmt!(Expression(e), loc)
     }
 
+    ///
+    /*pub fn quantifiers(init: Stmt, range: Expr, predicate: Expr, loc: Location) -> Self {
+        assert!(range.typ().is_bool());
+        assert!(range.typ().is_bool());
+        stmt!()
+    }*/
+
     // `for (init; cond; update) {body}`
     pub fn for_loop(init: Stmt, cond: Expr, update: Stmt, body: Stmt, loc: Location) -> Self {
         assert!(cond.typ().is_bool());

cprover_bindings/src/irep/to_irep.rs

@@ -379,6 +379,30 @@ impl ToIrep for ExprValue {
                 sub: elems.iter().map(|x| x.to_irep(mm)).collect(),
                 named_sub: linear_map![],
             },
+            ExprValue::Forall { variable, domain } => Irep {
+                id: IrepId::Forall,
+                sub: vec![
+                    Irep {
+                        id: IrepId::Tuple,
+                        sub: vec![variable.to_irep(mm)],
+                        named_sub: linear_map![],
+                    },
+                    domain.to_irep(mm),
+                ],
+                named_sub: linear_map![],
+            },
+            ExprValue::Exists { variable, domain } => Irep {
+                id: IrepId::Exists,
+                sub: vec![
+                    Irep {
+                        id: IrepId::Tuple,
+                        sub: vec![variable.to_irep(mm)],
+                        named_sub: linear_map![],
+                    },
+                    domain.to_irep(mm),
+                ],
+                named_sub: linear_map![],
+            },
         }
     }
 }

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -14,16 +14,22 @@ use crate::kani_middle::attributes;
 use crate::kani_middle::kani_functions::{KaniFunction, KaniHook};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::CIntType;
+use cbmc::goto_program::Symbol as GotoSymbol;
 use cbmc::goto_program::{BuiltinFn, Expr, Stmt, Type};
+use rustc_ast::Closure;
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Place};
+use stable_mir::ty::RigidTy;
+use stable_mir::ty::{ClosureKind, TyKind};
 use stable_mir::{CrateDef, ty::Span};
 use std::collections::HashMap;
 use std::rc::Rc;
 use tracing::debug;
 
+use cbmc::goto_program::ExprValue;
+
 pub trait GotocHook {
     /// if the hook applies, it means the codegen would do something special to it
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool;
@@ -649,6 +655,206 @@ impl GotocHook for LoopInvariantRegister {
     }
 }
 
+struct Forall;
+
+/// __CROVER_forall
+impl GotocHook for Forall {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniExists")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        instance: Instance,
+        fargs: Vec<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        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<Expr> = 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_forall
+impl GotocHook for Exists {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniExists")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        instance: Instance,
+        fargs: Vec<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        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<Expr> = 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)
+        }
+    }
+}
+
 pub fn fn_hooks() -> GotocHooks {
     let kani_lib_hooks = [
         (KaniHook::Assert, Rc::new(Assert) as Rc<dyn GotocHook>),
@@ -671,6 +877,8 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(LoopInvariantRegister),
+            Rc::new(Forall),
+            Rc::new(Exists),
         ],
     }
 }

kani-compiler/src/kani_middle/transform/quantifiers.rs

@@ -0,0 +1,75 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains code related to the MIR-to-MIR pass that performs the
+//! stubbing of functions and methods.
+use crate::kani_middle::codegen_units::Stubs;
+use crate::kani_middle::stubbing::{contract_host_param, validate_stub_const};
+use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody};
+use crate::kani_middle::transform::{TransformPass, TransformationType};
+use crate::kani_queries::QueryDb;
+use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::visit::{Location, MirVisitor};
+use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind};
+use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
+use stable_mir::CrateDef;
+use std::collections::HashMap;
+use std::fmt::Debug;
+use tracing::{debug, trace};
+use crate::kani_middle::find_fn_def;
+
+/// Replace the body of a function that is stubbed by the other.
+///
+/// This pass will replace the entire body, and it should only be applied to stubs
+/// that have a body.
+#[derive(Debug)]
+pub struct QuantifiersPass {
+    forall: Option<FnDef>,
+}
+
+impl TransformPass for QuantifiersPass {
+    fn transformation_type() -> TransformationType
+    where
+        Self: Sized,
+    {
+        TransformationType::Instrumentation
+    }
+
+    fn is_enabled(&self, query_db: &QueryDb) -> bool
+    where
+        Self: Sized,
+    {
+        true
+    }
+
+    /// Transform the function body by replacing it with the stub body.
+    fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+        trace!(function=?instance.name(), "transform");
+        println!("transform {:?}", self.forall);
+        /*let ty = instance.ty();
+        if let TyKind::RigidTy(RigidTy::FnDef(fn_def, mut args)) = ty.kind() {
+            if let Some(replace) = self.stubs.get(&fn_def) {
+                if let Some(idx) = contract_host_param(tcx, fn_def, *replace) {
+                    debug!(?idx, "FnStubPass::transform remove_host_param");
+                    args.0.remove(idx);
+                }
+                let new_instance = Instance::resolve(*replace, &args).unwrap();
+                debug!(from=?instance.name(), to=?new_instance.name(), "FnStubPass::transform");
+                if let Some(body) = FnStubValidator::validate(tcx, (fn_def, *replace), new_instance)
+                {
+                    return (true, body);
+                }
+            }
+        }*/
+        (false, body)
+    }
+}
+
+impl QuantifiersPass {
+    /// Build the pass with non-extern function stubs.
+    pub fn new(tcx: TyCtxt, ) -> QuantifiersPass {
+        let forall = find_fn_def(tcx, "KaniForall");
+        QuantifiersPass { forall }
+    }
+}