Add support to selectively havoc struct members

to goto-harness. By means of a new option `member-selection` the user can now
specify a struct-within-struct path, e.g. `struct_outer.struct_inner.data` to
specify only which member they want to havoc. Includes a test.

Author: petr-bauch

regression/goto-harness/select-struct-member-to-havoc/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  int data1;
+  struct innert
+  {
+    int inner_data1;
+    int inner_data2;
+  } inner;
+  int data2;
+} st_t;
+
+st_t dummy = {.data1 = 0,
+              .inner.inner_data1 = 0,
+              .inner.inner_data2 = 0,
+              .data2 = 0};
+
+void func(st_t *p)
+{
+  assert(dummy.data1 == 0); //should succeed
+  assert(dummy.inner.inner_data1 == 0);
+  assert(dummy.inner.inner_data2 == 0); //should fail
+  assert(dummy.data2 == 0);
+}

regression/goto-harness/select-struct-member-to-havoc/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --member-selection 'dummy.inner.inner_data2' --nondet-globals
+^\[func.assertion.\d+\] line \d+ assertion dummy.data1 == 0: SUCCESS$
+^\[func.assertion.\d+\] line \d+ assertion dummy.inner.inner_data1 == 0: SUCCESS$
+^\[func.assertion.\d+\] line \d+ assertion dummy.inner.inner_data2 == 0: FAILURE$
+^\[func.assertion.\d+\] line \d+ assertion dummy.data2 == 0: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+--
+^warning: ignoring

src/goto-harness/common_harness_generator_options.h

@@ -16,6 +16,7 @@ Author: Diffblue Ltd.
 #define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size"
 #define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT              \
   "function-pointer-can-be-null"
+#define COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT "member-selection"
 
 // clang-format off
 #define COMMON_HARNESS_GENERATOR_OPTIONS                                       \
@@ -24,6 +25,7 @@ Author: Diffblue Ltd.
   "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):"                         \
   "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):"                         \
   "(" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT "):"           \
+  "(" COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT "):"                       \
 // COMMON_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on
@@ -44,7 +46,9 @@ Author: Diffblue Ltd.
   "                              (default: 2)\n"                               \
   "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT               \
   " <function-name>,  name of the function(s) pointer parameters\n"            \
-  "              that can be NULL pointing."
+  "              that can be NULL pointing."                                   \
+  "--" COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT                           \
+  "              path to the member to be havoced\n"                           \
   // COMMON_HARNESS_GENERATOR_HELP
 
 // clang-format on

src/goto-harness/recursive_initialization.cpp

@@ -19,6 +19,7 @@ Author: Diffblue Ltd.
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
+#include <util/string_utils.h>
 
 #include <functional>
 #include <iterator>
@@ -86,6 +87,22 @@ bool recursive_initialization_configt::handle_option(
       [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
     return true;
   }
+  else if(option == COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT)
+  {
+    auto selection_spec_strings = split_string(
+      harness_options_parser::require_exactly_one_value(
+        COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT, values),
+      '.');
+
+    std::transform(
+      selection_spec_strings.begin(),
+      selection_spec_strings.end(),
+      std::back_inserter(selection_spec),
+      [](const std::string &member_name_string) {
+        return irep_idt{member_name_string};
+      });
+    return true;
+  }
   return false;
 }
 
@@ -114,10 +131,20 @@ void recursive_initializationt::initialize(
   const exprt &depth,
   code_blockt &body)
 {
+  if(
+    lhs.id() == ID_symbol && !initialization_config.selection_spec.empty() &&
+    initialization_config.selection_spec.front() ==
+      to_symbol_expr(lhs).get_identifier())
+  {
+    initialize_selected_member(lhs, depth, body);
+    return;
+  }
   // special handling for the case that pointer arguments should be treated
   // equal: if the equality is enforced (rather than the pointers may be equal),
   // then we don't even build the constructor functions
-  if(lhs.id() == ID_symbol)
+  if(
+    lhs.id() == ID_symbol &&
+    should_be_treated_equal(to_symbol_expr(lhs).get_identifier()))
   {
     const auto maybe_cluster_index =
       find_equal_cluster(to_symbol_expr(lhs).get_identifier());
@@ -956,3 +983,52 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
 
   return body;
 }
+
+void recursive_initializationt::initialize_selected_member(
+  const exprt &lhs,
+  const exprt &depth,
+  code_blockt &body)
+{
+  PRECONDITION(lhs.id() == ID_symbol);
+  PRECONDITION(lhs.type().id() == ID_struct_tag);
+  PRECONDITION(!initialization_config.selection_spec.empty());
+
+  auto component_member = lhs;
+  const namespacet ns{goto_model.symbol_table};
+
+  for(auto it = initialization_config.selection_spec.begin() + 1;
+      it != initialization_config.selection_spec.end();
+      it++)
+  {
+    if(component_member.type().id() != ID_struct_tag)
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "'" + id2string(*it) + "' is not a component name",
+        "--" COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT};
+    }
+    const auto &struct_tag_type = to_struct_tag_type(component_member.type());
+    const auto &struct_type = to_struct_type(ns.follow_tag(struct_tag_type));
+
+    bool found = false;
+    for(auto const &component : struct_type.components())
+    {
+      const auto &component_type = component.type();
+      const auto component_name = component.get_name();
+
+      if(*it == component_name)
+      {
+        component_member =
+          member_exprt{component_member, component_name, component_type};
+        found = true;
+        break;
+      }
+    }
+    if(!found)
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "'" + id2string(*it) + "' is not a component name",
+        "--" COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT};
+    }
+  }
+  initialize(component_member, depth, body);
+}

src/goto-harness/recursive_initialization.h

@@ -42,6 +42,8 @@ struct recursive_initialization_configt
 
   bool arguments_may_be_equal = false;
 
+  std::vector<irep_idt> selection_spec;
+
   std::string to_string() const; // for debugging purposes
 
   /// Parse the options specific for recursive initialisation
@@ -263,6 +265,16 @@ class recursive_initializationt
   /// \param result: symbol of the result parameter
   /// \return the body of the constructor
   code_blockt build_array_string_constructor(const symbol_exprt &result) const;
+
+  /// Select the specified struct-member to be non-deterministically
+  ///   initialized.
+  /// \param lhs: symbol expression of the top structure
+  /// \param depth: only to be passed
+  /// \param body: code block for the initializing assignment
+  void initialize_selected_member(
+    const exprt &lhs,
+    const exprt &depth,
+    code_blockt &body);
 };
 
 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H