Use remove-function-pointers code for restricted function pointers

We had two instances of code generating an if-else sequence of function
calls for function pointers. The code used with
--restrict-function-pointer, however, was not able to cope with type
mismatches. Make the code from remove_function_pointers re-usable in
both contexts, enabling support for additional type casts.

Fixes: #6368

Author: tautschnig

regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc

@@ -2,7 +2,7 @@ CORE
 main.c
 --function foo --pointer-check
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line \d+ invalid function pointer: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ no candidates for dereferenced function pointer: FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED

regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+typedef int (*fptr_t)(long long);
+
+void use_f(fptr_t fptr)
+{
+  assert(fptr(10) == 11);
+}
+
+int f(int x)
+{
+  return x + 1;
+}
+
+int g(int x)
+{
+  return x;
+}
+
+int main(void)
+{
+  int one = 1;
+
+  // We take the address of f and g. In this case remove_function_pointers()
+  // would create a case distinction involving both f and g in the function
+  // use_f() above.
+  use_f(one ? f : g);
+}

regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--restrict-function-pointer use_f.function_pointer_call.1/f
+\[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) == 11: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that the function f is permitted for the first function pointer
+call in function use_f, despite parameters having different integer types.

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1034,7 +1034,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         function_pointer_restrictionst::from_options(
           options, goto_model, log.get_message_handler());
 
-      restrict_function_pointers(goto_model, function_pointer_restrictions);
+      restrict_function_pointers(
+        ui_message_handler, goto_model, function_pointer_restrictions);
     }
   }
 

src/goto-programs/remove_function_pointers.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/source_location.h>
 #include <util/std_expr.h>
+#include <util/string_utils.h>
 
 #include <analyses/does_remove_const.h>
 
@@ -43,24 +44,8 @@ class remove_function_pointerst
     goto_programt &goto_program,
     const irep_idt &function_id);
 
-  // a set of function symbols
-  using functionst = remove_const_function_pointerst::functionst;
-
-  /// Replace a call to a dynamic function at location
-  /// target in the given goto-program by a case-split
-  /// over a given set of functions
-  /// \param goto_program: The goto program that contains target
-  /// \param function_id: Name of function containing the target
-  /// \param target: location with function call with function pointer
-  /// \param functions: The set of functions to consider
-  void remove_function_pointer(
-    goto_programt &goto_program,
-    const irep_idt &function_id,
-    goto_programt::targett target,
-    const functionst &functions);
-
 protected:
-  messaget log;
+  message_handlert &message_handler;
   const namespacet ns;
   symbol_tablet &symbol_table;
   bool add_safety_assertion;
@@ -88,21 +73,6 @@ class remove_function_pointerst
 
   typedef std::map<irep_idt, code_typet> type_mapt;
   type_mapt type_map;
-
-  bool is_type_compatible(
-    bool return_value_used,
-    const code_typet &call_type,
-    const code_typet &function_type);
-
-  bool arg_is_type_compatible(
-    const typet &call_type,
-    const typet &function_type);
-
-  void fix_argument_types(code_function_callt &function_call);
-  void fix_return_type(
-    const irep_idt &in_function_id,
-    code_function_callt &function_call,
-    goto_programt &dest);
 };
 
 remove_function_pointerst::remove_function_pointerst(
@@ -111,7 +81,7 @@ remove_function_pointerst::remove_function_pointerst(
   bool _add_safety_assertion,
   bool only_resolve_const_fps,
   const goto_functionst &goto_functions)
-  : log(_message_handler),
+  : message_handler(_message_handler),
     ns(_symbol_table),
     symbol_table(_symbol_table),
     add_safety_assertion(_add_safety_assertion),
@@ -130,9 +100,10 @@ remove_function_pointerst::remove_function_pointerst(
   }
 }
 
