Merge pull request diffblue#6026 from padhi-aws-forks/invariant_deref_fix

Fix havocing of arrays when enforcing loop invariants

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 dynamically allocated 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 dynamically allocated 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_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,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 __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 dynamically allocated 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.
+
+Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.

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,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\[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 dynamically allocated multi
+dimensional arrays are correctly havoced when enforcing 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 -- alias analysis is imprecise and returns `unknown`.

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,22 @@
+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 dynamically allocated multi
+dimensional arrays are correctly havoced when enforcing 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 -- alias analysis is imprecise and returns `unknown`.

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.

regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/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;
+  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_static_multi-dim_array_all_const_idx/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 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 multi dimensional arrays
+are correctly havoced when enforcing 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.