Correct handling of the java generic class signature

Previously the signature parsing would be confused into thinking that
there were two generic parameters when there were two bounds on the
first parameter. There exists TG-674 to make the conversion work
correctly.

Author: Thomas Kiley

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -103,15 +103,23 @@ void java_bytecode_convert_classt::convert(const classt &c)
               << " in parsed class "
               << c.name << "\n";
 #endif
-    for(auto t : java_generic_type_from_string(
-          id2string(c.name),
-          c.signature.value()))
+    try
     {
-      generic_class_type.generic_types()
-        .push_back(to_java_generic_parameter(t));
+      const std::vector<typet> &generic_types=java_generic_type_from_string(
+        id2string(c.name),
+        c.signature.value());
+      for(const typet &t : generic_types)
+      {
+        generic_class_type.generic_types()
+          .push_back(to_java_generic_parameter(t));
+      }
+      class_type=generic_class_type;
+    }
+    catch(unsupported_java_class_siganture_exceptiont)
+    {
+      // Do nothing: we don't support parsing for example double bounded or
+      // two entry elements
     }
-
-    class_type=generic_class_type;
   }
 
   class_type.set_tag(c.name);

src/java_bytecode/java_types.cpp

@@ -512,17 +512,20 @@ std::vector<typet> java_generic_type_from_string(
   const std::string &class_name,
   const std::string &src)
 {
-  /// the class signature is of the form <TX:Bound_X;TY:Bound_Y;>base_class
+  /// the class signature is of the form <TX:Bound_X;:BoundZ;TY:Bound_Y;>
   size_t signature_end=find_closing_delimiter(src, 0, '<', '>');
   INVARIANT(
     src[0]=='<' && signature_end!=std::string::npos,
     "Class signature has unexpected format");
   std::string signature(src.substr(1, signature_end-1));
 
+  if(signature.find(";:")!=std::string::npos)
+    throw unsupported_java_class_siganture_exceptiont();
+
   PRECONDITION(signature[signature.size()-1]==';');
 
   std::vector<typet> types;
-  size_t var_sep=signature.rfind(';');
+  size_t var_sep=signature.find(';');
   while(var_sep!=std::string::npos)
   {
     size_t bound_sep=signature.find(':');

src/java_bytecode/java_types.h

@@ -350,4 +350,16 @@ inline const typet &java_generics_class_type_bound(
   return gen_type.subtype();
 }
 
+
+/// An exception that is raised for unsupported class signature.
+/// Currently we do not parse multiple bounds.
+class unsupported_java_class_siganture_exceptiont:public std::logic_error
+{
+public:
+  unsupported_java_class_siganture_exceptiont():
+    std::logic_error(
+      "Unsupported class signature: multiple bounds")
+  {}
+};
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H

unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp

@@ -253,8 +253,11 @@ SCENARIO(
         class_typet class_type=to_class_type(symbol_type);
         REQUIRE(class_type.is_class());
         java_class_typet java_class_type=to_java_class_type(class_type);
-        REQUIRE(is_java_generics_class_type(java_class_type));
+        REQUIRE_FALSE(is_java_generics_class_type(java_class_type));
 
+        // TODO (tkiley): Extend this unit test when bounds are correctly
+        // parsed.
+#if 0
         java_generics_class_typet java_generics_class_type=
           to_java_generics_class_type(java_class_type);
         REQUIRE(java_generics_class_type.generic_types().size()==1);
@@ -271,9 +274,9 @@ SCENARIO(
           "java::generics$double_bound_element::T");
         THEN("Bound must be Number and dummyInterface")
         {
-          // TODO (tkiley): Extend this unit test when bounds are correctly
-          // parsed.
+
         }
+#endif
       }
     }
   }
@@ -293,7 +296,7 @@ SCENARIO(
 
       java_generics_class_typet java_generics_class_type=
         to_java_generics_class_type(java_class_type);
-      //REQUIRE(java_generics_class_type.generic_types().size()==2);
+      REQUIRE(java_generics_class_type.generic_types().size()==2);
 
       auto generic_param_iterator=
         java_generics_class_type.generic_types().cbegin();
@@ -327,7 +330,7 @@ SCENARIO(
           generic_type_var.type_variable().get_identifier()==
           "java::generics$two_elements::V");
         REQUIRE(
-          java_generics_class_type_var(0, java_generics_class_type)==
+          java_generics_class_type_var(1, java_generics_class_type)==
           "java::generics$two_elements::V");
       }
     }