Pass lambda method handles to method instruction conversion

Author: svorenova

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -303,6 +303,27 @@ code_typet member_type_lazy(
   return to_code_type(member_type_from_descriptor);
 }
 
+/// Retrieves the symbol of the lambda method associated with the given
+/// lambda method handle (bootstrap method).
+/// \param lambda_method_handles Vector of lambda method handles (bootstrap
+/// methods) of the class where the lambda is called
+/// \param index Index of the lambda method handle in the vector
+/// \return Symbol of the lambda method if the method handle does not have an
+/// unknown type
+optionalt<symbolt> java_bytecode_convert_methodt::get_lambda_method_symbol(
+  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
+  const irep_idt &index)
+{
+  const symbol_exprt &lambda_method_handle =
+    lambda_method_handles.at(std::stoi(id2string(index)));
+  // If the lambda method handle has an unknown type, it does not refer to
+  // any symbol (it is a symbol expression with empty identifier)
+  if(!lambda_method_handle.get_identifier().empty())
+    return symbol_table.lookup_ref(lambda_method_handle.get_identifier());
+  else
+    return {};
+}
+
 /// 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.
@@ -552,7 +573,11 @@ void java_bytecode_convert_methodt::convert(
   current_method=method_symbol.name;
   method_has_this=code_type.has_this();
   if((!m.is_abstract) && (!m.is_native))
-    method_symbol.value=convert_instructions(m, code_type, method_symbol.name);
+    method_symbol.value = convert_instructions(
+      m,
+      code_type,
+      method_symbol.name,
+      to_java_class_type(class_symbol.type).lambda_method_handles());
 }
 
 const bytecode_infot &java_bytecode_convert_methodt::get_bytecode_info(
@@ -923,7 +948,8 @@ static unsigned get_bytecode_type_width(const typet &ty)
 codet java_bytecode_convert_methodt::convert_instructions(
   const methodt &method,
   const code_typet &method_type,
-  const irep_idt &method_name)
+  const irep_idt &method_name,
+  const java_class_typet::java_lambda_method_handlest &lambda_method_handles)
 {
   const instructionst &instructions=method.instructions;
 
@@ -1208,7 +1234,19 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="invokedynamic")
     {
       // not used in Java
-      code_typet &code_type=to_code_type(arg0.type());
+      code_typet &code_type = to_code_type(arg0.type());
+
+      const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
+        lambda_method_handles,
+        code_type.get(ID_java_lambda_method_handle_index));
+      if(lambda_method_symbol.has_value())
+        debug() << "Converting invokedynamic for lambda: "
+                << lambda_method_symbol.value().name << eom;
+      else
+        debug() << "Converting invokedynamic for lambda with unknown handle "
+                   "type"
+                << eom;
+
       const code_typet::parameterst &parameters(code_type.parameters());
 
       pop(parameters.size());

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -235,13 +235,18 @@ class java_bytecode_convert_methodt:public messaget
     const address_mapt &amap,
     bool allow_merge=true);
 
+  optionalt<symbolt> get_lambda_method_symbol(
+    const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
+    const irep_idt &index);
+
   // conversion
   void convert(const symbolt &class_symbol, const methodt &);
 
   codet convert_instructions(
     const methodt &,
     const code_typet &,
-    const irep_idt &);
+    const irep_idt &,
+    const java_class_typet::java_lambda_method_handlest &);
 
   const bytecode_infot &get_bytecode_info(const irep_idt &statement);