Export additional interface for remove-function-pointers

that takes the target map as argument.

To avoid duplication we also refactor the existing functions a bit.

Author: petr-bauch

src/goto-programs/remove_function_pointers.cpp

@@ -38,23 +38,33 @@ class remove_function_pointerst
     bool only_resolve_const_fps,
     const goto_functionst &goto_functions);
 
-  void operator()(goto_functionst &goto_functions);
-
+  /// Call the function pointer removal via an operator
+  /// \param goto_functions: functions to modify
+  /// \param target_map: candidate functions
+  void operator()(
+    goto_functionst &goto_functions,
+    const possible_fp_targets_mapt &target_map);
+
+  /// Call the function pointer removal within the \p goto_program
+  /// \param goto_program: program to modify
+  /// \param function_id: identifier of the function pointer to be removed
+  /// \param target_map: candidate functions
   bool remove_function_pointers(
     goto_programt &goto_program,
-    const irep_idt &function_id);
+    const irep_idt &function_id,
+    const possible_fp_targets_mapt &target_map);
 
   // 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
+  /// \p 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(
+  void remove_function_pointer_non_const(
     goto_programt &goto_program,
     const irep_idt &function_id,
     goto_programt::targett target,
@@ -66,7 +76,7 @@ class remove_function_pointerst
   /// \param call_site: the call site of the function pointer under analysis
   /// \return the set of the potential functions
   functionst get_function_pointer_targets(
-    const goto_modelt &goto_model,
+    const goto_functionst &goto_functions,
     goto_programt::const_targett &call_site);
 
   /// Go through a single function body and find all potential function the
@@ -78,6 +88,13 @@ class remove_function_pointerst
     const goto_programt &goto_program,
     goto_programt::const_targett &call_site);
 
+  /// Go through the whole model and find all potential function the pointer at
+  ///   all call sites
+  /// \param goto_model: model to search for potential functions
+  /// \return a map from ids to sets of function candidates
+  possible_fp_targets_mapt
+  get_function_pointer_targets(const goto_functionst &goto_functions);
+
 protected:
   messaget log;
   const namespacet ns;
@@ -104,10 +121,12 @@ class remove_function_pointerst
   /// \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
-  void remove_function_pointer(
+  /// \param functions: potential candidate functions
+  void remove_function_pointer_const(
     goto_programt &goto_program,
     const irep_idt &function_id,
-    goto_programt::targett target);
+    goto_programt::targett target,
+    const functionst &functions);
 
   std::unordered_set<irep_idt> address_taken;
 
