Extend to support multiple members for havocing

petr-bauch · petr-bauch · commit 65bfa600ff01 · 2020-01-28T12:52:54.000Z
via a comma-separated list. Plus one more test.
diff --git a/regression/goto-harness/select-multiple-members-to-havoc/main.c b/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);
+}
diff --git a/regression/goto-harness/select-multiple-members-to-havoc/test.desc b/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
diff --git a/regression/goto-harness/select-struct-member-to-havoc/test.desc b/regression/goto-harness/select-struct-member-to-havoc/test.desc
@@ -1,6 +1,6 @@
 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
+--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$
diff --git a/src/goto-harness/common_harness_generator_options.h b/src/goto-harness/common_harness_generator_options.h
@@ -16,7 +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"
+#define COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT "havoc-member"
 
 // clang-format off
 #define COMMON_HARNESS_GENERATOR_OPTIONS                                       \
@@ -25,7 +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_HAVOC_MEMBER_OPT "):"                           \
 // COMMON_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on
@@ -47,7 +47,7 @@ Author: Diffblue Ltd.
   "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT               \
   " <function-name>,  name of the function(s) pointer parameters\n"            \
   "              that can be NULL pointing."                                   \
-  "--" COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT                           \
+  "--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT                               \
   "              path to the member to be havoced\n"                           \
   // COMMON_HARNESS_GENERATOR_HELP
 
diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp
@@ -87,20 +87,26 @@ 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)
+  else if(option == COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT)
   {
-    auto selection_spec_strings = split_string(
+    const auto list_of_members_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};
-      });
+        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;
@@ -131,20 +137,22 @@ 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())
+  if(lhs.id() == ID_symbol && !initialization_config.selection_specs.empty())
   {
-    initialize_selected_member(lhs, depth, body);
-    return;
+    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
-  if(
-    lhs.id() == ID_symbol &&
-    should_be_treated_equal(to_symbol_expr(lhs).get_identifier()))
+  if(lhs.id() == ID_symbol)
   {
     const auto maybe_cluster_index =
       find_equal_cluster(to_symbol_expr(lhs).get_identifier());
@@ -987,24 +995,23 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
 void recursive_initializationt::initialize_selected_member(
   const exprt &lhs,
   const exprt &depth,
-  code_blockt &body)
+  code_blockt &body,
+  const std::vector<irep_idt> &selection_spec)
 {
   PRECONDITION(lhs.id() == ID_symbol);
   PRECONDITION(lhs.type().id() == ID_struct_tag);
-  PRECONDITION(!initialization_config.selection_spec.empty());
+  PRECONDITION(!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++)
+  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_MEMBER_SELECTION_OPT};
+        "--" 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));
@@ -1027,7 +1034,7 @@ void recursive_initializationt::initialize_selected_member(
     {
       throw invalid_command_line_argument_exceptiont{
         "'" + id2string(*it) + "' is not a component name",
-        "--" COMMON_HARNESS_GENERATOR_MEMBER_SELECTION_OPT};
+        "--" COMMON_HARNESS_GENERATOR_HAVOC_MEMBER_OPT};
     }
   }
   initialize(component_member, depth, body);
diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h
@@ -42,7 +42,7 @@ struct recursive_initialization_configt
 
   bool arguments_may_be_equal = false;
 
-  std::vector<irep_idt> selection_spec;
+  std::vector<std::vector<irep_idt>> selection_specs;
 
   std::string to_string() const; // for debugging purposes
 
@@ -271,10 +271,13 @@ class recursive_initializationt
   /// \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);
+    code_blockt &body,
+    const std::vector<irep_idt> &selection_spec);
 };
 
 #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
