Merge pull request #6012 from ArenBabikian/loop-quantifiers-temp

Allow quantifiers within loop invariants

Author: SaswatPadhi

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.