Merge pull request #1937 from svorenova/lambda_tg2711

[TG-2478] Make Bootstrap methods available in method/instruction conversion

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -310,6 +310,18 @@ void java_bytecode_convert_classt::convert(const classt &c)
     }
   }
 
+  // now do lambda method handles (bootstrap methods)
+  for(const auto &lambda_entry : c.lambda_method_handle_map)
+  {
+    // if the handle is of unknown type, we still need to store it to preserve
+    // the correct indexing (invokedynamic instructions will retrieve
+    // method handles by index)
+    lambda_entry.second.is_unknown_handle()
+      ? class_type.add_unknown_lambda_method_handle()
+      : class_type.add_lambda_method_handle(
+          "java::" + id2string(lambda_entry.second.lambda_method_ref));
+  }
+
   // produce class symbol
   symbolt new_symbol;
   new_symbol.base_name=c.name;

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -306,6 +306,25 @@ 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 size_t &index)
+{
+  const symbol_exprt &lambda_method_handle = lambda_method_handles.at(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());
+  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.
@@ -555,7 +574,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(
@@ -926,7 +949,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;
 
@@ -1211,7 +1235,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_int(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 size_t &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);
 

src/java_bytecode/java_bytecode_parse_tree.h

@@ -193,6 +193,7 @@ class java_bytecode_parse_treet
     public:
       method_handle_typet handle_type;
       irep_idt lambda_method_name;
+      irep_idt lambda_method_ref;
       irep_idt interface_type;
       irep_idt method_type;
       u2_valuest u2_values;
@@ -208,6 +209,11 @@ class java_bytecode_parse_treet
         lambda_method_handle.u2_values = std::move(params);
         return lambda_method_handle;
       }
+
+      bool is_unknown_handle() const
+      {
+        return handle_type == method_handle_typet::UNKNOWN_HANDLE;
+      }
     };
 
     // TODO(tkiley): This map shouldn't be interacted with directly (instead

src/java_bytecode/java_bytecode_parser.cpp

@@ -843,6 +843,7 @@ void java_bytecode_parsert::rconstant_pool()
         it->expr.id("invokedynamic");
         const pool_entryt &nameandtype_entry=pool_entry(it->ref2);
         typet type=type_entry(nameandtype_entry.ref2);
+        type.set(ID_java_lambda_method_handle_index, it->ref1);
         it->expr.type()=type;
       }
       break;
@@ -1776,9 +1777,9 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
   const name_and_type_infot &name_and_type =
     ref_entry.get_name_and_type(pool_entry_lambda);
 
-  const std::string method_name =
+  const std::string method_ref =
     class_entry.get_name(pool_entry_lambda) + "." +
-    name_and_type.get_name(pool_entry_lambda) +
+    name_and_type.get_name(pool_entry_lambda) + ':' +
     name_and_type.get_descriptor(pool_entry_lambda);
 
   lambda_method_handlet lambda_method_handle;
@@ -1791,6 +1792,7 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
     //                "new" when it is a class variable, instantiated in <init>
     lambda_method_handle.lambda_method_name =
       name_and_type.get_name(pool_entry_lambda);
+    lambda_method_handle.lambda_method_ref = method_ref;
     lambda_method_handle.handle_type =
       method_handle_typet::LAMBDA_METHOD_HANDLE;
 

src/java_bytecode/java_types.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/c_types.h>
 #include <util/optional.h>
+#include <util/std_expr.h>
 
 class java_class_typet:public class_typet
 {
@@ -30,6 +31,30 @@ class java_class_typet:public class_typet
   {
     return set(ID_access, access);
   }
+
+  typedef std::vector<symbol_exprt> java_lambda_method_handlest;
+
+  const java_lambda_method_handlest &lambda_method_handles() const
+  {
+    return (const java_lambda_method_handlest &)find(
+             ID_java_lambda_method_handles)
+      .get_sub();
+  }
+
+  java_lambda_method_handlest &lambda_method_handles()
+  {
+    return (java_lambda_method_handlest &)add(ID_java_lambda_method_handles)
+      .get_sub();
+  }
+
+  void add_lambda_method_handle(const irep_idt &identifier)
+  {
+    lambda_method_handles().emplace_back(identifier);
+  }
+  void add_unknown_lambda_method_handle()
+  {
+    lambda_method_handles().emplace_back();
+  }
 };
 
 inline const java_class_typet &to_java_class_type(const typet &type)

src/util/irep_ids.def

@@ -836,6 +836,8 @@ IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol)
 IREP_ID_TWO(generic_types, #generic_types)
 IREP_ID_TWO(implicit_generic_types, #implicit_generic_types)
 IREP_ID_TWO(type_variables, #type_variables)
+IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index)
+IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
 IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)

unit/Makefile

@@ -23,6 +23,8 @@ SRC += unit_tests.cpp \
        java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
+       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
+       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
        miniBDD_new.cpp \
        java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
        java_bytecode/java_utils_test.cpp \

unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp

@@ -18,7 +18,7 @@ SCENARIO(
   {
     const symbol_tablet symbol_table = load_java_class_lazy(
       "LocalLambdas",
-      "./java_bytecode/java_bytecode_parser/lambda_examples/",
+      "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
       "LocalLambdas.test");
 
     THEN("Then the lambdas should be loaded")
@@ -68,7 +68,7 @@ SCENARIO(
   {
     const symbol_tablet symbol_table = load_java_class_lazy(
       "MemberLambdas",
-      "./java_bytecode/java_bytecode_parser/lambda_examples/",
+      "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
       "MemberLambdas.test");
 
     THEN("Then the lambdas should be loaded")
@@ -117,7 +117,7 @@ SCENARIO(
   {
     const symbol_tablet symbol_table = load_java_class_lazy(
       "StaticLambdas",
-      "./java_bytecode/java_bytecode_parser/lambda_examples/",
+      "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
       "StaticLambdas.test");
 
     THEN("Then the lambdas should be loaded")
@@ -166,7 +166,7 @@ SCENARIO(
   {
     const symbol_tablet symbol_table = load_java_class_lazy(
       "OuterMemberLambdas$Inner",
-      "./java_bytecode/java_bytecode_parser/lambda_examples/",
+      "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
       "OuterMemberLambdas$Inner.test");
 
     THEN("Then the lambdas should be loaded")
@@ -192,7 +192,7 @@ SCENARIO(
 {
   const symbol_tablet symbol_table = load_java_class_lazy(
     "ExternalLambdaAccessor",
-    "./java_bytecode/java_bytecode_parser/lambda_examples/",
+    "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
     "ExternalLambdaAccessor.test");
 
   THEN("Then the lambdas should be loaded")