Allow function pointer arguments to be equal

for the function-call goto-harness.

We add a new command-line option `treat-pointers-equal` that takes a list of
formal parameter names and results in a harness that only generates constructor
for one of the pointers. The other pointers are simply assigned with the
constructed one.

Author: petr-bauch

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

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+void func(st_t *p, st_t *q)
+{
+  assert(p != NULL);
+  assert(p->next != NULL);
+
+  assert(p == q);
+}

regression/goto-harness/pointer-function-parameters-equal-simple/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --harness-type call-function --treat-pointers-equal p,q
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

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_equal;
+  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;
 
@@ -112,6 +115,16 @@ void function_call_harness_generatort::handle_option(
     p_impl->function_parameters_to_treat_as_arrays.insert(
       values.begin(), values.end());
   }
+  else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT)
+  {
+    for(auto const &value : values)
+    {
+      for(auto const &param_id : split_string(value, ','))
+      {
+        p_impl->function_parameters_to_treat_equal.insert(param_id);
+      }
+    }
+  }
   else if(option == FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT)
   {
     for(auto const &array_size_pair : values)
@@ -183,6 +196,8 @@ void function_call_harness_generatort::implt::generate(
   recursive_initialization_config.mode = function_to_call.mode;
   recursive_initialization_config.pointers_to_treat_as_arrays =
     function_arguments_to_treat_as_arrays;
+  recursive_initialization_config.pointers_to_treat_equal =
+    function_arguments_to_treat_equal;
   recursive_initialization_config.array_name_to_associated_array_size_variable =
     function_argument_to_associated_array_size;
   for(const auto &pair : function_argument_to_associated_array_size)
@@ -238,7 +253,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
 {
   recursive_initialization->initialize(
     lhs, from_integer(0, signed_int_type()), block);
-  if(lhs.type().id() == ID_pointer)
+  if(recursive_initialization->needs_freeing(lhs))
     global_pointers.insert(to_symbol_expr(lhs));
 }
 
@@ -258,6 +273,46 @@ void function_call_harness_generatort::validate_options(
       "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
       " --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
   }
+
+  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)
+  {
+    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())
+    {
+      if(formal_param.get_identifier() == decorated_pointer_id)
+      {
+        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(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();
+      }
+    }
+    if(!is_a_param)
+    {
+      throw invalid_command_line_argument_exceptiont{
+        id2string(pointer_id) + " is not a parameter",
+        "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
+    }
+  }
 }
 
 const symbolt &
@@ -348,6 +403,11 @@ 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())
     {
@@ -377,7 +437,7 @@ void function_call_harness_generatort::implt::call_function(
   for(auto const &argument : arguments)
   {
     generate_initialisation_code_for(function_body, argument);
-    if(argument.type().id() == ID_pointer)
+    if(recursive_initialization->needs_freeing(argument))
       global_pointers.insert(to_symbol_expr(argument));
   }
   code_function_callt function_call{function_to_call.symbol_expr(),

src/goto-harness/function_harness_generator_options.h

@@ -15,6 +15,8 @@ Author: Diffblue Ltd.
 #define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT "nondet-globals"
 #define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT                  \
   "treat-pointer-as-array"
+#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT                    \
+  "treat-pointers-equal"
 #define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT                   \
   "associated-array-size"
 #define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING                    \
@@ -25,6 +27,7 @@ Author: Diffblue Ltd.
   "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):"                             \
   "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")"                        \
   "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT "):"               \
+  "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT "):"                 \
   "(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT "):"                \
   "(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING "):"                 \
 // FUNCTION_HARNESS_GENERATOR_OPTIONS
@@ -43,6 +46,9 @@ Author: Diffblue Ltd.
   "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT                   \
   " 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"                           \
   "--" 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

@@ -100,6 +100,19 @@ void recursive_initializationt::initialize(
   const exprt &depth,
   code_blockt &body)
 {
+  if(
+    lhs.id() == ID_symbol &&
+    should_be_treated_equal(to_symbol_expr(lhs).get_identifier()))
+  {
+    if(common_arguments_origin.has_value())
+    {
+      body.add(code_assignt{lhs, *common_arguments_origin});
+      return;
+    }
+    else
+      common_arguments_origin = lhs;
+  }
+
   const irep_idt &fun_name = build_constructor(lhs);
   const symbolt &fun_symbol = goto_model.symbol_table.lookup_ref(fun_name);
 
@@ -280,6 +293,13 @@ 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
+{
+  return initialization_config.pointers_to_treat_equal.find(pointer_name) !=
+         initialization_config.pointers_to_treat_equal.end();
+}
+
 bool recursive_initializationt::is_array_size_parameter(
   const irep_idt &cmdline_arg) const
 {
@@ -763,3 +783,17 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
 
   return body;
 }
+
+bool recursive_initializationt::needs_freeing(const exprt &expr) const
+{
+  if(expr.type().id() != ID_pointer)
+    return false;
+  if(common_arguments_origin.has_value() && 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;
+  }
+  return true;
+}

src/goto-harness/recursive_initialization.h

@@ -37,6 +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::string to_string() const; // for debugging purposes
 
@@ -81,19 +82,23 @@ class recursive_initializationt
       !has_prefix(id2string(symbol.name), CPROVER_PREFIX));
   }
 
+  bool needs_freeing(const exprt &expr) const;
+
 private:
   const recursive_initialization_configt initialization_config;
   goto_modelt &goto_model;
   irep_idt max_depth_var_name;
   irep_idt min_depth_var_name;
   type_constructor_namest type_constructor_names;
+  optionalt<exprt> common_arguments_origin;
 
   /// 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;
   bool is_array_size_parameter(const irep_idt &cmdline_arg) const;
   optionalt<irep_idt>
   get_associated_size_variable(const irep_idt &array_name) const;