Search static fields inherited from interfaces

Previously we assumed that static fields, like regular fields, could only be
inherited from ordinary classes, but in fact they can also come from interfaces.
We therefore augment resolve-inherited-component to optionally search in all ancestors
including interfaces, and use that facility when searching for inherited static fields.

Author: smowton

src/goto-programs/remove_virtual_functions.cpp

@@ -390,11 +390,11 @@ void remove_virtual_functionst::get_functions(
   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_inherited_componentt::inherited_componentt
-    &resolved_call = get_virtual_call_target(class_id, function_name);
+    &resolved_call = get_virtual_call_target(class_id, function_name, false);
 
   dispatch_table_entryt root_function;
 

src/goto-programs/resolve_inherited_component.cpp

@@ -40,17 +40,25 @@ resolve_inherited_componentt::resolve_inherited_componentt(
 /// \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)
+    const irep_idt &class_id,
+    const irep_idt &component_name,
+    bool include_interfaces)
 {
   PRECONDITION(!class_id.empty());
   PRECONDITION(!component_name.empty());
 
-  irep_idt current_class=class_id;
-  while(!current_class.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);
 
@@ -62,9 +70,16 @@ resolve_inherited_componentt::inherited_componentt
     const class_hierarchyt::idst &parents=
       class_hierarchy.class_map[current_class].parents;
 
-    if(parents.empty())
-      break;
-    current_class=parents.front();
+    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();

src/goto-programs/resolve_inherited_component.h

@@ -57,7 +57,9 @@ class resolve_inherited_componentt
   };
 
   inherited_componentt operator()(
-    const irep_idt &class_id, const irep_idt &component_name);
+    const irep_idt &class_id,
+    const irep_idt &component_name,
+    bool include_interfaces);
 
   static irep_idt build_full_component_identifier(
     const irep_idt &class_name, const irep_idt &component_name);

src/java_bytecode/ci_lazy_methods.cpp

@@ -570,7 +570,7 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
 
   resolve_inherited_componentt call_resolver(symbol_table, class_hierarchy);
   const resolve_inherited_componentt::inherited_componentt resolved_call =
-    call_resolver(classname, call_basename);
+    call_resolver(classname, call_basename, false);
 
   if(resolved_call.is_valid())
     return resolved_call.get_full_component_identifier();

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2817,7 +2817,8 @@ bool java_bytecode_convert_methodt::is_method_inherited(
       methodid,
       classname,
       symbol_table,
-      class_hierarchy);
+      class_hierarchy,
+      false);
   return inherited_method.is_valid();
 }
 

src/java_bytecode/java_bytecode_language.cpp

@@ -451,13 +451,16 @@ static void create_stub_global_symbols(
         INVARIANT(
           !class_id.empty(), "get/putstatic should specify a class");
 
+        // The final 'true' parameter here includes interfaces, as they can
+        // define static fields.
         resolve_inherited_componentt::inherited_componentt referred_component =
           get_inherited_component(
             class_id,
             component,
             "java::" + id2string(parse_tree.parsed_class.name),
             symbol_table,
-            class_hierarchy);
+            class_hierarchy,
+            true);
         if(!referred_component.is_valid())
         {
           // Create a new stub global on the first incomplete (stub) parent of

src/java_bytecode/java_utils.cpp

@@ -337,19 +337,22 @@ std::string pretty_print_java_type(const std::string &fqn_java_type)
 ///   scoped components are visible from a particular use site.
 /// \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
 ///   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 class_hierarchyt &class_hierarchy)
+  const class_hierarchyt &class_hierarchy,
+  bool include_interfaces)
 {
   resolve_inherited_componentt component_resolver(
     symbol_table, class_hierarchy);
   const resolve_inherited_componentt::inherited_componentt resolved_component =
-    component_resolver(component_class_id, component_name);
+    component_resolver(component_class_id, component_name, include_interfaces);
 
   // resolved_component is a pair (class-name, component-name) found by walking
   // the chain of class inheritance (not interfaces!) and stopping on the first

src/java_bytecode/java_utils.h

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