Add support for nondet initialisation of strings.

Add support for nondet-initialisation of strings in
the function-call goto-harness leveraging pointer
nondet initialisation.

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

Author: NlightNFotis

regression/goto-harness/nondet_strings/main.c

@@ -0,0 +1,6 @@
+#include <assert.h>
+
+void function(char *pointer, int size)
+{
+  assert(pointer[size - 1] == '\0');
+}

regression/goto-harness/nondet_strings/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--harness-type call-function --function function --treat-pointer-as-cstring pointer --associated-array-size pointer:size
+\[function.assertion.\d+\] line \d+ assertion pointer\[size - 1\] == \'\\0\': SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--

src/goto-harness/function_call_harness_generator.cpp

@@ -48,6 +48,9 @@ struct function_call_harness_generatort::implt
   std::set<irep_idt> function_parameters_to_treat_as_arrays;
   std::set<irep_idt> function_arguments_to_treat_as_arrays;
 
+  std::set<irep_idt> function_parameters_to_treat_as_cstrings;
+  std::set<irep_idt> function_arguments_to_treat_as_cstrings;
+
   std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
   std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
 
@@ -178,6 +181,11 @@ void function_call_harness_generatort::handle_option(
       }
     }
   }
+  else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING)
+  {
+    p_impl->function_parameters_to_treat_as_cstrings.insert(
+      values.begin(), values.end());
+  }
   else
   {
     throw invalid_command_line_argument_exceptiont{
@@ -217,6 +225,15 @@ void function_call_harness_generatort::implt::generate(
     recursive_initialization_config.variables_that_hold_array_sizes.insert(
       pair.second);
   }
+  recursive_initialization_config.pointers_to_treat_as_cstrings =
+    function_arguments_to_treat_as_cstrings;
+  // std::transform(
+  //   function_argument_to_associated_array_size.begin(),
+  //   function_argument_to_associated_array_size.end(),
+  //   std::inserter(
+  //     recursive_initialization_config.variables_that_hold_array_sizes,
+  //     recursive_initialization_config.variables_that_hold_array_sizes.end()),
+  //   [](const std::pair<irep_idt, irep_idt> &p) { return p.second; });
   recursive_initialization = util_make_unique<recursive_initializationt>(
     recursive_initialization_config, goto_model);
 
@@ -385,6 +402,12 @@ function_call_harness_generatort::implt::declare_arguments(
     {
       function_arguments_to_treat_as_arrays.insert(argument_name);
     }
+
+    if(function_parameters_to_treat_as_cstrings.count(parameter_name) != 0)
+    {
+      function_arguments_to_treat_as_cstrings.insert(argument_name);
+    }
+
     auto it = function_parameter_to_associated_array_size.find(parameter_name);
     if(it != function_parameter_to_associated_array_size.end())
     {

src/goto-harness/function_harness_generator_options.h

@@ -20,6 +20,8 @@ Author: Diffblue Ltd.
   "treat-pointer-as-array"
 #define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT                   \
   "associated-array-size"
+#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING                    \
+  "treat-pointer-as-cstring"
 
 // clang-format off
 #define FUNCTION_HARNESS_GENERATOR_OPTIONS                                     \
@@ -31,6 +33,7 @@ Author: Diffblue Ltd.
   "(" 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_TREAT_POINTER_AS_CSTRING "):"                 \
 // FUNCTION_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on

src/goto-harness/recursive_initialization.cpp

@@ -17,6 +17,8 @@ Author: Diffblue Ltd.
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
+#include <functional>
+
 recursive_initializationt::recursive_initializationt(
   recursive_initialization_configt initialization_config,
   goto_modelt &goto_model)
@@ -38,20 +40,27 @@ void recursive_initializationt::initialize(
   }
   else if(type.id() == ID_pointer)
   {
-    if(
-      lhs.id() == ID_symbol &&
-      should_be_treated_as_array(to_symbol_expr(lhs).get_identifier()))
+    if(lhs.id() == ID_symbol)
     {
-      initialize_dynamic_array(lhs, depth, known_tags, body);
-    }
-    else
-    {
-      initialize_pointer(lhs, depth, known_tags, body);
+      auto const &lhs_symbol = to_symbol_expr(lhs);
+      if(should_be_treated_as_cstring(lhs_symbol.get_identifier()))
+      {
+        initialize_cstring(lhs, depth, known_tags, body);
+        return;
+      }
+      else if(should_be_treated_as_array(lhs_symbol.get_identifier()))
+      {
+        initialize_dynamic_array(
+          lhs, depth, known_tags, body, default_array_member_initialization());
+        return;
+      }
     }
+    initialize_pointer(lhs, depth, known_tags, body);
   }
   else if(type.id() == ID_array)
   {
-    initialize_array(lhs, depth, known_tags, body);
+    initialize_array(
+      lhs, depth, known_tags, body, default_array_member_initialization());
   }
   else
   {
@@ -163,19 +172,17 @@ void recursive_initializationt::initialize_array(
   const exprt &array,
   const std::size_t depth,
   const recursion_sett &known_tags,
-  code_blockt &body)
+  code_blockt &body,
+  array_convertert array_member_initialization)
 {
   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);
+    array_member_initialization(
+      array, array_size, index, depth, known_tags, body);
   }
 }
 
@@ -202,11 +209,19 @@ optionalt<irep_idt> recursive_initializationt::get_associated_size_variable(
     array_name);
 }
 
+bool recursive_initializationt::should_be_treated_as_cstring(
+  const irep_idt &pointer_name) const
+{
+  return initialization_config.pointers_to_treat_as_cstrings.count(
+           pointer_name) != 0;
+}
+
 void recursive_initializationt::initialize_dynamic_array(
   const exprt &pointer,
   const std::size_t depth,
   const recursion_sett &known_tags,
-  code_blockt &body)
+  code_blockt &body,
+  array_convertert array_initialization)
 {
   PRECONDITION(pointer.type().id() == ID_pointer);
 
@@ -269,7 +284,8 @@ void recursive_initializationt::initialize_dynamic_array(
     std::size_t array_counter = 0;
     for(const auto &array_variable : array_variables)
     {
-      initialize(array_variable, depth + 1, known_tags, body);
+      initialize_array(
+      array_variable, depth + 1, known_tags, body, array_initialization);
       body.add(code_assignt{
         index_exprt{arrays, from_integer(array_counter++, size_type())},
         address_of_exprt{
@@ -303,6 +319,16 @@ void recursive_initializationt::initialize_dynamic_array(
   body.add(code_assignt{pointer, index_exprt{arrays, nondet_index}});
 }
 
+void recursive_initializationt::initialize_cstring(
+  const exprt &pointer,
+  std::size_t depth,
+  const recursion_sett &known_tags,
+  code_blockt &body)
+{
+  initialize_dynamic_array(
+    pointer, depth, known_tags, body, cstring_member_initialization());
+}
+
 std::string recursive_initialization_configt::to_string() const
 {
   std::ostringstream out{};
@@ -332,6 +358,57 @@ std::string recursive_initialization_configt::to_string() const
         << associated_array_size.second;
   }
   out << "\n  ]";
+  out << "\n  pointers_to_treat_as_cstrings = [";
+  for(const auto &pointer_to_treat_as_string_name :
+      pointers_to_treat_as_cstrings)
+  {
+    out << "\n    " << pointer_to_treat_as_string_name << std::endl;
+  }
+  out << "\n  ]";
   out << "\n}";
   return out.str();
 }
+
+recursive_initializationt::array_convertert
+recursive_initializationt::default_array_member_initialization()
+{
+  return [this](
+           const exprt &array,
+           const std::size_t length,
+           const std::size_t current_index,
+           const std::size_t depth,
+           const recursion_sett &known_tags,
+           code_blockt &body) {
+    PRECONDITION(array.type().id() == ID_array);
+    initialize(
+      index_exprt{array, from_integer(current_index, size_type())},
+      depth,
+      known_tags,
+      body);
+  };
+}
+
+recursive_initializationt::array_convertert
+recursive_initializationt::cstring_member_initialization()
+{
+  return [this](
+           const exprt &array,
+           const std::size_t length,
+           const std::size_t current_index,
+           const std::size_t depth,
+           const recursion_sett &known_tags,
+           code_blockt &body) {
+    PRECONDITION(array.type().id() == ID_array);
+    PRECONDITION(array.type().subtype() == char_type());
+    auto const member =
+      index_exprt{array, from_integer(current_index, size_type())};
+    if(current_index + 1 == length)
+    {
+      body.add(code_assignt{member, from_integer(0, array.type().subtype())});
+    }
+    else
+    {
+      initialize(member, depth, known_tags, body);
+    }
+  };
+}

src/goto-harness/recursive_initialization.h

@@ -32,6 +32,8 @@ struct recursive_initialization_configt
   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_cstrings;
+
   std::string to_string() const; // for debugging purposes
 };
 
@@ -81,12 +83,31 @@ class recursive_initializationt
     std::size_t depth,
     const recursion_sett &known_tags,
     code_blockt &body);
+
+  using array_convertert = std::function<void(
+    const exprt &pointer,
+    std::size_t length,
+    std::size_t current_index,
+    std::size_t depth,
+    const recursion_sett &known_tags,
+    code_blockt &body)>;
+  array_convertert default_array_member_initialization();
+  array_convertert cstring_member_initialization();
+
   void initialize_array(
     const exprt &array,
     std::size_t depth,
     const recursion_sett &known_tags,
-    code_blockt &body);
+    code_blockt &body,
+    array_convertert array_member_initialization);
   void initialize_dynamic_array(
+    const exprt &pointer,
+    std::size_t depth,
+    const recursion_sett &known_tags,
+    code_blockt &body,
+    array_convertert array_member_initialization);
+
+  void initialize_cstring(
     const exprt &pointer,
     std::size_t depth,
     const recursion_sett &known_tags,
@@ -96,6 +117,7 @@ class recursive_initializationt
   bool is_array_size_parameter(const irep_idt &cmdline_arg) const;
   optionalt<irep_idt>
   get_associated_size_variable(const irep_idt &array_name) const;
+  bool should_be_treated_as_cstring(const irep_idt &pointer_name) const;
 };
 
 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H