Merge pull request #5171 from xbauch/feature/function-harness-param-equal

Allow function pointer arguments to be equal

Author: petr-bauch

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

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  struct st *next;
+  int data;
+} st1_t;
+
+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-maybe/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 --treat-pointers-equal 'p,q;r,s,t' --treat-pointers-equal-maybe
+^EXIT=10$
+^SIGNAL=0$
+^\[func.assertion.\d+\] line \d+ assertion p == q: FAILURE$
+^\[func.assertion.\d+\] line \d+ assertion \(void \*\)p != \(void \*\)r: SUCCESS$
+^\[func.assertion.\d+\] line \d+ assertion r == s: FAILURE$
+^\[func.assertion.\d+\] line \d+ assertion r == t: FAILURE$
+VERIFICATION FAILED
+--
+^warning: ignoring

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

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st1
+{
+  struct st *next;
+  int data;
+} st1_t;
+
+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

@@ -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;r,s,t'
+^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::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;
 
@@ -112,6 +115,21 @@ 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_cluster : split_string(value, ';'))
+      {
+        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);
+      }
+    }
+  }
   else if(option == FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT)
   {
     for(auto const &array_size_pair : values)
@@ -151,6 +169,10 @@ void function_call_harness_generatort::handle_option(
     p_impl->function_parameters_to_treat_as_cstrings.insert(
       values.begin(), values.end());
   }
+  else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT)
+  {
+    p_impl->recursive_initialization_config.arguments_may_be_equal = true;
+  }
   else
   {
     throw invalid_command_line_argument_exceptiont{
@@ -183,6 +205,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)
@@ -199,9 +223,9 @@ void function_call_harness_generatort::implt::generate(
   call_function(arguments, function_body);
   for(const auto &global_pointer : global_pointers)
   {
-    function_body.add(code_function_callt{
-      recursive_initialization->get_free_function(), {global_pointer}});
+    recursive_initialization->free_if_possible(global_pointer, function_body);
   }
+  recursive_initialization->free_cluster_origins(function_body);
   add_harness_function_to_goto_model(std::move(function_body));
 }
 
@@ -238,7 +262,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 +282,49 @@ 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 &equal_cluster : p_impl->function_parameters_to_treat_equal)
+  {
+    for(auto const &pointer_id : equal_cluster)
+    {
+      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 &
@@ -365,6 +432,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;
 }
@@ -377,7 +460,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,18 +15,24 @@ 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                    \
   "treat-pointer-as-cstring"
+#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT              \
+  "treat-pointers-equal-maybe"
 
 // clang-format off
 #define FUNCTION_HARNESS_GENERATOR_OPTIONS                                     \
   "(" 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_TREAT_POINTERS_EQUAL_MAYBE_OPT ")"            \
 // FUNCTION_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on
@@ -43,6 +49,11 @@ 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,r[;s,t]    treat the function parameters `q,r' equal\n"                \
+  "                              to parameter `p'; `s` to `t` and so on\n"     \
+  "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT               \
+  "                function parameters equality is non-deterministic\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,13 +93,54 @@ 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)
 {
+  // 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)
+  {
+    const auto maybe_cluster_index =
+      find_equal_cluster(to_symbol_expr(lhs).get_identifier());
+    if(maybe_cluster_index.has_value())
+    {
+      if(common_arguments_origins[*maybe_cluster_index].has_value())
+      {
+        const auto set_equal_case =
+          code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]};
+        if(initialization_config.arguments_may_be_equal)
+        {
+          const irep_idt &fun_name = build_constructor(lhs);
+          const symbolt &fun_symbol =
+            goto_model.symbol_table.lookup_ref(fun_name);
+          const auto proper_init_case = code_function_callt{
+            fun_symbol.symbol_expr(), {depth, address_of_exprt{lhs}}};
+
+          body.add(code_ifthenelset{
+            side_effect_expr_nondett{bool_typet{}, source_locationt{}},
+            set_equal_case,
+            proper_init_case});
+        }
+        else
+        {
+          body.add(set_equal_case);
+        }
+        return;
+      }
+      else
+      {
+        common_arguments_origins[*maybe_cluster_index] = lhs;
+      }
+    }
+  }
+
   const irep_idt &fun_name = build_constructor(lhs);
   const symbolt &fun_symbol = goto_model.symbol_table.lookup_ref(fun_name);
 
@@ -280,6 +321,19 @@ bool recursive_initializationt::should_be_treated_as_array(
          initialization_config.pointers_to_treat_as_arrays.end();
 }
 
+optionalt<recursive_initializationt::equal_cluster_idt>
+recursive_initializationt::find_equal_cluster(const irep_idt &name) const
+{
+  for(equal_cluster_idt 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(
   const irep_idt &cmdline_arg) const
 {
@@ -763,3 +817,49 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
 
   return body;
 }
+
+bool recursive_initializationt::needs_freeing(const exprt &expr) const
+{
+  return expr.type().id() == ID_pointer && expr.type().id() != ID_code;
+}
+
+void recursive_initializationt::free_if_possible(
+  const exprt &expr,
+  code_blockt &body)
+{
+  PRECONDITION(expr.id() == ID_symbol);
+  const auto expr_id = to_symbol_expr(expr).get_identifier();
+  const auto maybe_cluster_index = find_equal_cluster(expr_id);
+  const auto call_free = code_function_callt{get_free_function(), {expr}};
+  if(!maybe_cluster_index.has_value())
+  {
+    // not in any equality cluster -> just free
+    body.add(call_free);
+    return;
+  }
+
+  if(
+    to_symbol_expr(*common_arguments_origins[*maybe_cluster_index])
+        .get_identifier() != expr_id &&
+    initialization_config.arguments_may_be_equal)
+  {
+    // in equality cluster but not common origin -> free if not equal to origin
+    const auto condition =
+      notequal_exprt{expr, *common_arguments_origins[*maybe_cluster_index]};
+    body.add(code_ifthenelset{condition, call_free});
+  }
+  else
+  {
+    // expr is common origin, leave freeing until the rest of the cluster is
+    // freed
+    return;
+  }
+}
+
+void recursive_initializationt::free_cluster_origins(code_blockt &body)
+{
+  for(auto const &origin : common_arguments_origins)
+  {
+    body.add(code_function_callt{get_free_function(), {*origin}});
+  }
+}