Merge pull request #5183 from xbauch/feature/selective-struct-havoc

Goto-harness support to selectively havoc struct members

Author: hannes-steffenhagen-diffblue

regression/goto-harness/select-multiple-members-to-havoc/main.c

@@ -0,0 +1,46 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  int data11;
+  struct innert1
+  {
+    int inner_data11;
+    int inner_data12;
+  } inner1;
+  int data12;
+} st1_t;
+
+typedef struct st2
+{
+  int data21;
+  struct innert2
+  {
+    int inner_data21;
+    int inner_data22;
+  } inner2;
+  int data22;
+} st2_t;
+
+st1_t dummy1 = {.data11 = 0,
+                .inner1.inner_data11 = 0,
+                .inner1.inner_data12 = 0,
+                .data12 = 0};
+
+st2_t dummy2 = {.data21 = 0,
+                .inner2.inner_data21 = 0,
+                .inner2.inner_data22 = 0,
+                .data22 = 0};
+
+void func(st1_t *p)
+{
+  assert(dummy1.data11 == 0); //should succeed
+  assert(dummy1.inner1.inner_data11 == 0);
+  assert(dummy1.inner1.inner_data12 == 0); //should fail
+  assert(dummy1.data12 == 0);
+  assert(dummy2.data21 == 0);              //should succeed
+  assert(dummy2.inner2.inner_data21 == 0); //should fail
+  assert(dummy2.inner2.inner_data22 == 0);
+  assert(dummy2.data22 == 0);
+}

regression/goto-harness/select-multiple-members-to-havoc/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --havoc-member 'dummy1.inner1.inner_data12,dummy2.inner2.inner_data21' --nondet-globals
+^\[func.assertion.\d+\] line \d+ assertion dummy1.data11 == 0: SUCCESS$
+^\[func.assertion.\d+\] line \d+ assertion dummy1.inner1.inner_data11 == 0: SUCCESS$
+^\[func.assertion.\d+\] line \d+ assertion dummy1.inner1.inner_data12 == 0: FAILURE$
+^\[func.assertion.\d+\] line \d+ assertion dummy1.data12 == 0: SUCCESS$
+^\[func.assertion.\d+\] line \d+ assertion dummy2.inner2.inner_data21 == 0: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+--
+^warning: ignoring

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 --havoc-member '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_HAVOC_MEMBER_OPT "havoc-member"
 
 // 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_HAVOC_MEMBER_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_HAVOC_MEMBER_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,28 @@ bool recursive_initialization_configt::handle_option(
       [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
     return true;
   }
+  else if(option == COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT)
+  {
+    const auto list_of_members_string =
+      harness_options_parser::require_exactly_one_value(
+        COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT, values);
+    const auto list_of_members = split_string(list_of_members_string, ',');
+    for(const auto &member : list_of_members)
+    {
+      const auto selection_spec_strings = split_string(member, '.');
+
+      selection_specs.push_back({});
+      auto &selection_spec = selection_specs.back();
+      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,6 +137,18 @@ void recursive_initializationt::initialize(
   const exprt &depth,
   code_blockt &body)
 {
+  if(lhs.id() == ID_symbol && !initialization_config.selection_specs.empty())
+  {
+    auto lhs_id = to_symbol_expr(lhs).get_identifier();
+    for(const auto &selection_spec : initialization_config.selection_specs)
+    {
+      if(selection_spec.front() == lhs_id)
+      {
+        initialize_selected_member(lhs, depth, body, selection_spec);
+        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
@@ -956,3 +991,51 @@ 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,
+  const std::vector<irep_idt> &selection_spec)
+{
+  PRECONDITION(lhs.id() == ID_symbol);
+  PRECONDITION(lhs.type().id() == ID_struct_tag);
+  PRECONDITION(!selection_spec.empty());
+
+  auto component_member = lhs;
+  const namespacet ns{goto_model.symbol_table};
+
+  for(auto it = selection_spec.begin() + 1; it != 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_HAVOC_MEMBER_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_HAVOC_MEMBER_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<std::vector<irep_idt>> selection_specs;
+
   std::string to_string() const; // for debugging purposes
 
   /// Parse the options specific for recursive initialisation
@@ -263,6 +265,19 @@ 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
+  /// \param selection_spec: the user specification of the particular member to
+  ///   havoc
+  void initialize_selected_member(
+    const exprt &lhs,
+    const exprt &depth,
+    code_blockt &body,
+    const std::vector<irep_idt> &selection_spec);
 };
 
 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H