Add array initialisation support in default goto-harness.

regression/goto-harness/associated-size-parameter/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+void test(int *array, int size)
+{
+  for(int i = 0; i < size; i++)
+    array[i] = i;
+
+  for(int i = 0; i < size; i++)
+    assert(array[i] == i);
+}

regression/goto-harness/associated-size-parameter/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--harness-type call-function --function test --associated-array-size array:size
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--

regression/goto-harness/chain.sh

@@ -23,5 +23,11 @@ if [ -e "${name}-mod.gb" ] ; then
   rm -f "${name}-mod.gb"
 fi
 
-$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} 
-$cbmc --function $entry_point "${name}-mod.gb" --unwind 20 --unwinding-assertions
+# `# some comment` is an inline comment - basically, cause bash to execute an empty command
+
+$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
+$cbmc --function $entry_point "${name}-mod.gb" \
+  --pointer-check `# because we want to see out of bounds errors` \
+  --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
+  --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \
+  # cbmc args end

regression/goto-harness/pointer-to-array-function-parameters-max-size/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+void test(int *arr, int sz)
+{
+  assert(sz < 10);
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = 0;
+  }
+}

regression/goto-harness/pointer-to-array-function-parameters-max-size/test.desc

@@ -0,0 +1,14 @@
+CORE
+test.c
+--harness-type call-function --function test --max-array-size 10 --associated-array-size arr:sz
+\[test.assertion.1\] line \d+ assertion sz < 10: FAILURE
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+unwinding assertion loop \d: FAILURE

regression/goto-harness/pointer-to-array-function-parameters-min-size/test.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+void min_array_size_test(int *arr, int sz)
+{
+  assert(sz > 2);
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = i;
+  }
+  for(int i = 0; i < sz; ++i)
+  {
+    assert(arr[i] == i);
+  }
+}

regression/goto-harness/pointer-to-array-function-parameters-min-size/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--harness-type call-function --function min_array_size_test --max-array-size 3 --min-array-size 3 --associated-array-size arr:sz
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+unwinding assertion loop \d: FAILURE

