Merge pull request #3472 from hannes-steffenhagen-diffblue/feature-nondet-array-init

Add nondet initialisation for statically sized arrays

Author: hannes-steffenhagen-diffblue

regression/cbmc/array-function-parameters/test.c

@@ -0,0 +1,37 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct list_nodet list_nodet;
+
+struct list_nodet
+{
+  int val;
+  struct list_nodet *next;
+};
+
+struct Test
+{
+  list_nodet *lists[4];
+};
+
+void test(struct Test Test)
+{
+  // array elements are nondet initialised (min-null-tree-depth is respected)
+  assert(Test.lists[0]->next);
+  assert(Test.lists[1]->next);
+  assert(Test.lists[2]->next);
+  assert(Test.lists[3]->next);
+
+  // array elements are nondet initialised (max-nondet-tree-depth is respected)
+  assert(!Test.lists[0]->next->next);
+  assert(!Test.lists[1]->next->next);
+  assert(!Test.lists[2]->next->next);
+  assert(!Test.lists[3]->next->next);
+
+  // array elements are not all initialised to the same size
+  assert(Test.lists[0] != Test.lists[1]);
+  assert(Test.lists[1] != Test.lists[2]);
+  assert(Test.lists[2] != Test.lists[3]);
+
+  assert(!Test.lists[4]);
+}

regression/cbmc/array-function-parameters/test.desc

@@ -0,0 +1,17 @@
+CORE
+test.c
+--function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check
+\[test.assertion.1\] line \d+ assertion Test.lists\[0\]->next: SUCCESS
+\[test.assertion.2\] line \d+ assertion Test.lists\[1\]->next: SUCCESS
+\[test.assertion.3\] line \d+ assertion Test.lists\[2\]->next: SUCCESS
+\[test.assertion.4\] line \d+ assertion Test.lists\[3\]->next: SUCCESS
+\[test.assertion.5\] line \d+ assertion !Test.lists\[0\]->next->next: SUCCESS
+\[test.assertion.6\] line \d+ assertion !Test.lists\[1\]->next->next: SUCCESS
+\[test.assertion.7\] line \d+ assertion !Test.lists\[2\]->next->next: SUCCESS
+\[test.assertion.8\] line \d+ assertion !Test.lists\[3\]->next->next: SUCCESS
+\[test.assertion.9\] line \d+ assertion Test.lists\[0\] != Test.lists\[1\]: SUCCESS
+\[test.assertion.10\] line \d+ assertion Test.lists\[1\] != Test.lists\[2\]: SUCCESS
+\[test.assertion.11\] line \d+ assertion Test.lists\[2\] != Test.lists\[3\]: SUCCESS
+\[test.array_bounds.1\] line \d+ array `Test'.lists upper bound in Test.lists\[\(signed long int\)4\]: FAILURE
+\[test.assertion.12\] line \d+ assertion !Test.lists\[4\]: FAILURE
+--

scripts/delete_failing_smt2_solver_tests

@@ -71,6 +71,9 @@ rm Typecast1/test.desc
 rm Union_Initialization1/test.desc
 rm address_space_size_limit1/test.desc
 rm address_space_size_limit3/test.desc
+rm argv1/test.desc
+rm argv1/test.desc
+rm array-function-parameters/test.desc
 rm array-tests/test.desc
 rm bounds_check1/test.desc
 rm byte_update2/test.desc

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -58,6 +58,19 @@ class symbol_factoryt
     const exprt &expr,
     const std::size_t depth = 0,
     recursion_sett recursion_set = recursion_sett());
+
+private:
+  /// Generate initialisation code for each array element
+  /// \param assignments: The code block to add code to
+  /// \param expr: An expression of array type
+  /// \param depth: The struct recursion depth
+  /// \param recursion_set: The struct recursion set
+  /// \see gen_nondet_init For the meaning of the last 2 parameters
+  void gen_nondet_array_init(
+    code_blockt &assignments,
+    const exprt &expr,
+    std::size_t depth,
+    const recursion_sett &recursion_set);
 };
 
 /// Create a symbol for a pointer to point to
@@ -201,6 +214,10 @@ void symbol_factoryt::gen_nondet_init(
       gen_nondet_init(assignments, me, depth, recursion_set);
     }
   }
+  else if(type.id() == ID_array)
+  {
+    gen_nondet_array_init(assignments, expr, depth, recursion_set);
+  }
   else
   {
     // If type is a ID_c_bool then add the following code to assignments:
@@ -216,6 +233,25 @@ void symbol_factoryt::gen_nondet_init(
   }
 }
 
+void symbol_factoryt::gen_nondet_array_init(
+  code_blockt &assignments,
+  const exprt &expr,
+  std::size_t depth,
+  const recursion_sett &recursion_set)
+{
+  auto const &array_type = to_array_type(expr.type());
+  auto const array_size = numeric_cast_v<size_t>(array_type.size());
+  DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
+  for(size_t index = 0; index < array_size; ++index)
+  {
+    gen_nondet_init(
+      assignments,
+      index_exprt(expr, from_integer(index, size_type())),
+      depth,
+      recursion_set);
+  }
+}
+
 /// Creates a symbol and generates code so that it can vary over all possible
 /// values for its type. For pointers this involves allocating symbols which it
 /// can point to.