Add support for function pointers to goto-harness

Also add support for having multiple constructors for the
same type with different behaviours and different signatures.
We are doing this because we need some types to be sometimes
nullable and sometimes not, and for example, for arrays we
sometimes need to pass a size parameter and sometimes not.

Author: NlightNFotis

regression/goto-harness/function_pointer_argument/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+typedef int (*fptr)(int a, int b);
+
+int max_normal(int first, int second)
+{
+  return first >= second ? first : second;
+}
+
+int max_crazy(int first, int second)
+{
+  return first >= second ? second : first;
+}
+
+void use_fptr(fptr max, int first, int second)
+{
+  int m = max(first, second);
+  assert(m == first || m == second);
+  assert(m >= first && m >= second);
+}

regression/goto-harness/function_pointer_argument/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.c
+--harness-type call-function --harness-function-name harness --function use_fptr
+^EXIT=10$
+^SIGNAL=0$
+\[use_fptr.assertion.1\] line \d+ assertion m == first \|\| m == second: SUCCESS
+\[use_fptr.assertion.2\] line \d+ assertion m >= first && m >= second: FAILURE
+--
+^warning: ignoring

regression/goto-harness/function_pointer_nullable/test.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef int (*fptr_t)(void);
+
+void entry_point(fptr_t f, fptr_t f_but_may_be_null)
+{
+  assert(f != (void *)0);                 // expected to succeed
+  assert(f == (void *)0);                 // expected to fail
+  assert(f_but_may_be_null != (void *)0); // expected to fail
+  assert(f_but_may_be_null == (void *)0); // expected to fail
+  assert(f_but_may_be_null == (void *)0 || f() == f_but_may_be_null());
+}
+
+int f(void)
+{
+  return 42;
+}

regression/goto-harness/function_pointer_nullable/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--harness-type call-function --function entry_point --function-pointer-can-be-null __goto_harness::f_but_may_be_null
+^EXIT=10$
+^SIGNAL=0$
+\[entry_point.assertion.1\] line \d+ assertion f != \(void \*\)0: SUCCESS
+\[entry_point.assertion.2\] line \d+ assertion f == \(void \*\)0: FAILURE
+\[entry_point.assertion.3\] line \d+ assertion f_but_may_be_null != \(void \*\)0: FAILURE
+\[entry_point.assertion.4\] line \d+ assertion f_but_may_be_null == \(void \*\)0: FAILURE
+\[entry_point.assertion.5\] line \d+ assertion f_but_may_be_null == \(void \*\)0 || f\(\) == f_but_may_be_null\(\): SUCCESS
+--
+^warning: ignoring

src/goto-harness/common_harness_generator_options.h

