cprover
lambda_synthesis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java lambda code synthesis
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #include "lambda_synthesis.h"
13 
16 #include "java_types.h"
17 #include "java_utils.h"
18 #include "synthetic_methods_map.h"
19 
20 #include <util/message.h>
21 #include <util/namespace.h>
22 #include <util/prefix.h>
23 #include <util/symbol_table.h>
24 
25 #include <string.h>
26 
27 static std::string escape_symbol_special_chars(std::string input)
28 {
29  for(auto &c : input)
30  {
31  if(c == '$' || c == ':' || c == '.')
32  c = '_';
33  }
34  return input;
35 }
36 
38  const irep_idt &method_identifier,
39  std::size_t instruction_address)
40 {
41  return "java::lambda_synthetic_class$" +
43  id2string(strip_java_namespace_prefix(method_identifier))) +
44  "$" + std::to_string(instruction_address);
45 }
46 
56  const symbol_table_baset &symbol_table,
57  const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
58  const size_t index)
59 {
60  // Check if we don't have enough bootstrap methods to satisfy the requested
61  // lambda. This could happen if we fail to parse one of the methods, or if
62  // the class type is partly or entirely synthetic, such as the types created
63  // internally by the string solver.
64  if(index >= lambda_method_handles.size())
65  return {};
66  const auto &lambda_method_handle = lambda_method_handles.at(index);
67  // If the lambda method handle has an unknown type, it does not refer to
68  // any symbol (it has an empty identifier)
69  if(
70  lambda_method_handle.get_handle_kind() !=
72  return lambda_method_handle;
73  return {};
74 }
75 
78  const symbol_tablet &symbol_table,
79  const irep_idt &method_identifier,
80  const java_method_typet &dynamic_method_type)
81 {
82  const namespacet ns{symbol_table};
83  const auto &method_symbol = ns.lookup(method_identifier);
84  const auto &declaring_class_symbol =
85  ns.lookup(*declaring_class(method_symbol));
86 
87  const auto &class_type = to_java_class_type(declaring_class_symbol.type);
88  const auto &lambda_method_handles = class_type.lambda_method_handles();
89  auto lambda_handle_index =
90  dynamic_method_type.get_int(ID_java_lambda_method_handle_index);
92  symbol_table, lambda_method_handles, lambda_handle_index);
93 }
94 
95 class no_unique_unimplemented_method_exceptiont : public std::exception
96 {
97 public:
98  explicit no_unique_unimplemented_method_exceptiont(const std::string &s)
99  : message(s)
100  {
101  }
102  const std::string message;
103 };
104 
106 {
108  const java_class_typet::methodt *a,
109  const java_class_typet::methodt *b) const
110  {
111  return a->get_base_name() == b->get_base_name()
112  ? (a->get_descriptor() == b->get_descriptor()
113  ? 0
114  : a->get_descriptor() < b->get_descriptor())
115  : a->get_base_name() < b->get_base_name();
116  }
117 };
118 
121 typedef std::map<
123  bool,
126 
135 get_interface_methods(const irep_idt &interface_id, const namespacet &ns)
136 {
137  static const irep_idt jlo = "java::java.lang.Object";
138  // Terminate recursion at Object; any other base of an interface must
139  // itself be an interface.
140  if(jlo == interface_id)
141  return {};
142 
143  const java_class_typet &interface =
144  to_java_class_type(ns.lookup(interface_id).type);
145 
146  if(interface.get_is_stub())
147  {
149  "produces a type that inherits the stub type " + id2string(interface_id));
150  }
151 
153 
154  // First accumulate definitions from child types:
155  for(const auto &base : interface.bases())
156  {
157  const methods_by_name_and_descriptort base_methods =
158  get_interface_methods(base.type().get_identifier(), ns);
159  for(const auto &base_method : base_methods)
160  {
161  if(base_method.second)
162  {
163  // Any base definition fills any abstract definition from another base:
164  all_methods[base_method.first] = true;
165  }
166  else
167  {
168  // An abstract method incoming from a base falls to any existing
169  // definition, so only insert if not present:
170  all_methods.emplace(base_method.first, false);
171  }
172  }
173  }
174 
175  // Now insert defintions from this class:
176  for(const auto &method : interface.methods())
177  {
178  static const irep_idt equals = "equals";
179  static const irep_idt equals_descriptor = "(Ljava/lang/Object;)Z";
180  static const irep_idt hashCode = "hashCode";
181  static const irep_idt hashCode_descriptor = "()I";
182  if(
183  (method.get_base_name() == equals &&
184  method.get_descriptor() == equals_descriptor) ||
185  (method.get_base_name() == hashCode &&
186  method.get_descriptor() == hashCode_descriptor))
187  {
188  // Ignore any uses of functions that are certainly defined on
189  // java.lang.Object-- even if explicitly made abstract, they can't be the
190  // implemented method of a functional interface.
191  continue;
192  }
193 
194  // Note unlike inherited definitions, an abstract definition here *does*
195  // wipe out a non-abstract definition (i.e. a default method) from a parent
196  // type.
197  all_methods[&method] =
198  !ns.lookup(method.get_name()).type.get_bool(ID_C_abstract);
199  }
200 
201  return all_methods;
202 }
203 
205  const symbol_tablet &symbol_table,
206  const struct_tag_typet &functional_interface_tag,
207  const irep_idt &method_identifier,
208  const int instruction_address,
209  const messaget &log)
210 {
211  const namespacet ns{symbol_table};
212  try
213  {
214  const methods_by_name_and_descriptort all_methods =
215  get_interface_methods(functional_interface_tag.get_identifier(), ns);
216 
217  const java_class_typet::methodt *method_and_descriptor_to_implement =
218  nullptr;
219 
220  for(const auto &entry : all_methods)
221  {
222  if(!entry.second)
223  {
224  if(method_and_descriptor_to_implement != nullptr)
225  {
227  "produces a type with at least two unimplemented methods");
228  }
229  method_and_descriptor_to_implement = entry.first;
230  }
231  }
232 
233  if(!method_and_descriptor_to_implement)
234  {
236  "produces a type with no unimplemented methods");
237  }
238  return method_and_descriptor_to_implement;
239  }
241  {
242  log.debug() << "ignoring invokedynamic at " << method_identifier
243  << " address " << instruction_address << " with type "
244  << functional_interface_tag.get_identifier() << " which "
245  << e.message << "." << messaget::eom;
246  return {};
247  }
248 }
249 
251  const irep_idt &synthetic_class_name,
253  const struct_tag_typet &functional_interface_tag,
254  const java_method_typet &dynamic_method_type)
255 {
256  java_class_typet synthetic_class_type;
257  // Tag = name without 'java::' prefix, matching the convention used by
258  // java_bytecode_convert_class.cpp
259  synthetic_class_type.set_tag(
260  strip_java_namespace_prefix(synthetic_class_name));
261  synthetic_class_type.set_name(synthetic_class_name);
262  synthetic_class_type.set_synthetic(true);
263  synthetic_class_type.set(ID_java_lambda_method_handle, lambda_method_handle);
264  struct_tag_typet base_tag("java::java.lang.Object");
265  synthetic_class_type.add_base(base_tag);
266  synthetic_class_type.add_base(functional_interface_tag);
267 
268  // Add the class fields:
269 
270  {
271  java_class_typet::componentt base_field;
272  const irep_idt base_field_name("@java.lang.Object");
273  base_field.set_name(base_field_name);
274  base_field.set_base_name(base_field_name);
275  base_field.set_pretty_name(base_field_name);
276  base_field.set_access(ID_private);
277  base_field.type() = base_tag;
278  synthetic_class_type.components().emplace_back(std::move(base_field));
279 
280  std::size_t field_idx = 0;
281  for(const auto &param : dynamic_method_type.parameters())
282  {
283  irep_idt field_basename = "capture_" + std::to_string(field_idx++);
284 
286  new_field.set_name(field_basename);
287  new_field.set_base_name(field_basename);
288  new_field.set_pretty_name(field_basename);
289  new_field.set_access(ID_private);
290  new_field.type() = param.type();
291  synthetic_class_type.components().emplace_back(std::move(new_field));
292  }
293  }
294 
295  symbolt synthetic_class_symbol = type_symbolt{synthetic_class_type};
296  synthetic_class_symbol.name = synthetic_class_name;
297  synthetic_class_symbol.mode = ID_java;
298  return synthetic_class_symbol;
299 }
300 
302  synthetic_methods_mapt &synthetic_methods,
303  const irep_idt &synthetic_class_name,
304  java_method_typet constructor_type) // dynamic_method_type
305 {
307  irep_idt constructor_name = id2string(synthetic_class_name) + ".<init>";
308  constructor_symbol.name = constructor_name;
310  constructor_symbol.base_name = "<init>";
311  constructor_symbol.mode = ID_java;
312 
313  synthetic_methods[constructor_name] =
315 
316  constructor_type.set_is_constructor();
317  constructor_type.return_type() = empty_typet();
318 
319  size_t field_idx = 0;
320  for(auto &param : constructor_type.parameters())
321  {
322  irep_idt param_basename = "param_" + std::to_string(field_idx++);
323  param.set_base_name(param_basename);
324  param.set_identifier(
325  id2string(constructor_name) + "::" + id2string(param_basename));
326  }
327 
328  java_method_typet::parametert constructor_this_param;
329  constructor_this_param.set_this();
330  constructor_this_param.set_base_name("this");
331  constructor_this_param.set_identifier(id2string(constructor_name) + "::this");
332  constructor_this_param.type() =
333  java_reference_type(struct_tag_typet(synthetic_class_name));
334 
335  constructor_type.parameters().insert(
336  constructor_type.parameters().begin(), constructor_this_param);
337 
338  constructor_symbol.type = constructor_type;
339  set_declaring_class(constructor_symbol, synthetic_class_name);
340  return constructor_symbol;
341 }
342 
344  synthetic_methods_mapt &synthetic_methods,
345  const java_class_typet::methodt &method_to_implement,
346  const irep_idt &synthetic_class_name)
347 {
348  const std::string implemented_method_name =
349  id2string(synthetic_class_name) + "." +
350  id2string(method_to_implement.get_base_name()) + ":" +
351  id2string(method_to_implement.get_descriptor());
352 
354  implemented_method_symbol.name = implemented_method_name;
355  synthetic_methods[implemented_method_symbol.name] =
358  implemented_method_symbol.base_name = method_to_implement.get_base_name();
360  implemented_method_symbol.type = method_to_implement.type();
361  auto &implemented_method_type = to_code_type(implemented_method_symbol.type);
362  implemented_method_type.parameters()[0].type() =
363  java_reference_type(struct_tag_typet(synthetic_class_name));
364 
365  size_t field_idx = 0;
366  for(auto &param : implemented_method_type.parameters())
367  {
368  irep_idt param_basename =
369  field_idx == 0 ? "this" : "param_" + std::to_string(field_idx);
370  param.set_base_name(param_basename);
371  param.set_identifier(
372  id2string(implemented_method_name) + "::" + id2string(param_basename));
373 
374  ++field_idx;
375  }
376 
377  set_declaring_class(implemented_method_symbol, synthetic_class_name);
379 }
380 
381 // invokedynamic will be called with operands that should be stored in a
382 // synthetic object implementing the interface type that it returns. For
383 // example, "invokedynamic f(a, b, c) -> MyInterface" should result in the
384 // creation of the synthetic class:
385 // public class SyntheticCapture implements MyInterface {
386 // private int a;
387 // private float b;
388 // private Other c;
389 // public SyntheticCapture(int a, float b, Other c) {
390 // this.a = a; this.b = b; this.c = c;
391 // }
392 // public void myInterfaceMethod(int d) {
393 // f(a, b, c, d);
394 // }
395 // }
396 // This method just creates the outline; the methods will be populated on
397 // demand via java_bytecode_languaget::convert_lazy_method.
398 
399 // Check that we understand the lambda method handle; if we don't then
400 // we will not create a synthetic class at all, and the corresponding
401 // invoke instruction will return null when eventually converted by
402 // java_bytecode_convert_method.
404  const irep_idt &method_identifier,
406  symbol_tablet &symbol_table,
407  synthetic_methods_mapt &synthetic_methods,
408  message_handlert &message_handler)
409 {
410  const messaget log{message_handler};
411 
412  for(const auto &instruction : instructions)
413  {
414  if(strcmp(bytecode_info[instruction.bytecode].mnemonic, "invokedynamic"))
415  continue;
416  const auto &dynamic_method_type =
417  to_java_method_type(instruction.args.at(0).type());
418  const auto lambda_handle = lambda_method_handle(
419  symbol_table, method_identifier, dynamic_method_type);
420  if(!lambda_handle)
421  {
422  log.debug() << "ignoring invokedynamic at " << method_identifier
423  << " address " << instruction.address
424  << " with unknown handle type" << messaget::eom;
425  continue;
426  }
427  const auto &functional_interface_tag = to_struct_tag_type(
428  to_java_reference_type(dynamic_method_type.return_type()).subtype());
429  const auto unimplemented_method = try_get_unique_unimplemented_method(
430  symbol_table,
431  functional_interface_tag,
432  method_identifier,
433  instruction.address,
434  log);
435  if(!unimplemented_method)
436  continue;
437  log.debug() << "identified invokedynamic at " << method_identifier
438  << " address " << instruction.address << " for lambda: "
439  << lambda_handle->get_lambda_method_identifier()
440  << messaget::eom;
441  const irep_idt synthetic_class_name =
442  lambda_synthetic_class_name(method_identifier, instruction.address);
443  symbol_table.add(constructor_symbol(
444  synthetic_methods, synthetic_class_name, dynamic_method_type));
445  symbol_table.add(implemented_method_symbol(
446  synthetic_methods, *unimplemented_method, synthetic_class_name));
447  symbol_table.add(synthetic_class_symbol(
448  synthetic_class_name,
449  *lambda_handle,
450  functional_interface_tag,
451  dynamic_method_type));
452  }
453 }
454 
456  const irep_idt &identifier,
457  const irep_idt &base_name,
458  const irep_idt &pretty_name,
459  const typet &type,
460  const irep_idt &declaring_class,
461  symbol_table_baset &symbol_table,
462  message_handlert &log)
463 {
464  const auto *existing_symbol = symbol_table.lookup(identifier);
465  if(existing_symbol)
466  return *existing_symbol;
467 
469  identifier,
470  base_name,
471  pretty_name,
472  type,
474  symbol_table,
475  log);
476  return symbol_table.lookup_ref(identifier);
477 }
478 
480  const irep_idt &function_id,
481  symbol_table_baset &symbol_table,
482  message_handlert &message_handler)
483 {
484  code_blockt result;
485  namespacet ns(symbol_table);
486 
487  const symbolt &function_symbol = ns.lookup(function_id);
488  const auto &parameters = to_code_type(function_symbol.type).parameters();
489 
490  const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol));
491  const class_typet &class_type = to_class_type(class_symbol.type);
492 
493  const symbol_exprt this_param(
494  parameters.at(0).get_identifier(), parameters.at(0).type());
495  const dereference_exprt deref_this(this_param);
496 
497  // Call super-constructor (always java.lang.Object):
498  const irep_idt jlo("java::java.lang.Object");
499  const irep_idt jlo_constructor(id2string(jlo) + ".<init>:()V");
500  const auto jlo_reference = java_reference_type(struct_tag_typet(jlo));
501  code_typet::parametert jlo_this_param{jlo_reference};
502  jlo_this_param.set_this();
503 
504  java_method_typet jlo_constructor_type(
505  code_typet::parameterst{jlo_this_param}, empty_typet());
506  const auto &jlo_constructor_symbol = get_or_create_method_symbol(
507  jlo_constructor,
508  "<init>",
509  jlo_constructor,
510  jlo_constructor_type,
511  jlo,
512  symbol_table,
513  message_handler);
514  code_function_callt super_constructor_call(
515  jlo_constructor_symbol.symbol_expr(),
516  code_function_callt::argumentst{typecast_exprt(this_param, jlo_reference)});
517  result.add(super_constructor_call);
518 
519  // Store captured parameters:
520  auto field_iterator = std::next(class_type.components().begin());
521  for(const auto &parameter : parameters)
522  {
523  // Give the parameter its symbol:
524  parameter_symbolt param_symbol;
525  param_symbol.name = parameter.get_identifier();
526  param_symbol.base_name = parameter.get_base_name();
527  param_symbol.mode = ID_java;
528  param_symbol.type = parameter.type();
529  symbol_table.add(param_symbol);
530 
531  if(parameter.get_this())
532  continue;
533 
534  code_assignt assign_field(
535  member_exprt(deref_this, field_iterator->get_name(), parameter.type()),
536  symbol_exprt(parameter.get_identifier(), parameter.type()));
537  result.add(assign_field);
538 
539  ++field_iterator;
540  }
541 
542  return std::move(result);
543 }
544 
546  const irep_idt &function_id,
547  const irep_idt &basename,
548  const typet &type,
549  symbol_table_baset &symbol_table,
550  code_blockt &method)
551 {
552  irep_idt new_var_name = id2string(function_id) + "::" + id2string(basename);
553  auxiliary_symbolt new_instance_var_symbol;
554  new_instance_var_symbol.name = new_var_name;
555  new_instance_var_symbol.base_name = basename;
556  new_instance_var_symbol.mode = ID_java;
557  new_instance_var_symbol.type = type;
558  bool add_failed = symbol_table.add(new_instance_var_symbol);
559  POSTCONDITION(!add_failed);
560  symbol_exprt new_instance_var = new_instance_var_symbol.symbol_expr();
561  method.add(code_declt{new_instance_var});
562 
563  return new_instance_var;
564 }
565 
577  const irep_idt &function_id,
578  const symbolt &lambda_method_symbol,
579  symbol_table_baset &symbol_table,
580  code_blockt &result)
581 {
582  // We must instantiate the object, then call the requested constructor
583  const auto &method_type = to_code_type(lambda_method_symbol.type);
584  INVARIANT(
585  method_type.get_bool(ID_constructor),
586  "REF_NewInvokeSpecial lambda must refer to a constructor");
587  const auto &created_type = method_type.parameters().at(0).type();
588  irep_idt created_class =
589  to_struct_tag_type(created_type.subtype()).get_identifier();
590 
591  // Call static init if it exists:
592  irep_idt static_init_name = clinit_wrapper_name(created_class);
593  if(const auto *static_init_symbol = symbol_table.lookup(static_init_name))
594  {
595  result.add(code_function_callt{static_init_symbol->symbol_expr(), {}});
596  }
597 
598  // Make a local to hold the new instance:
599  symbol_exprt new_instance_var = create_and_declare_local(
600  function_id,
601  "newinvokespecial_instance",
602  created_type,
603  symbol_table,
604  result);
605 
606  // Instantiate the object:
607  side_effect_exprt java_new_expr(ID_java_new, created_type, {});
608  result.add(code_assignt{new_instance_var, java_new_expr});
609 
610  return new_instance_var;
611 }
612 
615 static optionalt<irep_idt> get_unboxing_method(const typet &maybe_boxed_type)
616 {
617  const irep_idt &boxed_type_id =
618  to_struct_tag_type(maybe_boxed_type.subtype()).get_identifier();
619  const java_boxed_type_infot *boxed_type_info =
620  get_boxed_type_info_by_name(boxed_type_id);
621  return boxed_type_info ? boxed_type_info->unboxing_function_name
623 }
624 
629  const symbolt &function_symbol,
630  const symbol_tablet &symbol_table)
631 {
632  const auto &method_type = to_java_method_type(function_symbol.type);
633  if(!method_type.has_this())
634  return function_symbol.symbol_expr();
635  const irep_idt &declared_on_class_id =
636  to_struct_tag_type(method_type.get_this()->type().subtype())
637  .get_identifier();
638  const auto &this_symbol = symbol_table.lookup_ref(declared_on_class_id);
639  if(to_java_class_type(this_symbol.type).get_final())
640  return function_symbol.symbol_expr();
641 
642  // Neither final nor static; make a class_method_descriptor_exprt that will
643  // trigger remove_virtual_functions to produce a virtual dispatch table:
644 
645  const std::string &function_name = id2string(function_symbol.name);
646  const auto method_name_start_idx = function_name.rfind('.');
647  const irep_idt mangled_method_name =
648  function_name.substr(method_name_start_idx + 1);
649 
650  return class_method_descriptor_exprt{function_symbol.type,
651  mangled_method_name,
652  declared_on_class_id,
653  function_symbol.base_name};
654 }
655 
686  exprt expr,
687  const typet &required_type,
688  code_blockt &code_block,
689  symbol_table_baset &symbol_table,
690  const irep_idt &function_id,
691  const std::string &role)
692 {
693  const typet &original_type = expr.type();
694  const bool original_is_pointer = can_cast_type<pointer_typet>(original_type);
695  const bool required_is_pointer = can_cast_type<pointer_typet>(required_type);
696 
697  if(original_is_pointer == required_is_pointer)
698  {
699  return expr;
700  }
701 
702  // One is a pointer, the other a primitive -- box or unbox as necessary, and
703  // check the types are consistent:
704 
705  const auto *primitive_type_info = get_java_primitive_type_info(
706  original_is_pointer ? required_type : original_type);
707  INVARIANT(
708  primitive_type_info != nullptr,
709  "A Java non-pointer type involved in a type disagreement should"
710  " be a primitive");
711 
712  const irep_idt fresh_local_name =
713  role + (original_is_pointer ? "_unboxed" : "_boxed");
714 
715  const symbol_exprt fresh_local = create_and_declare_local(
716  function_id, fresh_local_name, required_type, symbol_table, code_block);
717 
718  const irep_idt transform_function_id =
719  original_is_pointer
720  ? get_unboxing_method(original_type) // Use static type if known
721  .value_or(primitive_type_info->unboxing_function_name)
722  : primitive_type_info->boxed_type_factory_method;
723 
724  const symbolt &transform_function_symbol =
725  symbol_table.lookup_ref(transform_function_id);
726 
727  const typet &transform_function_param_type =
728  to_code_type(transform_function_symbol.type).parameters()[0].type();
729  const exprt cast_expr =
730  typecast_exprt::conditional_cast(expr, transform_function_param_type);
731 
732  code_block.add(code_function_callt{
733  fresh_local,
734  make_function_expr(transform_function_symbol, symbol_table),
735  {expr}});
736 
737  return std::move(fresh_local);
738 }
739 
744  exprt expr,
745  const typet &required_type,
746  code_blockt &code_block,
747  symbol_table_baset &symbol_table,
748  const irep_idt &function_id,
749  const std::string &role)
750 {
753  expr, required_type, code_block, symbol_table, function_id, role),
754  required_type);
755 }
756 
774  const irep_idt &function_id,
775  symbol_table_baset &symbol_table,
776  message_handlert &message_handler)
777 {
778  // Call the bound method with the capture parameters, then the actual
779  // parameters. Note one of the capture params might be the `this` parameter
780  // of a virtual call -- that depends on whether the callee is a static or an
781  // instance method.
782 
783  code_blockt result;
784  namespacet ns(symbol_table);
785 
786  const symbolt &function_symbol = ns.lookup(function_id);
787  const auto &function_type = to_code_type(function_symbol.type);
788  const auto &parameters = function_type.parameters();
789 
790  const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol));
791  const java_class_typet &class_type = to_java_class_type(class_symbol.type);
792 
793  const symbol_exprt this_param(
794  parameters.at(0).get_identifier(), parameters.at(0).type());
795  const dereference_exprt deref_this(this_param);
796 
797  code_function_callt::argumentst lambda_method_args;
798  for(const auto &field : class_type.components())
799  {
800  if(field.get_name() == "@java.lang.Object")
801  continue;
802  lambda_method_args.push_back(
803  member_exprt(deref_this, field.get_name(), field.type()));
804  }
805 
806  for(const auto &parameter : parameters)
807  {
808  // Give the parameter its symbol:
809  parameter_symbolt param_symbol;
810  param_symbol.name = parameter.get_identifier();
811  param_symbol.base_name = parameter.get_base_name();
812  param_symbol.mode = ID_java;
813  param_symbol.type = parameter.type();
814  symbol_table.add(param_symbol);
815 
816  if(parameter.get_this())
817  continue;
818 
819  lambda_method_args.push_back(param_symbol.symbol_expr());
820  }
821 
822  const auto &lambda_method_handle =
824  class_type.find(ID_java_lambda_method_handle));
825 
826  const auto &lambda_method_symbol =
827  ns.lookup(lambda_method_handle.get_lambda_method_identifier());
828  const auto handle_type = lambda_method_handle.get_handle_kind();
829  const auto is_constructor_lambda =
830  handle_type ==
832  const auto use_virtual_dispatch =
833  handle_type ==
835 
836  if(is_constructor_lambda)
837  {
838  auto new_instance_var = instantiate_new_object(
839  function_id, lambda_method_symbol, symbol_table, result);
840 
841  // Prepend the newly created object to the lambda arg list:
842  lambda_method_args.insert(lambda_method_args.begin(), new_instance_var);
843  }
844 
845  const auto &lambda_method_descriptor =
846  lambda_method_handle.get_lambda_method_descriptor();
847  exprt callee;
848  if(use_virtual_dispatch)
849  callee = lambda_method_descriptor;
850  else
851  callee = lambda_method_symbol.symbol_expr();
852 
853  // Adjust boxing if required:
854  const code_typet &callee_type = to_code_type(lambda_method_symbol.type);
855  const auto &callee_parameters = callee_type.parameters();
856  const auto &callee_return_type = callee_type.return_type();
857  INVARIANT(
858  callee_parameters.size() == lambda_method_args.size(),
859  "should have args for every parameter");
860  for(unsigned i = 0; i < callee_parameters.size(); ++i)
861  {
862  lambda_method_args[i] = adjust_type_if_necessary(
863  std::move(lambda_method_args[i]),
864  callee_parameters[i].type(),
865  result,
866  symbol_table,
867  function_id,
868  "param" + std::to_string(i));
869  }
870 
871  if(function_type.return_type() != empty_typet() && !is_constructor_lambda)
872  {
873  symbol_exprt result_local = create_and_declare_local(
874  function_id, "return_value", callee_return_type, symbol_table, result);
875  result.add(code_function_callt(result_local, callee, lambda_method_args));
876  exprt adjusted_local = adjust_type_if_necessary(
877  result_local,
878  function_type.return_type(),
879  result,
880  symbol_table,
881  function_id,
882  "retval");
883  result.add(code_returnt{adjusted_local});
884  }
885  else
886  {
887  result.add(code_function_callt(callee, lambda_method_args));
888  }
889 
890  if(is_constructor_lambda)
891  {
892  // Return the newly-created object.
894  lambda_method_args.at(0), function_type.return_type())});
895  }
896 
897  return std::move(result);
898 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
irept::get_int
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:69
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
java_class_typet::componentt
Definition: java_types.h:202
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
class_typet
Class type.
Definition: std_types.h:320
invokedynamic_synthetic_method
codet invokedynamic_synthetic_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create the body for the synthetic method implementing an invokedynamic method.
Definition: lambda_synthesis.cpp:773
bytecode_infot::mnemonic
const char * mnemonic
Definition: bytecode_info.h:46
java_class_typet::method_handle_kindt::LAMBDA_VIRTUAL_METHOD_HANDLE
@ LAMBDA_VIRTUAL_METHOD_HANDLE
Virtual call to the given interface or method.
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:89
java_class_typet::set_synthetic
void set_synthetic(bool synthetic)
marks class synthetic
Definition: java_types.h:436
set_declaring_class
void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
Sets the identifier of the class which declared a given symbol to declaring_class.
Definition: java_utils.cpp:585
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
java_bytecode_parse_treet::methodt::instructionst
std::vector< instructiont > instructionst
Definition: java_bytecode_parse_tree.h:92
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:376
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
compare_base_name_and_descriptort
Definition: lambda_synthesis.cpp:106
lambda_method_handle
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)
Definition: lambda_synthesis.cpp:77
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:782
struct_typet::add_base
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition: std_types.cpp:88
get_interface_methods
static const methods_by_name_and_descriptort get_interface_methods(const irep_idt &interface_id, const namespacet &ns)
Find all methods defined by this method and its parent types, returned as a map from const java_class...
Definition: lambda_synthesis.cpp:135
create_invokedynamic_synthetic_classes
void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)
Definition: lambda_synthesis.cpp:403
declaring_class
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
Definition: java_utils.cpp:579
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
java_class_typet::methodt
Definition: java_types.h:243
get_unboxing_method
static optionalt< irep_idt > get_unboxing_method(const typet &maybe_boxed_type)
If maybe_boxed_type is a boxed primitive return its unboxing method; otherwise return empty.
Definition: lambda_synthesis.cpp:615
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
@ INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
A generated constructor for a class capturing the parameters of an invokedynamic instruction.
synthetic_method_typet::INVOKEDYNAMIC_METHOD
@ INVOKEDYNAMIC_METHOD
A generated method for a class capturing the parameters of an invokedynamic instruction.
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
no_unique_unimplemented_method_exceptiont::message
const std::string message
Definition: lambda_synthesis.cpp:102
create_and_declare_local
static symbol_exprt create_and_declare_local(const irep_idt &function_id, const irep_idt &basename, const typet &type, symbol_table_baset &symbol_table, code_blockt &method)
Definition: lambda_synthesis.cpp:545
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:160
synthetic_methods_mapt
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Definition: synthetic_methods_map.h:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
java_class_typet
Definition: java_types.h:199
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4508
java_class_typet::java_lambda_method_handlet
Represents a lambda call to a method.
Definition: java_types.h:484
strip_java_namespace_prefix
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
Definition: java_utils.cpp:417
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
methods_by_name_and_descriptort
std::map< const java_class_typet::methodt *, bool, compare_base_name_and_descriptort > methods_by_name_and_descriptort
Map from method, indexed by name and descriptor but not defining class, onto defined-ness (i....
Definition: lambda_synthesis.cpp:125
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
java_class_typet::methodt::type
const java_method_typet & type() const
Definition: java_types.h:252
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
java_boxed_type_infot
Return type for get_boxed_type_info_by_name.
Definition: java_utils.h:57
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
java_reference_typet::subtype
struct_tag_typet & subtype()
Definition: java_types.h:614
empty_typet
The empty type.
Definition: std_types.h:46
no_unique_unimplemented_method_exceptiont::no_unique_unimplemented_method_exceptiont
no_unique_unimplemented_method_exceptiont(const std::string &s)
Definition: lambda_synthesis.cpp:98
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
struct_union_typet::set_tag
void set_tag(const irep_idt &tag)
Definition: std_types.h:164
java_class_typet::java_lambda_method_handlest
std::vector< java_lambda_method_handlet > java_lambda_method_handlest
Definition: java_types.h:517
code_typet::set_is_constructor
void set_is_constructor()
Definition: std_types.h:892
java_bytecode_parse_tree.h
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
to_java_reference_type
const java_reference_typet & to_java_reference_type(const typet &type)
Definition: java_types.h:632
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
java_class_typet::method_handle_kindt::LAMBDA_CONSTRUCTOR_HANDLE
@ LAMBDA_CONSTRUCTOR_HANDLE
Instantiate the needed type then call a constructor.
synthetic_class_symbol
symbolt synthetic_class_symbol(const irep_idt &synthetic_class_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)
Definition: lambda_synthesis.cpp:250
code_typet
Base type of functions.
Definition: std_types.h:736
message_handlert
Definition: message.h:28
create_method_stub_symbol
void create_method_stub_symbol(const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, const typet &type, const irep_idt &declaring_class, symbol_table_baset &symbol_table, message_handlert &message_handler)
Definition: java_bytecode_convert_method.cpp:99
java_bytecode_convert_method.h
JAVA Bytecode Language Conversion.
java_class_typet::method_handle_kindt::UNKNOWN_HANDLE
@ UNKNOWN_HANDLE
Can't be called.
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
java_class_typet::get_final
bool get_final() const
Definition: java_types.h:385
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
try_get_unique_unimplemented_method
static const java_class_typet::methodt * try_get_unique_unimplemented_method(const symbol_tablet &symbol_table, const struct_tag_typet &functional_interface_tag, const irep_idt &method_identifier, const int instruction_address, const messaget &log)
Definition: lambda_synthesis.cpp:204
escape_symbol_special_chars
static std::string escape_symbol_special_chars(std::string input)
Definition: lambda_synthesis.cpp:27
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:787
box_or_unbox_type_if_necessary
exprt box_or_unbox_type_if_necessary(exprt expr, const typet &required_type, code_blockt &code_block, symbol_table_baset &symbol_table, const irep_idt &function_id, const std::string &role)
If expr needs (un)boxing to satisfy required_type, add the required symbols to symbol_table and code ...
Definition: lambda_synthesis.cpp:685
code_typet::parametert::set_this
void set_this()
Definition: std_types.h:807
no_unique_unimplemented_method_exceptiont
Definition: lambda_synthesis.cpp:96
invokedynamic_synthetic_constructor
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
Definition: lambda_synthesis.cpp:479
adjust_type_if_necessary
exprt adjust_type_if_necessary(exprt expr, const typet &required_type, code_blockt &code_block, symbol_table_baset &symbol_table, const irep_idt &function_id, const std::string &role)
Box or unbox expr as per box_or_unbox_type_if_necessary, then cast the result to required_type.
Definition: lambda_synthesis.cpp:743
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: std_types.h:1513
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
lambda_synthesis.h
Java lambda code synthesis.
java_class_typet::components
const componentst & components() const
Definition: java_types.h:226
java_class_typet::methodt::get_descriptor
const irep_idt & get_descriptor() const
Gets the method's descriptor – the mangled form of its type.
Definition: java_types.h:288
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
make_function_expr
exprt make_function_expr(const symbolt &function_symbol, const symbol_tablet &symbol_table)
Produce a class_method_descriptor_exprt or symbol_exprt for function_symbol depending on whether virt...
Definition: lambda_synthesis.cpp:628
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
compare_base_name_and_descriptort::operator()
int operator()(const java_class_typet::methodt *a, const java_class_typet::methodt *b) const
Definition: lambda_synthesis.cpp:107
code_typet::parametert
Definition: std_types.h:753
java_class_typet::set_name
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
Definition: java_types.h:566
type_symbolt
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:146
clinit_wrapper_name
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
Definition: java_static_initializers.cpp:65
java_boxed_type_infot::unboxing_function_name
const irep_idt unboxing_function_name
Name of the function defined on the boxed type that returns the boxed value.
Definition: java_utils.h:60
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
constructor_symbol
static symbolt constructor_symbol(synthetic_methods_mapt &synthetic_methods, const irep_idt &synthetic_class_name, java_method_typet constructor_type)
Definition: lambda_synthesis.cpp:301
get_or_create_method_symbol
static const symbolt & get_or_create_method_symbol(const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, const typet &type, const irep_idt &declaring_class, symbol_table_baset &symbol_table, message_handlert &log)
Definition: lambda_synthesis.cpp:455
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
messaget::debug
mstreamt & debug() const
Definition: message.h:429
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:184
get_boxed_type_info_by_name
const java_boxed_type_infot * get_boxed_type_info_by_name(const irep_idt &type_name)
If type_name is a Java boxed type tag, return information about it, otherwise return null.
Definition: java_utils.cpp:42
java_types.h
instantiate_new_object
static symbol_exprt instantiate_new_object(const irep_idt &function_id, const symbolt &lambda_method_symbol, symbol_table_baset &symbol_table, code_blockt &result)
Instantiates an object suitable for calling a given constructor (but does not actually call it).
Definition: lambda_synthesis.cpp:576
get_lambda_method_handle
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)
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap m...
Definition: lambda_synthesis.cpp:55
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
symbol_table.h
Author: Diffblue Ltd.
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition: bytecode_info.cpp:16
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
implemented_method_symbol
static symbolt implemented_method_symbol(synthetic_methods_mapt &synthetic_methods, const java_class_typet::methodt &method_to_implement, const irep_idt &synthetic_class_name)
Definition: lambda_synthesis.cpp:343
java_utils.h
java_method_typet
Definition: java_types.h:103
lambda_synthetic_class_name
irep_idt lambda_synthetic_class_name(const irep_idt &method_identifier, std::size_t instruction_address)
Definition: lambda_synthesis.cpp:37
get_java_primitive_type_info
const java_primitive_type_infot * get_java_primitive_type_info(const typet &maybe_primitive_type)
If primitive_type is a Java primitive type, return information about it, otherwise return null.
Definition: java_utils.cpp:69
synthetic_methods_map.h
Synthetic methods are particular methods internally generated by the Java frontend,...
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
validation_modet::INVARIANT
@ INVARIANT
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35