Merge pull request #5884 from padhi-aws-forks/loop_invariant_contract_fix

Enforce __CPROVER_loop_invariant contracts in goto-instrument

Author: feliperodri

regression/contracts/invar_check_01/main.c

@@ -1,7 +1,3 @@
-// invar_check_02
-
-// This test checks that loop invariants adequately handle continues.
-
 #include <assert.h>
 
 int main()
@@ -11,17 +7,17 @@ int main()
 
   while(r > 0)
     __CPROVER_loop_invariant(r >= 0)
-  { 
-    --r;
-    if (r < 5)
-    {
-      continue;
-    }
-    else
     {
       --r;
+      if(r <= 1)
+      {
+        break;
+      }
+      else
+      {
+        --r;
+      }
     }
-  }
 
   assert(r == 0);
 

regression/contracts/invar_check_01/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* 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/invar_check_02/test.desc

@@ -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 || r == 1);
+
+  return 0;
+}

regression/contracts/invar_check_03/test.desc

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

regression/contracts/invar_check_04/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 < 5)
+      {
+        continue;
+      }
+      else
+      {
+        --r;
+      }
+    }
+
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts/invar_check_04/test.desc

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

regression/contracts/invar_check_02/main.c renamed to regression/contracts/invar_check_break_fail/main.c

@@ -1,10 +1,3 @@
-// invar_check_03
-
-// This test checks the use of loop invariants on a larger problem --- in this
-// case, the partition portion 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.
-
 #include <assert.h>
 
 void swap(int *a, int *b)
@@ -15,13 +8,13 @@ void swap(int *a, int *b)
 }
 
 int main()
-{ 
+{
   int arr0, arr1, arr2, arr3, arr4;
   arr0 = 1;
   arr1 = 2;
   arr2 = 0;
   arr3 = 4;
-  arr4 = 3; 
+  arr4 = 3;
   int *arr[5] = {&arr0, &arr1, &arr2, &arr3, &arr4};
   int pivot = 2;
 
@@ -30,6 +23,8 @@ int main()
   int r = 1;
   while(h > l)
     __CPROVER_loop_invariant(
+      // Turn off `clang-format` because it breaks the `==>` operator.
+      /* clang-format off */
       h >= l &&
       0 <= l && l < 5 &&
       0 <= h && h < 5 &&
@@ -49,26 +44,35 @@ int main()
       (2 > h ==> arr2 >= pivot) &&
       (3 > h ==> arr3 >= pivot) &&
       (4 > h ==> arr4 >= pivot)
+      /* clang-format on */
     )
-  {
-    if(*(arr[h]) <= pivot && *(arr[l]) >= pivot) {
-      swap(arr[h], arr[l]);
-      if (r == h) {
-        r = l;
-        h--;
+    {
+      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 if(r == l) {
-        r = h;
+      else if(*(arr[h]) <= pivot)
+      {
         l++;
       }
+      else
+      {
+        h--;
+      }
     }
-    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);
@@ -81,5 +85,7 @@ int main()
   assert(2 > r ==> arr2 >= pivot);
   assert(3 > r ==> arr3 >= pivot);
   assert(4 > r ==> arr4 >= pivot);
+  /* clang-format on */
+
   return r;
 }

regression/contracts/invar_check_break_fail/test.desc

@@ -0,0 +1,25 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* 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/invar_check_break_pass/main.c

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

regression/contracts/invar_check_break_pass/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.3\] .* Check loop invariant before entry: SUCCESS$
+^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion x == y \+ 2 \* n: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that multiple loops and `for` loops are correctly handled.