Add support for nested quantifiers in function contracts

This adds support for nested quantifiers in funtion contracts.
We recusrively handle quantifiers that are nested within other
quantifiers or within and/or/implies statements.

Author: ArenBabikian

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,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test asserts the postconditions of f1.

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,10 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test asserts the preconditions of f1.

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,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test asserts the postconditions of f1.

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,10 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+This test asserts the postconditions of f1.

src/goto-instrument/code_contracts.cpp

@@ -168,23 +168,29 @@ 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();
+  // 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.
+  if(
+    expression.id() == ID_and || expression.id() == ID_or ||
+    expression.id() == ID_implies)
+  {
+    // For binary connectives, recursively check for
+    // nested quantified formulae in the left and right terms
+    exprt left = expression.operands().at(0);
+    add_quantified_variable(left, replace, mode);
+    exprt right = expression.operands().at(1);
+    add_quantified_variable(right, replace, mode);
+  }
+  else if(expression.id() == ID_exists || expression.id() == ID_forall)
+  {
+    // When a quantified expression is found,
+    // 1. get quantified symbol
+    exprt tuple = expression.operands().at(0);
+    exprt quantified_variable = tuple.operands().at(0);
     symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
 
-    // create fresh symbol
+    // 2. create fresh symbol
     symbolt new_symbol = get_fresh_aux_symbol(
       quantified_symbol.type(),
       id2string(quantified_symbol.get_identifier()),
@@ -193,10 +199,14 @@ void code_contractst::add_quantified_variable(
       mode,
       symbol_table);
 
-    // add created fresh symbol to expression map
+    // 3. add created fresh symbol to expression map
     symbol_exprt q(
       quantified_symbol.get_identifier(), quantified_symbol.type());
     replace.insert(q, new_symbol.symbol_expr());
+
+    // 4. recursively check for nested quantified formulae
+    exprt quantified_expression = expression.operands().at(1);
+    add_quantified_variable(quantified_expression, replace, mode);
   }
 }
 

src/goto-instrument/code_contracts.h

@@ -167,8 +167,9 @@ 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,