Implement lambda code synthesis

This scans invokedynamic instructions during class-loading, creating a synthetic type
for each one that we can understand, and registers its constructor (which captures)
and method (which passes captured and actual parameters to the real lambda function)
as synthetic methods. These are then created on demand using the same mechanism as
e.g. synthetic static initializer methods.

Prior to this change invokedynamic instructions were always stubbed to return null.
With this change they actually work, so you can verify programs that use lambdas,
such as assert ((MyInterface)(x -> x + 1))(1) == 2

Author: smowton

jbmc/src/java_bytecode/Makefile

@@ -37,6 +37,7 @@ SRC = assignments_from_json.cpp \
       java_string_literals.cpp \
       java_types.cpp \
       java_utils.cpp \
+      lambda_synthesis.cpp \
       load_method_by_regex.cpp \
       mz_zip_archive.cpp \
       remove_exceptions.cpp \

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_string_literal_expr.h"
 #include "java_types.h"
 #include "java_utils.h"
+#include "lambda_synthesis.h"
 #include "pattern.h"
 #include "remove_exceptions.h"
 
@@ -303,24 +304,6 @@ java_method_typet member_type_lazy(
   return to_java_method_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 has a known 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 irept &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());
-  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.
@@ -631,8 +614,7 @@ void java_bytecode_convert_methodt::convert(
   if((!m.is_abstract) && (!m.is_native))
   {
     code_blockt code(convert_parameter_annotations(m, method_type));
-    code.append(convert_instructions(
-      m, to_java_class_type(class_symbol.type).lambda_method_handles()));
+    code.append(convert_instructions(m));
     method_symbol.value = std::move(code);
   }
 }
@@ -1061,9 +1043,8 @@ code_blockt java_bytecode_convert_methodt::convert_parameter_annotations(
   return code;
 }
 
-code_blockt java_bytecode_convert_methodt::convert_instructions(
-  const methodt &method,
-  const java_class_typet::java_lambda_method_handlest &lambda_method_handles)
+code_blockt
+java_bytecode_convert_methodt::convert_instructions(const methodt &method)
 {
   const instructionst &instructions=method.instructions;
 
@@ -1317,10 +1298,9 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     }
     else if(bytecode == BC_invokedynamic)
     {
-      // not used in Java
       if(
-        const auto res = convert_invoke_dynamic(
-          lambda_method_handles, i_it->source_location, arg0))
+        const auto res =
+          convert_invoke_dynamic(i_it->source_location, i_it->address, arg0, c))
       {
         results.resize(1);
         results[0] = *res;
@@ -2957,40 +2937,71 @@ code_blockt java_bytecode_convert_methodt::convert_astore(
 }
 
 optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
-  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
   const source_locationt &location,
-  const exprt &arg0)
+  std::size_t instruction_address,
+  const exprt &arg0,
+  codet &result_code)
 {
   const java_method_typet &method_type = to_java_method_type(arg0.type());
+  const java_method_typet::parameterst &parameters(method_type.parameters());
+  const typet &return_type = method_type.return_type();
 
-  const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
-    lambda_method_handles,
-    method_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;
+  // Note these must be popped regardless of whether we understand the lambda
+  // method or not
+  code_function_callt::argumentst arguments = pop(parameters.size());
 
-  const java_method_typet::parameterst &parameters(method_type.parameters());
+  irep_idt synthetic_class_name =
+    lambda_synthetic_class_name(method_id, instruction_address);
 
-  pop(parameters.size());
+  if(!symbol_table.has_symbol(synthetic_class_name))
+  {
+    // We failed to parse the invokedynamic handle as a Java 8+ lambda;
+    // give up and return null.
+    const auto value = zero_initializer(return_type, location, ns);
+    if(!value.has_value())
+    {
+      error().source_location = location;
+      error() << "failed to zero-initialize return type" << eom;
+      throw 0;
+    }
+    return value;
+  }
 
-  const typet &return_type = method_type.return_type();
+  // Construct an instance of the synthetic class created for this invokedynamic
+  // site:
 
-  if(return_type.id() == ID_empty)
-    return {};
+  irep_idt constructor_name = id2string(synthetic_class_name) + ".<init>";
+
+  const symbolt &constructor_symbol = ns.lookup(constructor_name);
 
-  const auto value = zero_initializer(return_type, location, ns);
-  if(!value.has_value())
+  code_blockt result;
+
+  // SyntheticType lambda_new = new SyntheticType;
+  const reference_typet ref_type =
+    java_reference_type(struct_tag_typet(synthetic_class_name));
+  side_effect_exprt java_new_expr(ID_java_new, ref_type, location);
+  const exprt new_instance = tmp_variable("lambda_new", ref_type);
+  result.add(code_assignt(new_instance, java_new_expr, location));
+
+  // lambda_new.<init>(capture_1, capture_2, ...);
+  // Add the implicit 'this' parameter:
+  arguments.insert(arguments.begin(), new_instance);
+  code_function_callt constructor_call(
+    constructor_symbol.symbol_expr(), arguments);
+  constructor_call.add_source_location() = location;
+  result.add(constructor_call);
+  if(needed_lazy_methods)
   {
-    error().source_location = location;
-    error() << "failed to zero-initialize return type" << eom;
-    throw 0;
+    needed_lazy_methods->add_needed_method(constructor_symbol.name);
+    needed_lazy_methods->add_needed_class(synthetic_class_name);
   }
-  return value;
+
+  result_code = std::move(result);
+
+  if(return_type.id() == ID_empty)
+    return {};
+  else
+    return new_instance;
 }
 
 void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr(

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -293,20 +293,14 @@ 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 &);
 
   code_blockt convert_parameter_annotations(
     const methodt &method,
     const java_method_typet &method_type);
 
