add signature to method pretty names

Author: Daniel Kroening

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -363,20 +363,6 @@ void java_bytecode_convert_method_lazy(
   else
     member_type.set_access(ID_default);
 
-  if(is_constructor(method_symbol.base_name))
-  {
-    // we use full.class_name.class_name(...) as pretty name
-    // for constructors
-    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)
   {
@@ -389,6 +375,23 @@ 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.class_name(...) as pretty name
+    // for constructors
+    method_symbol.pretty_name=
+      id2string(class_symbol.pretty_name)+"."+
+      id2string(class_symbol.base_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())
   {

src/java_bytecode/java_types.cpp

@@ -884,3 +884,54 @@ 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(type.id()==ID_symbol)
+    return id2string(strip_java_namespace_prefix(
+      to_symbol_type(type).get_identifier()));
+  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