regression/goto-harness/pointer-to-array-function-parameters-multi-arg-right/test.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int is_prefix_of(
+  const char *string,
+  int string_size,
+  const char *prefix,
+  int prefix_size)
+{
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+
+  for(int ix = 0; ix < prefix_size; ++ix)
+  {
+    if(string[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}

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

@@ -0,0 +1,8 @@
+CORE
+test.c
+--harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
+^SIGNAL=0$
+^EXIT=0$
+VERIFICATION SUCCESSFUL
+--
+unwinding assertion loop \d+: FAILURE

regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stddef.h>
+
+int is_prefix_of(
+  const char *string,
+  size_t string_size,
+  const char *prefix,
+  size_t prefix_size)
+{
+  if(string_size < prefix_size)
+  {
+    return 0;
+  }
+  assert(prefix_size <= string_size);
+  // oh no! we should have used prefix_size here
+  for(int ix = 0; ix < string_size; ++ix)
+  {
+    if(string[ix] != prefix[ix])
+    {
+      return 0;
+    }
+  }
+  return 1;
+}

regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
+^EXIT=10$
+^SIGNAL=0$
+\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
+VERIFICATION FAILED
+--

regression/goto-harness/pointer-to-array-function-parameters-with-size/test.c

@@ -0,0 +1,7 @@
+void test(int *arr, int sz)
+{
+  for(int i = 0; i < sz; ++i)
+  {
+    arr[i] = 0;
+  }
+}

regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
+^EXIT=0$
+^SIGNAL=0$
+\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+--

regression/goto-harness/pointer-to-array-function-parameters/test.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+void test(int *arr)
+{
+  // works because the arrays we generate have at least one element
+  arr[0] = 5;
+
+  // doesn't work because our arrays have at most ten elements
+  arr[10] = 10;
+}

regression/goto-harness/pointer-to-array-function-parameters/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--harness-type call-function --function test --treat-pointer-as-array arr
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--

src/goto-harness/function_call_harness_generator.cpp

@@ -21,6 +21,10 @@ Author: Diffblue Ltd.
 #include <goto-programs/goto_convert.h>
 #include <goto-programs/goto_model.h>
 
+#include <algorithm>
+#include <iterator>
+#include <set>
+
 #include "function_harness_generator_options.h"
 #include "goto_harness_parse_options.h"
 #include "recursive_initialization.h"
@@ -41,6 +45,12 @@ struct function_call_harness_generatort::implt
   recursive_initialization_configt recursive_initialization_config;
   std::unique_ptr<recursive_initializationt> recursive_initialization;
 
+  std::set<irep_idt> function_parameters_to_treat_as_arrays;
+  std::set<irep_idt> function_arguments_to_treat_as_arrays;
+
+  std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
+  std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
+
   /// \see goto_harness_generatort::generate
   void generate(goto_modelt &goto_model, const irep_idt &harness_function_name);
   /// Iterate over the symbol table and generate initialisation code for
@@ -117,6 +127,57 @@ void function_call_harness_generatort::handle_option(
         "--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT};
     }
   }
+  else if(option == FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT)
+  {
+    p_impl->recursive_initialization_config.max_dynamic_array_size =
+      require_one_size_value(
+        FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT, values);
+  }
+  else if(option == FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT)
+  {
+    p_impl->recursive_initialization_config.min_dynamic_array_size =
+      require_one_size_value(
+        FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values);
+  }
+  else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT)
+  {
+    p_impl->function_parameters_to_treat_as_arrays.insert(
+      values.begin(), values.end());
+  }
+  else if(option == FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT)
+  {
+    for(auto const &array_size_pair : values)
+    {
+      try
+      {
+        std::string array;
+        std::string size;
+        split_string(array_size_pair, ':', array, size);
+        // --associated-array-size implies --treat-pointer-as-array
+        // but it is not an error to specify both, so we don't check
+        // for duplicates here
+        p_impl->function_parameters_to_treat_as_arrays.insert(array);
+        auto const inserted =
+          p_impl->function_parameter_to_associated_array_size.emplace(
+            array, size);
+        if(!inserted.second)
+        {
+          throw invalid_command_line_argument_exceptiont{
+            "can not have two associated array sizes for one array",
+            "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT};
+        }
+      }
+      catch(const deserialization_exceptiont &)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "`" + array_size_pair +
+            "' is in an invalid format for array size pair",
+          "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT,
+          "array_name:size_name, where both are the names of function "
+          "parameters"};
+      }
+    }
+  }
   else
   {
     throw invalid_command_line_argument_exceptiont{
@@ -145,7 +206,17 @@ void function_call_harness_generatort::implt::generate(
   code_blockt function_body{};
   auto const arguments = declare_arguments(function_body);
 
+  // configure and create recursive initialisation object
   recursive_initialization_config.mode = function_to_call.mode;
+  recursive_initialization_config.pointers_to_treat_as_arrays =
+    function_arguments_to_treat_as_arrays;
+  recursive_initialization_config.array_name_to_associated_array_size_variable =
+    function_argument_to_associated_array_size;
+  for(const auto &pair : function_argument_to_associated_array_size)
+  {
+    recursive_initialization_config.variables_that_hold_array_sizes.insert(
+      pair.second);
+  }
   recursive_initialization = util_make_unique<recursive_initializationt>(
     recursive_initialization_config, goto_model);
 
@@ -197,6 +268,15 @@ void function_call_harness_generatort::validate_options()
     throw invalid_command_line_argument_exceptiont{
       "required parameter entry function not set",
       "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
+  if(
+    p_impl->recursive_initialization_config.min_dynamic_array_size >
+    p_impl->recursive_initialization_config.max_dynamic_array_size)
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "min dynamic array size cannot be greater than max dynamic array size",
+      "--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
+      " --" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
+  }
 }
 
 std::size_t function_call_harness_generatort::require_one_size_value(
@@ -287,13 +367,41 @@ function_call_harness_generatort::implt::declare_arguments(
                                             function_to_call.location,
                                             "__goto_harness",
                                             *symbol_table};
+  std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
   for(const auto &parameter : parameters)
   {
     auto argument = allocate_objects.allocate_automatic_local_object(
       parameter.type(), parameter.get_base_name());
+    parameter_name_to_argument_name.insert(
+      {parameter.get_base_name(), argument.get_identifier()});
     arguments.push_back(argument);
   }
 
+  for(const auto &pair : parameter_name_to_argument_name)
+  {
+    auto const &parameter_name = pair.first;
+    auto const &argument_name = pair.second;
+    if(function_parameters_to_treat_as_arrays.count(parameter_name) != 0)
+    {
+      function_arguments_to_treat_as_arrays.insert(argument_name);
+    }
+    auto it = function_parameter_to_associated_array_size.find(parameter_name);
+    if(it != function_parameter_to_associated_array_size.end())
+    {
+      auto const &associated_array_size_parameter = it->second;
+      auto associated_array_size_argument =
+        parameter_name_to_argument_name.find(associated_array_size_parameter);
+      if(
+        associated_array_size_argument == parameter_name_to_argument_name.end())
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "associated array size is not there",
+          "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT};
+      }
+      function_argument_to_associated_array_size.insert(
+        {argument_name, associated_array_size_argument->second});
+    }
+  }
   allocate_objects.declare_created_symbols(function_body);
   return arguments;
 }

src/goto-harness/function_harness_generator_options.h

@@ -14,13 +14,23 @@ Author: Diffblue Ltd.
 #define FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "min-null-tree-depth"
 #define FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT                   \
   "max-nondet-tree-depth"
+#define FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size"
+#define FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size"
+#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT                  \
+  "treat-pointer-as-array"
+#define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT                   \
+  "associated-array-size"
 
 // clang-format off
 #define FUNCTION_HARNESS_GENERATOR_OPTIONS                                     \
   "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):"                             \
   "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")"                        \
   "(" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):"                  \
   "(" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):"                \
+  "(" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):"                       \
+  "(" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):"                       \
+  "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT "):"               \
+  "(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT "):"                \
 // FUNCTION_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on
@@ -38,6 +48,20 @@ Author: Diffblue Ltd.
   "--" FUNCTION_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"                                \
+  "--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT                           \
+  " N    minimum size of dynamically created arrays (default: 1)\n"            \
+  "--" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT                           \
+  " N    maximum size of dynamically created arrays (default: 2)\n"            \
+  "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT                   \
+  " parameter    treat the function parameter with the name `parameter'\n"     \
+  "                   as an array\n"                                           \
+  "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT                    \
+  " array_name:size_name\n"                                                    \
+  "                                set the parameter <size_name> to the size\n"\
+  "                                of the array <array_name>\n"                \
+  "                                (implies "                                  \
+  "-- " FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT                   \
+  " <array_name>)\n"                                                           \
   // FUNCTION_HARNESS_GENERATOR_HELP
 
 // clang-format on