Store lambda methods kinds in java_class_typet

This paves the way for supporting multiple lambda method kinds, e.g. newinvokespecial lambdas
which instantiate and construct a type.

Author: smowton

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -426,7 +426,8 @@ void java_bytecode_convert_classt::convert(
     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));
+          "java::" + id2string(lambda_entry.second.lambda_method_ref),
+          lambda_entry.second.handle_type);
   }
 
   // Load annotations

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 
 #include "bytecode_info.h"
+#include "java_types.h"
 
 struct java_bytecode_parse_treet
 {
@@ -224,16 +225,11 @@ struct java_bytecode_parse_treet
     irep_idt outer_class; // when no outer class is set, there is no outer class
     size_t enum_elements=0;
 
-    enum class method_handle_typet
-    {
-      LAMBDA_METHOD_HANDLE,
-      UNKNOWN_HANDLE
-    };
-
     typedef std::vector<u2> u2_valuest;
     struct lambda_method_handlet
     {
-      method_handle_typet handle_type = method_handle_typet::UNKNOWN_HANDLE;
+      java_class_typet::method_handle_typet handle_type =
+        java_class_typet::method_handle_typet::UNKNOWN_HANDLE;
       irep_idt lambda_method_name;
       irep_idt lambda_method_ref;
       irep_idt interface_type;
@@ -255,7 +251,8 @@ struct java_bytecode_parse_treet
 
       bool is_unknown_handle() const
       {
-        return handle_type == method_handle_typet::UNKNOWN_HANDLE;
+        return handle_type ==
+               java_class_typet::method_handle_typet::UNKNOWN_HANDLE;
       }
     };
 

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -54,8 +54,7 @@ class java_bytecode_parsert final : public parsert
   using fieldt = java_bytecode_parse_treet::fieldt;
   using instructiont = java_bytecode_parse_treet::instructiont;
   using annotationt = java_bytecode_parse_treet::annotationt;
-  using method_handle_typet =
-    java_bytecode_parse_treet::classt::method_handle_typet;
+  using method_handle_typet = java_class_typet::method_handle_typet;
   using lambda_method_handlet =
     java_bytecode_parse_treet::classt::lambda_method_handlet;
 
@@ -330,6 +329,11 @@ class method_handle_infot : public structured_pool_entryt
     reference_index = entry.ref2;
   }
 
+  method_handle_kindt get_reference_kind() const
+  {
+    return reference_kind;
+  }
+
   base_ref_infot get_reference(const pool_entry_lookupt &pool_entry) const
   {
     const base_ref_infot ref_entry{pool_entry(reference_index)};

jbmc/src/java_bytecode/java_types.h

@@ -450,34 +450,62 @@ class java_class_typet:public class_typet
     set(ID_interface, interface);
   }
 
-  // it may be better to introduce a class like
-  // class java_lambda_method_handlet : private irept
-  // {
-  //   java_lambda_method_handlet(const irep_idt &id) : irept(id)
-  //   {
-  //   }
-  //
-  //   const irep_idt &get_lambda_method_handle() const
-  //   {
-  //     return id();
-  //   }
-  // };
-  using java_lambda_method_handlest = irept::subt;
+  enum class method_handle_typet
+  {
+    LAMBDA_METHOD_HANDLE,
+    LAMBDA_CONSTRUCTOR_HANDLE,
+    UNKNOWN_HANDLE
+  };
+
+  class java_lambda_method_handlet : public irept
+  {
+  public:
+    java_lambda_method_handlet(
+      const irep_idt &id,
+      method_handle_typet handle_type)
+      : irept(id)
+    {
+      set(ID_handle_type, static_cast<int>(handle_type));
+    }
+
+    java_lambda_method_handlet()
+    {
+      set(
+        ID_handle_type, static_cast<int>(method_handle_typet::UNKNOWN_HANDLE));
+    }
+
+    const irep_idt &get_lambda_method_identifier() const
+    {
+      return id();
+    }
+
+    method_handle_typet get_handle_type() const
+    {
+      return (method_handle_typet)get_int(ID_handle_type);
+    }
+  };
+
+  using java_lambda_method_handlest = std::vector<java_lambda_method_handlet>;
 
   const java_lambda_method_handlest &lambda_method_handles() const
   {
-    return find(ID_java_lambda_method_handles).get_sub();
+    return (const java_lambda_method_handlest &)find(
+             ID_java_lambda_method_handles)
+      .get_sub();
   }
 
   java_lambda_method_handlest &lambda_method_handles()
   {
-    return add(ID_java_lambda_method_handles).get_sub();
+    return (java_lambda_method_handlest &)add(ID_java_lambda_method_handles)
+      .get_sub();
   }
 
