Refinements to class_method_descriptor_exprt

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -263,7 +263,7 @@ bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
     // didn't already exist. It can't be instantiated already, otherwise it
     // would give a concrete definition of the called method, and
     // candidate_target_methods would be non-empty.
-    const irep_idt &call_class = virtual_function.get_class_name();
+    const irep_idt &call_class = virtual_function.class_id();
     bool was_missing = instantiated_classes.count(call_class) == 0;
     CHECK_RETURN(was_missing);
     any_new_classes = true;
@@ -292,13 +292,13 @@ bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
     }
 
     // Check that `get_virtual_method_target` returns a method now
-    const irep_idt &call_basename = virtual_function.get_component_name();
-    const irep_idt method_name = get_virtual_method_target(
-      instantiated_classes, call_basename, call_class, symbol_table);
-    CHECK_RETURN(!method_name.empty());
+    const irep_idt &method_name = virtual_function.mangled_method_name();
+    const irep_idt method_id = get_virtual_method_target(
+      instantiated_classes, method_name, call_class, symbol_table);
+    CHECK_RETURN(!method_id.empty());
 
     // Add what it returns to methods_to_convert_later
-    methods_to_convert_later.insert(method_name);
+    methods_to_convert_later.insert(method_id);
   }
   return any_new_classes;
 }