-  code_blockt convert_instructions(
-    const methodt &,
-    const java_class_typet::java_lambda_method_handlest &);
+  code_blockt convert_instructions(const methodt &);
 
   codet get_clinit_call(const irep_idt &classname);
 
@@ -350,9 +344,10 @@ class java_bytecode_convert_methodt:public messaget
       &ret_instructions) const;
 
   optionalt<exprt> convert_invoke_dynamic(
-    const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
     const source_locationt &location,
-    const exprt &arg0);
+    std::size_t instruction_address,
+    const exprt &arg0,
+    codet &result_code);
 
   code_blockt convert_astore(
     const irep_idt &statement,

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -40,6 +40,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_string_literal_expr.h"
 #include "java_string_literals.h"
 #include "java_utils.h"
+#include "lambda_synthesis.h"
 
 #include "expr2java.h"
 #include "load_method_by_regex.h"
@@ -719,6 +720,25 @@ bool java_bytecode_languaget::typecheck(
     }
   }
 
+  // Now add synthetic classes for every invokedynamic instruction found (it
+  // makes this easier that all interface types and their methods have been
+  // created above):
+  for(const auto &id_and_symbol : symbol_table)
+  {
+    if(id_and_symbol.second.type.id() != ID_code)
+      continue;
+    auto cmb = method_bytecode.get(id_and_symbol.first);
+    if(!cmb)
+      continue;
+
+    create_invokedynamic_synthetic_classes(
+      id_and_symbol.first,
+      cmb->get().method.instructions,
+      symbol_table,
+      synthetic_methods,
+      get_message_handler());
+  }
+
   // Now that all classes have been created in the symbol table we can populate
   // the class hierarchy:
   class_hierarchy(symbol_table);
@@ -1031,6 +1051,15 @@ static void notify_static_method_calls(
           expr_dynamic_cast<symbol_exprt>(fn_call->function());
         needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
       }
+      else if(
+        it->id() == ID_side_effect &&
+        to_side_effect_expr(*it).get_statement() == ID_function_call)
+      {
+        const auto &call_expr = to_side_effect_expr_function_call(*it);
+        const symbol_exprt &fn_sym =
+          expr_dynamic_cast<symbol_exprt>(call_expr.function());
+        needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
+      }
     }
   }
 }
@@ -1136,6 +1165,14 @@ bool java_bytecode_languaget::convert_single_method(
           get_pointer_type_selector(),
           get_message_handler());
       break;
+    case synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR:
+      writable_symbol.value = get_invokedynamic_synthetic_constructor(
+        function_id, symbol_table, get_message_handler());
+      break;
+    case synthetic_method_typet::INVOKEDYNAMIC_METHOD:
+      writable_symbol.value = get_invokedynamic_synthetic_method(
+        function_id, symbol_table, get_message_handler());
+      break;
     }
     // Notify lazy methods of static calls made from the newly generated
     // function: