JBMC: Run remove-virtual-functions as each function is converted

This means lazy loading drivers do not need to understand virtual
function calls, as they have already been converted into explicit
dispatch tables.

Author: smowton

src/goto-programs/remove_virtual_functions.cpp

@@ -24,8 +24,7 @@ class remove_virtual_functionst
 {
 public:
   remove_virtual_functionst(
-    const symbol_tablet &_symbol_table,
-    const goto_functionst &goto_functions);
+    const symbol_tablet &_symbol_table);
 
   void operator()(goto_functionst &goto_functions);
 
@@ -65,8 +64,7 @@ class remove_virtual_functionst
 };
 
 remove_virtual_functionst::remove_virtual_functionst(
-  const symbol_tablet &_symbol_table,
-  const goto_functionst &goto_functions):
+  const symbol_tablet &_symbol_table):
   ns(_symbol_table),
   symbol_table(_symbol_table)
 {
@@ -436,9 +434,7 @@ void remove_virtual_functions(
   const symbol_tablet &symbol_table,
   goto_functionst &goto_functions)
 {
-  remove_virtual_functionst
-    rvf(symbol_table, goto_functions);
-
+  remove_virtual_functionst rvf(symbol_table);
   rvf(goto_functions);
 }
 
@@ -448,15 +444,24 @@ void remove_virtual_functions(goto_modelt &goto_model)
     goto_model.symbol_table, goto_model.goto_functions);
 }
 
+void remove_virtual_functions(goto_model_functiont &function)
+{
+  remove_virtual_functionst rvf(function.get_symbol_table());
+  bool changed = rvf.remove_virtual_functions(
+    function.get_goto_function().body);
+  // Give fresh location numbers to `function`, in case it has grown:
+  if(changed)
+    function.compute_location_numbers();
+}
+
 void remove_virtual_function(
   goto_modelt &goto_model,
   goto_programt &goto_program,
   goto_programt::targett instruction,
   const dispatch_table_entriest &dispatch_table,
   virtual_dispatch_fallback_actiont fallback_action)
 {
-  remove_virtual_functionst
-    rvf(goto_model.symbol_table, goto_model.goto_functions);
+  remove_virtual_functionst rvf(goto_model.symbol_table);
 
   rvf.remove_virtual_function(
     goto_program, instruction, dispatch_table, fallback_action);

src/goto-programs/remove_virtual_functions.h

@@ -25,6 +25,12 @@ void remove_virtual_functions(
   const symbol_tablet &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(goto_model_functiont &function);
+
 /// 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

src/jbmc/jbmc_parse_options.cpp

@@ -648,6 +648,8 @@ void jbmc_parse_optionst::process_goto_function(
     remove_asm(goto_function, symbol_table);
     // Removal of RTTI inspection:
     remove_instanceof(goto_function, symbol_table);
+    // Java virtual functions -> explicit dispatch tables:
+    remove_virtual_functions(function);
   }
 
   catch(const char *e)
@@ -678,8 +680,6 @@ bool jbmc_parse_optionst::process_goto_functions(
     remove_java_new(goto_model, get_message_handler());
 
     status() << "Removal of virtual functions" << eom;
-    // Java virtual functions -> explicit dispatch tables:
-    remove_virtual_functions(goto_model);
     // remove catch and throw (introduces instanceof but request it is removed)
     remove_exceptions(
       goto_model, remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);