More regression tests for havocing dynamic arrays

These regression tests currently fail due to imprecision in alias
analysis (see: diffblue#6021).

In future, we could either improve the alias analysis, or add manual
assigns clause annotations on these loops and make sure that the arrays
are correctly havoced.

Author: SaswatPadhi

regression/contracts/invar_havoc_dynamic_multi-dim_array/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  char ***data = malloc(SIZE * sizeof(char **));
+  for(unsigned i = 0; i < SIZE; i++)
+  {
+    data[i] = malloc(SIZE * sizeof(char *));
+    for(unsigned j = 0; j < SIZE; j++)
+      data[i][j] = malloc(SIZE * sizeof(char));
+  }
+
+  data[1][2][3] = 0;
+  char *old_data123 = &(data[1][2][3]);
+
+  for(unsigned i = 0; i < SIZE; i++)
+    __CPROVER_loop_invariant(i <= SIZE)
+    {
+      data[i][(i + 1) % SIZE][(i + 2) % SIZE] = 1;
+    }
+
+  assert(__CPROVER_same_object(old_data123, &(data[1][2][3])));
+  assert(data[1][2][3] == 0);
+}

regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc

@@ -0,0 +1,20 @@
+KNOWNBUG
+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 __CPROVER_same_object(old_data123, &(data\[1\]\[2\]\[3\])): SUCCESS$
+^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Test case related to issue #6020: it checks that arrays are correctly havoced
+when enforcing loop invariant contracts.
+The `__CPROVER_same_object(old_data123, &(data[1][2][3]))` assertion is expected
+to pass -- we should not mistakenly havoc the allocations, just their values.
+However, the `data[1][2][3] == 0` assertion is expected to fail since `data`
+is havoced.
+
+Blocked on issue #6021.

regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  char ***data = malloc(SIZE * sizeof(char **));
+  for(unsigned i = 0; i < SIZE; i++)
+  {
+    data[i] = malloc(SIZE * sizeof(char *));
+    for(unsigned j = 0; j < SIZE; j++)
+      data[i][j] = malloc(SIZE * sizeof(char));
+  }
+
+  data[1][2][3] = 0;
+  data[4][5][6] = 0;
+
+  for(unsigned i = 0; i < SIZE; i++)
+    __CPROVER_loop_invariant(i <= SIZE)
+    {
+      data[4][5][6] = 1;
+    }
+
+  assert(data[4][5][6] == 0);
+  assert(data[1][2][3] == 0);
+}

regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc

@@ -0,0 +1,20 @@
+KNOWNBUG
+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 data\[4\]\[5\]\[6\] == 0: FAILURE$
+^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Test case related to issue #6020: it checks that arrays are correctly havoced
+when enforcing loop invariant contracts.
+The `data[4][5][6] == 0` assertion is expected to fail since `data[4][5][6]`
+is havoced and the invariant does not reestablish its value.
+However, the `data[1][2][3] == 0` assertion is expected to pass -- we should
+not havoc the entire `data` array, if only a constant index if being modified.
+
+Blocked on issue #6021.

regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  char ***data = malloc(SIZE * sizeof(char **));
+  for(unsigned i = 0; i < SIZE; i++)
+  {
+    data[i] = malloc(SIZE * sizeof(char *));
+    for(unsigned j = 0; j < SIZE; j++)
+      data[i][j] = malloc(SIZE * sizeof(char));
+  }
+
+  data[1][2][3] = 0;
+  data[4][5][6] = 0;
+
+  for(unsigned i = 0; i < SIZE; i++)
+    __CPROVER_loop_invariant(i <= SIZE)
+    {
+      data[4][i][6] = 1;
+    }
+
+  assert(data[1][2][3] == 0);
+  assert(data[4][5][6] == 0);
+}

regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc

@@ -0,0 +1,21 @@
+KNOWNBUG
+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 data\[1\]\[2\]\[3\] == 0: FAILURE$
+^\[main.assertion.2\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Test case related to issue #6020: it checks that arrays are correctly havoced
+when enforcing loop invariant contracts.
+Here, both assertions are expected to fail -- the entire `data` array should
+be havoced since we are assigning to a non-constant index.
+We _could_ do a more precise analysis in future where we only havoc
+`data[4][5][6]` but not `data[1][2][3]` since the latter clearly cannot be
+modified in the given loop.
+
+Blocked on issue #6021.