@@ -384,11 +403,11 @@ void remove_function_pointerst::try_remove_const_fp(
 
 remove_function_pointerst::functionst
 remove_function_pointerst::get_function_pointer_targets(
-  const goto_modelt &goto_model,
+  const goto_functionst &goto_functions,
   goto_programt::const_targett &call_site)
 {
   functionst functions;
-  for(const auto &function_pair : goto_model.goto_functions.function_map)
+  for(const auto &function_pair : goto_functions.function_map)
   {
     const auto &function_body = function_pair.second.body;
     const auto &candidates =
@@ -445,15 +464,12 @@ remove_function_pointerst::get_function_pointer_targets(
   return functions;
 }
 
-void remove_function_pointerst::remove_function_pointer(
+void remove_function_pointerst::remove_function_pointer_const(
   goto_programt &goto_program,
   const irep_idt &function_id,
-  goto_programt::targett target)
+  goto_programt::targett target,
+  const functionst &functions)
 {
-  goto_programt::const_targett const_target = target;
-  const auto functions =
-    get_function_pointer_targets(goto_program, const_target);
-
   if(only_remove_const_function_pointers_called)
   {
     auto call = target->get_function_call();
@@ -468,11 +484,12 @@ void remove_function_pointerst::remove_function_pointer(
     // Since we haven't found functions, we would now resort to
     // replacing the function pointer with any function with a valid signature
     // Since we don't want to do that, we abort.
-    remove_function_pointer(goto_program, function_id, target, functions);
+    remove_function_pointer_non_const(
+      goto_program, function_id, target, functions);
   }
 }
 
-void remove_function_pointerst::remove_function_pointer(
+void remove_function_pointerst::remove_function_pointer_non_const(
   goto_programt &goto_program,
   const irep_idt &function_id,
   goto_programt::targett target,
@@ -501,7 +518,8 @@ void remove_function_pointerst::remove_function_pointer(
 
 bool remove_function_pointerst::remove_function_pointers(
   goto_programt &goto_program,
-  const irep_idt &function_id)
+  const irep_idt &function_id,
+  const possible_fp_targets_mapt &target_map)
 {
   bool did_something=false;
 
@@ -512,7 +530,8 @@ bool remove_function_pointerst::remove_function_pointers(
 
       if(code.function().id()==ID_dereference)
       {
-        remove_function_pointer(goto_program, function_id, target);
+        remove_function_pointer_const(
+          goto_program, function_id, target, target_map.at(function_id));
         did_something=true;
       }
     }
@@ -523,7 +542,9 @@ bool remove_function_pointerst::remove_function_pointers(
   return did_something;
 }
 
-void remove_function_pointerst::operator()(goto_functionst &functions)
+void remove_function_pointerst::operator()(
+  goto_functionst &functions,
+  const possible_fp_targets_mapt &target_map)
 {
   bool did_something=false;
 
@@ -534,7 +555,7 @@ void remove_function_pointerst::operator()(goto_functionst &functions)
   {
     goto_programt &goto_program=f_it->second.body;
 
-    if(remove_function_pointers(goto_program, f_it->first))
+    if(remove_function_pointers(goto_program, f_it->first, target_map))
       did_something=true;
   }
 
@@ -559,7 +580,10 @@ bool remove_function_pointers(
       only_remove_const_fps,
       goto_functions);
 
-  return rfp.remove_function_pointers(goto_program, function_id);
+  return rfp.remove_function_pointers(
+    goto_program,
+    function_id,
+    rfp.get_function_pointer_targets(goto_functions));
 }
 
 void remove_function_pointers(
@@ -577,7 +601,7 @@ void remove_function_pointers(
       only_remove_const_fps,
       goto_functions);
 
-  rfp(goto_functions);
+  rfp(goto_functions, rfp.get_function_pointer_targets(goto_functions));
 }
 
 void remove_function_pointers(message_handlert &_message_handler,
@@ -593,19 +617,28 @@ void remove_function_pointers(message_handlert &_message_handler,
     only_remove_const_fps);
 }
 
-possible_fp_targets_mapt get_function_pointer_targets(
-  message_handlert &message_handler,
-  goto_modelt &goto_model)
+void remove_function_pointers(
+  message_handlert &_message_handler,
+  goto_modelt &goto_model,
+  const possible_fp_targets_mapt &target_map,
+  bool add_safety_assertion,
+  bool only_remove_const_fps)
 {
   remove_function_pointerst rfp(
-    message_handler,
+    _message_handler,
     goto_model.symbol_table,
-    false,
-    false,
+    add_safety_assertion,
+    only_remove_const_fps,
     goto_model.goto_functions);
 
+  rfp(goto_model.goto_functions, target_map);
+}
+
+possible_fp_targets_mapt
+remove_function_pointerst::get_function_pointer_targets(
+  const goto_functionst &goto_functions)
+{
   possible_fp_targets_mapt target_map;
-  const auto &goto_functions = goto_model.goto_functions;
   for(const auto &function_pair : goto_functions.function_map)
   {
     const auto &instructions = function_pair.second.body.instructions;
@@ -622,13 +655,27 @@ possible_fp_targets_mapt get_function_pointer_targets(
               .pointer())
             .get_identifier();
         target_map.emplace(
-          function_id, rfp.get_function_pointer_targets(goto_model, target));
+          function_id, get_function_pointer_targets(goto_functions, target));
       }
     }
   }
   return target_map;
 }
 
+possible_fp_targets_mapt get_function_pointer_targets(
+  message_handlert &message_handler,
+  goto_modelt &goto_model)
+{
+  remove_function_pointerst rfp(
+    message_handler,
+    goto_model.symbol_table,
+    false,
+    false,
+    goto_model.goto_functions);
+
+  return rfp.get_function_pointer_targets(goto_model.goto_functions);
+}
+
 goto_programt remove_function_pointerst::build_new_code(
   const functionst &functions,
   const code_function_callt &code,

src/goto-programs/remove_function_pointers.h

@@ -29,6 +29,11 @@ class symbol_tablet;
 using possible_fp_targetst = remove_const_function_pointerst::functionst;
 using possible_fp_targets_mapt = std::map<irep_idt, possible_fp_targetst>;
 
+/// Go through the whole model and find all potential function the pointer at
+///   all call sites
+/// \param message_handler: a message handler for reporting
+/// \param goto_model: model to search for potential functions
+/// \return a map from ids to sets of function candidates
 possible_fp_targets_mapt get_function_pointer_targets(
   message_handlert &message_handler,
   goto_modelt &goto_model);
@@ -41,6 +46,20 @@ void remove_function_pointers(
   bool add_safety_assertion,
   bool only_remove_const_fps=false);
 
+/// Replace all calls to a dynamic function by a case-split over a given set of
+///   candidate functions
+/// \param message_handler: a message handler for reporting
+/// \param goto_model: model to search for potential functions
+/// \param target_map: candidate functions
+/// \param add_safety_assertion: check that at least one function matches
+/// \param only_remove_const_fps: restrict the pointer remove to const
+void remove_function_pointers(
+  message_handlert &_message_handler,
+  goto_modelt &goto_model,
+  const possible_fp_targets_mapt &target_map,
+  bool add_safety_assertion,
+  bool only_remove_const_fps = false);
+
 void remove_function_pointers(
   message_handlert &_message_handler,
   symbol_tablet &symbol_table,