-bool remove_function_pointerst::arg_is_type_compatible(
+static bool arg_is_type_compatible(
   const typet &call_type,
-  const typet &function_type)
+  const typet &function_type,
+  const namespacet &ns)
 {
   if(call_type == function_type)
     return true;
@@ -156,10 +127,11 @@ bool remove_function_pointerst::arg_is_type_compatible(
          pointer_offset_bits(function_type, ns);
 }
 
-bool remove_function_pointerst::is_type_compatible(
+bool function_is_type_convertable(
   bool return_value_used,
   const code_typet &call_type,
-  const code_typet &function_type)
+  const code_typet &function_type,
+  const namespacet &ns)
 {
   // we are willing to ignore anything that's returned
   // if we call with 'void'
@@ -172,8 +144,8 @@ bool remove_function_pointerst::is_type_compatible(
   }
   else
   {
-    if(!arg_is_type_compatible(call_type.return_type(),
-                               function_type.return_type()))
+    if(!arg_is_type_compatible(
+         call_type.return_type(), function_type.return_type(), ns))
       return false;
   }
 
@@ -198,16 +170,15 @@ bool remove_function_pointerst::is_type_compatible(
       return false;
 
     for(std::size_t i=0; i<call_parameters.size(); i++)
-      if(!arg_is_type_compatible(call_parameters[i].type(),
-                                 function_parameters[i].type()))
+      if(!arg_is_type_compatible(
+           call_parameters[i].type(), function_parameters[i].type(), ns))
         return false;
   }
 
   return true;
 }
 
-void remove_function_pointerst::fix_argument_types(
-  code_function_callt &function_call)
+static void fix_argument_types(code_function_callt &function_call)
 {
   const code_typet &code_type = to_code_type(function_call.function().type());
 
@@ -230,9 +201,10 @@ void remove_function_pointerst::fix_argument_types(
   }
 }
 
-void remove_function_pointerst::fix_return_type(
+static void fix_return_type(
   const irep_idt &in_function_id,
   code_function_callt &function_call,
+  symbol_tablet &symbol_table,
   goto_programt &dest)
 {
   // are we returning anything at all?
@@ -245,6 +217,7 @@ void remove_function_pointerst::fix_return_type(
   if(function_call.lhs().type() == code_type.return_type())
     return;
 
+  const namespacet ns(symbol_table);
   const symbolt &function_symbol =
     ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
 
@@ -292,6 +265,7 @@ void remove_function_pointerst::remove_function_pointer(
   remove_const_function_pointerst::functionst functions;
   does_remove_constt const_removal_check(goto_program, ns);
   const auto does_remove_const = const_removal_check();
+  messaget log{message_handler};
   if(does_remove_const.first)
   {
     log.warning().source_location = does_remove_const.second;
@@ -344,7 +318,8 @@ void remove_function_pointerst::remove_function_pointer(
         continue;
 
       // type-compatible?
-      if(!is_type_compatible(return_value_used, call_type, t.second))
+      if(!function_is_type_convertable(
+           return_value_used, call_type, t.second, ns))
         continue;
 
       if(t.first=="pthread_mutex_cleanup")
@@ -355,14 +330,56 @@ void remove_function_pointerst::remove_function_pointer(
     }
   }
 
-  remove_function_pointer(goto_program, function_id, target, functions);
+  ::remove_function_pointer(
+    message_handler,
+    symbol_table,
+    goto_program,
+    function_id,
+    target,
+    functions,
+    add_safety_assertion);
 }
 
-void remove_function_pointerst::remove_function_pointer(
+static std::string function_pointer_assertion_comment(
+  const std::unordered_set<symbol_exprt, irep_hash> &candidates)
+{
+  std::stringstream comment;
+
+  comment << "dereferenced function pointer at must be ";
+
+  if(candidates.size() == 1)
+  {
+    comment << candidates.begin()->get_identifier();
+  }
+  else if(candidates.empty())
+  {
+    comment.str("no candidates for dereferenced function pointer");
+  }
+  else
+  {
+    comment << "one of [";
+
+    join_strings(
+      comment,
+      candidates.begin(),
+      candidates.end(),
+      ", ",
+      [](const symbol_exprt &s) { return s.get_identifier(); });
+
+    comment << ']';
+  }
+
+  return comment.str();
+}
+
+void remove_function_pointer(
+  message_handlert &message_handler,
+  symbol_tablet &symbol_table,
   goto_programt &goto_program,
   const irep_idt &function_id,
   goto_programt::targett target,
-  const functionst &functions)
+  const std::unordered_set<symbol_exprt, irep_hash> &functions,
+  const bool add_safety_assertion)
 {
   const exprt &function = target->call_function();
   const exprt &pointer = to_dereference_expr(function).pointer();
@@ -387,7 +404,7 @@ void remove_function_pointerst::remove_function_pointer(
     fix_argument_types(new_call);
 
     goto_programt tmp;
-    fix_return_type(function_id, new_call, tmp);
+    fix_return_type(function_id, new_call, symbol_table, tmp);
 
     auto call = new_code_calls.add(goto_programt::make_function_call(new_call));
     new_code_calls.destructive_append(tmp);
@@ -411,7 +428,8 @@ void remove_function_pointerst::remove_function_pointer(
     goto_programt::targett t =
       new_code_gotos.add(goto_programt::make_assertion(false_exprt()));
     t->source_location.set_property_class("pointer dereference");
-    t->source_location.set_comment("invalid function pointer");
+    t->source_location.set_comment(
+      function_pointer_assertion_comment(functions));
   }
   new_code_gotos.add(goto_programt::make_assumption(false_exprt()));
 
@@ -449,6 +467,7 @@ void remove_function_pointerst::remove_function_pointer(
   target->type=OTHER;
 
   // report statistics
+  messaget log{message_handler};
   log.statistics().source_location = target->source_location;
   log.statistics() << "replacing function pointer by " << functions.size()
                    << " possible targets" << messaget::eom;

src/goto-programs/remove_function_pointers.h

@@ -14,10 +14,11 @@ Date: June 2003
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
 
-#include <util/irep.h>
+#include "goto_program.h"
+
+#include <unordered_set>
 
 class goto_functionst;
-class goto_programt;
 class goto_modelt;
 class message_handlert;
 class symbol_tablet;
@@ -46,4 +47,32 @@ bool remove_function_pointers(
   bool add_safety_assertion,
   bool only_remove_const_fps = false);
 
+/// Replace a call to a dynamic function at location
+/// target in the given goto-program by a case-split
+/// over a given set of functions
+/// \param message_handler: Message handler
+/// \param symbol_table: Symbol table
+/// \param goto_program: The goto program that contains target
+/// \param function_id: Name of function containing the target
+/// \param target: location with function call with function pointer
+/// \param functions: The set of functions to consider
+/// \param add_safety_assertion: Iff true, include an assertion that the
+//         pointer matches one of the candidate functions
+void remove_function_pointer(
+  message_handlert &message_handler,
+  symbol_tablet &symbol_table,
+  goto_programt &goto_program,
+  const irep_idt &function_id,
+  goto_programt::targett target,
+  const std::unordered_set<symbol_exprt, irep_hash> &functions,
+  const bool add_safety_assertion);
+
+/// Returns true iff \p call_type can be converted to produce a function call of
+/// the same type as \p function_type.
+bool function_is_type_convertable(
+  bool return_value_used,
+  const code_typet &call_type,
+  const code_typet &function_type,
+  const namespacet &ns);
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H