Cleanup regression tests for quantified contracts

regression/contracts/quantifiers-exists-ensures-01/main.c → regression/contracts/quantifiers-exists-both-enforce/main.c

@@ -1,22 +1,20 @@
 // clang-format off
 int f1(int *arr)
-  __CPROVER_assigns(*arr)
+  __CPROVER_requires(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 8) && arr[i] == 0
+  })
   __CPROVER_ensures(__CPROVER_exists {
     int i;
-    (0 <= i && i < 10) ==> arr[i] == i
+    (0 <= i && i < 8) && arr[i] == 0
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
-
   return 0;
 }
 
 int main()
 {
-  int arr[10];
+  int arr[8];
   f1(arr);
 }

regression/contracts/quantifiers-exists-both-enforce/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the ENSURES clause being enforced in this case,
+are supported only if the quantifier is bound to a constant range.

regression/contracts/quantifiers-exists-both-replace/main.c

@@ -0,0 +1,42 @@
+#include <stdlib.h>
+
+#define MAX_LEN 8
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_requires(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // constant bounds for explicit unrolling with SAT backend
+      (0 <= i && i < MAX_LEN) && (
+        // actual symbolic bound for `i`
+        i < len && arr[i] == 0
+      )
+    }
+  )
+  __CPROVER_ensures(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // constant bounds for explicit unrolling with SAT backend
+      (0 <= i && i < MAX_LEN) && (
+        // actual symbolic bound for `i`
+        i < len && arr[i] == 0
+      )
+    }
+  )
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len);
+  if(len > 0)
+    arr[0] = 0;
+
+  f1(arr, len);
+}

regression/contracts/quantifiers-exists-both-replace/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the REQUIRES clause being replaced in this case,
+are supported only if the quantifier is bound to a constant range.

regression/contracts/quantifiers-exists-ensures-enforce/main.c

@@ -0,0 +1,40 @@
+// clang-format off
+int f1(int *arr)
+  __CPROVER_assigns(*arr)
+  __CPROVER_ensures(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] == i
+  })
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+// clang-format off
+int f2(int *arr)
+  __CPROVER_assigns(*arr)
+  __CPROVER_ensures(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] != 0
+  })
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = 0;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f2(arr);
+  f1(arr);
+}

regression/contracts/quantifiers-exists-ensures-enforce/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+within positive contexts (enforced ENSURES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the ENSURES clause being enforced in this case,
+are supported only if the quantifier is bound to a constant range.

regression/contracts/quantifiers-exists-ensures-replace/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+#define MAX_LEN 128
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_ensures(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // test replacement with symbolic bound
+      (0 <= i && i < len) && arr[i] == 0
+    }
+  )
+// clang-format on
+{
+  // we are only checking for contract replacement
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len * sizeof(int));
+
+  f1(arr, len);
+
+  bool found_zero = false;
+  for(int i = 0; i <= MAX_LEN; i++)
+  {
+    if(i < len)
+      found_zero |= (arr[i] == 0);
+  }
+
+  // clang-format off
+  assert(len > 0 ==> found_zero);
+  // clang-format on
+}

regression/contracts/quantifiers-exists-ensures-replace/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line .* assertion len > 0 ==> found_zero: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+within negative contexts (replaced ENSURES clauses).
+
+This is fully supported (without requiring full unrolling) with the SAT backend.