diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 614809a8e00..374aae97fac 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -547,7 +547,7 @@ irep_idt ci_lazy_methodst::get_virtual_method_target( if(!instantiated_classes.count(classname)) return irep_idt(); - resolve_inherited_componentt call_resolver(symbol_table, class_hierarchy); + resolve_inherited_componentt call_resolver{symbol_table}; const auto resolved_call = call_resolver(classname, call_basename, false); if(resolved_call) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index cf4c4ccd83f..166c53f83cc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -3209,8 +3209,8 @@ bool java_bytecode_convert_methodt::is_method_inherited( const irep_idt &classname, const irep_idt &methodid) const { - const auto inherited_method = get_inherited_component( - classname, methodid, symbol_table, class_hierarchy, false); + const auto inherited_method = + get_inherited_component(classname, methodid, symbol_table, false); return inherited_method.has_value(); } @@ -3224,7 +3224,7 @@ irep_idt java_bytecode_convert_methodt::get_static_field( const irep_idt &component_name) const { const auto inherited_method = get_inherited_component( - class_identifier, component_name, symbol_table, class_hierarchy, true); + class_identifier, component_name, symbol_table, true); INVARIANT( inherited_method.has_value(), "static field should be in symbol table"); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index c5f46b549e7..999ba58f9d3 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -672,8 +672,8 @@ static void create_stub_global_symbols( // The final 'true' parameter here includes interfaces, as they can // define static fields. - const auto referred_component = get_inherited_component( - class_id, component, symbol_table, class_hierarchy, true); + const auto referred_component = + get_inherited_component(class_id, component, symbol_table, true); if(!referred_component) { // Create a new stub global on an arbitrary incomplete ancestor of the diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index aceaff37895..ad1f1570417 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -371,7 +371,6 @@ std::string pretty_print_java_type(const std::string &fqn_java_type) /// \param component_name: component basename to search for. If searching for /// A.b, this is "b". /// \param symbol_table: global symbol table. -/// \param class_hierarchy: global class hierarchy. /// \param include_interfaces: if true, search for the given component in all /// ancestors including interfaces, rather than just parents. /// \return the concrete component referred to if any is found, or an invalid @@ -381,11 +380,9 @@ get_inherited_component( const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, - const class_hierarchyt &class_hierarchy, bool include_interfaces) { - resolve_inherited_componentt component_resolver( - symbol_table, class_hierarchy); + resolve_inherited_componentt component_resolver{symbol_table}; const auto resolved_component = component_resolver(component_class_id, component_name, include_interfaces); diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index c5891a43ccf..c49682f59b8 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -122,7 +122,6 @@ get_inherited_component( const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, - const class_hierarchyt &class_hierarchy, bool include_interfaces); bool is_non_null_library_global(const irep_idt &); diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 188fca08060..e47d23277b2 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -589,8 +589,7 @@ void get_virtual_calleest::get_functions( const std::string function_name_string(id2string(function_name)); INVARIANT(!class_id.empty(), "All virtual functions must have a class"); - resolve_inherited_componentt get_virtual_call_target( - symbol_table, class_hierarchy); + resolve_inherited_componentt get_virtual_call_target{symbol_table}; const function_call_resolvert resolve_function_call = [&get_virtual_call_target]( const irep_idt &class_id, const irep_idt &function_name) { diff --git a/src/goto-programs/resolve_inherited_component.cpp b/src/goto-programs/resolve_inherited_component.cpp index 97003d73092..ace9bd78438 100644 --- a/src/goto-programs/resolve_inherited_component.cpp +++ b/src/goto-programs/resolve_inherited_component.cpp @@ -12,16 +12,10 @@ Author: Diffblue Ltd. /// See the operator() method comment /// \param symbol_table: The symbol table to resolve the component against -/// \param class_hierarchy: A prebuilt class_hierachy based on the symbol_table -/// resolve_inherited_componentt::resolve_inherited_componentt( - const symbol_tablet &symbol_table, - const class_hierarchyt &class_hierarchy) - : class_hierarchy(class_hierarchy), symbol_table(symbol_table) + const symbol_tablet &symbol_table) + : symbol_table(symbol_table) { - // We require the class_hierarchy to be already populated if we are being - // supplied it. - PRECONDITION(!class_hierarchy.class_map.empty()); } /// Given a class and a component, identify the concrete field or method it is @@ -58,10 +52,16 @@ resolve_inherited_componentt::operator()( return inherited_componentt(current_class, component_name); } - const auto current_class_id = class_hierarchy.class_map.find(current_class); - if(current_class_id != class_hierarchy.class_map.end()) + const auto current_class_symbol_it = + symbol_table.symbols.find(current_class); + + if(current_class_symbol_it != symbol_table.symbols.end()) { - const class_hierarchyt::idst &parents = current_class_id->second.parents; + const auto parents = + make_range(to_struct_type(current_class_symbol_it->second.type).bases()) + .map([](const struct_typet::baset &base) { + return base.type().get_identifier(); + }); if(include_interfaces) { @@ -71,7 +71,7 @@ resolve_inherited_componentt::operator()( else { if(!parents.empty()) - classes_to_visit.push_back(parents.front()); + classes_to_visit.push_back(*parents.begin()); } } } diff --git a/src/goto-programs/resolve_inherited_component.h b/src/goto-programs/resolve_inherited_component.h index daa0615b21d..7805e765ba2 100644 --- a/src/goto-programs/resolve_inherited_component.h +++ b/src/goto-programs/resolve_inherited_component.h @@ -21,8 +21,7 @@ Author: Diffblue Ltd. class resolve_inherited_componentt { public: - resolve_inherited_componentt( - const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy); + explicit resolve_inherited_componentt(const symbol_tablet &symbol_table); class inherited_componentt { @@ -54,7 +53,6 @@ class resolve_inherited_componentt const irep_idt &class_name, const irep_idt &component_name); private: - const class_hierarchyt &class_hierarchy; const symbol_tablet &symbol_table; };