Add support for nested quantifiers in function contracts

This adds support for nested quantifiers in funtion contracts.
We recursively handle quantifiers that are nested within other
quantifiers or within Boolean connectives.

f

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,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,11 +26,13 @@ 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>
 #include <util/pointer_predicates.h>
 #include <util/replace_symbol.h>
+#include <util/std_expr.h>
 
 #include "loop_utils.h"
 
@@ -168,35 +170,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,