Fix havocing of arrays when enforcing invariants

As reported in #6020, only the first element of an array was being
havoced earlier.

In this change, we fix this behavior using `havoc_object`.

Author: SaswatPadhi

regression/contracts/invar_havoc_dynamic_array/main.c

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

regression/contracts/invar_havoc_dynamic_array/test.desc

@@ -0,0 +1,17 @@
+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 data\[5\] == 0: FAILURE$
+^\[main.assertion.2\] .* assertion data\[5\] == 1: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Test case related to issue #6020: it checks that arrays are correctly havoced
+when enforcing loop invariant contracts.
+The `data[5] == 0` assertion is expected to fail since `data` is havoced.
+The `data[5] == 1` assertion is also expected to fail since the invariant does
+not reestablish the value for `data[5]`.

regression/contracts/invar_havoc_dynamic_array_const_idx/main.c

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

regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc

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

regression/contracts/invar_havoc_static_array/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  char data[SIZE];
+  data[5] = 0;
+
+  for(unsigned i = 0; i < SIZE; i++)
+    __CPROVER_loop_invariant(i <= SIZE)
+    {
+      data[i] = 1;
+    }
+
+  assert(data[5] == 0);
+  assert(data[5] == 1);
+}

regression/contracts/invar_havoc_static_array/test.desc

@@ -0,0 +1,17 @@
+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 data\[5\] == 0: FAILURE$
+^\[main.assertion.2\] .* assertion data\[5\] == 1: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Test case related to issue #6020: it checks that arrays are correctly havoced
+when enforcing loop invariant contracts.
+The `data[5] == 0` assertion is expected to fail since `data` is havoced.
+The `data[5] == 1` assertion is also expected to fail since the invariant does
+not reestablish the value for `data[5]`.

regression/contracts/invar_havoc_static_array_const_idx/main.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  char data[SIZE];
+  data[1] = 0;
+  data[4] = 0;
+
+  for(unsigned i = 0; i < SIZE; i++)
+    __CPROVER_loop_invariant(i <= SIZE)
+    {
+      data[1] = i;
+    }
+
+  assert(data[1] == 0 || data[1] == 1);
+  assert(data[4] == 0);
+}

regression/contracts/invar_havoc_static_array_const_idx/test.desc

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

regression/contracts/invar_havoc_static_multi-dim_array/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+void main()
+{
+  char data[SIZE][SIZE][SIZE];
+
+  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_static_multi-dim_array/test.desc

@@ -0,0 +1,19 @@
+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 __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 multi dimensional arrays
+are correctly havoced when enforcing 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.