Merge pull request #1617 from NlightNFotis/fotis/pretty_print_bugfix

[TG-1157] Fix pretty printing routine

Author: chrisr-diffblue

src/java_bytecode/generate_java_generic_type.cpp

@@ -14,20 +14,6 @@
 #include <java_bytecode/java_types.h>
 #include <java_bytecode/java_utils.h>
 
-/// Strip the package name from a java type, for the type to be
-/// pretty printed (java::java.lang.Integer -> Integer).
-/// \param fqn_java_type The java type we want to pretty print.
-/// \return The pretty printed type if there was a match of the
-//  qualifiers, or the type as it was passed otherwise.
-static std::string pretty_print_java_type(const std::string &fqn_java_type)
-{
-  const std::string java_lang("java::java.lang.");
-  const std::string package_name(java_class_to_package(fqn_java_type) + ".");
-  if(package_name == java_lang)
-    return fqn_java_type.substr(java_lang.length());
-  return fqn_java_type;
-}
-
 generate_java_generic_typet::generate_java_generic_typet(
   message_handlert &message_handler):
     message_handler(message_handler)

src/java_bytecode/java_utils.cpp

@@ -305,3 +305,23 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
   PRECONDITION(has_prefix(to_strip_str, prefix));
   return to_strip_str.substr(prefix.size(), std::string::npos);
 }
+
+/// Strip the package name from a java type, for the type to be
+/// pretty printed (java::java.lang.Integer -> Integer).
+/// \param fqn_java_type The java type we want to pretty print.
+/// \return The pretty printed type if there was a match of the
+//  qualifiers, or the type as it was passed otherwise.
+std::string pretty_print_java_type(const std::string &fqn_java_type)
+{
+  std::string result(fqn_java_type);
+  const std::string java_cbmc_string("java::");
+  // Remove the CBMC internal java identifier
+  if(has_prefix(fqn_java_type, java_cbmc_string))
+    result = fqn_java_type.substr(java_cbmc_string.length());
+  // If the class is in package java.lang strip
+  // package name due to default import
+  const std::string java_lang_string("java.lang.");
+  if(has_prefix(result, java_lang_string))
+    result = result.substr(java_lang_string.length());
+  return result;
+}

src/java_bytecode/java_utils.h

@@ -94,4 +94,6 @@ exprt make_function_application(
 
 irep_idt strip_java_namespace_prefix(const irep_idt &to_strip);
 
+std::string pretty_print_java_type(const std::string &fqn_java_type);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -7,6 +7,9 @@
 
 \*******************************************************************/
 
+#include <map>
+#include <string>
+
 #include <testing-utils/catch.hpp>
 #include <testing-utils/load_java_class.h>
 #include <testing-utils/require_type.h>
@@ -179,7 +182,7 @@ SCENARIO(
   // We want to test that the specialized/instantiated class has it's field
   // type updated, so find the specialized class, not the generic class.
   const irep_idt test_class =
-    "java::generic_field_array_instantiation$generic<java::array[reference]"
+    "java::generic_field_array_instantiation$generic<array[reference]"
     "of_java::java.lang.Float>";
 
   GIVEN("A generic type instantiated with an array type")
@@ -224,15 +227,15 @@ SCENARIO(
     GIVEN("A generic type instantiated with different array types")
     {
       const irep_idt test_class_integer =
-        "java::generic_field_array_instantiation$generic<java::array[reference]"
+        "java::generic_field_array_instantiation$generic<array[reference]"
         "of_"
         "java::java.lang.Integer>";
 
       const irep_idt test_class_int =
-        "java::generic_field_array_instantiation$generic<java::array[int]>";
+        "java::generic_field_array_instantiation$generic<array[int]>";
 
       const irep_idt test_class_float =
-        "java::generic_field_array_instantiation$generic<java::array[float]>";
+        "java::generic_field_array_instantiation$generic<array[float]>";
 
       const struct_typet::componentt &component_g =
         require_type::require_component(
@@ -330,7 +333,7 @@ SCENARIO(
         "table")
       {
         const std::string specialised_string =
-          "<java::array[reference]of_"
+          "<array[reference]of_"
           "java::java.lang.Float>";
         const irep_idt specialised_class_name = id2string(harness_class) + "$" +
                                                 id2string(inner_class) +

unit/java_bytecode/java_utils_test.cpp

@@ -341,3 +341,30 @@ SCENARIO("find_closing_semi_colon_for_reference_type", "[core][java_util_test]")
     REQUIRE(find_closing_semi_colon_for_reference_type(descriptor, 10) == 19);
   }
 }
+
+SCENARIO("Test pretty printing auxiliary function", "[core][java_util_test]")
+{
+  using std::map;
+  using std::string;
+
+  WHEN("We have a series of cbmc internal java types")
+  {
+    // NOLINTNEXTLINE
+    const map<string, string> types{
+      // map<Input, Output>
+      {"java::java.lang.Integer", "Integer"},
+      {"java::CustomClass", "CustomClass"},
+      {"java.lang.String", "String"},
+      {"Hashmap", "Hashmap"},
+      // We shouldn't prune types not imported in default import
+      {"java.util.HashSet", "java.util.HashSet"}};
+
+    THEN("We need to make sure that the types get pruned correctly.")
+    {
+      for(const auto &pair : types)
+      {
+        REQUIRE(pretty_print_java_type(pair.first) == pair.second);
+      }
+    }
+  }
+}