Run remove-virtual-functions on a per-function basis

src/goto-programs/goto_functions_template.h

@@ -103,15 +103,26 @@ class goto_functions_templatet
   typedef std::map<irep_idt, goto_functiont> function_mapt;
   function_mapt function_map;
 
-  goto_functions_templatet()
+private:
+  /// A location number such that numbers in the interval
+  /// [unused_location_number, MAX_UINT] are all unused. There might still be
+  /// unused numbers below this.
+  /// If numbering a new function or renumbering a function, starting from this
+  /// number is safe.
+  unsigned unused_location_number;
+
+public:
+  goto_functions_templatet():
+    unused_location_number(0)
   {
   }
 
   goto_functions_templatet(const goto_functions_templatet &)=delete;
   goto_functions_templatet &operator=(const goto_functions_templatet &)=delete;
 
   goto_functions_templatet(goto_functions_templatet &&other):
-    function_map(std::move(other.function_map))
+    function_map(std::move(other.function_map)),
+    unused_location_number(other.unused_location_number)
   {
   }
 
@@ -133,6 +144,7 @@ class goto_functions_templatet
     std::ostream &out) const;
 
   void compute_location_numbers();
+  void compute_location_numbers(goto_programt &);
   void compute_loop_numbers();
   void compute_target_numbers();
   void compute_incoming_edges();
@@ -186,13 +198,23 @@ void goto_functions_templatet<bodyT>::output(
 template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_location_numbers()
 {
-  unsigned nr=0;
+  unused_location_number = 0;
   for(auto &func : function_map)
   {
-    func.second.body.compute_location_numbers(nr);
+    // Side-effect: bumps unused_location_number.
+    func.second.body.compute_location_numbers(unused_location_number);
   }
 }
 
+template <class bodyT>
+void goto_functions_templatet<bodyT>::compute_location_numbers(
+  goto_programt &program)
+{
+  // Renumber just this single function. Use fresh numbers in case it has
+  // grown since it was last numbered.
+  program.compute_location_numbers(unused_location_number);
+}
+
 template <class bodyT>
 void goto_functions_templatet<bodyT>::compute_incoming_edges()
 {

src/goto-programs/goto_model.h

@@ -67,4 +67,62 @@ class goto_modelt
   void unload(const irep_idt &name) { goto_functions.unload(name); }
 };
 
+/// Interface providing access to a single function in a GOTO model, plus its
+/// associated symbol table.
+/// Its purpose is to permit GOTO program renumbering (a non-const operation on
+/// goto_functionst) without providing a non-const reference to the entire
+/// function map. For example, incremental function loading uses this, as in
+/// that situation functions other than the one currently being loaded should
+/// not be altered.
+class goto_model_functiont
+{
+public:
+  /// Construct a function wrapper
+  /// \param goto_model: will be used to ensure unique numbering of
+  ///   goto programs, specifically incrementing its unused_location_number
+  ///   member each time a program is re-numbered.
+  /// \param goto_function: function to wrap.
+  explicit goto_model_functiont(
+    goto_modelt &goto_model, goto_functionst::goto_functiont &goto_function):
+  goto_model(goto_model),
+  goto_function(goto_function)
+  {
+  }
+
+  /// Re-number our goto_function. After this method returns all instructions'
+  /// location numbers may have changed, but will be globally unique and in
+  /// program order within the program.
+  void compute_location_numbers()
+  {
+    goto_model.goto_functions.compute_location_numbers(goto_function.body);
+  }
+
+  /// Get symbol table
+  /// \return symbol table from the associated GOTO model
+  symbol_tablet &get_symbol_table()
+  {
+    return goto_model.symbol_table;
+  }
+
+  /// Get GOTO function
+  /// \return the wrapped GOTO function
+  goto_functionst::goto_functiont &get_goto_function()
+  {
+    return goto_function;
+  }
+
+  /// Get GOTO model. This returns a const reference because this interface is
+  /// intended for use where non-const access to the whole model should not be
+  /// allowed.
+  /// \return const view of the whole GOTO model.
+  const goto_modelt &get_goto_model()
+  {
+    return goto_model;
+  }
+
+private:
+  goto_modelt &goto_model;
+  goto_functionst::goto_functiont &goto_function;
+};
+
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H

src/goto-programs/goto_program_template.h

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <sstream>
 #include <string>
 
+#include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 #include <util/source_location.h>
@@ -512,7 +513,12 @@ class goto_program_templatet
   void compute_location_numbers(unsigned &nr)
   {
     for(auto &i : instructions)
+    {
+      INVARIANT(
+        nr != std::numeric_limits<unsigned>::max(),
+        "Too many location numbers assigned");
       i.location_number=nr++;
+    }
   }
 
   /// Compute location numbers

src/goto-programs/lazy_goto_model.cpp

@@ -30,7 +30,8 @@ lazy_goto_modelt::lazy_goto_modelt(
       symbol_table,
       [this] (goto_functionst::goto_functiont &function) -> void
       {
-        this->post_process_function(function, symbol_table);
+        goto_model_functiont model_function(*goto_model, function);
+        this->post_process_function(model_function);
       },
       message_handler),
     post_process_function(std::move(post_process_function)),
@@ -49,7 +50,8 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
       symbol_table,
       [this] (goto_functionst::goto_functiont &function) -> void
       {
-        this->post_process_function(function, symbol_table);
+        goto_model_functiont model_function(*goto_model, function);
+        this->post_process_function(model_function);
       },
       other.message_handler),
     language_files(std::move(other.language_files)),

