Avoid recomputing class hierarchy

The class hierarchy never changes once the symbol table is computed. By sharing one instance
owned by the driver program, particularly across function passes, we can avoid many potentially
expensive recomputations.

Author: smowton

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -673,9 +673,12 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
 
     // remove Java throw and catch
     // This introduces instanceof, so order is important:
-    remove_exceptions(goto_model, get_message_handler());
-    // remove rtti
-    remove_instanceof(goto_model, get_message_handler());
+    remove_exceptions(goto_model, nullptr, get_message_handler());
+
+    // Java instanceof -> clsid comparison:
+    class_hierarchyt class_hierarchy;
+    class_hierarchy(goto_model.symbol_table);
+    remove_instanceof(goto_model, class_hierarchy, get_message_handler());
 
     // do partial inlining
     status() << "Partial Inlining" << eom;

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -87,21 +87,31 @@ class remove_exceptionst
 
   explicit remove_exceptionst(
     symbol_table_baset &_symbol_table,
+    const class_hierarchyt *class_hierarchy,
     function_may_throwt _function_may_throw,
     bool remove_added_instanceof,
     message_handlert &message_handler)
     : symbol_table(_symbol_table),
+      class_hierarchy(class_hierarchy),
       function_may_throw(_function_may_throw),
       remove_added_instanceof(remove_added_instanceof),
       message_handler(message_handler)
   {
+    if(remove_added_instanceof)
+    {
+      INVARIANT(
+        class_hierarchy != nullptr,
+        "remove_exceptions needs a class hierarchy to remove instanceof "
+        "statements");
+    }
   }
 
   void operator()(goto_functionst &goto_functions);
   void operator()(goto_programt &goto_program);
 
 protected:
   symbol_table_baset &symbol_table;
+  const class_hierarchyt *class_hierarchy;
   function_may_throwt function_may_throw;
   bool remove_added_instanceof;
   message_handlert &message_handler;
@@ -345,7 +355,14 @@ void remove_exceptionst::add_exception_dispatch_sequence(
         t_exc->guard=check;
 
         if(remove_added_instanceof)
-          remove_instanceof(t_exc, goto_program, symbol_table, message_handler);
+        {
+          remove_instanceof(
+            t_exc,
+            goto_program,
+            symbol_table,
+            *class_hierarchy,
+            message_handler);
+        }
       }
     }
   }
@@ -576,6 +593,7 @@ void remove_exceptionst::operator()(goto_programt &goto_program)
 /// removes throws/CATCH-POP/CATCH-PUSH
 void remove_exceptions(
   symbol_table_baset &symbol_table,
+  const class_hierarchyt *class_hierarchy,
   goto_functionst &goto_functions,
   message_handlert &message_handler,
   remove_exceptions_typest type)
@@ -589,6 +607,7 @@ void remove_exceptions(
     };
   remove_exceptionst remove_exceptions(
     symbol_table,
+    class_hierarchy,
     function_may_throw,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
     message_handler);
