Clean resolve inherited component

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -548,11 +548,10 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
     return irep_idt();
 
   resolve_inherited_componentt call_resolver(symbol_table, class_hierarchy);
-  const resolve_inherited_componentt::inherited_componentt resolved_call =
-    call_resolver(classname, call_basename, false);
+  const auto resolved_call = call_resolver(classname, call_basename, false);
 
-  if(resolved_call.is_valid())
-    return resolved_call.get_full_component_identifier();
+  if(resolved_call)
+    return resolved_call->get_full_component_identifier();
   else
     return irep_idt();
 }

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -3147,14 +3147,9 @@ bool java_bytecode_convert_methodt::is_method_inherited(
   const irep_idt &classname,
   const irep_idt &methodid) const
 {
-  resolve_inherited_componentt::inherited_componentt inherited_method =
-    get_inherited_component(
-      classname,
-      methodid,
-      symbol_table,
-      class_hierarchy,
-      false);
-  return inherited_method.is_valid();
+  const auto inherited_method = get_inherited_component(
+    classname, methodid, symbol_table, class_hierarchy, false);
+  return inherited_method.has_value();
 }
 
 /// Get static field identifier referred to by `class_identifier.component_name`
@@ -3166,18 +3161,13 @@ irep_idt java_bytecode_convert_methodt::get_static_field(
   const irep_idt &class_identifier,
   const irep_idt &component_name) const
 {
-  resolve_inherited_componentt::inherited_componentt inherited_method =
-    get_inherited_component(
-      class_identifier,
-      component_name,
-      symbol_table,
-      class_hierarchy,
-      true);
+  const auto inherited_method = get_inherited_component(
+    class_identifier, component_name, symbol_table, class_hierarchy, true);
 
   INVARIANT(
-    inherited_method.is_valid(), "static field should be in symbol table");
+    inherited_method.has_value(), "static field should be in symbol table");
 
-  return inherited_method.get_full_component_identifier();
+  return inherited_method->get_full_component_identifier();
 }
 
 /// Create temporary variables if a write instruction can have undesired side-

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -591,14 +591,9 @@ static void create_stub_global_symbols(
 
         // 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,
-            symbol_table,
-            class_hierarchy,
-            true);
-        if(!referred_component.is_valid())
+        const auto referred_component = get_inherited_component(
+          class_id, component, symbol_table, class_hierarchy, true);
+        if(!referred_component)
         {
           // Create a new stub global on an arbitrary incomplete ancestor of the
           // class that was referred to. This is just a guess, but we have no

jbmc/src/java_bytecode/java_utils.cpp

@@ -330,7 +330,8 @@ std::string pretty_print_java_type(const std::string &fqn_java_type)
 ///   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(
+optionalt<resolve_inherited_componentt::inherited_componentt>
+get_inherited_component(
   const irep_idt &component_class_id,
   const irep_idt &component_name,
   const symbol_tablet &symbol_table,
@@ -339,22 +340,22 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
 {
   resolve_inherited_componentt component_resolver(
     symbol_table, class_hierarchy);
-  const resolve_inherited_componentt::inherited_componentt resolved_component =
+  const auto resolved_component =
     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
   // class that contains a component of equal name and type to `component_name`
 
-  if(resolved_component.is_valid())
+  if(resolved_component)
   {
     // Directly defined on the class referred to?
-    if(component_class_id == resolved_component.get_class_identifier())
-      return resolved_component;
+    if(component_class_id == resolved_component->get_class_identifier())
+      return *resolved_component;
 
     // No, may be inherited from some parent class; check it is visible:
-    const symbolt &component_symbol=
-      *symbol_table.lookup(resolved_component.get_full_component_identifier());
+    const symbolt &component_symbol =
+      *symbol_table.lookup(resolved_component->get_full_component_identifier());
 
     irep_idt access = component_symbol.type.get(ID_access);
     if(access.empty())
@@ -363,7 +364,7 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
     if(access==ID_public || access==ID_protected)
     {
       // since the component is public, it is inherited
-      return resolved_component;
+      return *resolved_component;
     }
 
     // components with the default access modifier are only
@@ -372,14 +373,12 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
     {
       const std::string &class_package=
         java_class_to_package(id2string(component_class_id));
-      const std::string &component_package=
-        java_class_to_package(
-          id2string(
-            resolved_component.get_class_identifier()));
+      const std::string &component_package = java_class_to_package(
+        id2string(resolved_component->get_class_identifier()));
       if(component_package == class_package)
-        return resolved_component;
+        return *resolved_component;
       else
-        return resolve_inherited_componentt::inherited_componentt();
+        return {};
     }
 
     if(access==ID_private)
@@ -391,14 +390,14 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
       // to `classname`, a component can only become "more accessible". So, if
       // the last occurrence is private, all others before must be private as
       // well, and none is inherited in `classname`.
-      return resolve_inherited_componentt::inherited_componentt();
+      return {};
     }
 
     UNREACHABLE; // Unexpected access modifier
   }
   else
   {
-    return resolve_inherited_componentt::inherited_componentt();
+    return {};
   }
 }
 

jbmc/src/java_bytecode/java_utils.h

@@ -97,7 +97,8 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip);
 
 std::string pretty_print_java_type(const std::string &fqn_java_type);
 
