Remove function pointers slightly more precisely

Scans the goto program for assigns to function pointers and builds a map of assigns to those function pointers. Then uses only these functions to replace the function pointer with.

If a function pointer is ever written to with anything more complicated than a straight forward address_of a function, defaults to normal behaviour.

Only works for:
- standalone function pointers
- function pointers that are 1 level deep in a struct

Current unsound-ness to be fixed:
- if a function pointer is part of a struct, and the struct is assigned to in total, this is not detected.

Author: polgreen

src/goto-programs/remove_function_pointers.cpp

@@ -30,6 +30,10 @@ Author: Daniel Kroening, [email protected]
 #include "compute_called_functions.h"
 #include "remove_const_function_pointers.h"
 
+#include <iostream>
+
+#define UNKNOWN_ASSIGN "##unknown##"
+
 class remove_function_pointerst:public messaget
 {
 public:
@@ -48,6 +52,12 @@ class remove_function_pointerst:public messaget
   const namespacet ns;
   symbol_tablet &symbol_table;
   bool add_safety_assertion;
+  std::map<irep_idt, std::unordered_set<irep_idt>> function_pointer_map;
+  std::size_t number_of_function_pointers_replaced;
+  std::size_t max_size_of_case_split;
+  std::size_t total_number_of_replacement_candidates;
+
+
 
   // We can optionally halt the FP removal if we aren't able to use
   // remove_const_function_pointerst to successfully narrow to a small
@@ -80,6 +90,13 @@ class remove_function_pointerst:public messaget
     code_function_callt &function_call,
     goto_programt &dest);
 
+  /// scans through goto functions and builds a map of function
+  /// pointers to a set of functions that have been written to each pointer,
+  /// stored as irep_idts.
+  /// The map is stored as variable in remove_function_pointerst
+  /// \param goto_functions goto functions to scan through
+  void get_all_writes_to_pointers(goto_functionst &goto_functions);
+
   void
   compute_address_taken_in_symbols(std::unordered_set<irep_idt> &address_taken)
   {
@@ -90,6 +107,12 @@ class remove_function_pointerst:public messaget
   }
 };
 
+static irep_idt get_member_identifier(const member_exprt &member)
+{
+  return id2string(member.symbol().get_identifier()) +
+      id2string(member.get_component_name());
+}
+
 remove_function_pointerst::remove_function_pointerst(
   message_handlert &_message_handler,
   symbol_tablet &_symbol_table,
@@ -99,6 +122,9 @@ remove_function_pointerst::remove_function_pointerst(
   ns(_symbol_table),
   symbol_table(_symbol_table),
   add_safety_assertion(_add_safety_assertion),
+  number_of_function_pointers_replaced(0u),
+  max_size_of_case_split(0u),
+  total_number_of_replacement_candidates(0u),
   only_resolve_const_fps(only_resolve_const_fps)
 {
   compute_address_taken_in_symbols(address_taken);
@@ -255,6 +281,7 @@ void remove_function_pointerst::fix_return_type(
     old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()));
 }
 
+
 void remove_function_pointerst::remove_function_pointer(
   goto_programt &goto_program,
   goto_programt::targett target)
@@ -348,6 +375,41 @@ void remove_function_pointerst::remove_function_pointer(
     }
   }
 
+  // we only handle cases where the LHS is a symbol or a member of a struct
+  if(pointer.id() == ID_symbol || pointer.id() == ID_member)
+  {
+    irep_idt identifier;
+    if(pointer.id() == ID_symbol)
+      identifier =
+        to_symbol_expr(to_dereference_expr(code.function()).pointer())
+          .get_identifier();
+    else
+    {
+      identifier = get_member_identifier(to_member_expr(pointer));
+    }
+
+    if(function_pointer_map.find(identifier) != function_pointer_map.end())
+    {
+      status() << "Replacing function pointer from map of possible assigns\n";
+      if(
+        function_pointer_map[identifier].find(UNKNOWN_ASSIGN) ==
+        function_pointer_map[identifier].end())
+      {
+        for(auto func_itr = functions.begin(); func_itr != functions.end();)
+        {
+          if(
+            function_pointer_map[identifier].find(func_itr->get_identifier()) ==
+            function_pointer_map[identifier].end())
+          {
+            func_itr = functions.erase(func_itr);
+          }
+          else
+            func_itr++;
+        }
+      }
+    }
+  }
+
   // the final target is a skip
   goto_programt final_skip;
 
