Merge pull request #1606 from NlightNFotis/fotis_tg1157/pretty_printing

[TG-1157] New class for specialised generic class types.

Author: chrisr-diffblue

src/java_bytecode/generate_java_generic_type.cpp

@@ -14,6 +14,20 @@
 #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)
@@ -73,8 +87,8 @@ symbolt generate_java_generic_typet::operator()(
     pre_modification_size==after_modification_size,
     "All components in the original class should be in the new class");
 
-  const java_class_typet &new_java_class = construct_specialised_generic_type(
-    generic_class_definition, new_tag, replacement_components);
+  const java_specialized_generic_class_typet new_java_class =
+    construct_specialised_generic_type(new_tag, replacement_components);
   const type_symbolt &class_symbol =
     build_symbol_from_specialised_class(new_java_class);
 
@@ -196,14 +210,14 @@ irep_idt generate_java_generic_typet::build_generic_tag(
     .generic_type_arguments())
   {
     if(!first)
-      new_tag_buffer << ",";
+      new_tag_buffer << ", ";
     first=false;
 
     INVARIANT(
       !is_java_generic_parameter(type_argument),
       "Only create full concretized generic types");
     const irep_idt &id(id2string(type_argument.subtype().get(ID_identifier)));
-    new_tag_buffer << id2string(id);
+    new_tag_buffer << pretty_print_java_type(id2string(id));
     if(is_java_array_tag(id))
     {
       const typet &element_type =
@@ -227,25 +241,17 @@ irep_idt generate_java_generic_typet::build_generic_tag(
   return new_tag_buffer.str();
 }
 
-/// Build the specalised version of the specific class, with the specified
+/// Build the specialised version of the specific class, with the specified
 /// parameters and name.
-/// \param generic_class_definition: The generic class we are specialising
 /// \param new_tag: The new name for the class (like Generic<java::Float>)
 /// \param new_components: The specialised components
 /// \return The newly constructed class.
-java_class_typet
+java_specialized_generic_class_typet
 generate_java_generic_typet::construct_specialised_generic_type(
-  const java_generic_class_typet &generic_class_definition,
   const irep_idt &new_tag,
   const struct_typet::componentst &new_components) const
 {
-  java_class_typet specialised_class = generic_class_definition;
-  // We are specialising the logic - so we don't want to be marked as generic
-  specialised_class.set(ID_C_java_generics_class_type, false);
-  specialised_class.set(ID_name, "java::" + id2string(new_tag));
-  specialised_class.set(ID_base_name, new_tag);
-  specialised_class.components() = new_components;
-  return specialised_class;
+  return java_specialized_generic_class_typet{new_tag, new_components};
 }
 
 /// Construct the symbol to be moved into the symbol table

src/java_bytecode/generate_java_generic_type.h

@@ -33,8 +33,7 @@ class generate_java_generic_typet
     const java_generic_class_typet &replacement_type,
     const java_generic_typet &generic_reference) const;
 
-  java_class_typet construct_specialised_generic_type(
-    const java_generic_class_typet &generic_class_definition,
+  java_specialized_generic_class_typet construct_specialised_generic_type(
     const irep_idt &new_tag,
     const struct_typet::componentst &new_components) const;
 

src/java_bytecode/java_types.h

@@ -374,4 +374,55 @@ void get_dependencies_from_generic_parameters(
   const typet &,
   std::set<irep_idt> &);
 
+class java_specialized_generic_class_typet : public java_class_typet
+{
+public:
+  /// Build the specialised version of the specific class, with the specified
+  /// parameters and name.
+  /// \param new_tag: The new name for the class (like Generic<java::Float>)
+  /// \param new_components: The specialised components
+  /// \return The newly constructed class.
+  java_specialized_generic_class_typet(
+    const irep_idt &new_tag,
+    const struct_typet::componentst &new_components)
+  {
+    set(ID_C_specialized_generic_java_class, true);
+    // We are specialising the logic - so we don't want to be marked as generic
+    set(ID_C_java_generics_class_type, false);
+    set(ID_name, "java::" + id2string(new_tag));
+    set(ID_base_name, id2string(new_tag));
+    components() = new_components;
+    const std::string &class_tag = id2string(new_tag);
+    set_tag(class_tag.substr(0, class_tag.find('<')));
+  }
+};
+
+inline bool is_java_specialized_generic_class_type(const typet &type)
+{
+  return type.get_bool(ID_C_specialized_generic_java_class);
+}
+
+inline bool is_java_specialized_generic_class_type(typet &type)
+{
+  return type.get_bool(ID_C_specialized_generic_java_class);
+}
+
+inline java_specialized_generic_class_typet
+to_java_specialized_generic_class_type(const typet &type)
+{
+  INVARIANT(
+    is_java_specialized_generic_class_type(type),
+    "Tried to convert a type that was not a specialised generic java class");
+  return static_cast<const java_specialized_generic_class_typet &>(type);
+}
+
+inline java_specialized_generic_class_typet
+to_java_specialized_generic_class_type(typet &type)
+{
+  INVARIANT(
+    is_java_specialized_generic_class_type(type),
+    "Tried to convert a type that was not a specialised generic java class");
+  return static_cast<const java_specialized_generic_class_typet &>(type);
+}
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H

src/util/irep_ids.def

@@ -830,6 +830,7 @@ IREP_ID_ONE(integer_dereference)
 IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter)
 IREP_ID_TWO(C_java_generic_type, #java_generic_type)
 IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
+IREP_ID_TWO(C_specialized_generic_java_class, #specialized_generic_java_class)
 IREP_ID_TWO(generic_types, #generic_types)
 IREP_ID_TWO(type_variables, #type_variables)
 IREP_ID_ONE(havoc_object)

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -40,8 +40,7 @@ SCENARIO(
   "generate_java_generic_type_from_file",
   "[core][java_bytecode][generate_java_generic_type]")
 {
-  auto expected_symbol=
-    "java::generic_two_fields$bound_element<java::java.lang.Integer>";
+  auto expected_symbol = "java::generic_two_fields$bound_element<Integer>";
 
   GIVEN("A generic java type with two generic fields and a concrete "
           "substitution")
@@ -56,8 +55,8 @@ SCENARIO(
     REQUIRE(new_symbol_table.has_symbol(expected_symbol));
     THEN("The class should contain two instantiated fields.")
     {
-      const auto &class_symbol=new_symbol_table.lookup(
-        "java::generic_two_fields$bound_element<java::java.lang.Integer>");
+      const auto &class_symbol = new_symbol_table.lookup(
+        "java::generic_two_fields$bound_element<Integer>");
       const typet &symbol_type=class_symbol->type;
 
       REQUIRE(symbol_type.id()==ID_struct);
@@ -89,10 +88,8 @@ SCENARIO(
   "generate_java_generic_type_from_file_two_params",
   "[core][java_bytecode][generate_java_generic_type]")
 {
-  auto expected_symbol=
-    "java::generic_two_parameters$KeyValuePair"
-      "<java::java.lang.String,"
-      "java::java.lang.Integer>";
+  auto expected_symbol =
+    "java::generic_two_parameters$KeyValuePair<String, Integer>";
 
   GIVEN("A generic java type with two generic parameters, like a Hashtable")
   {
@@ -133,10 +130,8 @@ SCENARIO(
   // After we have loaded the class and converted the generics,
   // the presence of these two symbols in the symbol table is
   // proof enough that we did the work we needed to do correctly.
-  auto first_expected_symbol=
-    "java::generic_two_instances$element<java::java.lang.Boolean>";
-  auto second_expected_symbol=
-    "java::generic_two_instances$element<java::java.lang.Integer>";
+  auto first_expected_symbol = "java::generic_two_instances$element<Boolean>";
+  auto second_expected_symbol = "java::generic_two_instances$element<Integer>";
 
   GIVEN("A generic java type with a field that refers to another generic with"
           " an uninstantiated parameter.")
@@ -284,9 +279,8 @@ SCENARIO(
         "There should be a specialised version of the class in the symbol "
         "table")
       {
-        const irep_idt specialised_class_name = id2string(harness_class) + "$" +
-                                                id2string(inner_class) +
-                                                "<java::java.lang.Float>";
+        const irep_idt specialised_class_name =
+          id2string(harness_class) + "$" + id2string(inner_class) + "<Float>";
         REQUIRE(new_symbol_table.has_symbol(specialised_class_name));
 
         const symbolt test_class_symbol =