havoc_slice documentation, implementation and regression tests

Author: Remi Delmas

doc/cprover-manual/api.md

@@ -211,6 +211,57 @@ returns true when it is safe to do both.  These predicates can be given an
 optional size; when the size argument is not given, the size of the subtype
 (which must not be **void**) of the pointer type is used.
 
+#### \_\_CPROVER\_havoc\_object
+
+
+This function requires a valid pointer and updates **all bytes** of the
+underlying object with nondeterministic values.
+
+```C
+void __CPROVER_havoc_object(void *p);
+```
+
+**Warning**
+
+This primitive havocs object bytes before
+the given `p` and after `p + sizeof(*p)`:
+
+```C
+struct foo {
+  int x;
+  int y;
+  int z;
+};
+
+struct foo thefoo = {.x = 1; .y = 2, .z = 3};
+
+int* p = &thefoo.y; // pointing to thefoo.y
+
+__CPROVER_havoc_object(p); // makes the whole struct nondet
+__CPROVER_assert(thefoo.x == 1, "fails because `thefoo.x` is now nondet");
+__CPROVER_assert(thefoo.y == 2, "fails because `thefoo.y` is now nondet");
+__CPROVER_assert(thefoo.z == 3, "fails because `thefoo.z` is now nondet");
+```
+
+#### \_\_CPROVER\_havoc\_slice
+
+This function requires requires that `__CPROVER_w_ok(p, size)` holds,
+and updates `size` consecutive bytes of the underlying object, starting at `p`,
+with nondeterministic values.
+
+```C
+void __CPROVER_havoc_slice(void *p, __CPROVER_size_t size);
+```
+
+**Caveat**
+
+- If the slice contains bytes that can be interpreted as pointers by the
+  program, this will cause these pointers to become invalid
+  (i.e. they will not point to anything meaningful).
+- If this slice only contains bytes that are not interpreted as pointers
+  by the program, then havocing the slice is equivalent to making the
+  interpretation of these bytes nondeterministic.
+
 ### Predefined Types and Symbols
 
 #### \_\_CPROVER\_bitvector

regression/cbmc/havoc_slice/declarations.h

@@ -0,0 +1,26 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+// HAVOC STRUCT MEMBERS
+// TODO take into account plaform/pointer size in the tests
+typedef struct
+{
+  uint16_t a;    // 2 bytes
+  uint16_t b[5]; // 10 bytes
+  uint32_t c;    // 4 bytes
+  uint16_t *d;   // 4 or 8 bytes
+  union {
+    uint16_t a;    // 2 bytes
+    uint16_t b[5]; // 10 bytes
+    uint32_t c;    // 4 bytes
+    uint16_t *d;   // 4 or 8 bytes
+  } u;             // 10 bytes
+} st;              // 30 or 34 bytes total
+
+//                0  2          12   16       24       34
+//                |  |          |    |        |        |
+// struct layout: aa bbbbbbbbbb cccc dddddddd uuuuuuuuuu
+// union layout :                             aa--------
+//                                            bbbbbbbbbb
+//                                            cccc------
+//                                            dddddddd--

regression/cbmc/havoc_slice/test_array_slice_1.c

@@ -0,0 +1,17 @@
+void main(void)
+{
+  // INITIALIZE
+  int a[5] = {0, 1, 2, 3, 4};
+  int old_a[5] = {0, 1, 2, 3, 4};
+
+  // HAVOC ARRAY SLICE
+  __CPROVER_havoc_slice(a + 2, 2 * sizeof(*a));
+
+  // POSTCONDITIONS
+  __CPROVER_assert(a[0] == old_a[0], "expecting SUCCESS");
+  __CPROVER_assert(a[1] == old_a[1], "expecting SUCCESS");
+  __CPROVER_assert(a[2] == old_a[2], "expecting FAILURE");
+  __CPROVER_assert(a[3] == old_a[3], "expecting FAILURE");
+  __CPROVER_assert(a[4] == old_a[4], "expecting SUCCESS");
+  return;
+}

regression/cbmc/havoc_slice/test_array_slice_1.desc

@@ -0,0 +1,10 @@
+CORE
+test_array_slice_1.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^.*expecting FAILURE: SUCCESS$
+^.*expecting SUCCESS: FAILURE$
+^.*dereference .*: FAILURE$

regression/cbmc/havoc_slice/test_array_slice_2.c

