Resolving signature/descriptor mismatch for methods

We want to use signature whenever possible. In certain cases, the number of input parameters in the descriptor is
higher than in the signature. For example for enums and inner classes,
in these cases descriptor has the correct form (although without generics information).

Author: svorenova

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