Add option handling for dynamic array initialisation

Adds the
 --pointers-to-treat-as-arrays
 --associated-array-sizes
 --max-dynamic-array-size

options. The intended behaviour is that the former should indicate which of
the function parameters to an entry function that are pointers should be backed
by an array, the parameter that should hold the size of that array (if any) and
the maximum size of such an array (minimum 1) respectively.

These options currently have no effect and will be implemented in a later commit

Author: hannes-steffenhagen-diffblue

src/ansi-c/ansi_c_language.h

@@ -22,13 +22,26 @@ Author: Daniel Kroening, [email protected]
 // clang-format off
 #define OPT_ANSI_C_LANGUAGE \
   "(max-nondet-tree-depth):" \
-  "(min-null-tree-depth):"
+  "(min-null-tree-depth):" \
+  "(pointers-to-treat-as-arrays):" \
+  "(associated-array-sizes):" \
+  "(max-dynamic-array-size):" \
 
 #define HELP_ANSI_C_LANGUAGE \
   " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */\
   "                              at level N pointers are set to null\n" \
   " --min-null-tree-depth N      minimum level at which a pointer can first be\n" /* NOLINT(*) */\
-  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */
+  "                              NULL in a recursively nondet initialized struct\n" /* NOLINT(*) */\
+  " --pointers-to-treat-as-arrays <identifier,...>  comma separated list of\n" \
+  "                               identifiers that should be initialized as arrays\n" /* NOLINT(*) */ \
+  " --associated-array-sizes <identifier:identifier...>\n" \
+  "                               comma separated list of colon separated pairs\n" /* NOLINT(*) */ \
+  "                               of identifiers; The first element of the pair \n" /* NOLINT(*) */ \
+  "                               should be the name of an array pointer \n" \
+  "                               (see --pointers-to-treat-as-arrays),\n" \
+  "                               the second an integer parameter that\n" \
+  "                               should hold its size\n" \
+  " --max-dynamic-array-size <size>  max size for dynamically allocated arrays\n" /* NOLINT(*) */
 // clang-format on
 
 class ansi_c_languaget:public languaget

src/ansi-c/c_object_factory_parameters.cpp

@@ -8,7 +8,117 @@ Author: Daniel Poetzl
 
 #include "c_object_factory_parameters.h"
 
+#include <util/cmdline.h>
+#include <util/exception_utils.h>
+#include <util/optional_utils.h>
+#include <util/string_utils.h>
+
+#include <algorithm>
+#include <string>
+
 void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
 {
   parse_object_factory_options(cmdline, options);
+  if(cmdline.isset("pointers-to-treat-as-arrays"))
+  {
+    options.set_option(
+      "pointers-to-treat-as-arrays",
+      cmdline.get_comma_separated_values("pointers-to-treat-as-arrays"));
+  }
+  if(cmdline.isset("associated-array-sizes"))
+  {
+    options.set_option(
+      "associated-array-sizes",
+      cmdline.get_comma_separated_values("associated-array-sizes"));
+  }
+  if(cmdline.isset("max-dynamic-array-size"))
+  {
+    options.set_option(
+      "max-dynamic-array-size", cmdline.get_value("max-dynamic-array-size"));
+  }
+}
+
+void c_object_factory_parameterst::set(const optionst &options)
+{
+  object_factory_parameterst::set(options);
+  auto const &pointers_to_treat_as_array =
+    options.get_list_option("pointers-to-treat-as-arrays");
+  std::transform(
+    std::begin(pointers_to_treat_as_array),
+    std::end(pointers_to_treat_as_array),
+    std::inserter(
+      this->pointers_to_treat_as_array, this->pointers_to_treat_as_array.end()),
+    id2string);
+
+  if(options.is_set("max-dynamic-array-size"))
+  {
+    max_dynamic_array_size =
+      options.get_unsigned_int_option("max-dynamic-array-size");
+    if(max_dynamic_array_size == 0)
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "Max dynamic array size must be >= 1", "--max-dynamic-array-size");
+    }
+  }
+  if(options.is_set("associated-array-sizes"))
+  {
+    array_name_to_associated_array_size_variable.clear();
+    variables_that_hold_array_sizes.clear();
+    auto const &array_size_pairs =
+      options.get_list_option("associated-array-sizes");
+    for(auto const &array_size_pair : array_size_pairs)
+    {
+      std::string array_name;
+      std::string size_name;
+      try
+      {
+        split_string(array_size_pair, ':', array_name, size_name);
+      }
+      catch(const deserialization_exceptiont &e)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "can't parse parameter value",
+          "--associated-array-sizes",
+          "pairs of array/size parameter names, separated by a ':' colon"};
+      }
+      auto const mapping_insert_result =
+        array_name_to_associated_array_size_variable.insert(
+          {irep_idt{array_name}, irep_idt{size_name}});
+      if(!mapping_insert_result.second)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "duplicate associated size entries for array `" + array_name +
+            "', existing: `" + id2string(mapping_insert_result.first->second) +
+            "', tried to insert: `" + size_name + "'",
+          "--associated-array-sizes"};
+      }
+      auto const size_name_insert_result =
+        variables_that_hold_array_sizes.insert(irep_idt{size_name});
+      if(!size_name_insert_result.second)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          "using size parameter `" + size_name + "' more than once",
+          "--associated-array-sizes"};
+      }
+    }
+  }
+}
+
+bool c_object_factory_parameterst::is_array_size_parameter(irep_idt id) const
+{
+  return variables_that_hold_array_sizes.find(id) !=
+         end(variables_that_hold_array_sizes);
+}
+
+optionalt<irep_idt> c_object_factory_parameterst::get_associated_size_variable(
+  irep_idt array_id) const
+{
+  return optional_lookup(
+    array_name_to_associated_array_size_variable, array_id);
+}
+
+bool c_object_factory_parameterst::should_be_treated_as_array(irep_idt id) const
+{
+  return pointers_to_treat_as_array.find(id) !=
+         pointers_to_treat_as_array.end();
 }

src/ansi-c/c_object_factory_parameters.h

@@ -9,7 +9,11 @@ Author: Daniel Poetzl
 #ifndef CPROVER_ANSI_C_C_OBJECT_FACTORY_PARAMETERS_H
 #define CPROVER_ANSI_C_C_OBJECT_FACTORY_PARAMETERS_H
 
+#include <map>
+#include <set>
 #include <util/object_factory_parameters.h>
+#include <util/optional.h>
+#include <util/options.h>
 
 struct c_object_factory_parameterst final : public object_factory_parameterst
 {
@@ -21,6 +25,19 @@ struct c_object_factory_parameterst final : public object_factory_parameterst
     : object_factory_parameterst(options)
   {
   }
+
+  bool should_be_treated_as_array(irep_idt id) const;
+  bool is_array_size_parameter(irep_idt id) const;
+  optionalt<irep_idt> get_associated_size_variable(irep_idt array_id) const;
+
+  void set(const optionst &options) override;
+
+  std::size_t max_dynamic_array_size = 2;
+
+private:
+  std::set<irep_idt> pointers_to_treat_as_array;
+  std::set<irep_idt> variables_that_hold_array_sizes;
+  std::map<irep_idt, irep_idt> array_name_to_associated_array_size_variable;
 };
 
 /// Parse the c object factory parameters from a given command line