-  void add_lambda_method_handle(const irep_idt &identifier)
+  void add_lambda_method_handle(
+    const irep_idt &identifier,
+    method_handle_typet handle_type)
   {
     // creates a symbol_exprt for the identifier and pushes it in the vector
-    lambda_method_handles().emplace_back(identifier);
+    lambda_method_handles().emplace_back(identifier, handle_type);
   }
   void add_unknown_lambda_method_handle()
   {

jbmc/src/java_bytecode/lambda_synthesis.cpp

@@ -51,7 +51,8 @@ irep_idt lambda_synthetic_class_name(
 ///   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 has a known type
-static optionalt<symbolt> get_lambda_method_symbol(
+static optionalt<java_class_typet::java_lambda_method_handlet>
+get_lambda_method_handle(
   const symbol_table_baset &symbol_table,
   const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
   const size_t index)
@@ -62,15 +63,18 @@ static optionalt<symbolt> get_lambda_method_symbol(
   // internally by the string solver.
   if(index >= lambda_method_handles.size())
     return {};
-  const irept &lambda_method_handle = lambda_method_handles.at(index);
+  const auto &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 has an empty identifier)
-  if(!lambda_method_handle.id().empty())
-    return symbol_table.lookup_ref(lambda_method_handle.id());
+  if(
+    lambda_method_handle.get_handle_type() !=
+    java_class_typet::method_handle_typet::UNKNOWN_HANDLE)
+    return lambda_method_handle;
   return {};
 }
 
-static optionalt<irep_idt> lambda_method_name(
+static optionalt<java_class_typet::java_lambda_method_handlet>
+lambda_method_handle(
   const symbol_tablet &symbol_table,
   const irep_idt &method_identifier,
   const java_method_typet &dynamic_method_type)
@@ -84,11 +88,8 @@ static optionalt<irep_idt> lambda_method_name(
   const auto &lambda_method_handles = class_type.lambda_method_handles();
   auto lambda_handle_index =
     dynamic_method_type.get_int(ID_java_lambda_method_handle_index);
-  const auto lambda_method_symbol = get_lambda_method_symbol(
+  return get_lambda_method_handle(
     symbol_table, lambda_method_handles, lambda_handle_index);
-  if(lambda_method_symbol)
-    return lambda_method_symbol->name;
-  return {};
 }
 
 static optionalt<irep_idt> interface_method_id(
@@ -131,7 +132,7 @@ static optionalt<irep_idt> interface_method_id(
 
 symbolt synthetic_class_symbol(
   const irep_idt &synthetic_class_name,
-  const irep_idt &lambda_method_name,
+  const java_class_typet::java_lambda_method_handlet &lambda_method_handle,
   const struct_tag_typet &functional_interface_tag,
   const java_method_typet &dynamic_method_type)
 {
@@ -142,8 +143,7 @@ symbolt synthetic_class_symbol(
     strip_java_namespace_prefix(synthetic_class_name));
   synthetic_class_type.set_name(synthetic_class_name);
   synthetic_class_type.set_synthetic(true);
-  synthetic_class_type.set(
-    ID_java_lambda_method_identifier, lambda_method_name);
+  synthetic_class_type.set(ID_java_lambda_method_handle, lambda_method_handle);
   struct_tag_typet base_tag("java::java.lang.Object");
   synthetic_class_type.add_base(base_tag);
   synthetic_class_type.add_base(functional_interface_tag);
@@ -309,9 +309,9 @@ void create_invokedynamic_synthetic_classes(
       continue;
     const auto &dynamic_method_type =
       to_java_method_type(instruction.args.at(0).type());
-    const auto lambda_method_name = ::lambda_method_name(
+    const auto lambda_handle = lambda_method_handle(
       symbol_table, method_identifier, dynamic_method_type);
-    if(!lambda_method_name)
+    if(!lambda_handle)
     {
       log.debug() << "ignoring invokedynamic at " << method_identifier
                   << " address " << instruction.address
@@ -329,8 +329,9 @@ void create_invokedynamic_synthetic_classes(
     if(!interface_method_id)
       continue;
     log.debug() << "identified invokedynamic at " << method_identifier
-                << " address " << instruction.address
-                << " for lambda: " << *lambda_method_name << messaget::eom;
+                << " address " << instruction.address << " for lambda: "
+                << lambda_handle->get_lambda_method_identifier()
+                << messaget::eom;
     const irep_idt synthetic_class_name =
       lambda_synthetic_class_name(method_identifier, instruction.address);
     symbol_table.add(constructor_symbol(
@@ -342,7 +343,7 @@ void create_invokedynamic_synthetic_classes(
       synthetic_class_name));
     symbol_table.add(synthetic_class_symbol(
       synthetic_class_name,
-      *lambda_method_name,
+      *lambda_handle,
       functional_interface_tag,
       dynamic_method_type));
   }
@@ -488,8 +489,13 @@ codet invokedynamic_synthetic_method(
     lambda_method_args.push_back(param_symbol.symbol_expr());
   }
 
+  const auto &lambda_method_handle =
+    static_cast<const java_class_typet::java_lambda_method_handlet &>(
+      class_type.find(ID_java_lambda_method_handle));
+
   const auto &lambda_method_symbol =
-    ns.lookup(class_type.get(ID_java_lambda_method_identifier));
+    ns.lookup(lambda_method_handle.get_lambda_method_identifier());
+  const auto handle_type = lambda_method_handle.get_handle_type();
 
   if(return_type != empty_typet())
   {

src/util/irep_ids.def

@@ -647,6 +647,8 @@ IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol)
 IREP_ID_ONE(generic_types)
 IREP_ID_TWO(implicit_generic_types, #implicit_generic_types)
 IREP_ID_ONE(type_variables)
+IREP_ID_ONE(handle_type)
+IREP_ID_ONE(java_lambda_method_handle)
 IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index)
 IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles)
 IREP_ID_TWO(java_lambda_method_identifier, lambda_method_identifier)