Fix bug: goto-cc crash when there are two quantifers in one proof (#4221)

This PR allows multiple quantifiers in the same harness.
Thanks @tautschnig for fixing the bug from CBMC side.

Resolves #4020

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

Author: thanhnguyen-aws

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -318,9 +318,11 @@ impl GotocCtx<'_> {
     pub fn handle_quantifiers(&mut self) {
         // Store the found quantifiers and the inlined results.
         let mut to_modify: BTreeMap<InternedString, SymbolValues> = BTreeMap::new();
+        let mut suffix_count: u16 = 0;
         for (key, symbol) in self.symbol_table.iter() {
             if let SymbolValues::Stmt(stmt) = &symbol.value {
-                let new_stmt_val = SymbolValues::Stmt(self.handle_quantifiers_in_stmt(stmt));
+                let new_stmt_val =
+                    SymbolValues::Stmt(self.handle_quantifiers_in_stmt(stmt, &mut suffix_count));
                 to_modify.insert(*key, new_stmt_val);
             }
         }
@@ -332,7 +334,7 @@ impl GotocCtx<'_> {
     }
 
     /// Find all quantifier expressions in `stmt` and recursively inline functions.
-    fn handle_quantifiers_in_stmt(&self, stmt: &Stmt) -> Stmt {
+    fn handle_quantifiers_in_stmt(&self, stmt: &Stmt, suffix_count: &mut u16) -> Stmt {
         match &stmt.body() {
             // According to the hook handling for quantifiers, quantifier expressions must be of form
             // lhs = typecast(qex, c_bool)
@@ -345,13 +347,13 @@ impl GotocCtx<'_> {
                             let mut visited_func_symbols: HashSet<InternedString> = 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 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,
+                                    suffix_count,
                                 )
                                 .unwrap(),
                                 *domain.location(),
@@ -406,11 +408,14 @@ impl GotocCtx<'_> {
             }
             // Recursively find quantifier expressions.
             StmtBody::Block(stmts) => Stmt::block(
-                stmts.iter().map(|stmt| self.handle_quantifiers_in_stmt(stmt)).collect(),
+                stmts
+                    .iter()
+                    .map(|stmt| self.handle_quantifiers_in_stmt(stmt, suffix_count))
+                    .collect(),
                 *stmt.location(),
             ),
             StmtBody::Label { label, body } => {
-                self.handle_quantifiers_in_stmt(body).with_label(*label)
+                self.handle_quantifiers_in_stmt(body, suffix_count).with_label(*label)
             }
             _ => stmt.clone(),
         }

tests/expected/quantifiers/multiple_quantifiers.expected

@@ -0,0 +1,6 @@
+main.assertion.2\
+	 - Status: SUCCESS\
+	 - Description: "assertion failed: kani::exists!(| i in (0, len) |\
+*rebuilt_ptr.wrapping_byte_offset(4*i as isize) == 0)"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/quantifiers/multiple_quantifiers.rs

@@ -0,0 +1,45 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
+
+/// Example of code using multiple quantifiers
+use std::mem;
+
+#[kani::proof]
+fn main() {
+    let original_v = vec![kani::any::<u32>(); 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)
+        );
+    }
+}

tests/expected/quantifiers/simple_four_quantifiers.expected

@@ -0,0 +1,19 @@
+main.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: quan1"
+
+main.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: quan2"
+
+main.assertion.3\
+         - Status: SUCCESS\
+         - Description: "assertion failed: quan3"
+
+
+main.assertion.4\
+         - Status: SUCCESS\
+         - Description: "assertion failed: quan4"
+
+VERIFICATION:- SUCCESSFUL
+

tests/expected/quantifiers/simple_four_quantifiers.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
+
+/// Example of code using multiple quantifiers
+
+#[kani::proof]
+fn main() {
+    let quan1 = kani::forall!(|i in (4, 100)| i < 1000);
+    let quan2 = kani::forall!(|i in (2, 6)| i < 7 );
+    let quan3 = kani::exists!(|i in (0, 10)| i == 8);
+    let quan4 = kani::exists!(|i in (0, 9)| i % 2 == 0);
+    assert!(quan1);
+    assert!(quan2);
+    assert!(quan3);
+    assert!(quan4);
+}