Add support for quantifiers in loop contracts

Author: ArenBabikian

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

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+#define N 16
+
+void main()
+{
+  int a[N];
+  a[10] = 0;
+
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant(
+      (0 <= i) && (i <= N) &&
+      __CPROVER_forall {
+        int k;
+        // constant bounds for explicit unrolling with SAT backend
+        (0 <= k && k <= N) ==> (
+          // the actual symbolic bound for `k`
+          k < i ==> a[k] == 1
+        )
+      }
+    )
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+
+  assert(a[10] == 1);
+}

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

@@ -0,0 +1,15 @@
+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
+^\[main.assertion.1\] line .* assertion a\[10\] == 1: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test case checks the handling of a `forall` quantifier within a loop invariant.
+
+This test case uses explicit constant bounds on the quantified variable,
+so that it can be unrolled (to conjunctions) with the SAT backend.

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,21 @@
+KNOWNBUG 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 .*: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test case checks the handling of a universal 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.
+
+It has been tagged `KNOWNBUG` for now since `contracts` regression tests are not run with SMT backend yet.

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

@@ -0,0 +1,42 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define MAX_SIZE 64
+
+void main()
+{
+  unsigned N;
+  __CPROVER_assume(N <= MAX_SIZE);
+
+  int *a = malloc(N * sizeof(int));
+
+  for(int i = 0; i < N; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant(
+      (0 <= i) && (i <= N) &&
+      (i != 0 ==> __CPROVER_exists {
+        int k;
+        // constant bounds for explicit unrolling with SAT backend
+        (0 <= k && k <= MAX_SIZE) && (
+          // the actual symbolic bound for `k`
+          k < i && a[k] == 1
+        )
+      })
+    )
+    // clang-format on
+    {
+      a[i] = 1;
+    }
+
+  // clang-format off
+  assert(
+    N != 0 ==> __CPROVER_exists {
+    int k;
+    // constant bounds for explicit unrolling with SAT backend
+    (0 <= k && k <= MAX_SIZE) && (
+      // the actual symbolic bound for `k`
+      k < N && a[k] == 1
+    )
+  });
+  // clang-format on
+}

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

@@ -0,0 +1,16 @@
+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
+^\[main.assertion.1\] line .* assertion .*: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test case checks the handling of an existential quantifier, with a symbolic
+upper bound, within a loop invariant.
+
+This test case uses explicit constant bounds on the quantified variable,
+so that it can be unrolled (to conjunctions) with the SAT backend.

src/goto-instrument/code_contracts.cpp

@@ -114,9 +114,21 @@ void code_contractst::check_apply_invariants(
   // build the havocking code
   goto_programt havoc_code;
 
-  // assert the invariant
-  {
-    code_assertt assertion{invariant};
+  // 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;
+  };
+
+  // Generate: assert(invariant) just before the loop
+  // We use a block scope to create a temporary assertion,
+  // and immediately convert it to goto instructions.
+  {
+    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(
@@ -126,10 +138,14 @@ void code_contractst::check_apply_invariants(
   // havoc variables being written to
   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);
+  // Generate: assume(invariant) just after havocing
+  // We use a block scope to create a temporary assumption,
+  // and immediately convert it to goto instructions.
+  {
+    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())
@@ -143,9 +159,11 @@ void code_contractst::check_apply_invariants(
   // Use insert_before_swap to preserve jumps to loop head.
   goto_function.body.insert_before_swap(loop_head, havoc_code);
 
-  // assert the invariant at the end of the loop body
+  // Generate: assert(invariant) just after the loop exits
+  // We use a block scope to create a temporary assertion,
+  // and immediately convert it to goto instructions.
   {
-    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(