Add get-inherited-method utility

This takes inheritance from interface default methods into account.

Author: smowton

src/goto-programs/resolve_inherited_component.cpp

@@ -106,3 +106,43 @@ irep_idt resolve_inherited_componentt::inherited_componentt::
   return resolve_inherited_componentt::build_full_component_identifier(
     class_identifier, component_identifier);
 }
+
+/// Given a class and a component, identify the concrete method it is
+/// resolved to. For example, a reference Child.abc refers to Child's method or
+/// field if it exists, or else Parent.abc, and so on regarding Parent's
+/// ancestors. If none are found, an empty string will be returned.
+/// This looks first for non-abstract methods inherited from the first base
+/// (i.e., for Java the superclass), then for non-abstract methods inherited
+/// otherwise (for Java, interface default methods), then for any abstract
+/// declaration.
+/// \param classname: The name of the class the function is being called on
+/// \param call_basename: The base name of the component (i.e. without the
+///   class specifier)
+/// \param symbol_table: Global symbol table
+/// \return The concrete component that has been resolved
+optionalt<resolve_inherited_componentt::inherited_componentt>
+get_inherited_method_implementation(
+  const irep_idt &call_basename,
+  const irep_idt &classname,
+  const symbol_tablet &symbol_table)
+{
+  resolve_inherited_componentt call_resolver{symbol_table};
+  auto exclude_abstract_methods = [&](const symbolt &symbol) {
+    return !symbol.type.get_bool(ID_C_abstract);
+  };
+
+  auto resolved_call =
+    call_resolver(classname, call_basename, false, exclude_abstract_methods);
+  if(!resolved_call)
+  {
+    // Check for a default implementation:
+    resolved_call =
+      call_resolver(classname, call_basename, true, exclude_abstract_methods);
+  }
+  if(!resolved_call)
+  {
+    // Finally accept any abstract definition, which will likely get stubbed:
+    resolved_call = call_resolver(classname, call_basename, true);
+  }
+  return resolved_call;
+}

src/goto-programs/resolve_inherited_component.h

@@ -59,4 +59,10 @@ class resolve_inherited_componentt
   const symbol_tablet &symbol_table;
 };
 
+optionalt<resolve_inherited_componentt::inherited_componentt>
+get_inherited_method_implementation(
+  const irep_idt &call_basename,
+  const irep_idt &classname,
+  const symbol_tablet &symbol_table);
+
 #endif // CPROVER_GOTO_PROGRAMS_RESOLVE_INHERITED_COMPONENT_H