Add function pointer nondet initialisation to goto-harness

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

src/goto-harness/recursive_initialization.cpp

@@ -169,6 +169,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);
+    }
     if(lhs_name.has_value())
     {
       if(should_be_treated_as_cstring(*lhs_name) && type == char_type())
@@ -192,7 +196,7 @@ code_blockt recursive_initializationt::build_constructor_body(
   }
 }
 
-const irep_idt &recursive_initializationt::build_constructor(const exprt &expr)
+irep_idt recursive_initializationt::build_constructor(const exprt &expr)
 {
   // for `expr` of type T builds a declaration of a function:
   //
@@ -786,7 +790,7 @@ 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().subtype().id() == ID_code)
     return false;
   if(common_arguments_origin.has_value() && expr.id() == ID_symbol)
   {
@@ -797,3 +801,54 @@ bool recursive_initializationt::needs_freeing(const exprt &expr) const
   }
   return true;
 }
+
+code_blockt recursive_initializationt::build_function_pointer_constructor(
+  const exprt &result)
+{
+  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<symbol_exprt> targets;
+
+  for(const auto &sym : goto_model.get_symbol_table())
+  {
+    if(sym.second.type == function_type)
+    {
+      targets.push_back(sym.second.symbol_expr());
+    }
+  }
+
+  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()}});
+  auto function_pointer_index = std::size_t{0};
+
+  for(const auto &target : targets)
+  {
+    auto const assign =
+      code_assignt{dereference_exprt{result}, address_of_exprt{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

@@ -176,7 +176,12 @@ class recursive_initializationt
   ///   it if not.
   /// \param expr: the expression to be constructed
   /// \return name of the constructor function
-  const irep_idt &build_constructor(const exprt &expr);
+  irep_idt build_constructor(const exprt &expr);
+
+  /// Constructor for function pointers.
+  /// \param result: symbol of the result parameter
+  /// \return the body of the constructor
+  code_blockt build_function_pointer_constructor(const exprt &result);
 
   /// Generic constructor for all pointers: only builds one pointee (not an
   ///   array) but may recourse in case the pointee contains more pointers, e.g.