Migrate loop contracts regressions to dfcc

Author: qinheping

regression/contracts-dfcc/github_6168_infinite_unwinding_bug/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+static int adder(const int *a, const int *b)
+{
+  return (*a + *b);
+}
+
+int main()
+{
+  int x = 1024;
+
+  int (*local_adder)(const int *, const int *) = adder;
+
+  while(x > 0)
+    __CPROVER_loop_invariant(1 == 1)
+    {
+      x += local_adder(&x, &x); // loop detection fails
+      //x += adder(&x, &x);       // works fine
+    }
+}

regression/contracts-dfcc/github_6168_infinite_unwinding_bug/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^\[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
+--
+--
+This is guarding against an issue described in https://github.com/diffblue/cbmc/issues/6168.

regression/contracts-dfcc/history-index/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int i, n, x[10];
+  __CPROVER_assume(x[0] == x[9]);
+  while(i < n)
+    __CPROVER_loop_invariant(x[0] == __CPROVER_loop_entry(x[0]))
+    {
+      x[0] = x[9] - 1;
+      x[0]++;
+    }
+  assert(x[0] == x[9]);
+}

regression/contracts-dfcc/history-index/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Tracking history of index expressions is not supported yet\.
+--
+This test checks that `ID_index` expressions are allowed within history variables.

regression/contracts-dfcc/history-invalid/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int foo(int x)
+{
+  return x;
+}
+
+int main()
+{
+  int i, n, x[10];
+  __CPROVER_assume(x[0] == x[9]);
+  while(i < n)
+    __CPROVER_loop_invariant(x[0] == __CPROVER_loop_entry(foo(x[0])))
+    {
+      x[0] = x[9] - 1;
+      x[0]++;
+    }
+  assert(x[0] == x[9]);
+}

regression/contracts-dfcc/history-invalid/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--dfcc --apply-loop-contracts
+^main.c.* error: Tracking history of side_effect expressions is not supported yet.$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test ensures that expressions with side effect, such as function calls,
+may not be used in history variables.

regression/contracts-dfcc/invar_assigns_empty/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main()
+{
+  while(1 == 1)
+    __CPROVER_assigns() __CPROVER_loop_invariant(1 == 1)
+    {
+    }
+}

regression/contracts-dfcc/invar_assigns_empty/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that empty assigns clause is supported 
+in loop contracts.

regression/contracts-dfcc/invar_check_break_fail/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+    {
+      --r;
+      if(r <= 1)
+      {
+        break;
+      }
+      else
+      {
+        --r;
+      }
+    }
+
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts-dfcc/invar_check_break_fail/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+This test is expected to fail along the code path where r is an even integer
+before entering the loop.
+The program is simply incompatible with the desired property in this case --
+there is no loop invariant that can establish the required assertion.

regression/contracts-dfcc/invar_check_break_pass/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    // clang-format off
+    __CPROVER_loop_invariant(r >= 0)
+    __CPROVER_decreases(r)
+    // clang-format on
+    {
+      --r;
+      if(r <= 1)
+      {
+        break;
+      }
+      else
+      {
+        --r;
+      }
+    }
+
+  assert(r == 0 || r == 1);
+
+  return 0;
+}

regression/contracts-dfcc/invar_check_break_pass/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that conditionals and `break` are correctly handled.

regression/contracts-dfcc/invar_check_continue/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    // clang-format off
+    __CPROVER_loop_invariant(r >= 0)
+    __CPROVER_decreases(r)
+    // clang-format on
+    {
+      --r;
+      if(r < 5)
+      {
+        continue;
+      }
+      else
+      {
+        --r;
+      }
+    }
+
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts-dfcc/invar_check_continue/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that conditionals and `continue` are correctly handled.

regression/contracts-dfcc/invar_check_large/main.c

