Improve pretty name of Java methods

regression/cbmc-java/package_friendly1/test.desc

@@ -1,7 +1,7 @@
 CORE symex-driven-lazy-loading-expected-failure
 main.class
 package_friendly1.class package_friendly2.class --show-goto-functions
-^main[.]main[\(][\)].*$
+^main[.]main[\(].*[\)].*$
 ^package_friendly2[.]operation2[\(][\)].*$
 ^EXIT=0$
 ^SIGNAL=0$

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -377,9 +377,17 @@ void java_bytecode_convert_classt::convert(
   if(!c.annotations.empty())
     convert_annotations(c.annotations, class_type.get_annotations());
 
+  // the base name is the name of the class without the package
+  const irep_idt base_name = [](const std::string &full_name) {
+    const size_t last_dot = full_name.find_last_of('.');
+    return last_dot == std::string::npos
+             ? full_name
+             : std::string(full_name, last_dot + 1, std::string::npos);
+  }(id2string(c.name));
+
   // produce class symbol
   symbolt new_symbol;
-  new_symbol.base_name=c.name;
+  new_symbol.base_name = base_name;
   new_symbol.pretty_name=c.name;
   new_symbol.name=qualified_classname;
   class_type.set(ID_name, new_symbol.name);

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -354,6 +354,7 @@ void java_bytecode_convert_method_lazy(
   method_symbol.mode=ID_java;
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
+
   if(m.is_public)
     member_type.set_access(ID_public);
   else if(m.is_protected)
@@ -363,18 +364,6 @@ void java_bytecode_convert_method_lazy(
   else
     member_type.set_access(ID_default);
 
-  if(is_constructor(method_symbol.base_name))
-  {
-    method_symbol.pretty_name=
-      id2string(class_symbol.pretty_name)+"."+
-      id2string(class_symbol.base_name)+"()";
-    member_type.set_is_constructor();
-  }
-  else
-    method_symbol.pretty_name=
-      id2string(class_symbol.pretty_name)+"."+
-      id2string(m.base_name)+"()";
-
   // do we need to add 'this' as a parameter?
   if(!m.is_static)
   {
@@ -387,6 +376,24 @@ void java_bytecode_convert_method_lazy(
     parameters.insert(parameters.begin(), this_p);
   }
 
+  const std::string signature_string = pretty_signature(member_type);
+
+  if(is_constructor(method_symbol.base_name))
+  {
+    // we use full.class_name(...) as pretty name
+    // for constructors -- the idea is that they have
+    // an empty declarator.
+    method_symbol.pretty_name=
+      id2string(class_symbol.pretty_name) + signature_string;
+
+    member_type.set_is_constructor();
+  }
+  else
+  {
+    method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
+                                id2string(m.base_name) + signature_string;
+  }
+
   // Load annotations
   if(!m.annotations.empty())
   {
@@ -559,22 +566,27 @@ void java_bytecode_convert_methodt::convert(
   method_symbol.location=m.source_location;
   method_symbol.location.set_function(method_identifier);
 
+  const std::string signature_string = pretty_signature(code_type);
+
   // Set up the pretty name for the method entry in the symbol table.
   // The pretty name of a constructor includes the base name of the class
   // instead of the internal method name "<init>". For regular methods, it's
   // just the base name of the method.
   if(is_constructor(method_symbol.base_name))
   {
-    method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
-                                id2string(class_symbol.base_name) + "()";
+    // we use full.class_name(...) as pretty name
+    // for constructors -- the idea is that they have
+    // an empty declarator.
+    method_symbol.pretty_name =
+      id2string(class_symbol.pretty_name) + signature_string;
     INVARIANT(
       code_type.get_is_constructor(),
       "Member type should have already been marked as a constructor");
   }
   else
   {
     method_symbol.pretty_name = id2string(class_symbol.pretty_name) + "." +
-                                id2string(method_symbol.base_name) + "()";
+                                id2string(m.base_name) + signature_string;
   }
 
   method_symbol.type = code_type;

src/java_bytecode/java_types.cpp

@@ -884,3 +884,64 @@ optionalt<size_t> java_generic_symbol_typet::generic_type_index(
   }
   return {};
 }
+
+std::string pretty_java_type(const typet &type)
+{
+  if(type == java_int_type())
+    return "int";
+  else if(type == java_long_type())
+    return "long";
+  else if(type == java_short_type())
+    return "short";
+  else if(type == java_byte_type())
+    return "byte";
+  else if(type == java_char_type())
+    return "char";
+  else if(type == java_float_type())
+    return "float";
+  else if(type == java_double_type())
+    return "double";
+  else if(type == java_boolean_type())
+    return "boolean";
+  else if(type == java_byte_type())
+    return "byte";
+  else if(is_reference(type))
+  {
+    if(type.subtype().id() == ID_symbol)
+    {
+      const auto &symbol_type = to_symbol_type(type.subtype());
+      const irep_idt &id = symbol_type.get_identifier();
+      if(is_java_array_tag(id))
+        return pretty_java_type(java_array_element_type(symbol_type)) + "[]";
+      else
+        return id2string(strip_java_namespace_prefix(id));
+    }
+    else
+      return "?";
+  }
+  else
+    return "?";
+}
+
+std::string pretty_signature(const code_typet &code_type)
+{
+  std::ostringstream result;
+  result << '(';
+
+  bool first = true;
+  for(const auto p : code_type.parameters())
+  {
+    if(p.get_this())
+      continue;
+
+    if(first)
+      first = false;
+    else
+      result << ", ";
+
+    result << pretty_java_type(p.type());
+  }
+
+  result << ')';
+  return result.str();
+}

src/java_bytecode/java_types.h

@@ -626,12 +626,18 @@ inline java_generic_symbol_typet &to_java_generic_symbol_type(typet &type)
 /// the type to be parsed normally, for example
 /// `java.util.HashSet<java.lang.Integer>` will be turned into
 /// `java.util.HashSet`
-std::string erase_type_arguments(const std::string &src);
+std::string erase_type_arguments(const std::string &);
 /// Returns the full class name, skipping over the generics. This turns any of
 /// these:
 ///   1. Signature: Lcom/package/OuterClass<TT;>.Inner;
 ///   2. Descriptor: Lcom.pacakge.OuterClass$Inner;
 /// into `com.package.OuterClass.Inner`
-std::string gather_full_class_name(const std::string &src);
+std::string gather_full_class_name(const std::string &);
+
+// turn java type into string
+std::string pretty_java_type(const typet &);
+
+// pretty signature for methods
+std::string pretty_signature(const code_typet &);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H