@@ -430,6 +492,10 @@ void remove_function_pointerst::remove_function_pointer(
   statistics().source_location=target->source_location;
   statistics() << "replacing function pointer by "
                << functions.size() << " possible targets" << eom;
+  number_of_function_pointers_replaced++;
+  total_number_of_replacement_candidates+=functions.size();
+  if(functions.size()>max_size_of_case_split)
+    max_size_of_case_split = functions.size();
 
   // list the names of functions when verbosity is at debug level
   conditional_output(
@@ -451,6 +517,7 @@ void remove_function_pointerst::remove_function_pointer(
     });
 }
 
+
 bool remove_function_pointerst::remove_function_pointers(
   goto_programt &goto_program)
 {
@@ -459,13 +526,12 @@ bool remove_function_pointerst::remove_function_pointers(
   Forall_goto_program_instructions(target, goto_program)
     if(target->is_function_call())
     {
-      const code_function_callt &code=
-        to_code_function_call(target->code);
+      const code_function_callt &code = to_code_function_call(target->code);
 
-      if(code.function().id()==ID_dereference)
+      if(code.function().id() == ID_dereference)
       {
         remove_function_pointer(goto_program, target);
-        did_something=true;
+        did_something = true;
       }
     }
 
@@ -475,8 +541,10 @@ bool remove_function_pointerst::remove_function_pointers(
   return did_something;
 }
 
+
 void remove_function_pointerst::operator()(goto_functionst &functions)
 {
+  get_all_writes_to_pointers(functions);
   bool did_something=false;
 
   for(goto_functionst::function_mapt::iterator f_it=
@@ -490,8 +558,23 @@ void remove_function_pointerst::operator()(goto_functionst &functions)
       did_something=true;
   }
 
+
   if(did_something)
+  {
     functions.compute_location_numbers();
+
+    std::cout << "Statistics:\n"
+              << "Replaced " << number_of_function_pointers_replaced
+              << " function pointers "
+              << " with " << total_number_of_replacement_candidates
+              << " possible candidate functions. \n"
+              << "Max number of candidates in a single replacement: "
+              << max_size_of_case_split << "\n"
+              << "Mean number of candidates in a single replacement: "
+              << total_number_of_replacement_candidates /
+                   number_of_function_pointers_replaced
+              << "\n";
+  }
 }
 
 bool remove_function_pointers(message_handlert &_message_handler,
@@ -535,10 +618,57 @@ void remove_function_pointers(message_handlert &_message_handler,
   bool add_safety_assertion,
   bool only_remove_const_fps)
 {
+
   remove_function_pointers(
     _message_handler,
     goto_model.symbol_table,
     goto_model.goto_functions,
     add_safety_assertion,
     only_remove_const_fps);
 }
+
+void remove_function_pointerst::get_all_writes_to_pointers(
+  goto_functionst &goto_functions)
+{
+  for(goto_functionst::function_mapt::iterator f_it =
+        goto_functions.function_map.begin();
+      f_it != goto_functions.function_map.end();
+      f_it++)
+  {
+    goto_programt &goto_program = f_it->second.body;
+    Forall_goto_program_instructions(target, goto_program)
+    {
+      if(!target->is_assign())
+        continue;
+
+      const code_assignt &code_assign = to_code_assign(target->code);
+      const auto &lhs = code_assign.lhs();
+      const auto &rhs = code_assign.rhs();
+
+      if(lhs.type().id() == ID_pointer && lhs.type().subtype().id() == ID_code)
+      {
+        irep_idt lhs_irep;
+        if(lhs.id() == ID_symbol)
+          lhs_irep = to_symbol_expr(lhs).get_identifier();
+        else if(lhs.id() == ID_member)
+        {
+          lhs_irep = get_member_identifier(to_member_expr(lhs));
+        }
+        else
+          continue;
+
+        if(rhs.id() == ID_address_of && rhs.type().subtype().id() == ID_code)
+        {
+          irep_idt rhs_irep =
+            to_symbol_expr(to_address_of_expr(rhs).object()).get_identifier();
+          if(function_pointer_map.find(lhs_irep) != function_pointer_map.end())
+            (function_pointer_map[lhs_irep]).insert(rhs_irep);
+          else
+            function_pointer_map[lhs_irep] = {{rhs_irep}};
+        }
+        else
+          function_pointer_map[lhs_irep] = {{UNKNOWN_ASSIGN}};
+      }
+    }
+  }
+}