Adding unit test for recursive generic class

Author: svorenova

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -119,6 +119,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
     {
       // Do nothing: we don't support parsing for example double bounded or
       // two entry elements
+
     }
   }
 
@@ -218,8 +219,9 @@ void java_bytecode_convert_classt::convert(
   typet field_type;
   if(f.signature.has_value())
   {
-    field_type=java_type_from_string(
-      f.signature.value(),
+    field_type=java_type_from_string_with_exception(
+      f.descriptor,
+      f.signature,
       id2string(class_symbol.name));
 
     /// this is for a free type variable, e.g., a field of the form `T f;`

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -366,8 +366,9 @@ void java_bytecode_convert_methodt::convert(
     typet t;
     if(v.signature.has_value())
     {
-      t=java_type_from_string(
-        v.signature.value(),
+      t=java_type_from_string_with_exception(
+        v.descriptor,
+        v.signature,
         id2string(class_symbol.name));
     }
     else

src/java_bytecode/java_bytecode_parser.cpp

@@ -339,8 +339,9 @@ void java_bytecode_parsert::get_class_refs()
     typet field_type;
     if(field.signature.has_value())
     {
-      field_type=java_type_from_string(
-        field.signature.value(),
+      field_type=java_type_from_string_with_exception(
+        field.descriptor,
+        field.signature,
         "java::"+id2string(parse_tree.parsed_class.name));
     }
     else
@@ -354,8 +355,9 @@ void java_bytecode_parsert::get_class_refs()
     typet method_type;
     if(method.signature.has_value())
     {
-      method_type=java_type_from_string(
-        method.signature.value(),
+      method_type=java_type_from_string_with_exception(
+        method.descriptor,
+        method.signature,
         "java::"+id2string(parse_tree.parsed_class.name));
     }
     else
@@ -367,8 +369,9 @@ void java_bytecode_parsert::get_class_refs()
       typet var_type;
       if(var.signature.has_value())
       {
-        var_type=java_type_from_string(
-          var.signature.value(),
+        var_type=java_type_from_string_with_exception(
+          var.descriptor,
+          var.signature,
           "java::"+id2string(parse_tree.parsed_class.name));
       }
       else

src/java_bytecode/java_local_variable_table.cpp

@@ -770,7 +770,16 @@ void java_bytecode_convert_methodt::setup_local_variables(
 #endif
     typet t;
     if(v.var.signature.has_value())
-      t=java_type_from_string(v.var.signature.value());
+    {
+      try
+      {
+        t=java_type_from_string(v.var.signature.value());
+      }
+      catch(unsupported_java_class_siganture_exceptiont &e)
+      {
+        t=java_type_from_string(v.var.descriptor);
+      }
+    }
     else
       t=java_type_from_string(v.var.descriptor);
 

src/java_bytecode/java_types.cpp

@@ -325,7 +325,8 @@ typet java_type_from_string(
       {
         std::size_t e_pos=find_closing_delimiter(src, f_pos, '<', '>');
         if(e_pos==std::string::npos)
-          return nil_typet();
+          throw unsupported_java_class_siganture_exceptiont(
+            "recursive generic");
 
         // construct container type
         std::string generic_container_class=src.substr(1, f_pos-1);
@@ -520,7 +521,7 @@ std::vector<typet> java_generic_type_from_string(
   std::string signature(src.substr(1, signature_end-1));
 
   if(signature.find(";:")!=std::string::npos)
-    throw unsupported_java_class_siganture_exceptiont();
+    throw unsupported_java_class_siganture_exceptiont("multiple bounds");
 
   PRECONDITION(signature[signature.size()-1]==';');
 

src/java_bytecode/java_types.h

@@ -356,10 +356,25 @@ inline const typet &java_generics_class_type_bound(
 class unsupported_java_class_siganture_exceptiont:public std::logic_error
 {
 public:
-  unsupported_java_class_siganture_exceptiont():
+  explicit unsupported_java_class_siganture_exceptiont(std::string type):
     std::logic_error(
-      "Unsupported class signature: multiple bounds")
-  {}
+      "Unsupported class signature: "+type)
+  {
+  }
 };
 
+inline typet java_type_from_string_with_exception(
+  const std::string &descriptor,
+  const optionalt<std::string> &signature,
+  const std::string &class_name) {
+  try
+  {
+    return java_type_from_string(signature.value(), class_name);
+  }
+  catch (unsupported_java_class_siganture_exceptiont &e)
+  {
+    return java_type_from_string(descriptor, class_name);
+  }
+}
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H

unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.class

@@ -0,0 +1,4 @@
+class RecursiveGeneric extends SimpleRecursiveGeneric<RecursiveGeneric>
+{
+
+}

unit/java_bytecode/java_bytecode_parse_generics/RecursiveGeneric.java

@@ -0,0 +1,4 @@
+class SimpleRecursiveGeneric<T extends SimpleRecursiveGeneric<T>>
+{
+  public T t;
+}

unit/java_bytecode/java_bytecode_parse_generics/SimpleRecursiveGeneric.class

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+ Module: Unit tests for parsing generic classes
+
+ Author: DiffBlue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <catch.hpp>
+
+#include <util/config.h>
+#include <util/cmdline.h>
+#include <util/language.h>
+#include <util/prefix.h>
+
+#include <java_bytecode/java_bytecode_language.h>
+#include <src/java_bytecode/load_java_class.h>
+
+#include <iostream>
+#include <util/namespace.h>
+
+SCENARIO(
+  "java_bytecode_parse_recursive_generic_class",
+  "[core][java_bytecode][java_bytecode_parse_generics]")
+{
+  const symbol_tablet &new_symbol_table=
+    load_java_class("RecursiveGeneric", ""
+      "./java_bytecode/java_bytecode_parse_generics");
+
+  std::string class_prefix="java::RecursiveGeneric";
+
+  REQUIRE(new_symbol_table.has_symbol(class_prefix));
+
+  // TODO: Extend this unit test when recursive generic types are correctly
+  // parsed.
+}