Add support for inheritence of Java static fields. Fixes TG-2457

src/goto-programs/Makefile

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

src/goto-programs/remove_virtual_functions.cpp

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include "class_hierarchy.h"
 #include "class_identifier.h"
 
-#include <goto-programs/resolve_concrete_function_call.h>
+#include <goto-programs/resolve_inherited_component.h>
 
 #include <util/c_types.h>
 #include <util/prefix.h>
@@ -48,7 +48,7 @@ class remove_virtual_functionst
 
   void get_functions(const exprt &, dispatch_table_entriest &);
   typedef std::function<
-    resolve_concrete_function_callt::concrete_function_callt(
+    resolve_inherited_componentt::inherited_componentt(
       const irep_idt &,
       const irep_idt &)>
     function_call_resolvert;
@@ -343,13 +343,14 @@ void remove_virtual_functionst::get_child_functions_rec(
     }
     if(function.symbol_expr == symbol_exprt())
     {
-      const resolve_concrete_function_callt::concrete_function_callt
+      const resolve_inherited_componentt::inherited_componentt
         &resolved_call = resolve_function_call(child, component_name);
       if(resolved_call.is_valid())
       {
         function.class_id = resolved_call.get_class_identifier();
         const symbolt &called_symbol =
-          symbol_table.lookup_ref(resolved_call.get_virtual_method_name());
+          symbol_table.lookup_ref(
+            resolved_call.get_full_component_identifier());
 
         function.symbol_expr = called_symbol.symbol_expr();
         function.symbol_expr.set(
@@ -384,16 +385,16 @@ void remove_virtual_functionst::get_functions(
   const std::string function_name_string(id2string(function_name));
   INVARIANT(!class_id.empty(), "All virtual functions must have a class");
 
-  resolve_concrete_function_callt get_virtual_call_target(
+  resolve_inherited_componentt get_virtual_call_target(
     symbol_table, class_hierarchy);
   const function_call_resolvert resolve_function_call =
     [&get_virtual_call_target](
       const irep_idt &class_id, const irep_idt &function_name) {
-      return get_virtual_call_target(class_id, function_name);
+    return get_virtual_call_target(class_id, function_name, false);
     };
 
-  const resolve_concrete_function_callt::concrete_function_callt
-    &resolved_call = get_virtual_call_target(class_id, function_name);
+  const resolve_inherited_componentt::inherited_componentt
+    &resolved_call = get_virtual_call_target(class_id, function_name, false);
 
   dispatch_table_entryt root_function;
 
@@ -402,7 +403,7 @@ void remove_virtual_functionst::get_functions(
     root_function.class_id=resolved_call.get_class_identifier();
 
     const symbolt &called_symbol =
-      symbol_table.lookup_ref(resolved_call.get_virtual_method_name());
+      symbol_table.lookup_ref(resolved_call.get_full_component_identifier());
 
     root_function.symbol_expr=called_symbol.symbol_expr();
     root_function.symbol_expr.set(
@@ -454,7 +455,7 @@ exprt remove_virtual_functionst::get_method(
   const irep_idt &component_name) const
 {
   const irep_idt &id=
-    resolve_concrete_function_callt::build_virtual_method_name(
+    resolve_inherited_componentt::build_full_component_identifier(
       class_id, component_name);
 
   const symbolt *symbol;

src/goto-programs/resolve_inherited_component.cpp

@@ -0,0 +1,117 @@
+/*******************************************************************\
+
+ Module: GOTO Program Utilities
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <algorithm>
+
+#include "resolve_inherited_component.h"
+
+/// See the operator() method comment.
+/// \param symbol_table: The symbol table to resolve the component against
+resolve_inherited_componentt::resolve_inherited_componentt(
+  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 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)
+{
+  // 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
+/// 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.
+/// \param class_id: The name of the class the function is being called on
+/// \param component_name: The base name of the component (i.e. without the
+///   class specifier)
+/// \param include_interfaces: If true, consider inheritence from interfaces
+///   (parent types other than the first listed)
+/// \return The concrete component that has been resolved
+resolve_inherited_componentt::inherited_componentt
+  resolve_inherited_componentt::operator()(
+    const irep_idt &class_id,
+    const irep_idt &component_name,
+    bool include_interfaces)
+{
+  PRECONDITION(!class_id.empty());
+  PRECONDITION(!component_name.empty());
+
+  std::vector<irep_idt> classes_to_visit;
+  classes_to_visit.push_back(class_id);
+  while(!classes_to_visit.empty())
+  {
+    irep_idt current_class = classes_to_visit.back();
+    classes_to_visit.pop_back();
+
+    const irep_idt &full_component_identifier=
+      build_full_component_identifier(current_class, component_name);
+
+    if(symbol_table.has_symbol(full_component_identifier))
+    {
+      return inherited_componentt(current_class, component_name);
+    }
+
+    const class_hierarchyt::idst &parents=
+      class_hierarchy.class_map[current_class].parents;
+
+    if(include_interfaces)
+    {
+      classes_to_visit.insert(
+        classes_to_visit.end(), parents.begin(), parents.end());
+    }
+    else
+    {
+      if(!parents.empty())
+        classes_to_visit.push_back(parents.front());
+    }
+  }
+
+  return inherited_componentt();
+}
+
+/// Build a component name as found in a GOTO symbol table equivalent to the
+/// name of a concrete component component_name on class class_name
+/// \param component_name: The name of the component
+/// \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
+///   component `component_name`
+irep_idt resolve_inherited_componentt::build_full_component_identifier(
+  const irep_idt &class_name, const irep_idt &component_name)
+{
+  // Verify the parameters are called in the correct order.
+  PRECONDITION(id2string(class_name).find("::")!=std::string::npos);
+  PRECONDITION(id2string(component_name).find("::")==std::string::npos);
+  return id2string(class_name)+'.'+id2string(component_name);
+}
+
+/// Get the full name of this function
+/// \return The symbol name for this function call
+irep_idt resolve_inherited_componentt::inherited_componentt::
+  get_full_component_identifier() const
+{
+  return resolve_inherited_componentt::build_full_component_identifier(
+    class_identifier, component_identifier);
+}
+
+/// Use to check if this inherited_componentt has been fully constructed.
+/// \return True if this represents a real concrete component
+bool resolve_inherited_componentt::inherited_componentt::is_valid() const
+{
+  return !class_identifier.empty();
+}