@@ -14,13 +14,16 @@ Author: Diffblue Ltd.
   "max-nondet-tree-depth"
 #define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size"
 #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"
 
 // clang-format off
 #define COMMON_HARNESS_GENERATOR_OPTIONS                                       \
   "(" COMMON_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):"                    \
   "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):"                  \
   "(" 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_OPTIONS
 
 // clang-format on
@@ -39,6 +42,9 @@ Author: Diffblue Ltd.
   "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT                             \
   " N            maximum size of dynamically created arrays\n"                 \
   "                              (default: 2)\n"                               \
+  "--" 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_HELP
 
 // clang-format on

src/goto-harness/function_call_harness_generator.cpp

@@ -173,6 +173,18 @@ void function_call_harness_generatort::handle_option(
   {
     p_impl->recursive_initialization_config.arguments_may_be_equal = true;
   }
+  else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT)
+  {
+    std::transform(
+      values.begin(),
+      values.end(),
+      std::inserter(
+        p_impl->recursive_initialization_config
+          .potential_null_function_pointers,
+        p_impl->recursive_initialization_config.potential_null_function_pointers
+          .end()),
+      [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
+  }
   else
   {
     throw invalid_command_line_argument_exceptiont{

src/goto-harness/recursive_initialization.cpp

@@ -187,7 +187,8 @@ code_blockt recursive_initializationt::build_constructor_body(
   const exprt &depth_symbol,
   const symbol_exprt &result_symbol,
   const optionalt<exprt> &size_symbol,
-  const optionalt<irep_idt> &lhs_name)
+  const optionalt<irep_idt> &lhs_name,
+  const bool is_nullable)
 {
   PRECONDITION(result_symbol.type().id() == ID_pointer);
   const typet &type = result_symbol.type().subtype();
@@ -197,6 +198,10 @@ code_blockt recursive_initializationt::build_constructor_body(
   }
   else if(type.id() == ID_pointer)
   {
+    if(type.subtype().id() == ID_code)
+    {
+      return build_function_pointer_constructor(result_symbol, is_nullable);
+    }
     if(lhs_name.has_value())
     {
       if(should_be_treated_as_cstring(*lhs_name) && type == char_type())
@@ -231,17 +236,23 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr)
   // void type_constructor_T(int depth_T, T *result_T, int *size);
   optionalt<irep_idt> size_var;
   optionalt<irep_idt> expr_name;
+  bool is_nullable = false;
+  bool has_size_param = false;
   if(expr.id() == ID_symbol)
   {
     expr_name = to_symbol_expr(expr).get_identifier();
+    is_nullable = initialization_config.potential_null_function_pointers.count(
+      expr_name.value());
     if(should_be_treated_as_array(*expr_name))
     {
       size_var = get_associated_size_variable(*expr_name);
+      has_size_param = true;
     }
   }
   const typet &type = expr.type();
-  if(type_constructor_names.find(type) != type_constructor_names.end())
-    return type_constructor_names[type];
+  const constructor_keyt key{type, is_nullable, has_size_param};
+  if(type_constructor_names.find(key) != type_constructor_names.end())
+    return type_constructor_names[key];
 
   const std::string &pretty_type = type2id(type);
   symbolt &depth_symbol =
@@ -282,7 +293,7 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr)
   }
   const symbolt &function_symbol = get_fresh_fun_symbol(
     "type_constructor_" + pretty_type, code_typet{fun_params, empty_typet{}});
-  type_constructor_names[type] = function_symbol.name;
+  type_constructor_names[key] = function_symbol.name;
   symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.name);
 
   // the body is specific for each type of expression
@@ -292,11 +303,12 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr)
     size_symbol_expr,
     // the expression name may be needed to decide if expr should be treated as
     // a string
-    expr_name);
+    expr_name,
+    is_nullable);
 
   goto_model.goto_functions.function_map[function_symbol.name].type =
     to_code_type(function_symbol.type);
-  return type_constructor_names[type];
+  return type_constructor_names.at(key);
 }
 
 symbol_exprt recursive_initializationt::get_malloc_function()
@@ -877,3 +889,58 @@ void recursive_initializationt::free_cluster_origins(code_blockt &body)
     body.add(code_function_callt{get_free_function(), {*origin}});
   }
 }