@@ -0,0 +1,98 @@
+#include <assert.h>
+
+void swap(int *a, int *b)
+{
+  *a ^= *b;
+  *b ^= *a;
+  *a ^= *b;
+}
+
+int main()
+{
+  int arr0, arr1, arr2, arr3, arr4;
+  arr0 = 1;
+  arr1 = 2;
+  arr2 = 0;
+  arr3 = 4;
+  arr4 = 3;
+  int *arr[5] = {&arr0, &arr1, &arr2, &arr3, &arr4};
+  int pivot = 2;
+
+  int h = 5 - 1;
+  int l = 0;
+  int r = 1;
+  while(h > l)
+    // clang-format off
+    __CPROVER_assigns(arr0, arr1, arr2, arr3, arr4, h, l, r)
+    __CPROVER_loop_invariant(
+      // Turn off `clang-format` because it breaks the `==>` operator.
+      h >= l &&
+      0 <= l && l < 5 &&
+      0 <= h && h < 5 &&
+      l <= r && r <= h &&
+      (r == 0 ==> arr0 == pivot) &&
+      (r == 1 ==> arr1 == pivot) &&
+      (r == 2 ==> arr2 == pivot) &&
+      (r == 3 ==> arr3 == pivot) &&
+      (r == 4 ==> arr4 == pivot) &&
+      (0 < l ==> arr0 <= pivot) &&
+      (1 < l ==> arr1 <= pivot) &&
+      (2 < l ==> arr2 <= pivot) &&
+      (3 < l ==> arr3 <= pivot) &&
+      (4 < l ==> arr4 <= pivot) &&
+      (0 > h ==> arr0 >= pivot) &&
+      (1 > h ==> arr1 >= pivot) &&
+      (2 > h ==> arr2 >= pivot) &&
+      (3 > h ==> arr3 >= pivot) &&
+      (4 > h ==> arr4 >= pivot)
+    )
+    __CPROVER_decreases(h - l)
+    // clang-format on
+    {
+      if(*(arr[h]) <= pivot && *(arr[l]) >= pivot)
+      {
+        swap(arr[h], arr[l]);
+        if(r == h)
+        {
+          r = l;
+          h--;
+        }
+        else if(r == l)
+        {
+          r = h;
+          l++;
+        }
+        else
+        {
+          h--;
+          l++;
+        }
+      }
+      else if(*(arr[h]) <= pivot)
+      {
+        l++;
+      }
+      else
+      {
+        h--;
+      }
+    }
+
+  // Turn off `clang-format` because it breaks the `==>` operator.
+  /* clang-format off */
+  assert(0 <= r && r < 5);
+  assert(*(arr[r]) == pivot);
+  assert(0 < r ==> arr0 <= pivot);
+  assert(1 < r ==> arr1 <= pivot);
+  assert(2 < r ==> arr2 <= pivot);
+  assert(3 < r ==> arr3 <= pivot);
+  assert(4 < r ==> arr4 <= pivot);
+  assert(0 > r ==> arr0 >= pivot);
+  assert(1 > r ==> arr1 >= pivot);
+  assert(2 > r ==> arr2 >= pivot);
+  assert(3 > r ==> arr3 >= pivot);
+  assert(4 > r ==> arr4 >= pivot);
+  /* clang-format on */
+
+  return r;
+}

regression/contracts-dfcc/invar_check_large/test.desc

@@ -0,0 +1,25 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion 0 <= r && r < 5: SUCCESS$
+^\[main.assertion.2\] .* assertion \*\(arr\[r\]\) == pivot: SUCCESS$
+^\[main.assertion.3\] .* assertion 0 < r ==> arr0 <= pivot: SUCCESS$
+^\[main.assertion.4\] .* assertion 1 < r ==> arr1 <= pivot: SUCCESS$
+^\[main.assertion.5\] .* assertion 2 < r ==> arr2 <= pivot: SUCCESS$
+^\[main.assertion.6\] .* assertion 3 < r ==> arr3 <= pivot: SUCCESS$
+^\[main.assertion.7\] .* assertion 4 < r ==> arr4 <= pivot: SUCCESS$
+^\[main.assertion.8\] .* assertion 0 > r ==> arr0 >= pivot: SUCCESS$
+^\[main.assertion.9\] .* assertion 1 > r ==> arr1 >= pivot: SUCCESS$
+^\[main.assertion.10\] .* assertion 2 > r ==> arr2 >= pivot: SUCCESS$
+^\[main.assertion.11\] .* assertion 3 > r ==> arr3 >= pivot: SUCCESS$
+^\[main.assertion.12\] .* assertion 4 > r ==> arr4 >= pivot: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks the invariant contracts on a larger problem --- in this case,
+the partition function of quicksort, applied to a fixed-length array.
+This serves as a stop-gap test until issues to do with quantifiers and
+side-effects in loop invariants are fixed.

regression/contracts-dfcc/invar_check_multiple_loops/main.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+int main()
+{
+  int r, n, x, y;
+  __CPROVER_assume(n > 0 && x == y);
+
+  for(r = 0; r < n; ++r)
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= r && r <= n)
+    __CPROVER_loop_invariant(x == y + r)
+    __CPROVER_decreases(n - r)
+    // clang-format on
+    {
+      x++;
+    }
+  while(r > 0)
+    // clang-format off
+    __CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r))
+    __CPROVER_decreases(r)
+    // clang-format on
+    {
+      y--;
+      r--;
+    }
+
+  assert(x == y + 2 * n);
+
+  return 0;
+}