src/goto-programs/lazy_goto_model.h

@@ -15,14 +15,12 @@
 class cmdlinet;
 class optionst;
 
-
 /// Model that holds partially loaded map of functions
 class lazy_goto_modelt
 {
 public:
-  typedef std::function<void(
-    goto_functionst::goto_functiont &function,
-    symbol_tablet &symbol_table)> post_process_functiont;
+  typedef std::function<void(goto_model_functiont &function)>
+    post_process_functiont;
   typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
 
   explicit lazy_goto_modelt(
@@ -53,11 +51,9 @@ class lazy_goto_modelt
     message_handlert &message_handler)
   {
     return lazy_goto_modelt(
-      [&handler] (
-        goto_functionst::goto_functiont &function,
-        symbol_tablet &symbol_table) -> void
+      [&handler] (goto_model_functiont &function)
       {
-        handler.process_goto_function(function, symbol_table);
+        handler.process_goto_function(function);
       },
       [&handler, &options] (goto_modelt &goto_model) -> bool
       {

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

@@ -637,15 +637,19 @@ int jbmc_parse_optionst::get_goto_program(
 }
 
 void jbmc_parse_optionst::process_goto_function(
-  goto_functionst::goto_functiont &function, symbol_tablet &symbol_table)
+  goto_model_functiont &function)
 {
+  symbol_tablet &symbol_table = function.get_symbol_table();
+  goto_functionst::goto_functiont &goto_function = function.get_goto_function();
   try
   {
     // Remove inline assembler; this needs to happen before
     // adding the library.
-    remove_asm(function, symbol_table);
+    remove_asm(goto_function, symbol_table);
     // Removal of RTTI inspection:
-    remove_instanceof(function, symbol_table);
+    remove_instanceof(goto_function, symbol_table);
+    // Java virtual functions -> explicit dispatch tables:
+    remove_virtual_functions(function);
   }
 
   catch(const char *e)
@@ -676,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);

src/jbmc/jbmc_parse_options.h

@@ -81,8 +81,7 @@ class jbmc_parse_optionst:
     const char **argv,
     const std::string &extra_options);
 
-  void process_goto_function(
-    goto_functionst::goto_functiont &function, symbol_tablet &symbol_table);
+  void process_goto_function(goto_model_functiont &function);
   bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
 
 protected:

unit/testing-utils/load_java_class.cpp

@@ -62,7 +62,7 @@ symbol_tablet load_java_class(
   // Construct a lazy_goto_modelt
   null_message_handlert message_handler;
   lazy_goto_modelt lazy_goto_model(
-    [] (goto_functionst::goto_functiont &function, symbol_tablet &symbol_table)
+    [] (goto_model_functiont &function)
     { },
     [] (goto_modelt &goto_model)
     { return false; },