User controlled havoc(ing) for memory-snapshot harness

regression/snapshot-harness/nondet_initialize_static_arrays/main.c

@@ -0,0 +1,51 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  struct st2 *to_st2;
+  int data;
+} st1_t;
+
+typedef struct st2
+{
+  struct st1 *to_st1;
+  int data;
+} st2_t;
+
+typedef struct st3
+{
+  st1_t *array[3];
+} st3_t;
+
+st3_t *p;
+
+void initialize()
+{
+  p = malloc(sizeof(st3_t));
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(p != NULL);
+  for(int index = 0; index < 3; index++)
+  {
+    // check that the arrays in structs (and structs in those arrays) were
+    // initialized up-to the input depth
+    assert(p->array[index]->to_st2 != NULL);
+    assert(p->array[index]->to_st2->to_st1 != NULL);
+    assert(p->array[index]->to_st2->to_st1->to_st2 == NULL);
+  }
+
+  // non-deterministically initializated objects should not be equal
+  assert(p->array[0] != p->array[1]);
+  assert(p->array[1] != p->array[2]);
+  assert(p->array[0] != p->array[2]);
+}

regression/snapshot-harness/nondet_initialize_static_arrays/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --min-null-tree-depth 10 --max-nondet-tree-depth 4 --havoc-variables p
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/main.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  struct st2 *to_st2;
+  int data;
+} st1_t;
+
+typedef struct st2
+{
+  struct st1 *to_st1;
+  int data;
+} st2_t;
+
+st1_t dummy1;
+st2_t dummy2;
+
+st1_t *p;
+
+void initialize()
+{
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(p != NULL);
+  assert(p->to_st2 != NULL);
+  assert(p->to_st2->to_st1 != NULL);
+  assert(p->to_st2->to_st1->to_st2 == NULL);
+
+  assert(p != &dummy1);
+  assert(p->to_st2 != &dummy2);
+  assert(p->to_st2->to_st1 != &dummy1);
+}

regression/snapshot-harness/pointer-function-parameters-struct-mutual-recursion/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables p --min-null-tree-depth 10 --max-nondet-tree-depth 3
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/pointer-to-array-char/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+#include <malloc.h>
+
+char *first;
+char *second;
+int array_size;
+
+void initialize()
+{
+  first = malloc(sizeof(char) * 12);
+  first = "1234567890a";
+  second = first;
+  array_size = 11;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(first == second);
+  assert(second[array_size - 1] == 'a');
+  return 0;
+}

regression/snapshot-harness/pointer-to-array-char/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+
+char *first = "12345678901";
+char *second;
+int string_size;
+const char *prefix;
+int prefix_size;
+
+void initialize()
+{
+  second = first;
+  string_size = 11;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(first == second);
+  if(prefix_size > 0)
+    assert(second[prefix_size - 1] != 'a');
+
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+
+  for(int ix = 0; ix < prefix_size; ++ix)
+  {
+    if(second[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix,prefix_size --size-of-array prefix:prefix_size --max-array-size 5
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/pointer-to-array-int/main.c

@@ -0,0 +1,44 @@
+#include <assert.h>
+#include <malloc.h>
+
+int *first;
+int *second;
+int *third;
+int array_size;
+const int *prefix;
+int prefix_size;
+
+void initialize()
+{
+  first = (int *)malloc(sizeof(int) * 5);
+  first[0] = 0;
+  first[1] = 1;
+  first[2] = 2;
+  first[3] = 3;
+  first[4] = 4;
+  second = first;
+  array_size = 5;
+  third = &array_size;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(first == second);
+  // The following assertions will be check in the following PR once
+  // dynamically allocated snapshots are properly implemented.
+  /* assert(array_size >= prefix_size); */
+  /* assert(prefix_size >= 0); */
+  /* assert(second[prefix_size] != 6); */
+  /* assert(second[4] == 4); */
+
+  /* for(int i = 0; i < prefix_size; i++) */
+  /*   assert(second[i] != prefix[i]); */
+  return 0;
+}

regression/snapshot-harness/pointer-to-array-int/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+first,second,array_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 4
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/snapshot-harness/pointer_07/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <malloc.h>
+
+int *p1;
+
+void initialize()
+{
+  p1 = malloc(sizeof(int));
+  *p1 = 1;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(p1[0] == 1);
+  assert(*p1 == 1);
+  p1[0] = 2;
+  assert(*p1 == 1);
+  assert(*p1 != 1);
+}

regression/snapshot-harness/pointer_07/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+p1 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion p1\[0\] == 1: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion \*p1 == 1: SUCCESS
+\[main.assertion.3\] line [0-9]+ assertion \*p1 == 1: FAILURE
+\[main.assertion.4\] line [0-9]+ assertion \*p1 != 1: SUCCESS
+--
+^warning: ignoring

regression/snapshot-harness/static-array-char/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+char tmp[12];
+char *first;
+char *second;
+int array_size;
+
+void initialize()
+{
+  tmp[0] = '1';
+  tmp[9] = '0';
+  tmp[10] = 'a';
+  first = (char *)tmp;
+  second = first;
+  array_size = 11;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(first == second);
+  assert(second[array_size - 1] == 'a');
+  assert(first[0] == '1');
+  assert(second[9] == '0');
+  return 0;
+}

regression/snapshot-harness/static-array-char/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+tmp,first,second,array_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

src/goto-harness/common_harness_generator_options.h

@@ -0,0 +1,46 @@
+/******************************************************************\
+
+Module: common_harness_generator_options
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#ifndef CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H
+#define CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H
+
+#define COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "min-null-tree-depth"
+#define COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT                     \
+  "max-nondet-tree-depth"
+#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size"
+#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size"
+
+// clang-format off
+#define COMMON_HARNESS_GENERATOR_OPTIONS                                       \
+  "(" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):"                    \
+  "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):"                  \
+  "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):"                         \
+  "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):"                         \
+// COMMON_HARNESS_GENERATOR_OPTIONS
+
+// clang-format on
+
+// clang-format off
+#define COMMON_HARNESS_GENERATOR_HELP                                          \
+  "--" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT                        \
+  " N       minimum level at which a pointer can first be NULL\n"              \
+  "                              in a recursively nondet initialized struct\n" \
+  "--" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT                      \
+  " N     limit size of nondet (e.g. input) object tree;\n"                    \
+  "                              at level N pointers are set to null\n"        \
+  "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT                             \
+  " N            minimum size of dynamically created arrays\n"                 \
+  "                              (default: 1)\n"                               \
+  "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT                             \
+  " N            maximum size of dynamically created arrays\n"                 \
+  "                              (default: 2)\n"                               \
+  // COMMON_HARNESS_GENERATOR_HELP
+
+// clang-format on
+
+#endif // CPROVER_GOTO_HARNESS_COMMON_HARNESS_GENERATOR_OPTIONS_H