Extend to clusters of equal parameters

Specified by a semi-colon separated list of comma separated names.

Author: petr-bauch

regression/goto-harness/pointer-function-parameters-equal-simple/main.c

@@ -1,16 +1,27 @@
 #include <assert.h>
 #include <stdlib.h>
 
-typedef struct st
+typedef struct st1
 {
   struct st *next;
   int data;
-} st_t;
+} st1_t;
 
-void func(st_t *p, st_t *q)
+typedef struct st2
+{
+  struct st *next;
+  int data;
+} st2_t;
+
+void func(st1_t *p, st1_t *q, st2_t *r, st2_t *s, st2_t *t)
 {
   assert(p != NULL);
   assert(p->next != NULL);
 
   assert(p == q);
+
+  assert((void *)p != (void *)r);
+
+  assert(r == s);
+  assert(r == t);
 }

regression/goto-harness/pointer-function-parameters-equal-simple/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 --treat-pointers-equal p,q
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal 'p,q;r,s,t'
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

src/goto-harness/function_call_harness_generator.cpp

@@ -48,8 +48,8 @@ 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_equal;
-  std::set<irep_idt> function_arguments_to_treat_equal;
+  std::vector<std::set<irep_idt>> function_parameters_to_treat_equal;
+  std::vector<std::set<irep_idt>> function_arguments_to_treat_equal;
 
   std::set<irep_idt> function_parameters_to_treat_as_cstrings;
   std::set<irep_idt> function_arguments_to_treat_as_cstrings;
