Merge pull request #1489 from svorenova/tg-865

Resolving signature/descriptor missmatch

Author: Thomas Kiley

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -203,7 +203,8 @@ void java_bytecode_convert_classt::convert(const classt &c)
       *class_symbol,
       method_identifier,
       method,
-      symbol_table);
+      symbol_table,
+      get_message_handler());
     lazy_methods[method_identifier]=std::make_pair(class_symbol, &method);
   }
 

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -248,6 +248,69 @@ const exprt java_bytecode_convert_methodt::variable(
   }
 }
 
+/// Returns the member type for a method, based on signature or descriptor
+/// \param descriptor
+///   descriptor of the method
+/// \param signature
+///   signature of the method
+/// \param class_name
+///   string containing the name of the corresponding class
+/// \param method_name
+///   string containing the name of the method
+/// \param message_handler
+///   message handler to collect warnings
+/// \return
+///   the constructed member type
+typet member_type_lazy(const std::string &descriptor,
+                       const optionalt<std::string> &signature,
+                       const std::string &class_name,
+                       const std::string &method_name,
+                       message_handlert &message_handler)
+{
+  // In order to construct the method type, we can either use signature or
+  // descriptor. Since only signature contains the generics info, we want to
+  // use signature whenever possible. We revert to using descriptor if (1) the
+  // signature does not exist, (2) an unsupported generics are present or
+  // (3) in the special case when the number of parameters in the descriptor
+  // does not match the number of parameters in the signature - e.g. for
+  // certain types of inner classes and enums (see unit tests for examples).
+
+  messaget message(message_handler);
+
+  typet member_type_from_descriptor=java_type_from_string(descriptor);
+  INVARIANT(member_type_from_descriptor.id()==ID_code, "Must be code type");
+  if(signature.has_value())
+  {
+    try
+    {
+      typet member_type_from_signature=java_type_from_string(
+        signature.value(),
+        class_name);
+      INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
+      if(to_code_type(member_type_from_signature).parameters().size()==
+         to_code_type(member_type_from_descriptor).parameters().size())
+      {
+        return member_type_from_signature;
+      }
+      else
+      {
+        message.warning() << "method: " << class_name << "." << method_name
+          << "\n signature: " << signature.value() << "\n descriptor: "
+          << descriptor << "\n different number of parameters, reverting to "
+          "descriptor" << message.eom;
+      }
+    }
+    catch(unsupported_java_class_signature_exceptiont &e)
+    {
+      message.warning() << "method: " << class_name << "." << method_name
+        << "\n could not parse signature: " << signature.value() << "\n "
+        << e.what() << "\n" << " reverting to descriptor: "
+        << descriptor << message.eom;
+    }
+  }
+  return member_type_from_descriptor;
+}
+
 /// This creates a method symbol in the symtab, but doesn't actually perform
 /// method conversion just yet. The caller should call
 /// java_bytecode_convert_method later to give the symbol/method a body.
@@ -256,14 +319,22 @@ const exprt java_bytecode_convert_methodt::variable(
 ///   (e.g. "x.y.z.f:(I)")
 /// `m`: parsed method object to convert
 /// `symbol_table`: global symbol table (will be modified)
+/// `message_handler`: message handler to collect warnings
 void java_bytecode_convert_method_lazy(
   const symbolt &class_symbol,
   const irep_idt &method_identifier,
   const java_bytecode_parse_treet::methodt &m,
-  symbol_tablet &symbol_table)
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
 {
   symbolt method_symbol;
-  typet member_type=java_type_from_string(m.descriptor);
+
+  typet member_type=member_type_lazy(
+    m.descriptor,
+    m.signature,
+    id2string(class_symbol.name),
+    id2string(m.base_name),
+    message_handler);
 
   method_symbol.name=method_identifier;
   method_symbol.base_name=m.base_name;

src/java_bytecode/java_bytecode_convert_method.h

@@ -53,6 +53,7 @@ void java_bytecode_convert_method_lazy(
   const symbolt &class_symbol,
   const irep_idt &method_identifier,
   const java_bytecode_parse_treet::methodt &,
-  symbol_tablet &symbol_table);
+  symbol_tablet &symbol_table,
+  message_handlert &);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_H

unit/java_bytecode/java_bytecode_parse_generics/AbstractGenericClass.class

@@ -0,0 +1,4 @@
+public abstract class AbstractGenericClass<T>
+{
+
+}

unit/java_bytecode/java_bytecode_parse_generics/AbstractGenericClass.java

@@ -0,0 +1,17 @@
+public class Outer<T>
+{
+  private class Inner
+  {
+    private final AbstractGenericClass<T> u;
+
+    Inner (AbstractGenericClass<T> t)
+    {
+      this.u = t;
+    }
+  }
+
+  private enum InnerEnum
+  {
+
+  }
+}

unit/java_bytecode/java_bytecode_parse_generics/Outer$Inner.class

@@ -17,6 +17,7 @@
 #include <java_bytecode/java_bytecode_language.h>
 #include <iostream>
 #include <testing-utils/load_java_class.h>
+#include <testing-utils/require_symbol.h>
 
 SCENARIO(
   "java_bytecode_parse_derived_generic_class",
@@ -33,12 +34,8 @@ SCENARIO(
     REQUIRE(new_symbol_table.has_symbol(class_prefix));
 
     const symbolt &derived_symbol=new_symbol_table.lookup_ref(class_prefix);
-    REQUIRE(derived_symbol.is_type);
-    const typet &derived_type=derived_symbol.type;
-    REQUIRE(derived_type.id()==ID_struct);
-    const class_typet &class_type=to_class_type(derived_type);
-    REQUIRE(class_type.is_class());
-    REQUIRE_FALSE(class_type.get_bool(ID_incomplete_class));
+    const class_typet &derived_class_type=
+      require_symbol::require_complete_class(derived_symbol);
 
     // TODO(tkiley): Currently we do not support extracting information
     // about the base classes generic information.