Add support for quantifiers in loop contracts

Author: ArenBabikian

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

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+void main()
+{
+  int N = 64, a[64];
+
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant(
+      (0 <= i) && (i <= N) &&
+      __CPROVER_forall {
+        int k;
+        (0 <= k && k < N) ==> 1 == 1
+      }
+    )
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+}

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

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] line .* Check loop invariant before entry: SUCCESS
+^\[main.2\] line .* Check that loop invariant is preserved: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test case checks the handling of a `forall` quantifier within a loop invariant.

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

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+void main()
+{
+  int N, a[64];
+  __CPROVER_assume(0 <= N && N < 64);
+
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant(
+      (0 <= i) && (i <= N) &&
+      __CPROVER_forall {
+        int k;
+        (0 <= k && k < i) ==> a[k] == 1
+      }
+    )
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+
+  // clang-format off
+  assert(__CPROVER_forall {
+    int k;
+    (0 <= k && k < N) ==> a[k] == 1
+  });
+  // clang-format on
+
+  int k;
+  __CPROVER_assume(0 <= k && k < N);
+  assert(a[k] == 1);
+}

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

@@ -0,0 +1,19 @@
+CORE --smt-backend --broken-cprover-smt-backend
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] line .* Check loop invariant before entry: SUCCESS
+^\[main.2\] line .* Check that loop invariant is preserved: SUCCESS
+^\[main.assertion.1\] line .* assertion __CPROVER_forall \{ int k; \(0 <= k && k < N\) ==> a\[k\] == 1 \}: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test case checks the handling of a `forall` quantifier, with a symbolic
+upper bound, within a loop invariant.
+
+The test is tagged:
+- `--smt-backend`:
+  because the SAT backend does not support (simply ignores) `forall` in negative (e.g. assume) contexts.
+- `--broken-cprover-smt-backend`:
+  because the CPROVER SMT2 solver cannot handle (errors out on) `forall` in negative (e.g. assume) contexts.

src/goto-instrument/code_contracts.cpp

@@ -114,9 +114,19 @@ void code_contractst::check_apply_invariants(
   // build the havocking code
   goto_programt havoc_code;
 
+  // process quantified variables correctly (introduce a fresh temporary)
+  // and return a copy of the invariant
+  const auto &invariant_expr = [&]() {
+    auto invariant_copy = invariant;
+    replace_symbolt replace;
+    code_contractst::add_quantified_variable(invariant_copy, replace, mode);
+    replace(invariant_copy);
+    return invariant_copy;
+  };
+
   // assert the invariant
   {
-    code_assertt assertion{invariant};
+    code_assertt assertion{invariant_expr()};
     assertion.add_source_location() = loop_head->source_location;
     converter.goto_convert(assertion, havoc_code, mode);
     havoc_code.instructions.back().source_location.set_comment(
@@ -127,9 +137,11 @@ void code_contractst::check_apply_invariants(
   build_havoc_code(loop_head, modifies, havoc_code);
 
   // assume the invariant
-  code_assumet assumption{invariant};
-  assumption.add_source_location() = loop_head->source_location;
-  converter.goto_convert(assumption, havoc_code, mode);
+  {
+    code_assumet assumption{invariant_expr()};
+    assumption.add_source_location() = loop_head->source_location;
+    converter.goto_convert(assumption, havoc_code, mode);
+  }
 
   // non-deterministically skip the loop if it is a do-while loop
   if(!loop_head->is_goto())
@@ -145,7 +157,7 @@ void code_contractst::check_apply_invariants(
 
   // assert the invariant at the end of the loop body
   {
-    code_assertt assertion{invariant};
+    code_assertt assertion{invariant_expr()};
     assertion.add_source_location() = loop_end->source_location;
     converter.goto_convert(assertion, havoc_code, mode);
     havoc_code.instructions.back().source_location.set_comment(
@@ -354,7 +366,7 @@ bool code_contractst::apply_function_contract(
 
   // Create a replace_symbolt object, for replacing expressions in the callee
   // with expressions from the call site (e.g. the return value).
-  // This object tracks replacements that are common to both ENSURES and REQUIRES.
+  // This object tracks replacements that are common to ENSURES and REQUIRES.
   replace_symbolt common_replace;
   if(type.return_type() != empty_typet())
   {