Merge pull request #4599 from smowton/smowton/feature/remove-virtual-functions-class-hierarchy

Remove-virtual-functions: avoid computing class_hierarchyt when possible

Author: smowton

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -753,7 +753,7 @@ void jbmc_parse_optionst::process_goto_function(
     *class_hierarchy,
     ui_message_handler);
   // Java virtual functions -> explicit dispatch tables:
-  remove_virtual_functions(function);
+  remove_virtual_functions(function, *class_hierarchy);
 
   auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
     return symbol_table.lookup_ref(id).value.is_nil() &&

src/goto-programs/remove_virtual_functions.cpp

@@ -76,13 +76,6 @@ class remove_virtual_functionst
     const irep_idt &function_id,
     goto_programt &goto_program);
 
-  goto_programt::targett remove_virtual_function(
-    const irep_idt &function_id,
-    goto_programt &goto_program,
-    goto_programt::targett target,
-    const dispatch_table_entriest &functions,
-    virtual_dispatch_fallback_actiont fallback_action);
-
 private:
   const class_hierarchyt &class_hierarchy;
   symbol_table_baset &symbol_table;
@@ -94,42 +87,6 @@ class remove_virtual_functionst
     goto_programt::targett target);
 };
 
-/// Replace specified virtual function call with a static call to its
-/// most derived implementation
-/// \param function_id: The identifier of the function we are currently
-///   analysing
-/// \param [in,out] goto_program: GOTO program to modify
-/// \param target: iterator to a function in the supplied GOTO program
-///   to replace. Must point to a virtual function call.
-/// \return Returns a pointer to the statement in the supplied GOTO
-///   program after replaced function call
-goto_programt::targett remove_virtual_functionst::remove_virtual_function(
-  const irep_idt &function_id,
-  goto_programt &goto_program,
-  goto_programt::targett target)
-{
-  const code_function_callt &code = target->get_function_call();
-
-  const exprt &function=code.function();
-  INVARIANT(
-    function.id()==ID_virtual_function,
-    "remove_virtual_function must take a virtual function call instruction");
-  INVARIANT(
-    !code.arguments().empty(),
-    "virtual function calls must have at least a this-argument");
-
-  get_virtual_calleest get_callees(symbol_table, class_hierarchy);
-  dispatch_table_entriest functions;
-  get_callees.get_functions(function, functions);
-
-  return remove_virtual_function(
-    function_id,
-    goto_program,
-    target,
-    functions,
-    virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION);
-}
-
 /// Create a concrete function call to replace a virtual one
 /// \param [in,out] call: the function call to update
 /// \param function_symbol: the function to be called