@@ -477,12 +477,12 @@ void ci_lazy_methodst::get_virtual_method_targets(
   std::unordered_set<irep_idt> &callable_methods,
   symbol_tablet &symbol_table)
 {
-  const auto &call_class = called_function.get_class_name();
+  const auto &call_class = called_function.class_id();
   INVARIANT(
     !call_class.empty(), "All virtual calls should be aimed at a class");
-  const auto &call_basename = called_function.get_component_name();
+  const auto &method_name = called_function.mangled_method_name();
   INVARIANT(
-    !call_basename.empty(),
+    !method_name.empty(),
     "Virtual function must have a reasonable name after removing class");
 
   class_hierarchyt::idst self_and_child_classes =
@@ -491,10 +491,10 @@ void ci_lazy_methodst::get_virtual_method_targets(
 
   for(const irep_idt &class_name : self_and_child_classes)
   {
-    const irep_idt method_name = get_virtual_method_target(
-      instantiated_classes, call_basename, class_name, symbol_table);
-    if(!method_name.empty())
-      callable_methods.insert(method_name);
+    const irep_idt method_id = get_virtual_method_target(
+      instantiated_classes, method_name, class_name, symbol_table);
+    if(!method_id.empty())
+      callable_methods.insert(method_id);
   }
 }
 

jbmc/src/java_bytecode/expr2java.cpp

@@ -422,9 +422,8 @@ std::string expr2javat::convert_with_precedence(
   {
     const class_method_descriptor_exprt &virtual_function =
       to_class_method_descriptor_expr(src);
-    return "CLASS_METHOD_DESCRIPTOR(" +
-           id2string(virtual_function.get_class_name()) + "." +
-           id2string(virtual_function.get_component_name()) + ")";
+    return "CLASS_METHOD_DESCRIPTOR(" + id2string(virtual_function.class_id()) +
+           "." + id2string(virtual_function.mangled_method_name()) + ")";
   }
   else if(
     const auto &literal = expr_try_dynamic_cast<java_string_literal_exprt>(src))

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2201,11 +2201,11 @@ void java_bytecode_convert_methodt::convert_invoke(
 
   if(use_this)
   {
-    irep_idt classname = class_method_descriptor.get(ID_C_class);
+    const irep_idt class_id = class_method_descriptor.class_id();
 
     if(parameters.empty() || !parameters[0].get_this())
     {
-      typet thistype = struct_tag_typet(classname);
+      typet thistype = struct_tag_typet(class_id);
       reference_typet object_ref_type = java_reference_type(thistype);
       java_method_typet::parametert this_p(object_ref_type);
       this_p.set_this();
@@ -2220,7 +2220,7 @@ void java_bytecode_convert_methodt::convert_invoke(
       if(is_constructor(invoked_method_id))
       {
         if(needed_lazy_methods)
-          needed_lazy_methods->add_needed_class(classname);
+          needed_lazy_methods->add_needed_class(class_id);
         method_type.set_is_constructor();
       }
       else
@@ -2267,16 +2267,16 @@ void java_bytecode_convert_methodt::convert_invoke(
   if(
     method_symbol == symbol_table.symbols.end() &&
     !(is_virtual && is_method_inherited(
-                      class_method_descriptor.get_class_name(),
-                      class_method_descriptor.get_component_name())))
+                      class_method_descriptor.class_id(),
+                      class_method_descriptor.mangled_method_name())))
   {
     create_method_stub_symbol(
       invoked_method_id,
-      class_method_descriptor.get_base_name(),
-      id2string(class_method_descriptor.get_class_name()).substr(6) + "." +
-        id2string(class_method_descriptor.get_base_name()) + "()",
+      class_method_descriptor.base_method_name(),
+      id2string(class_method_descriptor.class_id()).substr(6) + "." +
+        id2string(class_method_descriptor.base_method_name()) + "()",
       method_type,
-      class_method_descriptor.get_class_name(),
+      class_method_descriptor.class_id(),
       symbol_table,
       get_message_handler());
   }
@@ -2299,8 +2299,7 @@ void java_bytecode_convert_methodt::convert_invoke(
     {
       needed_lazy_methods->add_needed_method(invoked_method_id);
       // Calling a static method causes static initialization:
-      needed_lazy_methods->add_needed_class(
-        class_method_descriptor.get_class_name());
+      needed_lazy_methods->add_needed_class(class_method_descriptor.class_id());
     }
   }
 
@@ -2315,8 +2314,7 @@ void java_bytecode_convert_methodt::convert_invoke(
 
   if(!use_this)
   {
-    codet clinit_call =
-      get_clinit_call(class_method_descriptor.get_class_name());
+    codet clinit_call = get_clinit_call(class_method_descriptor.class_id());
     if(clinit_call.get_statement() != ID_skip)
       c = code_blockt({clinit_call, c});
   }
@@ -3224,13 +3222,13 @@ void java_bytecode_convert_method(
 /// a method inherited from a class (and not an interface!) from which
 /// \p classname inherits, either directly or indirectly.
 /// \param classname: class whose method is referenced
-/// \param methodid: method basename
+/// \param mangled_method_name: The particular overload of a given method.
 bool java_bytecode_convert_methodt::is_method_inherited(
   const irep_idt &classname,
-  const irep_idt &methodid) const
+  const irep_idt &mangled_method_name) const
 {
-  const auto inherited_method =
-    get_inherited_component(classname, methodid, symbol_table, false);
+  const auto inherited_method = get_inherited_component(
+    classname, mangled_method_name, symbol_table, false);
   return inherited_method.has_value();
 }
 

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -311,7 +311,7 @@ class java_bytecode_convert_methodt:public messaget
 
   bool is_method_inherited(
     const irep_idt &classname,
-    const irep_idt &methodid) const;
+    const irep_idt &mangled_method_name) const;
 
   irep_idt get_static_field(
     const irep_idt &class_identifier, const irep_idt &component_name) const;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -754,17 +754,14 @@ void java_bytecode_parsert::rconstant_pool()
 
         auto class_tag = java_classname(id2string(class_name_entry.s));
 
-        irep_idt component_name=
-          id2string(name_entry.s)+
-          ":"+id2string(pool_entry(nameandtype_entry.ref2).s);
+        irep_idt mangled_method_name =
+          id2string(name_entry.s) + ":" +
+          id2string(pool_entry(nameandtype_entry.ref2).s);
 
-        irep_idt class_name = class_tag.get_identifier();
-
-        irep_idt identifier=
-          id2string(class_name)+"."+id2string(component_name);
+        irep_idt class_id = class_tag.get_identifier();
 
         entry.expr = class_method_descriptor_exprt{
-          type, component_name, class_name, name_entry.s, identifier};
+          type, mangled_method_name, class_id, name_entry.s};
       }
       break;
 

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

@@ -133,11 +133,8 @@ SCENARIO(
   const symbolt &callee_symbol =
     symbol_table.lookup_ref("java::VirtualFunctionsTestParent.f:()V");
 
-  class_method_descriptor_exprt callee{callee_symbol.type,
-                                       "f:()V",
-                                       "java::VirtualFunctionsTestParent",
-                                       "f",
-                                       callee_symbol.name};
+  class_method_descriptor_exprt callee{
+    callee_symbol.type, "f:()V", "java::VirtualFunctionsTestParent", "f"};
 
   const code_function_callt call(
     callee,

src/util/std_expr.h

@@ -4588,45 +4588,92 @@ inline array_comprehension_exprt &to_array_comprehension_expr(exprt &expr)
   return ret;
 }
 
+inline void validate_expr(const class class_method_descriptor_exprt &value);
+
 /// An expression describing a method on a class
 class class_method_descriptor_exprt : public nullary_exprt
 {
 public:
+  /// \param class_id: Unique identifier in the symbol table, of the compile
+  ///   time type of the class which this expression is applied to. For example
+  ///   this could be - `java::java.lang.Object`.
+  /// \param base_method_name: The name of the method to which this expression
+  ///   is applied as would be seen in the source code. For example this could
+  ///   be - `toString`.
+  /// \param mangled_method_name: The method name after mangling it by
+  ///   combining it with the descriptor. The mangled name is distinguished from
+  ///   other overloads of the method with different counts of or types of
+  ///   parameters. It is not distinguished between different implementations
+  ///   within a class hierarchy. For example if the overall expression refers
+  ///   to the `java.lang.Object.toString` method, then the mangled_method_name
+  ///   would be `toString:()Ljava/lang/String;`
   explicit class_method_descriptor_exprt(
     typet _type,
-    irep_idt component_name,
-    irep_idt class_name,
-    irep_idt base_name,
-    irep_idt identifier)
+    irep_idt mangled_method_name,
+    irep_idt class_id,
+    irep_idt base_method_name)
     : nullary_exprt(ID_virtual_function, std::move(_type))
   {
-    set(ID_component_name, std::move(component_name));
-    set(ID_C_class, std::move(class_name));
-    set(ID_C_base_name, std::move(base_name));
-    set(ID_identifier, std::move(identifier));
+    irep_idt id = id2string(class_id) + "." + id2string(mangled_method_name);
+    set(ID_component_name, std::move(mangled_method_name));
+    set(ID_C_class, std::move(class_id));
+    set(ID_C_base_name, std::move(base_method_name));
+    set(ID_identifier, std::move(id));
+    validate_expr(*this);
   }
 
-  const irep_idt &get_component_name() const
+  /// The method name after mangling it by combining it with the descriptor.
+  /// The mangled name is distinguished from other overloads of the method with
+  /// different counts of or types of parameters. It is not distinguished
+  /// between different implementations within a class hierarchy. For example if
+  /// the overall expression refers to the `java.lang.Object.toString` method,
+  /// then the mangled_method_name would be `toString:()Ljava/lang/String;`
+  const irep_idt &mangled_method_name() const
   {
     return get(ID_component_name);
   }
 
-  const irep_idt &get_class_name() const
+  /// Unique identifier in the symbol table, of the compile time type of the
+  /// class which this expression is applied to. For example this could be -
+  /// `java::java.lang.Object`.
+  const irep_idt &class_id() const
   {
     return get(ID_C_class);
   }
 
-  const irep_idt &get_base_name() const
+  /// The name of the method to which this expression is applied as would be
+  /// seen in the source code. For example this could be - `toString`.
+  const irep_idt &base_method_name() const
   {
     return get(ID_C_base_name);
   }
 
+  /// A unique identifier of the combination of class and method overload to
+  /// which this expression refers. For example this could be -
+  /// `java::java.lang.Object.toString:()Ljava/lang/String;`.
   const irep_idt &get_identifier() const
   {
     return get(ID_identifier);
   }
 };
 
+inline void validate_expr(const class class_method_descriptor_exprt &value)
+{
+  validate_operands(value, 0, "class method descriptor must not have operands");
+  DATA_INVARIANT(
+    !value.mangled_method_name().empty(),
+    "class method descriptor must have a mangled method name.");
+  DATA_INVARIANT(
+    !value.class_id().empty(), "class method descriptor must have a class id.");
+  DATA_INVARIANT(
+    !value.base_method_name().empty(),
+    "class method descriptor must have a base method name.");
+  DATA_INVARIANT(
+    value.get_identifier() == id2string(value.class_id()) + "." +
+                                id2string(value.mangled_method_name()),
+    "class method descriptor must have an identifier in the expected format.");
+}
+
 /// \brief Cast an exprt to a \ref class_method_descriptor_exprt
 ///
 /// \a expr must be known to be \ref class_method_descriptor_exprt.