@@ -119,9 +119,14 @@ void function_call_harness_generatort::handle_option(
   {
     for(auto const &value : values)
     {
-      for(auto const &param_id : split_string(value, ','))
+      for(auto const &param_cluster : split_string(value, ';'))
       {
-        p_impl->function_parameters_to_treat_equal.insert(param_id);
+        std::set<irep_idt> equal_param_set;
+        for(auto const &param_id : split_string(param_cluster, ','))
+        {
+          equal_param_set.insert(param_id);
+        }
+        p_impl->function_parameters_to_treat_equal.push_back(equal_param_set);
       }
     }
   }
@@ -276,41 +281,44 @@ void function_call_harness_generatort::validate_options(
 
   auto function_to_call = goto_model.symbol_table.lookup_ref(p_impl->function);
   auto ftype = to_code_type(function_to_call.type);
-  for(auto const &pointer_id : p_impl->function_parameters_to_treat_equal)
+  for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal)
   {
-    std::string decorated_pointer_id =
-      id2string(p_impl->function) + "::" + id2string(pointer_id);
-    bool is_a_param = false;
-    typet common_type = empty_typet{};
-    for(auto const &formal_param : ftype.parameters())
+    for(auto const &pointer_id : equal_cluster)
     {
-      if(formal_param.get_identifier() == decorated_pointer_id)
+      std::string decorated_pointer_id =
+        id2string(p_impl->function) + "::" + id2string(pointer_id);
+      bool is_a_param = false;
+      typet common_type = empty_typet{};
+      for(auto const &formal_param : ftype.parameters())
       {
-        is_a_param = true;
-        if(formal_param.type().id() != ID_pointer)
-        {
-          throw invalid_command_line_argument_exceptiont{
-            id2string(pointer_id) + " is not a pointer parameter",
-            "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
-        }
-        if(common_type.id() != ID_empty)
+        if(formal_param.get_identifier() == decorated_pointer_id)
         {
-          if(common_type != formal_param.type())
+          is_a_param = true;
+          if(formal_param.type().id() != ID_pointer)
           {
             throw invalid_command_line_argument_exceptiont{
-              "pointer arguments of conflicting type",
+              id2string(pointer_id) + " is not a pointer parameter",
               "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
           }
+          if(common_type.id() != ID_empty)
+          {
+            if(common_type != formal_param.type())
+            {
+              throw invalid_command_line_argument_exceptiont{
+                "pointer arguments of conflicting type",
+                "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
+            }
+          }
+          else
+            common_type = formal_param.type();
         }
-        else
-          common_type = formal_param.type();
       }
-    }
-    if(!is_a_param)
-    {
-      throw invalid_command_line_argument_exceptiont{
-        id2string(pointer_id) + " is not a parameter",
-        "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
+      if(!is_a_param)
+      {
+        throw invalid_command_line_argument_exceptiont{
+          id2string(pointer_id) + " is not a parameter",
+          "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
+      }
     }
   }
 }
@@ -403,11 +411,6 @@ function_call_harness_generatort::implt::declare_arguments(
       function_arguments_to_treat_as_cstrings.insert(argument_name);
     }
 
-    if(function_parameters_to_treat_equal.count(parameter_name) != 0)
-    {
-      function_arguments_to_treat_equal.insert(argument_name);
-    }
-
     auto it = function_parameter_to_associated_array_size.find(parameter_name);
     if(it != function_parameter_to_associated_array_size.end())
     {
@@ -425,6 +428,22 @@ function_call_harness_generatort::implt::declare_arguments(
         {argument_name, associated_array_size_argument->second});
     }
   }
+
+  // translate the parameter to argument also in the equality clusters
+  for(auto const &equal_cluster : function_parameters_to_treat_equal)
+  {
+    std::set<irep_idt> cluster_argument_names;
+    for(auto const &parameter_name : equal_cluster)
+    {
+      INVARIANT(
+        parameter_name_to_argument_name.count(parameter_name) != 0,
+        id2string(parameter_name) + " is not a parameter");
+      cluster_argument_names.insert(
+        parameter_name_to_argument_name[parameter_name]);
+    }
+    function_arguments_to_treat_equal.push_back(cluster_argument_names);
+  }
+
   allocate_objects.declare_created_symbols(function_body);
   return arguments;
 }

src/goto-harness/function_harness_generator_options.h

@@ -47,8 +47,8 @@ Author: Diffblue Ltd.
   " p    treat the function parameter with the name `p' as\n"                  \
   "                              an array\n"                                   \
   "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT                     \
-  " p,q    treat the function parameter with the name `q' equal\n"             \
-  "                              to parameter `q'\n"                           \
+  " p,q,r[;s,t]    treat the function parameters `q,r' equal\n"                \
+  "                              to parameter `p'; `s` to `t` and so on\n"     \
   "--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT                    \
   " array_name:size_name\n"                                                    \
   "                              set the parameter <size_name> to the size"    \

src/goto-harness/recursive_initialization.cpp

@@ -93,24 +93,32 @@ recursive_initializationt::recursive_initializationt(
         initialization_config.min_null_tree_depth,
         signed_int_type())))
 {
+  common_arguments_origins.resize(
+    this->initialization_config.pointers_to_treat_equal.size());
 }
 
 void recursive_initializationt::initialize(
   const exprt &lhs,
   const exprt &depth,
   code_blockt &body)
 {
-  if(
-    lhs.id() == ID_symbol &&
-    should_be_treated_equal(to_symbol_expr(lhs).get_identifier()))
+  if(lhs.id() == ID_symbol)
   {
-    if(common_arguments_origin.has_value())
+    const auto maybe_cluster_index =
+      find_equal_cluster(to_symbol_expr(lhs).get_identifier());
+    if(maybe_cluster_index.has_value())
     {
-      body.add(code_assignt{lhs, *common_arguments_origin});
-      return;
+      if(common_arguments_origins[*maybe_cluster_index].has_value())
+      {
+        body.add(
+          code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]});
+        return;
+      }
+      else
+      {
+        common_arguments_origins[*maybe_cluster_index] = lhs;
+      }
     }
-    else
-      common_arguments_origin = lhs;
   }
 
   const irep_idt &fun_name = build_constructor(lhs);
@@ -293,11 +301,17 @@ bool recursive_initializationt::should_be_treated_as_array(
          initialization_config.pointers_to_treat_as_arrays.end();
 }
 
-bool recursive_initializationt::should_be_treated_equal(
-  const irep_idt &pointer_name) const
+optionalt<std::size_t>
+recursive_initializationt::find_equal_cluster(const irep_idt &name) const
 {
-  return initialization_config.pointers_to_treat_equal.find(pointer_name) !=
-         initialization_config.pointers_to_treat_equal.end();
+  for(size_t index = 0;
+      index != initialization_config.pointers_to_treat_equal.size();
+      ++index)
+  {
+    if(initialization_config.pointers_to_treat_equal[index].count(name) != 0)
+      return index;
+  }
+  return {};
 }
 
 bool recursive_initializationt::is_array_size_parameter(
@@ -786,14 +800,25 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
 
 bool recursive_initializationt::needs_freeing(const exprt &expr) const
 {
-  if(expr.type().id() != ID_pointer)
+  if(expr.type().id() != ID_pointer || expr.type().id() == ID_code)
     return false;
-  if(common_arguments_origin.has_value() && expr.id() == ID_symbol)
+  if(expr.id() == ID_symbol)
   {
-    auto origin_name =
-      to_symbol_expr(*common_arguments_origin).get_identifier();
     auto expr_name = to_symbol_expr(expr).get_identifier();
-    return origin_name == expr_name;
+    if(find_equal_cluster(expr_name).has_value())
+    {
+      for(auto const &origin_expr : common_arguments_origins)
+      {
+        if(!origin_expr.has_value())
+          continue;
+        INVARIANT(
+          origin_expr->id() == ID_symbol, "common origin is not a symbol");
+        auto origin_name = to_symbol_expr(*origin_expr).get_identifier();
+        if(origin_name == expr_name)
+          return true;
+      }
+      return false;
+    }
   }
   return true;
 }

src/goto-harness/recursive_initialization.h

@@ -37,7 +37,7 @@ struct recursive_initialization_configt
   std::map<irep_idt, irep_idt> array_name_to_associated_array_size_variable;
 
   std::set<irep_idt> pointers_to_treat_as_cstrings;
-  std::set<irep_idt> pointers_to_treat_equal;
+  std::vector<std::set<irep_idt>> pointers_to_treat_equal;
 
   std::string to_string() const; // for debugging purposes
 
@@ -90,15 +90,15 @@ class recursive_initializationt
   irep_idt max_depth_var_name;
   irep_idt min_depth_var_name;
   type_constructor_namest type_constructor_names;
-  optionalt<exprt> common_arguments_origin;
+  std::vector<optionalt<exprt>> common_arguments_origins;
 
   /// Get the malloc function as symbol exprt,
   /// and inserts it into the goto-model if it doesn't
   /// exist already.
   symbol_exprt get_malloc_function();
 
   bool should_be_treated_as_array(const irep_idt &pointer_name) const;
-  bool should_be_treated_equal(const irep_idt &pointer_name) const;
+  optionalt<std::size_t> find_equal_cluster(const irep_idt &name) const;
   bool is_array_size_parameter(const irep_idt &cmdline_arg) const;
   optionalt<irep_idt>
   get_associated_size_variable(const irep_idt &array_name) const;