Pulled out logic for finding the correct resolution for a given virtual call

When calling method f on a class A, if class A implements it, A::f is
called. If it doesn't then we should work up the class hierachy till we
find a class that fills in the gap. This was separately implemented in
different locations with varying levels of accuracy. This pulls all
three into a common class responsible for this.

Author: thk123

src/goto-programs/Makefile

@@ -49,6 +49,7 @@ SRC = basic_blocks.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
       replace_java_nondet.cpp \
+      resolve_concrete_function_call.cpp \
       safety_checker.cpp \
       set_properties.cpp \
       show_goto_functions.cpp \

src/goto-programs/remove_virtual_functions.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include "class_hierarchy.h"
 #include "class_identifier.h"
 
+#include <goto-programs/resolve_concrete_function_call.h>
+
 #include <util/c_types.h>
 #include <util/prefix.h>
 #include <util/type_eq.h>
@@ -258,32 +260,26 @@ void remove_virtual_functionst::get_functions(
 {
   const irep_idt class_id=function.get(ID_C_class);
   const irep_idt component_name=function.get(ID_component_name);
-  assert(!class_id.empty());
+  INVARIANT(!class_id.empty(), "All virtual functions must have a class");
+
+  resolve_concrete_function_callt get_virtual_call_target(
+    symbol_table, class_hierarchy);
+  const resolve_concrete_function_callt::concrete_function_callt &
+    resolved_call=get_virtual_call_target(class_id, component_name);
   functiont root_function;
 
-  // Start from current class, go to parents until something
-  // is found.
-  irep_idt c=class_id;
-  while(!c.empty())
+  if(resolved_call.is_valid())
   {
-    exprt method=get_method(c, component_name);
-    if(method.is_not_nil())
-    {
-      root_function.class_id=c;
-      root_function.symbol_expr=to_symbol_expr(method);
-      root_function.symbol_expr.set(ID_C_class, c);
-      break; // abort
-    }
+    root_function.class_id=resolved_call.get_class_identifier();
 
-    const class_hierarchyt::idst &parents=
-      class_hierarchy.class_map[c].parents;
+    const symbolt &called_symbol=
+      symbol_table.lookup(resolved_call.get_virtual_method_name());
 
-    if(parents.empty())
-      break;
-    c=parents.front();
+    root_function.symbol_expr=called_symbol.symbol_expr();
+    root_function.symbol_expr.set(
+      ID_C_class, resolved_call.get_class_identifier());
   }
-
-  if(root_function.class_id.empty())
+  else
   {
     // No definition here; this is an abstract function.
     root_function.class_id=class_id;
@@ -306,8 +302,9 @@ exprt remove_virtual_functionst::get_method(
   const irep_idt &class_id,
   const irep_idt &component_name) const
 {
-  irep_idt id=id2string(class_id)+"."+
-              id2string(component_name);
+  const irep_idt &id=
+    resolve_concrete_function_callt::build_virtual_method_name(
+      class_id, component_name);
 
   const symbolt *symbol;
   if(ns.lookup(id, symbol))

src/goto-programs/resolve_concrete_function_call.cpp

@@ -0,0 +1,102 @@
+/*******************************************************************\
+
+ Module: GOTO Program Utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <algorithm>
+
+#include "resolve_concrete_function_call.h"
+
+/// See the operator() method comment.
+/// \param symbol_table: The symbol table to resolve the function call in
+resolve_concrete_function_callt::resolve_concrete_function_callt(
+  const symbol_tablet &symbol_table):
+    symbol_table(symbol_table)
+{
+  class_hierarchy(symbol_table);
+}
+
+/// See the operator() method comment
+/// \param symbol_table: The symbol table to resolve the function call in
+/// \param class_hierarchy: A prebuilt class_hierachy based on the symbol_table
+///
+resolve_concrete_function_callt::resolve_concrete_function_callt(
+  const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy):
+    class_hierarchy(class_hierarchy),
+    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 virtual function call, identify what concrete call this would be
+/// resolved to. For example, calling a method on a class will call its
+/// implementions if it exists, else will call the first parent that provides an
+/// implementation. If none are found, an empty string will be returned.
+/// \param class_id: The name of the class the function is being called on
+/// \param component_name: The base name of the function (e.g. without the
+///   class specifier
+/// \return The concrete call that has been resolved
+resolve_concrete_function_callt::concrete_function_callt
+  resolve_concrete_function_callt::operator()(
+    const irep_idt &class_id, const irep_idt &component_name)
+{
+  PRECONDITION(!class_id.empty());
+  PRECONDITION(!component_name.empty());
+
+  irep_idt current_class=class_id;
+  while(!current_class.empty())
+  {
+    const irep_idt &virtual_method_name=
+      build_virtual_method_name(current_class, component_name);
+
+    if(symbol_table.has_symbol(virtual_method_name))
+    {
+      return concrete_function_callt(current_class, component_name);
+    }
+
+    const class_hierarchyt::idst &parents=
+      class_hierarchy.class_map[current_class].parents;
+
+    if(parents.empty())
+      break;
+    current_class=parents.front();
+  }
+
+  return concrete_function_callt();
+}
+
+/// Build a method name as found in a GOTO symbol table equivalent to the name
+/// of a concrete call of method component_method_name on class class_name
+/// \param component_method_name: The name of the function
+/// \param class_name: The class the implementation would be found on.
+/// \return A name for looking up in the symbol table for classes `class_name`'s
+///   implementation of `component_name`
+irep_idt resolve_concrete_function_callt::build_virtual_method_name(
+  const irep_idt &class_name, const irep_idt &component_method_name)
+{
+  // Verify the parameters are called in the correct order.
+  PRECONDITION(id2string(class_name).find("::")!=std::string::npos);
+  PRECONDITION(id2string(component_method_name).find("(")!=std::string::npos);
+  return id2string(class_name)+'.'+id2string(component_method_name);
+}
+
+/// Get the full name of this function
+/// \return The symbol name for this function call
+irep_idt resolve_concrete_function_callt::concrete_function_callt::
+  get_virtual_method_name() const
+{
+  return resolve_concrete_function_callt::build_virtual_method_name(
+    class_identifier, function_identifier);
+}
+
+/// Use to check if this concrete_function_callt has been fully constructed.
+/// \return True if this represents a real concrete function call
+bool resolve_concrete_function_callt::concrete_function_callt::is_valid() const
+{
+  return !class_identifier.empty();
+}

src/goto-programs/resolve_concrete_function_call.h

@@ -0,0 +1,75 @@
+/*******************************************************************\
+
+ Module: GOTO Program Utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+/// \file
+/// Given a virtual function call on a specific class, find which implementation
+/// needs to be used.
+
+#ifndef CPROVER_GOTO_PROGRAMS_RESOLVE_CONCRETE_FUNCTION_CALL_H
+#define CPROVER_GOTO_PROGRAMS_RESOLVE_CONCRETE_FUNCTION_CALL_H
+
+#include <util/symbol_table.h>
+#include <util/std_expr.h>
+#include <util/std_code.h>
+#include <goto-programs/class_hierarchy.h>
+
+class resolve_concrete_function_callt
+{
+public:
+  explicit resolve_concrete_function_callt(const symbol_tablet &symbol_table);
+  resolve_concrete_function_callt(
+    const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy);
+
+  class concrete_function_callt
+  {
+  public:
+    concrete_function_callt()
+    {}
+
+    concrete_function_callt(
+      const irep_idt &class_id, const irep_idt &method_id):
+        class_identifier(class_id),
+        function_identifier(method_id)
+    {}
+
+    irep_idt get_virtual_method_name() const;
+
+    irep_idt get_class_identifier() const
+    {
+      return class_identifier;
+    }
+
+    irep_idt get_function_identifier() const
+    {
+      return function_identifier;
+    }
+
+    bool is_valid() const;
+
+  private:
+    irep_idt class_identifier;
+    irep_idt function_identifier;
+  };
+
+  concrete_function_callt operator()(
+    const irep_idt &class_id, const irep_idt &component_name);
+
+  static irep_idt build_virtual_method_name(
+    const irep_idt &class_name, const irep_idt &component_method_name);
+
+private:
+  bool does_implementation_exist(
+    const irep_idt &class_name,
+    const irep_idt &component_method_name,
+    const irep_idt &calling_class_name);
+
+  class_hierarchyt class_hierarchy;
+  const symbol_tablet &symbol_table;
+};
+
+#endif // CPROVER_GOTO_PROGRAMS_RESOLVE_CONCRETE_FUNCTION_CALL_H

src/java_bytecode/gather_methods_lazily.cpp

@@ -15,6 +15,8 @@
 #include <util/suffix.h>
 #include <java_bytecode/java_string_library_preprocess.h>
 
+#include <goto-programs/resolve_concrete_function_call.h>
+
 
 gather_methods_lazilyt::gather_methods_lazilyt(
   const symbol_tablet &symbol_table,
@@ -468,41 +470,14 @@ irep_idt gather_methods_lazilyt::get_virtual_method_target(
   // Program-wide, is this class ever instantiated?
   if(!needed_classes.count(classname))
     return irep_idt();
-  auto methodid=build_virtual_method_name(classname, call_basename);
-  if(symbol_table.has_symbol(methodid))
-    return methodid;
+
+  resolve_concrete_function_callt call_resolver(symbol_table, class_hierarchy);
+  const resolve_concrete_function_callt ::concrete_function_callt &
+    resolved_call=call_resolver(classname, call_basename);
+
+  if(resolved_call.is_valid())
+    return resolved_call.get_virtual_method_name();
   else
-  {
-    // no method found for this specific classs, but a call to this class
-    // will be resolved in one of its base classes so we should work up the
-    // heirarchy to see if one resovles
-    class_hierarchyt::idst parent_classes=
-      class_hierarchy.get_parents_trans(classname);
-    for(const irep_idt &parent_class_id : parent_classes)
-    {
-      auto parent_method_id=
-        build_virtual_method_name(parent_class_id, call_basename);
-      if(symbol_table.has_symbol(parent_method_id))
-      {
-        return parent_method_id;
-      }
-    }
     return irep_idt();
-  }
 }
 
-
-/// Build a method name as found in a GOTO symbol table equivalent to the name
-/// of a concrete call of method component_method_name on class class_name
-/// \param component_method_name: The name of the function
-/// \param class_name: The class the implementation would be found on.
-/// \return A name for looking up in the symbol table for classes `class_name`'s
-///   implementation of `component_name`
-irep_idt gather_methods_lazilyt::build_virtual_method_name(
-  const irep_idt &class_name, const irep_idt &component_method_name)
-{
-  // Verify the parameters are called in the correct order.
-  PRECONDITION(id2string(class_name).find("::")!=std::string::npos);
-  PRECONDITION(id2string(component_method_name).find("(")!=std::string::npos);
-  return id2string(class_name)+'.'+id2string(component_method_name);
-}