@@ -0,0 +1,17 @@
+void main(void)
+{
+  // INITIALIZE
+  int a[5] = {0, 1, 2, 3, 4};
+  int old_a[5] = {0, 1, 2, 3, 4};
+
+  // HAVOC ARRAY SLICE
+  __CPROVER_havoc_slice(&a[2] - 1, 2 * sizeof(*a));
+
+  // POSTCONDITIONS
+  __CPROVER_assert(a[0] == old_a[0], "expecting SUCCESS");
+  __CPROVER_assert(a[1] == old_a[1], "expecting FAILURE");
+  __CPROVER_assert(a[2] == old_a[2], "expecting FAILURE");
+  __CPROVER_assert(a[3] == old_a[3], "expecting SUCCESS");
+  __CPROVER_assert(a[4] == old_a[4], "expecting SUCCESS");
+  return;
+}

regression/cbmc/havoc_slice/test_array_slice_2.desc

@@ -0,0 +1,10 @@
+CORE
+test_array_slice_2.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^.*expecting FAILURE: SUCCESS$
+^.*expecting SUCCESS: FAILURE$
+^.*dereference .*: FAILURE$

regression/cbmc/havoc_slice/test_array_symbolic_size.c

@@ -0,0 +1,46 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+// byte-level comparison
+#define CHECK_SLICE(A, OLD_A, I, IDX, HAVOC_SIZE)                              \
+  {                                                                            \
+    __CPROVER_assert(                                                          \
+      !(IDX <= I && I <= IDX + HAVOC_SIZE) | A[I] == OLD_A[I],                 \
+      "expecting FAILURE");                                                    \
+                                                                               \
+    __CPROVER_assert(                                                          \
+      (IDX <= I && I <= IDX + HAVOC_SIZE) | A[I] == OLD_A[I],                  \
+      "expecting SUCCESS");                                                    \
+  }
+
+// ARRAY WITH SYMBOLIC SIZE.
+void main(void)
+{
+  // INITIALIZE
+  uint32_t size;
+  __CPROVER_assume(5 == size);
+
+  char a[size];
+  char old_a[size];
+
+  __CPROVER_array_set(a, 0);
+  __CPROVER_array_set(old_a, 0);
+
+  uint32_t idx;
+  __CPROVER_assume(idx < size);
+
+  uint32_t havoc_size;
+  __CPROVER_assume(1 <= havoc_size && havoc_size <= size);
+  __CPROVER_assume(idx + havoc_size <= size);
+
+  // HAVOC SINGLE CELL
+  __CPROVER_havoc_slice(&a[idx], havoc_size);
+
+  // POSTCONDITIONS
+  CHECK_SLICE(a, old_a, 0, idx, havoc_size);
+  CHECK_SLICE(a, old_a, 1, idx, havoc_size);
+  CHECK_SLICE(a, old_a, 2, idx, havoc_size);
+  CHECK_SLICE(a, old_a, 3, idx, havoc_size);
+  CHECK_SLICE(a, old_a, 4, idx, havoc_size);
+  return;
+}

regression/cbmc/havoc_slice/test_array_symbolic_size.desc

@@ -0,0 +1,10 @@
+CORE thorough-paths thorough-smt-backend
+test_array_symbolic_size.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^.*expecting FAILURE: SUCCESS$
+^.*expecting SUCCESS: FAILURE$
+^.*dereference .*: FAILURE$

regression/cbmc/havoc_slice/test_nondet_conditional.c

@@ -0,0 +1,34 @@
+void main(void)
+{
+  // HAVOC through nondet conditional
+  typedef struct
+  {
+    int i;
+    int j;
+  } st;
+  int i = 10;
+  int old_i = 10;
+  st s = {20, 30};
+  st old_s = s;
+
+  _Bool c;
+
+  int *p = c ? &i : &s.i;
+
+  __CPROVER_havoc_slice(p, sizeof(*p));
+
+  if(c)
+  {
+    __CPROVER_assert(i == old_i, "expecting FAILURE");
+    __CPROVER_assert(s.i == old_s.i, "expecting SUCCESS");
+    __CPROVER_assert(s.j == old_s.j, "expecting SUCCESS");
+  }
+  else
+  {
+    __CPROVER_assert(i == old_i, "expecting SUCCESS");
+    __CPROVER_assert(s.i == old_s.i, "expecting FAILURE");
+    __CPROVER_assert(s.j == old_s.j, "expecting SUCCESS");
+  }
+
+  return;
+}

regression/cbmc/havoc_slice/test_nondet_conditional.desc

@@ -0,0 +1,10 @@
+CORE
+test_nondet_conditional.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^.*expecting FAILURE: SUCCESS$
+^.*expecting SUCCESS: FAILURE$
+^.*dereference .*: FAILURE$