@@ -285,6 +242,7 @@ static void process_this_argument(
 /// implementation. If there's a type mismatch between implementation
 /// and the instance type or if fallback_action is set to
 /// ASSUME_FALSE, then function is substituted with a call to ASSUME(false)
+/// \param symbol_table: Symbol table associated with \p goto_program
 /// \param function_id: The identifier of the function we are currently
 ///   analysing
 /// \param [in,out] goto_program: GOTO program to modify
@@ -297,7 +255,8 @@ static void process_this_argument(
 ///   with the most derived matching call
 /// \return Returns a pointer to the statement in the supplied GOTO
 ///   program after replaced function call
-goto_programt::targett remove_virtual_functionst::remove_virtual_function(
+static goto_programt::targett replace_virtual_function_with_dispatch_table(
+  symbol_table_baset &symbol_table,
   const irep_idt &function_id,
   goto_programt &goto_program,
   goto_programt::targett target,
@@ -308,6 +267,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
     target->is_function_call(),
     "remove_virtual_function must target a FUNCTION_CALL instruction");
 
+  namespacet ns(symbol_table);
   goto_programt::targett next_target = std::next(target);
 
   if(functions.empty())
@@ -499,6 +459,43 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
   return next_target;
 }
 
+/// Replace specified virtual function call with a static call to its
+/// most derived implementation
+/// \param function_id: The identifier of the function we are currently
+///   analysing
+/// \param [in,out] goto_program: GOTO program to modify
+/// \param target: iterator to a function in the supplied GOTO program
+///   to replace. Must point to a virtual function call.
+/// \return Returns a pointer to the statement in the supplied GOTO
+///   program after replaced function call
+goto_programt::targett remove_virtual_functionst::remove_virtual_function(
+  const irep_idt &function_id,
+  goto_programt &goto_program,
+  goto_programt::targett target)
+{
+  const code_function_callt &code = target->get_function_call();
+
+  const exprt &function = code.function();
+  INVARIANT(
+    function.id() == ID_virtual_function,
+    "remove_virtual_function must take a virtual function call instruction");
+  INVARIANT(
+    !code.arguments().empty(),
+    "virtual function calls must have at least a this-argument");
+
+  get_virtual_calleest get_callees(symbol_table, class_hierarchy);
+  dispatch_table_entriest functions;
+  get_callees.get_functions(function, functions);
+
+  return replace_virtual_function_with_dispatch_table(
+    symbol_table,
+    function_id,
+    goto_program,
+    target,
+    functions,
+    virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION);
+}
+
 /// Used by get_functions to track the most-derived parent that provides an
 /// override of a given function.
 /// \param this_id: class name
@@ -740,6 +737,8 @@ void remove_virtual_functionst::operator()(goto_functionst &functions)
 
 /// Remove virtual function calls from all functions in the specified
 /// list and replace them with their most derived implementations
+/// \param symbol_table: symbol table associated with \p goto_functions
+/// \param goto_functions: functions from which to remove virtual function calls
 void remove_virtual_functions(
   symbol_table_baset &symbol_table,
   goto_functionst &goto_functions)
@@ -750,14 +749,47 @@ void remove_virtual_functions(
   rvf(goto_functions);
 }
 
+/// Remove virtual function calls from all functions in the specified
+/// list and replace them with their most derived implementations
+/// \param symbol_table: symbol table associated with \p goto_functions
+/// \param goto_functions: functions from which to remove virtual function calls
+/// \param class_hierarchy: class hierarchy derived from symbol_table
+///   This should already be populated (i.e. class_hierarchyt::operator() has
+///   already been called)
+void remove_virtual_functions(
+  symbol_table_baset &symbol_table,
+  goto_functionst &goto_functions,
+  const class_hierarchyt &class_hierarchy)
+{
+  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
+  rvf(goto_functions);
+}
+
 /// Remove virtual function calls from the specified model
+/// \param goto_model: model from which to remove virtual functions
 void remove_virtual_functions(goto_modelt &goto_model)
 {
   remove_virtual_functions(
     goto_model.symbol_table, goto_model.goto_functions);
 }
 
+/// Remove virtual function calls from the specified model
+/// \param goto_model: model from which to remove virtual functions
+/// \param class_hierarchy: class hierarchy derived from model.symbol_table
+///   This should already be populated (i.e. class_hierarchyt::operator() has
+///   already been called)
+void remove_virtual_functions(
+  goto_modelt &goto_model,
+  const class_hierarchyt &class_hierarchy)
+{
+  remove_virtual_functions(
+    goto_model.symbol_table, goto_model.goto_functions, class_hierarchy);
+}
+
 /// Remove virtual function calls from the specified model function
+/// May change the location numbers in `function`.
+/// \param function: function from which virtual functions should be converted
+///   to explicit dispatch tables.
 void remove_virtual_functions(goto_model_functiont &function)
 {
   class_hierarchyt class_hierarchy;
@@ -767,6 +799,22 @@ void remove_virtual_functions(goto_model_functiont &function)
     function.get_function_id(), function.get_goto_function().body);
 }
 
+/// Remove virtual function calls from the specified model function
+/// May change the location numbers in `function`.
+/// \param function: function from which virtual functions should be converted
+///   to explicit dispatch tables.
+/// \param class_hierarchy: class hierarchy derived from function.symbol_table
+///   This should already be populated (i.e. class_hierarchyt::operator() has
+///   already been called)
+void remove_virtual_functions(
+  goto_model_functiont &function,
+  const class_hierarchyt &class_hierarchy)
+{
+  remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
+  rvf.remove_virtual_functions(
+    function.get_function_id(), function.get_goto_function().body);
+}
+
 /// Replace virtual function call with a static function call
 /// Achieved by substituting a virtual function with its most derived
 /// implementation. If there's a type mismatch between implementation
@@ -793,12 +841,13 @@ goto_programt::targett remove_virtual_function(
   const dispatch_table_entriest &dispatch_table,
   virtual_dispatch_fallback_actiont fallback_action)
 {
-  class_hierarchyt class_hierarchy;
-  class_hierarchy(symbol_table);
-  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
-
-  goto_programt::targett next = rvf.remove_virtual_function(
-    function_id, goto_program, instruction, dispatch_table, fallback_action);
+  goto_programt::targett next = replace_virtual_function_with_dispatch_table(
+    symbol_table,
+    function_id,
+    goto_program,
+    instruction,
+    dispatch_table,
+    fallback_action);
 
   goto_program.update();
 

src/goto-programs/remove_virtual_functions.h

@@ -26,19 +26,32 @@ class goto_model_functiont;
 class goto_modelt;
 class symbol_table_baset;
 
+// For all of the following the class-hierarchy and non-class-hierarchy
+// overloads are equivalent, but the class-hierarchy-taking one saves time if
+// you already have a class-hierarchy object available.
+
 void remove_virtual_functions(
   goto_modelt &goto_model);
 
+void remove_virtual_functions(
+  goto_modelt &goto_model,
+  const class_hierarchyt &class_hierarchy);
+
 void remove_virtual_functions(
   symbol_table_baset &symbol_table,
   goto_functionst &goto_functions);
 
-/// Remove virtual functions from one function.
-/// May change the location numbers in `function`.
-/// \param function: function from which virtual functions should be converted
-///   to explicit dispatch tables.
+void remove_virtual_functions(
+  symbol_table_baset &symbol_table,
+  goto_functionst &goto_functions,
+  const class_hierarchyt &class_hierarchy);
+
 void remove_virtual_functions(goto_model_functiont &function);
 
+void remove_virtual_functions(
+  goto_model_functiont &function,
+  const class_hierarchyt &class_hierarchy);
+
 /// Specifies remove_virtual_function's behaviour when the actual supplied
 /// parameter does not match any of the possible callee types
 enum class virtual_dispatch_fallback_actiont