Add support for nondet initialisation of dynamic C strings

Author: hannes-steffenhagen-diffblue

regression/cbmc/pointer-to-string-function-parameters/test.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stddef.h>
+#include <string.h>
+
+int test(char *string, size_t size)
+{
+  for(size_t ix = 0; ix + 1 < size; ++ix)
+  {
+    char c = string[ix];
+    // characters except the last should fall in printable range
+    assert(c == '\n' | c == '\r' | c == '\t' | (c >= 32 && c <= 126));
+  }
+  assert(strlen(string) + 1 == size);
+}

regression/cbmc/pointer-to-string-function-parameters/test.desc

@@ -0,0 +1,7 @@
+CORE
+test.c
+--function test --pointers-to-treat-as-string string --associated-array-sizes string:size --pointer-check --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

src/ansi-c/ansi_c_language.h

@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(pointers-to-treat-as-array):" \
   "(associated-array-sizes):" \
   "(max-dynamic-array-size):" \
+  "(pointers-to-treat-as-string):"
 
 #define HELP_ANSI_C_LANGUAGE \
   " --max-nondet-tree-depth N    limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */\

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -84,6 +84,13 @@ class symbol_factoryt
     std::size_t depth,
     const recursion_sett &recursion_set);
 
+  void gen_nondet_string_member_initialization(
+    code_blockt &assignments,
+    const exprt &array,
+    const exprt &array_size,
+    std::size_t depth,
+    const recursion_sett &recursion_set);
+
 private:
   /// Add a new variable symbol to the symbol table
   /// \param type: The type of the new variable
@@ -216,14 +223,29 @@ void symbol_factoryt::gen_nondet_init(
       using std::placeholders::_5;
       if(object_factory_params.should_be_treated_as_array(symbol_name))
       {
-        gen_array_initialization_t gen_array_initialization = std::bind(
-          &symbol_factoryt::gen_nondet_array_member_initialization,
-          this,
-          _1,
-          _2,
-          _3,
-          _4,
-          _5);
+        gen_array_initialization_t gen_array_initialization;
+        if(object_factory_params.should_be_treated_as_string(symbol_name))
+        {
+          gen_array_initialization = std::bind(
+            &symbol_factoryt::gen_nondet_string_member_initialization,
+            this,
+            _1,
+            _2,
+            _3,
+            _4,
+            _5);
+        }
+        else
+        {
+          gen_array_initialization = std::bind(
+            &symbol_factoryt::gen_nondet_array_member_initialization,
+            this,
+            _1,
+            _2,
+            _3,
+            _4,
+            _5);
+        }
         gen_nondet_size_array_init(
           assignments,
           symbol_expr,
@@ -524,6 +546,76 @@ void symbol_factoryt::gen_nondet_array_member_initialization(
   assignments.add(std::move(array_member_init));
 }
 
+void symbol_factoryt::gen_nondet_string_member_initialization(
+  code_blockt &assignments,
+  const exprt &array,
+  const exprt &array_size,
+  std::size_t depth,
+  const symbol_factoryt::recursion_sett &recursion_set)
+{
+  // for(size_t ix = 0; ix + 1 < array_size; ++ix) {
+  //   assume(arr[ix] == '\n'
+  //   || arr[ix] == '\t'
+  //   || arr[ix] == '\r'
+  //   || (32 <= arr[ix] && arr[ix] <= 126));
+  // }
+
+  auto const &array_index_symbol =
+    new_tmp_symbol(size_type(), CPROVER_PREFIX "array_index");
+  auto array_member_init = code_fort{};
+
+  array_member_init.init() = code_assignt{array_index_symbol.symbol_expr(),
+                                          from_integer(0, size_type())};
+
+  array_member_init.cond() = binary_exprt{
+    plus_exprt{array_index_symbol.symbol_expr(), from_integer(1, size_type())},
+    ID_lt,
+    array_size,
+    bool_typet{}};
+
+  auto const array_member = dereference_exprt{
+    plus_exprt{array, array_index_symbol.symbol_expr(), array.type()}};
+
+  auto array_member_init_body = code_blockt{};
+  array_member_init_body.add(code_assumet{typecast_exprt{
+    bitor_exprt{
+      typecast_exprt{equal_exprt{array_member, from_integer('\n', char_type())},
+                     signed_int_type()},
+      bitor_exprt{
+        typecast_exprt{
+          equal_exprt{array_member, from_integer('\t', char_type())},
+          signed_int_type()},
+        bitor_exprt{
+          typecast_exprt{
+            equal_exprt{array_member, from_integer('\r', char_type())},
+            signed_int_type()},
+          bitand_exprt{typecast_exprt{
+                         binary_relation_exprt{
+                           from_integer(32, char_type()), ID_le, array_member},
+                         signed_int_type()},
+                       typecast_exprt{
+                         binary_relation_exprt{
+                           array_member, ID_le, from_integer(126, char_type())},
+                         signed_int_type()}},
+        }}},
+    bool_typet{}}});
+  array_member_init_body.add(
+    code_assignt{array_index_symbol.symbol_expr(),
+                 plus_exprt{array_index_symbol.symbol_expr(),
+                            from_integer(1, size_type()),
+                            size_type()}});
+  array_member_init.body() = std::move(array_member_init_body);
+  assignments.add(std::move(array_member_init));
+
+  // array[array_size - 1] = '\0';
+  assignments.add(
+    code_assignt{dereference_exprt{plus_exprt{
+                   array,
+                   minus_exprt{array_size, from_integer(1, size_type())},
+                   array.type()}},
+                 from_integer(0, char_type())});
+}
+
 const symbolt &
 symbol_factoryt::gen_malloc_function(const irep_idt &malloc_symbol_name)
 {

src/ansi-c/c_object_factory_parameters.cpp

@@ -25,6 +25,12 @@ void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
       "pointers-to-treat-as-array",
       cmdline.get_comma_separated_values("pointers-to-treat-as-array"));
   }
+  if(cmdline.isset("pointers-to-treat-as-string"))
+  {
+    options.set_option(
+      "pointers-to-treat-as-string",
+      cmdline.get_comma_separated_values("pointers-to-treat-as-string"));
+  }
   if(cmdline.isset("associated-array-sizes"))
   {
     options.set_option(
@@ -38,6 +44,13 @@ void parse_c_object_factory_options(const cmdlinet &cmdline, optionst &options)
   }
 }
 
+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() ||
+         should_be_treated_as_string(id);
+}
+
 void c_object_factory_parameterst::set(const optionst &options)
 {
   object_factory_parameterst::set(options);
@@ -50,6 +63,16 @@ void c_object_factory_parameterst::set(const optionst &options)
       this->pointers_to_treat_as_array, this->pointers_to_treat_as_array.end()),
     id2string);
 
