Add support for quantifiers (#3993)

This PR add support for quantifiers. Especially, we inline function
calls in quantified expressions so that the result statement-expression
can be accepted by the CBMC backend.

RFC: [RFC
0010-quantifiers](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0010-quantifiers.md).

Resolves #2546 and
#836.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>

Author: 3 people

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/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) {

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<InternedString, Symbol>,
+    parameters_map: BTreeMap<InternedString, Vec<InternedString>>,
     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<T: Into<InternedString>, P: Into<InternedString>>(
+        &mut self,
+        function_name: T,
+        parameter: P,
+    ) {
+        let function_name = function_name.into();
+        let parameter = parameter.into();
+
+        self.parameters_map.entry(function_name).or_default().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<F: FnOnce(Option<&Symbol>) -> 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<T: Into<InternedString>>(&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<T: Into<InternedString>>(
+        &self,
+        name: T,
+    ) -> Option<&Vec<InternedString>> {
+        let name = name.into();
+        self.parameters_map.get(&name)
+    }
+
     pub fn machine_model(&self) -> &MachineModel {
         &self.machine_model
     }

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

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)

docs/src/reference/experimental/quantifiers.md

@@ -0,0 +1,56 @@
+# 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
+#[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
+#[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
+
+#[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.

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,23 @@ 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);
 
+            // 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);
+            }
+
             // 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 +75,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]));

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -199,6 +199,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;