Extend to allow conditional equality

between pointer arguments. Whether or not they will be equal is now a
non-deterministic choice. Freeing pointer had to be extended.

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

src/goto-harness/function_call_harness_generator.cpp

@@ -169,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{
@@ -219,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));
 }
 

src/goto-harness/function_harness_generator_options.h

@@ -21,6 +21,8 @@ Author: Diffblue Ltd.
   "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                                     \
@@ -30,6 +32,7 @@ Author: Diffblue Ltd.
   "(" 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
@@ -49,6 +52,8 @@ Author: Diffblue Ltd.
   "--" 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

@@ -102,6 +102,9 @@ void recursive_initializationt::initialize(
   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 =
@@ -110,8 +113,25 @@ void recursive_initializationt::initialize(
     {
       if(common_arguments_origins[*maybe_cluster_index].has_value())
       {
-        body.add(
-          code_assignt{lhs, *common_arguments_origins[*maybe_cluster_index]});
+        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
@@ -802,23 +822,47 @@ bool recursive_initializationt::needs_freeing(const exprt &expr) const
 {
   if(expr.type().id() != ID_pointer || expr.type().id() == ID_code)
     return false;
-  if(expr.id() == ID_symbol)
+  else
+    return true;
+}
+
+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())
   {
-    auto expr_name = to_symbol_expr(expr).get_identifier();
-    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;
-    }
+    // 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 equal to origin
+    const auto condition =
+      equal_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}});
   }
-  return true;
 }

src/goto-harness/recursive_initialization.h

@@ -39,6 +39,8 @@ struct recursive_initialization_configt
   std::set<irep_idt> pointers_to_treat_as_cstrings;
   std::vector<std::set<irep_idt>> pointers_to_treat_equal;
 
+  bool arguments_may_be_equal = false;
+
   std::string to_string() const; // for debugging purposes
 
   /// Parse the options specific for recursive initialisation
@@ -83,6 +85,8 @@ class recursive_initializationt
   }
 
   bool needs_freeing(const exprt &expr) const;
+  void free_if_possible(const exprt &expr, code_blockt &body);
+  void free_cluster_origins(code_blockt &body);
 
 private:
   const recursive_initialization_configt initialization_config;