+  auto const &pointers_to_treat_as_string =
+    options.get_list_option("pointers-to-treat-as-string");
+  std::transform(
+    std::begin(pointers_to_treat_as_string),
+    std::end(pointers_to_treat_as_string),
+    std::inserter(
+      this->pointers_to_treat_as_string,
+      this->pointers_to_treat_as_string.end()),
+    id2string);
+
   if(options.is_set("max-dynamic-array-size"))
   {
     max_dynamic_array_size =
@@ -117,8 +140,9 @@ optionalt<irep_idt> c_object_factory_parameterst::get_associated_size_variable(
     array_name_to_associated_array_size_variable, array_id);
 }
 
-bool c_object_factory_parameterst::should_be_treated_as_array(irep_idt id) const
+bool c_object_factory_parameterst::should_be_treated_as_string(
+  irep_idt id) const
 {
-  return pointers_to_treat_as_array.find(id) !=
-         pointers_to_treat_as_array.end();
+  return pointers_to_treat_as_string.find(id) !=
+         pointers_to_treat_as_string.end();
 }

src/ansi-c/c_object_factory_parameters.h

@@ -27,6 +27,7 @@ struct c_object_factory_parameterst final : public object_factory_parameterst
   }
 
   bool should_be_treated_as_array(irep_idt id) const;
+  bool should_be_treated_as_string(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;
 
@@ -38,6 +39,7 @@ struct c_object_factory_parameterst final : public object_factory_parameterst
   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;
+  std::set<irep_idt> pointers_to_treat_as_string;
 };
 
 /// Parse the c object factory parameters from a given command line