Add initialization of static arrays

Add non-det initialization of statically sized arrays.
This does element-wise initialisation.

Co-authored-by: Fotis Koutoulakis <[email protected]>
Co-authored-by: Hannes Steffenhagen <[email protected]>

Author: NlightNFotis

regression/goto-harness/nondet_initialize_static_arrays/main.c

@@ -0,0 +1,37 @@
+#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;
+
+st1_t dummy1;
+st2_t dummy2;
+
+void func(st3_t *p)
+{
+  assert(p != NULL);
+  for(int index = 0; index < 3; index++)
+  {
+    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);
+  }
+
+  assert(p->array[0] != p->array[1]);
+  assert(p->array[1] != p->array[2]);
+  assert(p->array[0] != p->array[2]);
+}

regression/goto-harness/nondet_initialize_static_arrays/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 4 --harness-type call-function
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/goto-harness/recursive_initialization.cpp

@@ -9,6 +9,7 @@ Author: Diffblue Ltd.
 #include "recursive_initialization.h"
 
 #include <util/allocate_objects.h>
+#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/irep.h>
@@ -38,6 +39,10 @@ void recursive_initializationt::initialize(
   {
     initialize_pointer(lhs, depth, known_tags, body);
   }
+  else if(type.id() == ID_array)
+  {
+    initialize_array(lhs, depth, known_tags, body);
+  }
   else
   {
     initialize_nondet(lhs, depth, known_tags, body);
@@ -138,3 +143,23 @@ void recursive_initializationt::initialize_nondet(
 {
   body.add(code_assignt{lhs, side_effect_expr_nondett{lhs.type()}});
 }
+
+void recursive_initializationt::initialize_array(
+  const exprt &array,
+  std::size_t depth,
+  const recursion_sett &known_tags,
+  code_blockt &body)
+{
+  PRECONDITION(array.type().id() == ID_array);
+  const auto &array_type = to_array_type(array.type());
+  const auto array_size =
+    numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
+  for(std::size_t index = 0; index < array_size; index++)
+  {
+    initialize(
+      index_exprt(array, from_integer(index, size_type())),
+      depth,
+      known_tags,
+      body);
+  }
+}

src/goto-harness/recursive_initialization.h

@@ -69,6 +69,13 @@ class recursive_initializationt
     std::size_t depth,
     const recursion_sett &known_tags,
     code_blockt &body);
+  // array stuff
+  // static array handling
+  void initialize_array(
+    const exprt &array,
+    std::size_t depth,
+    const recursion_sett &known_tags,
+    code_blockt &body);
 };
 
 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H