+
+code_blockt recursive_initializationt::build_function_pointer_constructor(
+  const symbol_exprt &result,
+  bool is_nullable)
+{
+  PRECONDITION(can_cast_type<pointer_typet>(result.type()));
+  const auto &result_type = to_pointer_type(result.type());
+  PRECONDITION(can_cast_type<pointer_typet>(result_type.subtype()));
+  const auto &function_pointer_type = to_pointer_type(result_type.subtype());
+  PRECONDITION(can_cast_type<code_typet>(function_pointer_type.subtype()));
+  const auto &function_type = to_code_type(function_pointer_type.subtype());
+
+  std::vector<exprt> targets;
+
+  for(const auto &sym : goto_model.get_symbol_table())
+  {
+    if(sym.second.type == function_type)
+    {
+      targets.push_back(address_of_exprt{sym.second.symbol_expr()});
+    }
+  }
+
+  if(is_nullable)
+    targets.push_back(null_pointer_exprt{function_pointer_type});
+
+  code_blockt body{};
+
+  const auto function_pointer_selector =
+    get_fresh_local_symexpr("function_pointer_selector");
+  body.add(
+    code_assignt{function_pointer_selector,
+                 side_effect_expr_nondett{function_pointer_selector.type(),
+                                          source_locationt{}}});
+  auto function_pointer_index = std::size_t{0};
+
+  for(const auto &target : targets)
+  {
+    auto const assign = code_assignt{dereference_exprt{result}, target};
+    if(function_pointer_index != targets.size() - 1)
+    {
+      auto const condition = equal_exprt{
+        function_pointer_selector,
+        from_integer(function_pointer_index, function_pointer_selector.type())};
+      auto const then = code_blockt{{assign, code_returnt{}}};
+      body.add(code_ifthenelset{condition, then});
+    }
+    else
+    {
+      body.add(assign);
+    }
+    ++function_pointer_index;
+  }
+
+  return body;
+}

src/goto-harness/recursive_initialization.h

@@ -27,6 +27,7 @@ struct recursive_initialization_configt
   std::size_t min_null_tree_depth = 1;
   std::size_t max_nondet_tree_depth = 2;
   irep_idt mode;
+  std::unordered_set<irep_idt> potential_null_function_pointers;
 
   // array stuff
   std::size_t max_dynamic_array_size = 2;
@@ -59,8 +60,30 @@ class recursive_initializationt
 {
 public:
   using recursion_sett = std::set<irep_idt>;
-  using type_constructor_namest = std::map<typet, irep_idt>;
   using equal_cluster_idt = std::size_t;
+  struct constructor_keyt
+  {
+    typet constructor_type;
+    bool is_nullable;
+    bool has_size_parameter;
+    bool operator<(const constructor_keyt &other) const
+    {
+      return std::tie(constructor_type, is_nullable, has_size_parameter) <
+             std::tie(
+               other.constructor_type,
+               other.is_nullable,
+               other.has_size_parameter);
+    };
+    bool operator==(const constructor_keyt &other) const
+    {
+      return std::tie(constructor_type, is_nullable, has_size_parameter) ==
+             std::tie(
+               other.constructor_type,
+               other.is_nullable,
+               other.has_size_parameter);
+    };
+  };
+  using type_constructor_namest = std::map<constructor_keyt, irep_idt>;
 
   recursive_initializationt(
     recursive_initialization_configt initialization_config,
@@ -170,19 +193,29 @@ class recursive_initializationt
   /// \param result_symbol: the symbol for `result` parameter
   /// \param size_symbol: maybe the symbol for `size` parameter
   /// \param lhs_name: the name of the original symbol
+  /// \param is_nullable: flag for setting a function pointer nullable
   /// \return the body of the constructor
   code_blockt build_constructor_body(
     const exprt &depth_symbol,
     const symbol_exprt &result_symbol,
     const optionalt<exprt> &size_symbol,
-    const optionalt<irep_idt> &lhs_name);
+    const optionalt<irep_idt> &lhs_name,
+    const bool is_nullable);
 
   /// Check if a constructor for the type of \p expr already exists and create
   ///   it if not.
   /// \param expr: the expression to be constructed
   /// \return name of the constructor function
   irep_idt build_constructor(const exprt &expr);
 
+  /// Constructor for function pointers.
+  /// \param result: symbol of the result parameter
+  /// \param is_nullable: if the function pointer can be null
+  /// \return the body of the constructor
+  code_blockt build_function_pointer_constructor(
+    const symbol_exprt &result,
+    bool is_nullable);
+
   /// Generic constructor for all pointers: only builds one pointee (not an
   ///   array) but may recourse in case the pointee contains more pointers, e.g.
   ///   a struct.