Generics support

regression/cbmc-java/iterator2/test.desc

@@ -1,6 +1,6 @@
 CORE
 iterator2.class
---cover location --unwind 3 --function iterator2.f 
+--cover location --unwind 3 --function iterator2.f
 ^EXIT=0$
 ^SIGNAL=0$
 ^.*SATISFIED$

src/java_bytecode/ci_lazy_methods.cpp

@@ -79,7 +79,7 @@ bool ci_lazy_methodst::operator()(
       {
         const irep_idt methodid="java::"+id2string(classname)+"."+
           id2string(method.name)+":"+
-          id2string(method.signature);
+          id2string(method.descriptor);
         method_worklist2.push_back(methodid);
       }
     }
@@ -505,4 +505,3 @@ irep_idt ci_lazy_methodst::get_virtual_method_target(
   else
     return irep_idt();
 }
-

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_language.h"
 #include "java_utils.h"
 
+#include <util/c_types.h>
 #include <util/arith_tools.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -93,6 +94,33 @@ void java_bytecode_convert_classt::convert(const classt &c)
   }
 
   java_class_typet class_type;
+  if(c.signature.has_value() && c.signature.value()[0]=='<')
+  {
+    java_generics_class_typet generic_class_type;
+#ifdef DEBUG
+    std::cout << "INFO: found generic class signature "
+              << c.signature.value()
+              << " in parsed class "
+              << c.name << "\n";
+#endif
+    try
+    {
+      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_signature_exceptiont)
+    {
+      warning() << "we currently don't support parsing for example double "
+        "bounded, recursive and wild card generics" << eom;
+    }
+  }
 
   class_type.set_tag(c.name);
   class_type.set(ID_base_name, c.name);
@@ -166,7 +194,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
     const irep_idt method_identifier=
       id2string(qualified_classname)+
       "."+id2string(method.name)+
-      ":"+method.signature;
+      ":"+method.descriptor;
     // Always run the lazy pre-stage, as it symbol-table
     // registers the function.
     debug() << "Adding symbol:  method '" << method_identifier << "'" << eom;