-resolve_inherited_componentt::inherited_componentt get_inherited_component(
+optionalt<resolve_inherited_componentt::inherited_componentt>
+get_inherited_component(
   const irep_idt &component_class_id,
   const irep_idt &component_name,
   const symbol_tablet &symbol_table,

src/goto-programs/remove_virtual_functions.cpp

@@ -48,7 +48,7 @@ class remove_virtual_functionst
     goto_programt &goto_program,
     goto_programt::targett target);
   typedef std::function<
-    resolve_inherited_componentt::inherited_componentt(
+    optionalt<resolve_inherited_componentt::inherited_componentt>(
       const irep_idt &,
       const irep_idt &)>
     function_call_resolvert;
@@ -399,18 +399,16 @@ void remove_virtual_functionst::get_child_functions_rec(
     }
     if(!function.symbol_expr.has_value())
     {
-      const resolve_inherited_componentt::inherited_componentt
-        &resolved_call = resolve_function_call(child, component_name);
-      if(resolved_call.is_valid())
+      const auto resolved_call = resolve_function_call(child, component_name);
+      if(resolved_call)
       {
-        function.class_id = resolved_call.get_class_identifier();
-        const symbolt &called_symbol =
-          symbol_table.lookup_ref(
-            resolved_call.get_full_component_identifier());
+        function.class_id = resolved_call->get_class_identifier();
+        const symbolt &called_symbol = symbol_table.lookup_ref(
+          resolved_call->get_full_component_identifier());
 
         function.symbol_expr = called_symbol.symbol_expr();
         function.symbol_expr->set(
-          ID_C_class, resolved_call.get_class_identifier());
+          ID_C_class, resolved_call->get_class_identifier());
       }
     }
     functions.push_back(function);
@@ -449,22 +447,22 @@ void remove_virtual_functionst::get_functions(
     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, false);
+  const auto resolved_call =
+    get_virtual_call_target(class_id, function_name, false);
 
   // might be an abstract function
   dispatch_table_entryt root_function(class_id);
 
-  if(resolved_call.is_valid())
+  if(resolved_call)
   {
-    root_function.class_id=resolved_call.get_class_identifier();
+    root_function.class_id = resolved_call->get_class_identifier();
 
     const symbolt &called_symbol =
-      symbol_table.lookup_ref(resolved_call.get_full_component_identifier());
+      symbol_table.lookup_ref(resolved_call->get_full_component_identifier());
 
     root_function.symbol_expr=called_symbol.symbol_expr();
     root_function.symbol_expr->set(
-      ID_C_class, resolved_call.get_class_identifier());
+      ID_C_class, resolved_call->get_class_identifier());
   }
 
   // iterate over all children, transitively

src/goto-programs/resolve_inherited_component.cpp

@@ -34,11 +34,11 @@ resolve_inherited_componentt::resolve_inherited_componentt(
 /// \param include_interfaces: If true, consider inheritance 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)
+optionalt<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());
@@ -76,7 +76,7 @@ resolve_inherited_componentt::inherited_componentt
     }
   }
 
-  return inherited_componentt();
+  return {};
 }
 
 /// Build a component name as found in a GOTO symbol table equivalent to the
@@ -102,10 +102,3 @@ irep_idt resolve_inherited_componentt::inherited_componentt::
   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();
-}

src/goto-programs/resolve_inherited_component.h

@@ -27,9 +27,6 @@ class resolve_inherited_componentt
   class inherited_componentt
   {
   public:
-    inherited_componentt()
-    {}
-
     inherited_componentt(
       const irep_idt &class_id, const irep_idt &component_id):
         class_identifier(class_id),
@@ -43,19 +40,12 @@ class resolve_inherited_componentt
       return class_identifier;
     }
 
-    irep_idt get_component_basename() const
-    {
-      return component_identifier;
-    }
-
-    bool is_valid() const;
-
   private:
     irep_idt class_identifier;
     irep_idt component_identifier;
   };
 
-  inherited_componentt operator()(
+  optionalt<inherited_componentt> operator()(
     const irep_idt &class_id,
     const irep_idt &component_name,
     bool include_interfaces);
@@ -64,11 +54,6 @@ class resolve_inherited_componentt
     const irep_idt &class_name, const irep_idt &component_name);
 
 private:
-  bool does_implementation_exist(
-    const irep_idt &class_name,
-    const irep_idt &component_name,
-    const irep_idt &user_class_name);
-
   const class_hierarchyt &class_hierarchy;
   const symbol_tablet &symbol_table;
 };