Merge pull request diffblue#4285 from NlightNFotis/nondet-strings

Add nondet initialisation of strings in goto-harness.

Author: NlightNFotis

doc/cprover-manual/goto-harness.md

@@ -261,3 +261,52 @@ options.
 If you have a function that takes an array parameter, but without an associated
 size parameter, you can also use the `--treat-pointer-as-array <parameter-name>`
 option.
+
+---
+
+If you want to non-deterministically initialise a pointer
+as a C string (character array with last element `'\0'`)
+then you can do that like this:
+
+``` C
+// nondet_string.c
+
+#include <assert.h>
+
+void function(char *pointer, int size)
+{
+  assert(pointer[size-1] == '\0');
+}
+```
+
+Then call the following:
+
+```
+$ goto-cc -o nondet_string.gb nondet_string.c
+$ goto-harness \
+  --harness-function-name harness \
+  --harness-type call-function \
+  --function function \
+  --treat-pointer-as-cstring pointer \
+  --associated-array-size pointer:size \
+  nondet_string.gb nondet_string-mod.gb
+$ cbmc --function harness nondet_string-mod.gb
+```
+
+Note that C strings are supported by the same mechanism
+behind the non-deterministic initialisation of pointers
+and arrays, so the same command line arguments apply, in
+particular `--associated-array-size`.
+
+This will result in:
+
+```
+[...]
+
+** Results:
+main.c function function
+[function.assertion.1] line 5 assertion pointer[size-1] == '\0': SUCCESS
+
+** 0 of 1 failed (1 iterations)
+VERIFICATION SUCCESSFUL
+```

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$
+--

regression/goto-harness/nondet_strings_failing_assertion/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int stringlength(char *s)
+{
+  int counter = 0;
+  while(*s++ != 0)
+    counter++;
+  return counter;
+}
+
+void calling_func(char *s, int length)
+{
+  // WRONG: This should be stringlength(s)
+  // +1 because length is going to be length
+  // of the array, not the string
+  assert(stringlength(s) == length);
+}

regression/goto-harness/nondet_strings_failing_assertion/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--harness-type call-function --function calling_func --treat-pointer-as-cstring s --associated-array-size s:length
+\[calling_func.assertion.\d+\] line \d+ assertion stringlength\(s\) == length: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/goto-harness/nondet_strings_should_only_have_zero_at_end/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int stringlength(char *s)
+{
+  int counter = 0;
+  while(*s++ != 0)
+    counter++;
+  return counter;
+}
+
+void calling_func(char *s, int length)
+{
+  // +1 because length is going to be length
+  // of the array, not the string
+  assert(stringlength(s) + 1 == length);
+}

regression/goto-harness/nondet_strings_should_only_have_zero_at_end/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--harness-type call-function --function calling_func --treat-pointer-as-cstring s --associated-array-size s:length
+\[calling_func.assertion.\d+\] line \d+ assertion stringlength\(s\) \+ 1 == length: 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,8 @@ 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;
   recursive_initialization = util_make_unique<recursive_initializationt>(
     recursive_initialization_config, goto_model);
 
@@ -385,6 +395,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,60 @@ 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);
+      // We shouldn't have `\0` anywhere but at the end of a string.
+      body.add(code_assumet{
+        notequal_exprt{member, from_integer(0, array.type().subtype())}});
+    }
+  };
+}