Use a common instance of class_hierarchyt in get_inherited_component

This avoids constructing a fresh class_hierarchyt with a consequent sweep of the
complete symbol table every time inheritence is queried.

Author: smowton

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2764,7 +2764,8 @@ void java_bytecode_convert_method(
   message_handlert &message_handler,
   size_t max_array_length,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
-  java_string_library_preprocesst &string_preprocess)
+  java_string_library_preprocesst &string_preprocess,
+  const class_hierarchyt &class_hierarchy)
 {
   static const std::unordered_set<std::string> methods_to_ignore
   {
@@ -2795,19 +2796,28 @@ void java_bytecode_convert_method(
     message_handler,
     max_array_length,
     needed_lazy_methods,
-    string_preprocess);
+    string_preprocess,
+    class_hierarchy);
 
   java_bytecode_convert_method(class_symbol, method);
 }
 
 /// Returns true iff method \p methodid from class \p classname is
 /// a method inherited from a class (and not an interface!) from which
 /// \p classname inherits, either directly or indirectly.
+/// \param classname: class whose method is referenced
+/// \param methodid: method basename
 bool java_bytecode_convert_methodt::is_method_inherited(
-  const irep_idt &classname, const irep_idt &methodid) const
+  const irep_idt &classname,
+  const irep_idt &methodid) const
 {
   resolve_inherited_componentt::inherited_componentt inherited_method =
-    get_inherited_component(classname, methodid, classname, symbol_table);
+    get_inherited_component(
+      classname,
+      methodid,
+      classname,
+      symbol_table,
+      class_hierarchy);
   return inherited_method.is_valid();
 }
 

src/java_bytecode/java_bytecode_convert_method.h

@@ -34,7 +34,8 @@ void java_bytecode_convert_method(
   message_handlert &message_handler,
   size_t max_array_length,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
-  java_string_library_preprocesst &string_preprocess);
+  java_string_library_preprocesst &string_preprocess,
+  const class_hierarchyt &class_hierarchy);
 
 void java_bytecode_convert_method_lazy(
   const symbolt &class_symbol,

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -35,14 +35,16 @@ class java_bytecode_convert_methodt:public messaget
     message_handlert &_message_handler,
     size_t _max_array_length,
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
-    java_string_library_preprocesst &_string_preprocess)
+    java_string_library_preprocesst &_string_preprocess,
+    const class_hierarchyt &class_hierarchy)
     : messaget(_message_handler),
       symbol_table(symbol_table),
       max_array_length(_max_array_length),
       needed_lazy_methods(std::move(needed_lazy_methods)),
       string_preprocess(_string_preprocess),
       slots_for_parameters(0),
-      method_has_this(false)
+      method_has_this(false),
+      class_hierarchy(class_hierarchy)
   {
   }
 
@@ -116,6 +118,7 @@ class java_bytecode_convert_methodt:public messaget
   bool method_has_this;
   std::map<irep_idt, bool> class_has_clinit_method;
   std::map<irep_idt, bool> any_superclass_has_clinit_method;
+  class_hierarchyt class_hierarchy;
 
   enum instruction_sizet
   {

src/java_bytecode/java_bytecode_language.cpp

@@ -426,9 +426,11 @@ static void create_stub_global_symbol(
 /// static fields, and nondet-initialised for primitives.
 /// \param parse_tree: class bytecode
 /// \param symbol_table: symbol table; may gain new symbols
+/// \param class_hierarchy: global class hierarchy
 static void create_stub_global_symbols(
   const java_bytecode_parse_treet &parse_tree,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  const class_hierarchyt &class_hierarchy)
 {
   namespacet ns(symbol_table);
   for(const auto &method : parse_tree.parsed_class.methods)
@@ -454,7 +456,8 @@ static void create_stub_global_symbols(
             class_id,
             component,
             "java::" + id2string(parse_tree.parsed_class.name),
-            symbol_table);
+            symbol_table,
+            class_hierarchy);
         if(!referred_component.is_valid())
         {
           irep_idt identifier =
@@ -523,6 +526,10 @@ bool java_bytecode_languaget::typecheck(
       return true;
   }
 
+  // Now that all classes have been created in the symbol table we can populate
+  // the class hierarchy:
+  class_hierarchy(symbol_table);
+
   // find and mark all implicitly generic class types
   // this can only be done once all the class symbols have been created
   for(const auto &c : java_class_loader.class_map)
@@ -582,7 +589,8 @@ bool java_bytecode_languaget::typecheck(
       journalling_symbol_tablet::wrap(symbol_table);
     for(const auto &c : java_class_loader.class_map)
     {
-      create_stub_global_symbols(c.second, symbol_table_journal);
+      create_stub_global_symbols(
+        c.second, symbol_table_journal, class_hierarchy);
     }
 
     stub_global_initializer_factory.create_stub_global_initializer_symbols(
@@ -875,7 +883,8 @@ bool java_bytecode_languaget::convert_single_method(
       get_message_handler(),
       max_user_array_length,
       std::move(needed_lazy_methods),
-      string_preprocess);
+      string_preprocess,
+      class_hierarchy);
     return false;
   }
 

src/java_bytecode/java_bytecode_language.h

@@ -174,6 +174,7 @@ class java_bytecode_languaget:public languaget
   const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
   synthetic_methods_mapt synthetic_methods;
   stub_global_initializer_factoryt stub_global_initializer_factory;
+  class_hierarchyt class_hierarchy;
 };
 
 std::unique_ptr<languaget> new_java_bytecode_language();

src/java_bytecode/java_utils.cpp

@@ -336,15 +336,18 @@ std::string pretty_print_java_type(const std::string &fqn_java_type)
 ///   component. The user class is relevant when determining whether package-
 ///   scoped components are visible from a particular use site.
 /// \param symbol_table: global symbol table.
+/// \param class_hierarchy: global class hierarchy.
 /// \return the concrete component referred to if any is found, or an invalid
 ///   resolve_inherited_componentt::inherited_componentt otherwise.
 resolve_inherited_componentt::inherited_componentt get_inherited_component(
   const irep_idt &component_class_id,
   const irep_idt &component_name,
   const irep_idt &user_class_id,
-  const symbol_tablet &symbol_table)
+  const symbol_tablet &symbol_table,
+  const class_hierarchyt &class_hierarchy)
 {
-  resolve_inherited_componentt component_resolver(symbol_table);
+  resolve_inherited_componentt component_resolver(
+    symbol_table, class_hierarchy);
   const resolve_inherited_componentt::inherited_componentt resolved_component =
     component_resolver(component_class_id, component_name);
 

src/java_bytecode/java_utils.h

@@ -102,6 +102,7 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
   const irep_idt &component_class_id,
   const irep_idt &component_name,
   const irep_idt &user_class_id,
-  const symbol_tablet &symbol_table);
+  const symbol_tablet &symbol_table,
+  const class_hierarchyt &class_hierarchy);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H