cprover
Loading...
Searching...
No Matches
lambda_synthesis.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java lambda code synthesis
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
12#include "lambda_synthesis.h"
13
14#include <util/message.h>
15#include <util/namespace.h>
17
21#include "java_types.h"
22#include "java_utils.h"
24
25#include <string.h>
26
27static 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() !=
73 return {};
74}
75
78 const symbol_table_baset &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
95class no_unique_unimplemented_method_exceptiont : public std::exception
96{
97public:
98 explicit no_unique_unimplemented_method_exceptiont(const std::string &s)
99 : message(s)
100 {
101 }
102 const std::string message;
103};
104
106{
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
121typedef std::map<
123 bool,
126
135get_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_table_baset &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 {
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 return type_symbolt{synthetic_class_name, synthetic_class_type, ID_java};
296}
297
299 synthetic_methods_mapt &synthetic_methods,
300 const irep_idt &synthetic_class_name,
301 java_method_typet constructor_type) // dynamic_method_type
302{
303 irep_idt constructor_name = id2string(synthetic_class_name) + ".<init>";
304 symbolt constructor_symbol{constructor_name, typet{}, ID_java};
306 constructor_symbol.base_name = "<init>";
307
308 synthetic_methods[constructor_name] =
310
311 constructor_type.set_is_constructor();
312 constructor_type.return_type() = empty_typet();
313
314 size_t field_idx = 0;
315 for(auto &param : constructor_type.parameters())
316 {
317 irep_idt param_basename = "param_" + std::to_string(field_idx++);
318 param.set_base_name(param_basename);
319 param.set_identifier(
320 id2string(constructor_name) + "::" + id2string(param_basename));
321 }
322
323 java_method_typet::parametert constructor_this_param(
324 java_reference_type(struct_tag_typet(synthetic_class_name)));
325 constructor_this_param.set_this();
326 constructor_this_param.set_base_name("this");
327 constructor_this_param.set_identifier(id2string(constructor_name) + "::this");
328
329 constructor_type.parameters().insert(
330 constructor_type.parameters().begin(), constructor_this_param);
331
332 constructor_symbol.type = constructor_type;
333 set_declaring_class(constructor_symbol, synthetic_class_name);
334 return constructor_symbol;
335}
336
338 synthetic_methods_mapt &synthetic_methods,
339 const java_class_typet::methodt &method_to_implement,
340 const irep_idt &synthetic_class_name)
341{
342 const std::string implemented_method_name =
343 id2string(synthetic_class_name) + "." +
344 id2string(method_to_implement.get_base_name()) + ":" +
345 id2string(method_to_implement.get_descriptor());
346
348 implemented_method_name, method_to_implement.type(), ID_java};
349 synthetic_methods[implemented_method_symbol.name] =
352 implemented_method_symbol.base_name = method_to_implement.get_base_name();
353 auto &implemented_method_type = to_code_type(implemented_method_symbol.type);
354 implemented_method_type.parameters()[0].type() =
355 java_reference_type(struct_tag_typet(synthetic_class_name));
356
357 size_t field_idx = 0;
358 for(auto &param : implemented_method_type.parameters())
359 {
360 irep_idt param_basename =
361 field_idx == 0 ? "this" : "param_" + std::to_string(field_idx);
362 param.set_base_name(param_basename);
363 param.set_identifier(
364 id2string(implemented_method_name) + "::" + id2string(param_basename));
365
366 ++field_idx;
367 }
368
369 set_declaring_class(implemented_method_symbol, synthetic_class_name);
371}
372
373// invokedynamic will be called with operands that should be stored in a
374// synthetic object implementing the interface type that it returns. For
375// example, "invokedynamic f(a, b, c) -> MyInterface" should result in the
376// creation of the synthetic class:
377// public class SyntheticCapture implements MyInterface {
378// private int a;
379// private float b;
380// private Other c;
381// public SyntheticCapture(int a, float b, Other c) {
382// this.a = a; this.b = b; this.c = c;
383// }
384// public void myInterfaceMethod(int d) {
385// f(a, b, c, d);
386// }
387// }
388// This method just creates the outline; the methods will be populated on
389// demand via java_bytecode_languaget::convert_lazy_method.
390
391// Check that we understand the lambda method handle; if we don't then
392// we will not create a synthetic class at all, and the corresponding
393// invoke instruction will return null when eventually converted by
394// java_bytecode_convert_method.
396 const irep_idt &method_identifier,
398 symbol_table_baset &symbol_table,
399 synthetic_methods_mapt &synthetic_methods,
400 message_handlert &message_handler)
401{
402 const messaget log{message_handler};
403
404 for(const auto &instruction : instructions)
405 {
406 if(strcmp(bytecode_info[instruction.bytecode].mnemonic, "invokedynamic"))
407 continue;
408 const auto &dynamic_method_type =
409 to_java_method_type(instruction.args.at(0).type());
410 const auto lambda_handle = lambda_method_handle(
411 symbol_table, method_identifier, dynamic_method_type);
412 if(!lambda_handle)
413 {
414 log.debug() << "ignoring invokedynamic at " << method_identifier
415 << " address " << instruction.address
416 << " with unknown handle type" << messaget::eom;
417 continue;
418 }
419 const auto &functional_interface_tag = to_struct_tag_type(
420 to_java_reference_type(dynamic_method_type.return_type()).subtype());
421 const auto unimplemented_method = try_get_unique_unimplemented_method(
422 symbol_table,
423 functional_interface_tag,
424 method_identifier,
425 instruction.address,
426 log);
427 if(!unimplemented_method)
428 continue;
429 log.debug() << "identified invokedynamic at " << method_identifier
430 << " address " << instruction.address << " for lambda: "
431 << lambda_handle->get_lambda_method_identifier()
432 << messaget::eom;
433 const irep_idt synthetic_class_name =
434 lambda_synthetic_class_name(method_identifier, instruction.address);
435 symbol_table.add(constructor_symbol(
436 synthetic_methods, synthetic_class_name, dynamic_method_type));
437 symbol_table.add(implemented_method_symbol(
438 synthetic_methods, *unimplemented_method, synthetic_class_name));
439 symbol_table.add(synthetic_class_symbol(
440 synthetic_class_name,
441 *lambda_handle,
442 functional_interface_tag,
443 dynamic_method_type));
444 }
445}
446
448 const irep_idt &identifier,
449 const irep_idt &base_name,
450 const irep_idt &pretty_name,
451 const typet &type,
453 symbol_table_baset &symbol_table,
454 message_handlert &log)
455{
456 const auto *existing_symbol = symbol_table.lookup(identifier);
457 if(existing_symbol)
458 return *existing_symbol;
459
461 identifier,
462 base_name,
463 pretty_name,
464 type,
466 symbol_table,
467 log);
468 return symbol_table.lookup_ref(identifier);
469}
470
472 const irep_idt &function_id,
473 symbol_table_baset &symbol_table,
474 message_handlert &message_handler)
475{
476 code_blockt result;
477 namespacet ns(symbol_table);
478
479 const symbolt &function_symbol = ns.lookup(function_id);
480 const auto &parameters = to_code_type(function_symbol.type).parameters();
481
482 const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol));
483 const class_typet &class_type = to_class_type(class_symbol.type);
484
485 const symbol_exprt this_param(
486 parameters.at(0).get_identifier(), parameters.at(0).type());
487 const dereference_exprt deref_this(this_param);
488
489 // Call super-constructor (always java.lang.Object):
490 const irep_idt jlo("java::java.lang.Object");
491 const irep_idt jlo_constructor(id2string(jlo) + ".<init>:()V");
492 const auto jlo_reference = java_reference_type(struct_tag_typet(jlo));
493 code_typet::parametert jlo_this_param{jlo_reference};
494 jlo_this_param.set_this();
495
496 java_method_typet jlo_constructor_type(
497 code_typet::parameterst{jlo_this_param}, empty_typet());
498 const auto &jlo_constructor_symbol = get_or_create_method_symbol(
499 jlo_constructor,
500 "<init>",
501 jlo_constructor,
502 jlo_constructor_type,
503 jlo,
504 symbol_table,
505 message_handler);
506 code_function_callt super_constructor_call(
507 jlo_constructor_symbol.symbol_expr(),
508 code_function_callt::argumentst{typecast_exprt(this_param, jlo_reference)});
509 result.add(super_constructor_call);
510
511 // Store captured parameters:
512 auto field_iterator = std::next(class_type.components().begin());
513 for(const auto &parameter : parameters)
514 {
515 // Give the parameter its symbol:
516 parameter_symbolt param_symbol;
517 param_symbol.name = parameter.get_identifier();
518 param_symbol.base_name = parameter.get_base_name();
519 param_symbol.mode = ID_java;
520 param_symbol.type = parameter.type();
521 symbol_table.add(param_symbol);
522
523 if(parameter.get_this())
524 continue;
525
526 code_frontend_assignt assign_field(
527 member_exprt(deref_this, field_iterator->get_name(), parameter.type()),
528 symbol_exprt(parameter.get_identifier(), parameter.type()));
529 result.add(assign_field);
530
531 ++field_iterator;
532 }
533
534 return std::move(result);
535}
536
538 const irep_idt &function_id,
539 const irep_idt &basename,
540 const typet &type,
541 symbol_table_baset &symbol_table,
542 code_blockt &method)
543{
544 irep_idt new_var_name = id2string(function_id) + "::" + id2string(basename);
545 auxiliary_symbolt new_instance_var_symbol;
546 new_instance_var_symbol.name = new_var_name;
547 new_instance_var_symbol.base_name = basename;
548 new_instance_var_symbol.mode = ID_java;
549 new_instance_var_symbol.type = type;
550 bool add_failed = symbol_table.add(new_instance_var_symbol);
551 POSTCONDITION(!add_failed);
552 symbol_exprt new_instance_var = new_instance_var_symbol.symbol_expr();
553 method.add(code_declt{new_instance_var});
554
555 return new_instance_var;
556}
557
569 const irep_idt &function_id,
570 const symbolt &lambda_method_symbol,
571 symbol_table_baset &symbol_table,
572 code_blockt &result)
573{
574 // We must instantiate the object, then call the requested constructor
575 const auto &method_type = to_code_type(lambda_method_symbol.type);
576 INVARIANT(
577 method_type.get_bool(ID_constructor),
578 "REF_NewInvokeSpecial lambda must refer to a constructor");
579 const auto &created_type = method_type.parameters().at(0).type();
580 irep_idt created_class =
581 to_struct_tag_type(to_reference_type(created_type).base_type())
583
584 // Call static init if it exists:
585 irep_idt static_init_name = clinit_wrapper_name(created_class);
586 if(const auto *static_init_symbol = symbol_table.lookup(static_init_name))
587 {
588 result.add(code_function_callt{static_init_symbol->symbol_expr(), {}});
589 }
590
591 // Make a local to hold the new instance:
592 symbol_exprt new_instance_var = create_and_declare_local(
593 function_id,
594 "newinvokespecial_instance",
595 created_type,
596 symbol_table,
597 result);
598
599 // Instantiate the object:
600 side_effect_exprt java_new_expr(ID_java_new, created_type, {});
601 result.add(code_frontend_assignt{new_instance_var, java_new_expr});
602
603 return new_instance_var;
604}
605
609get_unboxing_method(const pointer_typet &maybe_boxed_type)
610{
611 const irep_idt &boxed_type_id =
612 to_struct_tag_type(maybe_boxed_type.base_type()).get_identifier();
613 const java_boxed_type_infot *boxed_type_info =
614 get_boxed_type_info_by_name(boxed_type_id);
615 return boxed_type_info ? boxed_type_info->unboxing_function_name
617}
618
623 const symbolt &function_symbol,
624 const symbol_table_baset &symbol_table)
625{
626 const auto &method_type = to_java_method_type(function_symbol.type);
627 if(!method_type.has_this())
628 return function_symbol.symbol_expr();
629 const irep_idt &declared_on_class_id =
631 to_pointer_type(method_type.get_this()->type()).base_type())
633 const auto &this_symbol = symbol_table.lookup_ref(declared_on_class_id);
634 if(to_java_class_type(this_symbol.type).get_final())
635 return function_symbol.symbol_expr();
636
637 // Neither final nor static; make a class_method_descriptor_exprt that will
638 // trigger remove_virtual_functions to produce a virtual dispatch table:
639
640 const std::string &function_name = id2string(function_symbol.name);
641 const auto method_name_start_idx = function_name.rfind('.');
642 const irep_idt mangled_method_name =
643 function_name.substr(method_name_start_idx + 1);
644
645 return class_method_descriptor_exprt{function_symbol.type,
646 mangled_method_name,
647 declared_on_class_id,
648 function_symbol.base_name};
649}
650
681 exprt expr,
682 const typet &required_type,
683 code_blockt &code_block,
684 symbol_table_baset &symbol_table,
685 const irep_idt &function_id,
686 const std::string &role)
687{
688 const typet &original_type = expr.type();
689 const bool original_is_pointer = can_cast_type<pointer_typet>(original_type);
690 const bool required_is_pointer = can_cast_type<pointer_typet>(required_type);
691
692 if(original_is_pointer == required_is_pointer)
693 {
694 return expr;
695 }
696
697 // One is a pointer, the other a primitive -- box or unbox as necessary, and
698 // check the types are consistent:
699
700 const auto *primitive_type_info = get_java_primitive_type_info(
701 original_is_pointer ? required_type : original_type);
702 INVARIANT(
703 primitive_type_info != nullptr,
704 "A Java non-pointer type involved in a type disagreement should"
705 " be a primitive");
706
707 const irep_idt fresh_local_name =
708 role + (original_is_pointer ? "_unboxed" : "_boxed");
709
710 const symbol_exprt fresh_local = create_and_declare_local(
711 function_id, fresh_local_name, required_type, symbol_table, code_block);
712
713 const irep_idt transform_function_id =
714 original_is_pointer
716 to_pointer_type(original_type)) // Use static type if known
717 .value_or(primitive_type_info->unboxing_function_name)
718 : primitive_type_info->boxed_type_factory_method;
719
720 const symbolt &transform_function_symbol =
721 symbol_table.lookup_ref(transform_function_id);
722
723 const typet &transform_function_param_type =
724 to_code_type(transform_function_symbol.type).parameters()[0].type();
725 const exprt cast_expr =
726 typecast_exprt::conditional_cast(expr, transform_function_param_type);
727
728 code_block.add(code_function_callt{
729 fresh_local,
730 make_function_expr(transform_function_symbol, symbol_table),
731 {expr}});
732
733 return std::move(fresh_local);
734}
735
740 exprt expr,
741 const typet &required_type,
742 code_blockt &code_block,
743 symbol_table_baset &symbol_table,
744 const irep_idt &function_id,
745 const std::string &role)
746{
749 expr, required_type, code_block, symbol_table, function_id, role),
750 required_type);
751}
752
770 const irep_idt &function_id,
771 symbol_table_baset &symbol_table,
772 message_handlert &message_handler)
773{
774 // Call the bound method with the capture parameters, then the actual
775 // parameters. Note one of the capture params might be the `this` parameter
776 // of a virtual call -- that depends on whether the callee is a static or an
777 // instance method.
778
779 code_blockt result;
780 namespacet ns(symbol_table);
781
782 const symbolt &function_symbol = ns.lookup(function_id);
783 const auto &function_type = to_code_type(function_symbol.type);
784 const auto &parameters = function_type.parameters();
785
786 const symbolt &class_symbol = ns.lookup(*declaring_class(function_symbol));
787 const java_class_typet &class_type = to_java_class_type(class_symbol.type);
788
789 const symbol_exprt this_param(
790 parameters.at(0).get_identifier(), parameters.at(0).type());
791 const dereference_exprt deref_this(this_param);
792
793 code_function_callt::argumentst lambda_method_args;
794 for(const auto &field : class_type.components())
795 {
796 if(field.get_name() == "@java.lang.Object")
797 continue;
798 lambda_method_args.push_back(
799 member_exprt(deref_this, field.get_name(), field.type()));
800 }
801
802 for(const auto &parameter : parameters)
803 {
804 // Give the parameter its symbol:
805 parameter_symbolt param_symbol;
806 param_symbol.name = parameter.get_identifier();
807 param_symbol.base_name = parameter.get_base_name();
808 param_symbol.mode = ID_java;
809 param_symbol.type = parameter.type();
810 symbol_table.add(param_symbol);
811
812 if(parameter.get_this())
813 continue;
814
815 lambda_method_args.push_back(param_symbol.symbol_expr());
816 }
817
818 const auto &lambda_method_handle =
820 class_type.find(ID_java_lambda_method_handle));
821
822 const auto &lambda_method_symbol =
823 ns.lookup(lambda_method_handle.get_lambda_method_identifier());
824 const auto handle_type = lambda_method_handle.get_handle_kind();
825 const auto is_constructor_lambda =
826 handle_type ==
828 const auto use_virtual_dispatch =
829 handle_type ==
831
832 if(is_constructor_lambda)
833 {
834 auto new_instance_var = instantiate_new_object(
835 function_id, lambda_method_symbol, symbol_table, result);
836
837 // Prepend the newly created object to the lambda arg list:
838 lambda_method_args.insert(lambda_method_args.begin(), new_instance_var);
839 }
840
841 const auto &lambda_method_descriptor =
842 lambda_method_handle.get_lambda_method_descriptor();
843 exprt callee;
844 if(use_virtual_dispatch)
845 callee = lambda_method_descriptor;
846 else
847 callee = lambda_method_symbol.symbol_expr();
848
849 // Adjust boxing if required:
850 const code_typet &callee_type = to_code_type(lambda_method_symbol.type);
851 const auto &callee_parameters = callee_type.parameters();
852 const auto &callee_return_type = callee_type.return_type();
853 INVARIANT(
854 callee_parameters.size() == lambda_method_args.size(),
855 "should have args for every parameter");
856 for(unsigned i = 0; i < callee_parameters.size(); ++i)
857 {
858 lambda_method_args[i] = adjust_type_if_necessary(
859 std::move(lambda_method_args[i]),
860 callee_parameters[i].type(),
861 result,
862 symbol_table,
863 function_id,
864 "param" + std::to_string(i));
865 }
866
867 if(function_type.return_type() != empty_typet() && !is_constructor_lambda)
868 {
870 function_id, "return_value", callee_return_type, symbol_table, result);
871 result.add(code_function_callt(result_local, callee, lambda_method_args));
872 exprt adjusted_local = adjust_type_if_necessary(
873 result_local,
874 function_type.return_type(),
875 result,
876 symbol_table,
877 function_id,
878 "retval");
879 result.add(code_returnt{adjusted_local});
880 }
881 else
882 {
883 result.add(code_function_callt(callee, lambda_method_args));
884 }
885
886 if(is_constructor_lambda)
887 {
888 // Return the newly-created object.
890 lambda_method_args.at(0), function_type.return_type())});
891 }
892
893 return std::move(result);
894}
struct bytecode_infot const bytecode_info[]
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:153
An expression describing a method on a class.
Definition std_expr.h:3448
Class type.
Definition std_types.h:325
A codet representing sequential composition of program statements.
Definition std_code.h:130
void add(const codet &code)
Definition std_code.h:168
A goto_instruction_codet representing the declaration of a local variable.
A codet representing an assignment in the program.
Definition std_code.h:24
goto_instruction_codet representation of a function call statement.
goto_instruction_codet representation of a "return from afunction" statement.
void set_base_name(const irep_idt &name)
Definition std_types.h:585
void set_identifier(const irep_idt &identifier)
Definition std_types.h:580
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
void set_is_constructor()
Definition std_types.h:690
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
Data structure for representing an arbitrary statement in a program.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
signed int get_int(const irep_idt &name) const
Definition irep.cpp:62
Represents a lambda call to a method.
Definition java_types.h:482
const java_method_typet & type() const
Definition java_types.h:250
const irep_idt & get_descriptor() const
Gets the method's descriptor – the mangled form of its type.
Definition java_types.h:286
bool get_final() const
Definition java_types.h:383
const componentst & components() const
Definition java_types.h:224
void set_synthetic(bool synthetic)
marks class synthetic
Definition java_types.h:434
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:564
std::vector< java_lambda_method_handlet > java_lambda_method_handlest
Definition java_types.h:515
@ LAMBDA_VIRTUAL_METHOD_HANDLE
Virtual call to the given interface or method.
@ LAMBDA_CONSTRUCTOR_HANDLE
Instantiate the needed type then call a constructor.
struct_tag_typet & subtype()
Definition java_types.h:612
Extract member of struct or union.
Definition std_expr.h:2794
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & debug() const
Definition message.h:429
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
no_unique_unimplemented_method_exceptiont(const std::string &s)
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition symbol.h:179
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
An expression containing a side effect.
Definition std_code.h:1450
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:449
void add_base(const struct_tag_typet &base)
Add a base class/struct.
Definition std_types.cpp:98
void set_tag(const irep_idt &tag)
Definition std_types.h:169
const componentst & components() const
Definition std_types.h:147
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
irep_idt mode
Language mode.
Definition symbol.h:49
const irep_idt & get_identifier() const
Definition std_types.h:410
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition symbol.h:139
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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)
JAVA Bytecode Language Conversion.
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...
reference_typet java_reference_type(const typet &subtype)
const java_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:184
const java_reference_typet & to_java_reference_type(const typet &type)
Definition java_types.h:630
const java_class_typet & to_java_class_type(const typet &type)
Definition java_types.h:582
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.
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.
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.
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
static symbolt implemented_method_symbol(synthetic_methods_mapt &synthetic_methods, const java_class_typet::methodt &method_to_implement, const irep_idt &synthetic_class_name)
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)
static optionalt< irep_idt > get_unboxing_method(const pointer_typet &maybe_boxed_type)
If maybe_boxed_type is a boxed primitive return its unboxing method; otherwise return empty.
exprt make_function_expr(const symbolt &function_symbol, const symbol_table_baset &symbol_table)
Produce a class_method_descriptor_exprt or symbol_exprt for function_symbol depending on whether virt...
void create_invokedynamic_synthetic_classes(const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt::instructionst &instructions, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods, message_handlert &message_handler)
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 ...
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....
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
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).
static const java_class_typet::methodt * try_get_unique_unimplemented_method(const symbol_table_baset &symbol_table, const struct_tag_typet &functional_interface_tag, const irep_idt &method_identifier, const int instruction_address, const messaget &log)
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)
static optionalt< java_class_typet::java_lambda_method_handlet > lambda_method_handle(const symbol_table_baset &symbol_table, const irep_idt &method_identifier, const java_method_typet &dynamic_method_type)
static std::string escape_symbol_special_chars(std::string input)
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)
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.
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.
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...
irep_idt lambda_synthetic_class_name(const irep_idt &method_identifier, std::size_t instruction_address)
static symbolt constructor_symbol(synthetic_methods_mapt &synthetic_methods, const irep_idt &synthetic_class_name, java_method_typet constructor_type)
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...
Java lambda code synthesis.
nonstd::optional< T > optionalt
Definition optional.h:35
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define POSTCONDITION(CONDITION)
Definition invariant.h:479
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition std_types.h:381
const char * mnemonic
int operator()(const java_class_typet::methodt *a, const java_class_typet::methodt *b) const
Return type for get_boxed_type_info_by_name.
Definition java_utils.h:54
const irep_idt unboxing_function_name
Name of the function defined on the boxed type that returns the boxed value.
Definition java_utils.h:57
std::vector< instructiont > instructionst
Author: Diffblue Ltd.
Synthetic methods are particular methods internally generated by the Java frontend,...
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
@ INVOKEDYNAMIC_METHOD
A generated method for a class capturing the parameters of an invokedynamic instruction.
@ INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
A generated constructor for a class capturing the parameters of an invokedynamic instruction.