Java lambdas: support newinvokespecial lambdas

These encode a lambda that instantiates and constructs an instance of some type without
using an intermediate method.

Author: smowton

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1905,6 +1905,30 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
   std::replace(class_name.begin(), class_name.end(), '.', '$');
   // replace '/' for '.' (package)
   std::replace(class_name.begin(), class_name.end(), '/', '.');
+
+  // The following lambda kinds specified in the JVMS (see for example
+  // https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-5.html#jvms-5.4.3.5
+  // but which aren't actually created by javac. Java has no syntax for a field-
+  // refernce like this, and even writing a stereotypical lambda like
+  // Producer<FieldType> = instance -> instance.field does not generate this
+  // kind of handle, but rather a synthetic method implementing the getfield
+  // operation.
+  // We don't implement a handle kind that can't be produced yet, but should
+  // they ever turn up this is where to fix them.
+
+  if(
+    entry.get_reference_kind() ==
+      method_handle_infot::method_handle_kindt::REF_getField ||
+    entry.get_reference_kind() ==
+      method_handle_infot::method_handle_kindt::REF_putField ||
+    entry.get_reference_kind() ==
+      method_handle_infot::method_handle_kindt::REF_getStatic ||
+    entry.get_reference_kind() ==
+      method_handle_infot::method_handle_kindt::REF_putStatic)
+  {
+    return {};
+  }
+
   const std::string method_ref =
     class_name + "." + name_and_type.get_name(pool_entry_lambda) + ':' +
     name_and_type.get_descriptor(pool_entry_lambda);
@@ -1914,7 +1938,11 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
   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;
+  lambda_method_handle.handle_type =
+    entry.get_reference_kind() ==
+        method_handle_infot::method_handle_kindt::REF_newInvokeSpecial
+      ? method_handle_typet::LAMBDA_CONSTRUCTOR_HANDLE
+      : method_handle_typet::LAMBDA_METHOD_HANDLE;
 
   return lambda_method_handle;
 }

jbmc/src/java_bytecode/lambda_synthesis.cpp

@@ -508,6 +508,49 @@ codet invokedynamic_synthetic_constructor(
   return std::move(result);
 }
 
+static symbol_exprt instantiate_new_object(
+  const irep_idt &function_id,
+  const symbolt &lambda_method_symbol,
+  symbol_table_baset &symbol_table,
+  code_blockt &result)
+{
+  // We must instantiate the object, then call the requested constructor
+  const auto &method_type = to_code_type(lambda_method_symbol.type);
+  INVARIANT(
+    method_type.get_bool(ID_constructor),
+    "REF_NewInvokeSpecial lambda must refer to a constructor");
+  const auto &created_type = method_type.parameters().at(0).type();
+  irep_idt created_class =
+    to_struct_tag_type(created_type.subtype()).get_identifier();
+
+  // Call static init if it exists:
+  irep_idt static_init_name = clinit_wrapper_name(created_class);
+  if(const auto *static_init_symbol = symbol_table.lookup(static_init_name))
+  {
+    result.add(code_function_callt{static_init_symbol->symbol_expr(), {}});
+  }
+
+  // Make a local to hold the new instance:
+  irep_idt new_instance_var_basename = "newinvokespecial_instance";
+  irep_idt new_instance_var_name =
+    id2string(function_id) + "::" + id2string(new_instance_var_basename);
+  auxiliary_symbolt new_instance_var_symbol;
+  new_instance_var_symbol.name = new_instance_var_name;
+  new_instance_var_symbol.base_name = new_instance_var_basename;
+  new_instance_var_symbol.mode = ID_java;
+  new_instance_var_symbol.type = created_type;
+  bool add_failed = symbol_table.add(new_instance_var_symbol);
+  POSTCONDITION(!add_failed);
+  symbol_exprt new_instance_var = new_instance_var_symbol.symbol_expr();
+  result.add(code_declt{new_instance_var});
+
+  // Instantiate the object:
+  side_effect_exprt java_new_expr(ID_java_new, created_type, {});
+  result.add(code_assignt{new_instance_var, java_new_expr});
+
+  return new_instance_var;
+}
+
 codet invokedynamic_synthetic_method(
   const irep_idt &function_id,
   symbol_table_baset &symbol_table,
@@ -565,8 +608,20 @@ codet invokedynamic_synthetic_method(
   const auto &lambda_method_symbol =
     ns.lookup(lambda_method_handle.get_lambda_method_identifier());
   const auto handle_type = lambda_method_handle.get_handle_type();
+  const auto is_constructor_lambda =
+    handle_type ==
+    java_class_typet::method_handle_typet::LAMBDA_CONSTRUCTOR_HANDLE;
 
-  if(return_type != empty_typet())
+  if(is_constructor_lambda)
+  {
+    auto new_instance_var = instantiate_new_object(
+      function_id, lambda_method_symbol, symbol_table, result);
+
+    // Prepend the newly created object to the lambda arg list:
+    lambda_method_args.insert(lambda_method_args.begin(), new_instance_var);
+  }
+
+  if(return_type != empty_typet() && !is_constructor_lambda)
   {
     result.add(code_returnt(side_effect_expr_function_callt(
       lambda_method_symbol.symbol_expr(),
@@ -580,5 +635,12 @@ codet invokedynamic_synthetic_method(
       lambda_method_symbol.symbol_expr(), lambda_method_args));
   }
 
+  if(is_constructor_lambda)
+  {
+    // Return the newly-created object.
+    result.add(code_returnt{
+      typecast_exprt::conditional_cast(lambda_method_args.at(0), return_type)});
+  }
+
   return std::move(result);
 }