@@ -187,7 +215,49 @@ void java_bytecode_convert_classt::convert(
   symbolt &class_symbol,
   const fieldt &f)
 {
-  typet field_type=java_type_from_string(f.signature);
+  typet field_type;
+  if(f.signature.has_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;`
+    if(is_java_generic_parameter(field_type))
+    {
+#ifdef DEBUG
+      std::cout << "fieldtype: generic "
+                << to_java_generic_parameter(field_type).type_variable()
+                     .get_identifier()
+                << " name " << f.name << "\n";
+#endif
+    }
+
+    /// this is for a field that holds a generic type, wither with instantiated
+    /// or with free type variables, e.g., `List<T> l;` or `List<Integer> l;`
+    else if(is_java_generic_type(field_type))
+    {
+      java_generic_typet &with_gen_type=
+        to_java_generic_type(field_type);
+#ifdef DEBUG
+      std::cout << "fieldtype: generic container type "
+                << std::to_string(with_gen_type.generic_type_variables().size())
+                << " type " << with_gen_type.id()
+                << " name " << f.name
+                << " subtype id " << with_gen_type.subtype().id() << "\n";
+#endif
+      field_type=with_gen_type;
+    }
+
+    /// This case is not possible, a field is either a non-instantiated type
+    /// variable or a generics container type.
+    INVARIANT(
+      !is_java_generic_inst_parameter(field_type),
+      "Cannot be an instantiated type variable here.");
+  }
+  else
+    field_type=java_type_from_string(f.descriptor);
 
   // is this a static field?
   if(f.is_static)

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -252,7 +252,7 @@ const exprt java_bytecode_convert_methodt::variable(
 /// method conversion just yet. The caller should call
 /// java_bytecode_convert_method later to give the symbol/method a body.
 /// \par parameters: `class_symbol`: class this method belongs to
-/// `method_identifier`: fully qualified method name, including type signature
+/// `method_identifier`: fully qualified method name, including type descriptor
 ///   (e.g. "x.y.z.f:(I)")
 /// `m`: parsed method object to convert
 /// `symbol_table`: global symbol table (will be modified)
@@ -263,7 +263,7 @@ void java_bytecode_convert_method_lazy(
   symbol_tablet &symbol_table)
 {
   symbolt method_symbol;
-  typet member_type=java_type_from_string(m.signature);
+  typet member_type=java_type_from_string(m.descriptor);
 
   method_symbol.name=method_identifier;
   method_symbol.base_name=m.base_name;
@@ -317,7 +317,7 @@ void java_bytecode_convert_methodt::convert(
   // to retrieve the symbol (constructed by java_bytecode_convert_method_lazy)
   // associated to the method
   const irep_idt method_identifier=
-    id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.signature;
+    id2string(class_symbol.name)+"."+id2string(m.name)+":"+m.descriptor;
   method_id=method_identifier;
 
   const symbolt &old_sym=*symbol_table.lookup(method_identifier);
@@ -350,7 +350,17 @@ void java_bytecode_convert_methodt::convert(
     // Construct a fully qualified name for the parameter v,
     // e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a
     // symbol_exprt with the parameter and its type
-    typet t=java_type_from_string(v.signature);
+    typet t;
+    if(v.signature.has_value())
+    {
+      t=java_type_from_string_with_exception(
+        v.descriptor,
+        v.signature,
+        id2string(class_symbol.name));
+    }
+    else
+      t=java_type_from_string(v.descriptor);
+
     std::ostringstream id_oss;
     id_oss << method_id << "::" << v.name;
     irep_idt identifier(id_oss.str());

src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -28,6 +28,7 @@ void java_bytecode_parse_treet::classt::swap(
   std::swap(other.is_public, is_public);
   std::swap(other.is_protected, is_protected);
   std::swap(other.is_private, is_private);
+  std::swap(other.signature, signature);
   other.implements.swap(implements);
   other.fields.swap(fields);
   other.methods.swap(methods);
@@ -151,7 +152,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
     out << "synchronized ";
 
   out << name;
-  out << " : " << signature;
+  out << " : " << descriptor;
 
   out << '\n';
 
@@ -188,7 +189,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
   for(const auto &v : local_variable_table)
   {
     out << "    " << v.index << ": " << v.name << ' '
-        << v.signature << '\n';
+        << v.descriptor << '\n';
   }
 
   out << '\n';
@@ -212,7 +213,7 @@ void java_bytecode_parse_treet::fieldt::output(std::ostream &out) const
     out << "static ";
 
   out << name;
-  out << " : " << signature << ';';
+  out << " : " << descriptor << ';';
 
   out << '\n';
 }

src/java_bytecode/java_bytecode_parse_tree.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <set>
 
+#include <util/optional.h>
 #include <util/std_code.h>
 #include <util/std_types.h>
 
@@ -54,16 +55,17 @@ class java_bytecode_parse_treet
   class membert
   {
   public:
-    std::string signature;
+    std::string descriptor;
+    optionalt<std::string> signature;
     irep_idt name;
     bool is_public, is_protected, is_private, is_static, is_final;
     annotationst annotations;
 
     virtual void output(std::ostream &out) const = 0;
 
     membert():
-      is_public(false), is_protected(false), is_private(false),
-      is_static(false), is_final(false)
+      is_public(false), is_protected(false),
+      is_private(false), is_static(false), is_final(false)
     {
     }
   };
@@ -100,7 +102,8 @@ class java_bytecode_parse_treet
     {
     public:
       irep_idt name;
-      std::string signature;
+      std::string descriptor;
+      optionalt<std::string> signature;
       std::size_t index;
       std::size_t start_pc;
       std::size_t length;
@@ -174,7 +177,7 @@ class java_bytecode_parse_treet
 
     typedef std::list<irep_idt> implementst;
     implementst implements;
-
+    optionalt<std::string> signature;
     typedef std::list<fieldt> fieldst;
     typedef std::list<methodt> methodst;
     fieldst fields;