Supports nested quantifiers in function contracts

regression/contracts/quantifiers-nested-01/main.c

@@ -0,0 +1,24 @@
+// clang-format off
+int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  __CPROVER_forall
+  {
+    int j;
+    (0 <= i && i < 10 && i <= j && j < 10) ==> arr[i] <= arr[j]
+  }
+})
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}

regression/contracts/quantifiers-nested-01/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression
+nested within another forall expression.

regression/contracts/quantifiers-nested-02/main.c

@@ -0,0 +1,19 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
+  int i;
+  0 <= i && i < 9 ==> __CPROVER_forall
+  {
+    int j;
+    (i <= j && j < 10) ==> arr[i] <= arr[j]
+  }
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+  f1(arr);
+}

regression/contracts/quantifiers-nested-02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression
+nested within an implication.

regression/contracts/quantifiers-nested-03/main.c

@@ -0,0 +1,19 @@
+int f1(int *arr)
+  __CPROVER_ensures(__CPROVER_return_value == 0 && __CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] == i
+  })
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}

regression/contracts/quantifiers-nested-03/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of an exists expression
+nested within a conjunction.

regression/contracts/quantifiers-nested-04/main.c

@@ -0,0 +1,21 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(
+  __CPROVER_forall {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == 0
+  } ||
+  arr[9] == -1 ||
+  __CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] == i
+  }) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+  f1(arr);
+}

regression/contracts/quantifiers-nested-04/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of both a forall expression
+and an exists expression nested within a disjunction.

regression/contracts/quantifiers-nested-05/main.c

@@ -0,0 +1,15 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(!__CPROVER_forall {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == 0
+  }) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+  f1(arr);
+}

regression/contracts/quantifiers-nested-05/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of a forall expression
+nested within a negation.

regression/contracts/quantifiers-nested-06/main.c

@@ -0,0 +1,27 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(
+  (__CPROVER_forall {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == 0
+  } ? __CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == 0
+  } : 1 == 0) &&
+  (__CPROVER_forall {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == i
+  } ? 1 == 0 :
+    __CPROVER_forall {
+      int i;
+      (0 <= i && i < 10) ==> arr[i] == 0
+  })) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
+  f1(arr);
+}

regression/contracts/quantifiers-nested-06/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test case checks the handling of forall and exists expressions
+nested within ternary ITE expressions (condition ? true : false).

src/goto-instrument/code_contracts.cpp

@@ -26,6 +26,7 @@ Date: February 2016
 #include <util/expr_util.h>
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
+#include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
@@ -168,35 +169,68 @@ void code_contractst::add_quantified_variable(
   replace_symbolt &replace,
   irep_idt mode)
 {
-  // If the expression is a quantified expression, this function adds
-  // the quantified variable to the symbol table and to the expression map
-
-  // TODO Currently only works if the contract contains only a single
-  // quantified formula
-  // i.e. (1) the top-level element is a quantifier formula
-  // and (2) there are no inner quantifier formulae
-  // This TODO is handled in PR #5968
-
-  if(expression.id() == ID_exists || expression.id() == ID_forall)
-  {
-    // get quantified symbol
-    exprt tuple = expression.operands().front();
-    exprt quantified_variable = tuple.operands().front();
-    symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
-
-    // create fresh symbol
-    symbolt new_symbol = get_fresh_aux_symbol(
-      quantified_symbol.type(),
-      id2string(quantified_symbol.get_identifier()),
-      "tmp",
-      quantified_symbol.source_location(),
-      mode,
-      symbol_table);
-
-    // add created fresh symbol to expression map
-    symbol_exprt q(
-      quantified_symbol.get_identifier(), quantified_symbol.type());
-    replace.insert(q, new_symbol.symbol_expr());
+  if(expression.id() == ID_not || expression.id() == ID_typecast)
+  {
+    // For unary connectives, recursively check for
+    // nested quantified formulae in the term
+    const auto &unary_expression = to_unary_expr(expression);
+    add_quantified_variable(unary_expression.op(), replace, mode);
+  }
+  if(expression.id() == ID_notequal || expression.id() == ID_implies)
+  {
+    // For binary connectives, recursively check for
+    // nested quantified formulae in the left and right terms
+    const auto &binary_expression = to_binary_expr(expression);
+    add_quantified_variable(binary_expression.lhs(), replace, mode);
+    add_quantified_variable(binary_expression.rhs(), replace, mode);
+  }
+  if(expression.id() == ID_if)
+  {
+    // For ternary connectives, recursively check for
+    // nested quantified formulae in all three terms
+    const auto &if_expression = to_if_expr(expression);
+    add_quantified_variable(if_expression.cond(), replace, mode);
+    add_quantified_variable(if_expression.true_case(), replace, mode);
+    add_quantified_variable(if_expression.false_case(), replace, mode);
+  }
+  if(expression.id() == ID_and || expression.id() == ID_or)
+  {
+    // For multi-ary connectives, recursively check for
+    // nested quantified formulae in all terms
+    const auto &multi_ary_expression = to_multi_ary_expr(expression);
+    for(const auto &operand : multi_ary_expression.operands())
+    {
+      add_quantified_variable(operand, replace, mode);
+    }
+  }
+  else if(expression.id() == ID_exists || expression.id() == ID_forall)
+  {
+    // When a quantifier expression is found,
+    // 1. get quantified variables
+    const auto &quantifier_expression = to_quantifier_expr(expression);
+    const auto &quantified_variables = quantifier_expression.variables();
+    for(const auto &quantified_variable : quantified_variables)
+    {
+      // for each quantified variable...
+      const auto &quantified_symbol = to_symbol_expr(quantified_variable);
+
+      // 1.1 create fresh symbol
+      symbolt new_symbol = get_fresh_aux_symbol(
+        quantified_symbol.type(),
+        id2string(quantified_symbol.get_identifier()),
+        "tmp",
+        quantified_symbol.source_location(),
+        mode,
+        symbol_table);
+
+      // 1.2 add created fresh symbol to expression map
+      symbol_exprt q(
+        quantified_symbol.get_identifier(), quantified_symbol.type());
+      replace.insert(q, new_symbol.symbol_expr());
+
+      // 1.3 recursively check for nested quantified formulae
+      add_quantified_variable(quantifier_expression.where(), replace, mode);
+    }
   }
 }
 

src/goto-instrument/code_contracts.h

@@ -167,8 +167,10 @@ class code_contractst
   void
   add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);
 
-  /// If the expression is a quantified expression, this function adds
-  /// the quantified variable to the symbol table and to the expression map
+  /// This function recursively searches the expression to find nested or
+  /// non-nested quantified expressions. When a quantified expression is found,
+  /// the quantified variable is added to the symbol table
+  /// and to the expression map.
   void add_quantified_variable(
     exprt expression,
     replace_symbolt &replace,