@@ -605,13 +624,16 @@ void remove_exceptions(
 /// \param symbol_table: global symbol table. The `@inflight_exception` global
 ///   may be added if not already present. It will not be initialised; that is
 ///   the caller's responsibility.
+/// \param class_hierarchy: class hierarchy analysis of symbol_table.
+///   Only needed if type == REMOVE_ADDED_INSTANCEOF; otherwise may be null.
 /// \param message_handler: logging output
 /// \param type: specifies whether instanceof operations generated by this pass
 ///   should be lowered to class-identifier comparisons (using
 ///   remove_instanceof).
 void remove_exceptions(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt *class_hierarchy,
   message_handlert &message_handler,
   remove_exceptions_typest type)
 {
@@ -620,6 +642,7 @@ void remove_exceptions(
 
   remove_exceptionst remove_exceptions(
     symbol_table,
+    class_hierarchy,
     any_function_may_throw,
     type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF,
     message_handler);
@@ -640,9 +663,14 @@ void remove_exceptions(
 ///   remove_instanceof).
 void remove_exceptions(
   goto_modelt &goto_model,
+  const class_hierarchyt *class_hierarchy,
   message_handlert &message_handler,
   remove_exceptions_typest type)
 {
   remove_exceptions(
-    goto_model.symbol_table, goto_model.goto_functions, message_handler, type);
+    goto_model.symbol_table,
+    class_hierarchy,
+    goto_model.goto_functions,
+    message_handler,
+    type);
 }

jbmc/src/java_bytecode/remove_exceptions.h

@@ -14,6 +14,7 @@ Date:   December 2016
 #ifndef CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
 #define CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
 
+#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_model.h>
 
 #include <util/message.h>
@@ -34,12 +35,14 @@ enum class remove_exceptions_typest
 void remove_exceptions(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt *class_hierarchy,
   message_handlert &message_handler,
   remove_exceptions_typest type =
     remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);
 
 void remove_exceptions(
   goto_modelt &goto_model,
+  const class_hierarchyt *class_hierarchy,
   message_handlert &message_handler,
   remove_exceptions_typest type =
     remove_exceptions_typest::DONT_REMOVE_INSTANCEOF);

jbmc/src/java_bytecode/remove_instanceof.cpp

@@ -24,12 +24,14 @@ class remove_instanceoft
 {
 public:
   remove_instanceoft(
-    symbol_table_baset &symbol_table, message_handlert &message_handler)
+    symbol_table_baset &symbol_table,
+    const class_hierarchyt &class_hierarchy,
+    message_handlert &message_handler)
     : symbol_table(symbol_table)
+    , class_hierarchy(class_hierarchy)
     , ns(symbol_table)
     , message_handler(message_handler)
   {
-    class_hierarchy(symbol_table);
   }
 
   // Lower instanceof for a single function
@@ -40,8 +42,8 @@ class remove_instanceoft
 
 protected:
   symbol_table_baset &symbol_table;
+  const class_hierarchyt &class_hierarchy;
   namespacet ns;
-  class_hierarchyt class_hierarchy;
   message_handlert &message_handler;
 
   bool lower_instanceof(
@@ -240,14 +242,16 @@ bool remove_instanceoft::lower_instanceof(goto_programt &goto_program)
 /// \param target: The instruction to work on.
 /// \param goto_program: The function body containing the instruction.
 /// \param symbol_table: The symbol table to add symbols to.
+/// \param class_hierarchy: class hierarchy analysis of symbol_table
 /// \param message_handler: logging output
 void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
   rem.lower_instanceof(goto_program, target);
 }
 
@@ -256,13 +260,15 @@ void remove_instanceof(
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
 /// \param function: The function to work on.
 /// \param symbol_table: The symbol table to add symbols to.
+/// \param class_hierarchy: class hierarchy analysis of symbol_table
 /// \param message_handler: logging output
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
   rem.lower_instanceof(function.body);
 }
 
@@ -271,13 +277,15 @@ void remove_instanceof(
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
 /// \param goto_functions: The functions to work on.
 /// \param symbol_table: The symbol table to add symbols to.
+/// \param class_hierarchy: class hierarchy analysis of symbol_table
 /// \param message_handler: logging output
 void remove_instanceof(
   goto_functionst &goto_functions,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
-  remove_instanceoft rem(symbol_table, message_handler);
+  remove_instanceoft rem(symbol_table, class_hierarchy, message_handler);
   bool changed=false;
   for(auto &f : goto_functions.function_map)
     changed=rem.lower_instanceof(f.second.body) || changed;
@@ -289,12 +297,18 @@ void remove_instanceof(
 /// class-identifier test.
 /// \remarks Extra auxiliary variables may be introduced into symbol_table.
 /// \param goto_model: The functions to work on and the symbol table to add
+/// \param class_hierarchy: class hierarchy analysis of goto_model's symbol
+///   table
 /// \param message_handler: logging output
 /// symbols to.
 void remove_instanceof(
   goto_modelt &goto_model,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &message_handler)
 {
   remove_instanceof(
-    goto_model.goto_functions, goto_model.symbol_table, message_handler);
+    goto_model.goto_functions,
+    goto_model.symbol_table,
+    class_hierarchy,
+    message_handler);
 }

jbmc/src/java_bytecode/remove_instanceof.h

@@ -79,6 +79,7 @@ Author: Chris Smowton, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 #define CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 
+#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_model.h>
 
@@ -89,18 +90,24 @@ void remove_instanceof(
   goto_programt::targett target,
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &);
 
 void remove_instanceof(
   goto_functionst::goto_functiont &function,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &);
 
 void remove_instanceof(
   goto_functionst &goto_functions,
   symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy,
   message_handlert &);
 
-void remove_instanceof(goto_modelt &model, message_handlert &);
+void remove_instanceof(
+  goto_modelt &model,
+  const class_hierarchyt &class_hierarchy,
+  message_handlert &);
 
 #endif

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -529,6 +529,9 @@ int jbmc_parse_optionst::doit()
       *this, options, get_message_handler());
     lazy_goto_model.initialize(cmdline, options);
 
+    class_hierarchy = util_make_unique<class_hierarchyt>();
+    (*class_hierarchy)(lazy_goto_model.symbol_table);
+
     // The precise wording of this error matches goto-symex's complaint when no
     // __CPROVER_start exists (if we just go ahead and run it anyway it will
     // trip an invariant when it tries to load it)
@@ -606,12 +609,13 @@ int jbmc_parse_optionst::get_goto_program(
       *this, options, get_message_handler());
     lazy_goto_model.initialize(cmdline, options);
 
+    class_hierarchy = util_make_unique<class_hierarchyt>();
+    (*class_hierarchy)(lazy_goto_model.symbol_table);
+
     // Show the class hierarchy
     if(cmdline.isset("show-class-hierarchy"))
     {
-      class_hierarchyt hierarchy;
-      hierarchy(lazy_goto_model.symbol_table);
-      show_class_hierarchy(hierarchy, ui_message_handler);
+      show_class_hierarchy((*class_hierarchy), ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
 
@@ -702,7 +706,8 @@ void jbmc_parse_optionst::process_goto_function(
   try
   {
     // Removal of RTTI inspection:
-    remove_instanceof(goto_function, symbol_table, get_message_handler());
+    remove_instanceof(
+      goto_function, symbol_table, *class_hierarchy, get_message_handler());
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(function);
 
@@ -716,6 +721,7 @@ void jbmc_parse_optionst::process_goto_function(
       remove_exceptions(
         goto_function.body,
         symbol_table,
+        class_hierarchy.get(),
         get_message_handler(),
         remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
     }
@@ -857,6 +863,7 @@ bool jbmc_parse_optionst::process_goto_functions(
     // (introduces instanceof but request it is removed)
     remove_exceptions(
       goto_model,
+      class_hierarchy.get(),
       get_message_handler(),
       remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF);
 

jbmc/src/jbmc/jbmc_parse_options.h

@@ -121,6 +121,8 @@ class jbmc_parse_optionst:
   object_factory_parameterst object_factory_params;
   bool stub_objects_are_not_null;
 
+  std::unique_ptr<class_hierarchyt> class_hierarchy;
+
   void get_command_line_options(optionst &);
   int get_goto_program(
     std::unique_ptr<goto_modelt> &goto_model, const optionst &);

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -351,10 +351,15 @@ bool jdiff_parse_optionst::process_goto_program(
 
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
-    // remove catch and throw
-    remove_exceptions(goto_model, get_message_handler());
+
+    // remove Java throw and catch
+    // This introduces instanceof, so order is important:
+    remove_exceptions(goto_model, nullptr, get_message_handler());
+
     // Java instanceof -> clsid comparison:
-    remove_instanceof(goto_model, get_message_handler());
+    class_hierarchyt class_hierarchy;
+    class_hierarchy(goto_model.symbol_table);
+    remove_instanceof(goto_model, class_hierarchy, get_message_handler());
 
     mm_io(goto_model);
 

jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp

@@ -141,7 +141,10 @@ void load_and_test_method(
 
   // Emulate some of the passes that we'd normally do before replace_java_nondet
   // is called.
-  remove_instanceof(goto_function, symbol_table, null_message_handler);
+  class_hierarchyt class_hierarchy;
+  class_hierarchy(symbol_table);
+  remove_instanceof(
+    goto_function, symbol_table, class_hierarchy, null_message_handler);
 
   remove_virtual_functions(model_function);