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 "jar_file.h"
18#include "java_types.h"
19#include "java_utils.h"
21
22#include <util/message.h>
23#include <util/namespace.h>
24#include <util/symbol_table.h>
25
26#include <string.h>
27
28static std::string escape_symbol_special_chars(std::string input)
29{
30 for(auto &c : input)
31 {
32 if(c == '$' || c == ':' || c == '.')
33 c = '_';
34 }
35 return input;
36}
37
40 std::size_t instruction_address)
41{
42 return "java::lambda_synthetic_class$" +
45 "$" + std::to_string(instruction_address);
46}
47
57 const symbol_table_baset &symbol_table,
58 const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
59 const size_t index)
60{
61 // Check if we don't have enough bootstrap methods to satisfy the requested
62 // lambda. This could happen if we fail to parse one of the methods, or if
63 // the class type is partly or entirely synthetic, such as the types created
64 // internally by the string solver.
65 if(index >= lambda_method_handles.size())
66 return {};
67 const auto &lambda_method_handle = lambda_method_handles.at(index);
68 // If the lambda method handle has an unknown type, it does not refer to
69 // any symbol (it has an empty identifier)
70 if(
71 lambda_method_handle.get_handle_kind() !=
74 return {};
75}
76
79 const symbol_tablet &symbol_table,
82{
83 const namespacet ns{symbol_table};
84 const auto &method_symbol = ns.lookup(method_identifier);
85 const auto &declaring_class_symbol =
86 ns.lookup(*declaring_class(method_symbol));
87
89 const auto &lambda_method_handles = class_type.lambda_method_handles();
93 symbol_table, lambda_method_handles, lambda_handle_index);
94}
95
96class no_unique_unimplemented_method_exceptiont : public std::exception
97{
98public:
99 explicit no_unique_unimplemented_method_exceptiont(const std::string &s)
100 : message(s)
101 {
102 }
103 const std::string message;
104};
105
107{
110 const java_class_typet::methodt *b) const
111 {
112 return a->get_base_name() == b->get_base_name()
113 ? (a->get_descriptor() == b->get_descriptor()
114 ? 0
115 : a->get_descriptor() < b->get_descriptor())
116 : a->get_base_name() < b->get_base_name();
117 }
118};
119
122typedef std::map<
124 bool,
127
137{
138 static const irep_idt jlo = "java::java.lang.Object";
139 // Terminate recursion at Object; any other base of an interface must
140 // itself be an interface.
141 if(jlo == interface_id)
142 return {};
143
144 const java_class_typet &interface =
145 to_java_class_type(ns.lookup(interface_id).type);
146
147 if(interface.get_is_stub())
148 {
150 "produces a type that inherits the stub type " + id2string(interface_id));
151 }
152
154
155 // First accumulate definitions from child types:
156 for(const auto &base : interface.bases())
157 {
159 get_interface_methods(base.type().get_identifier(), ns);
160 for(const auto &base_method : base_methods)
161 {
162 if(base_method.second)
163 {
164 // Any base definition fills any abstract definition from another base:
165 all_methods[base_method.first] = true;
166 }
167 else
168 {
169 // An abstract method incoming from a base falls to any existing
170 // definition, so only insert if not present:
171 all_methods.emplace(base_method.first, false);
172 }
173 }
174 }
175
176 // Now insert defintions from this class:
177 for(const auto &method : interface.methods())
178 {
179 static const irep_idt equals = "equals";
180 static const irep_idt equals_descriptor = "(Ljava/lang/Object;)Z";
181 static const irep_idt hashCode = "hashCode";
182 static const irep_idt hashCode_descriptor = "()I";
183 if(
184 (method.get_base_name() == equals &&
185 method.get_descriptor() == equals_descriptor) ||
186 (method.get_base_name() == hashCode &&
187 method.get_descriptor() == hashCode_descriptor))
188 {
189 // Ignore any uses of functions that are certainly defined on
190 // java.lang.Object-- even if explicitly made abstract, they can't be the
191 // implemented method of a functional interface.
192 continue;
193 }
194
195 // Note unlike inherited definitions, an abstract definition here *does*
196 // wipe out a non-abstract definition (i.e. a default method) from a parent
197 // type.
198 all_methods[&method] =
199 !ns.lookup(method.get_name()).type.get_bool(ID_C_abstract);
200 }
201
202 return all_methods;
203}
204
206 const symbol_tablet &symbol_table,
209 const int instruction_address,
210 const messaget &log)
211{
212 const namespacet ns{symbol_table};
213 try
214 {
217
219 nullptr;
220
221 for(const auto &entry : all_methods)
222 {
223 if(!entry.second)
224 {
226 {
228 "produces a type with at least two unimplemented methods");
229 }
231 }
232 }
233
235 {
237 "produces a type with no unimplemented methods");
238 }
240 }
242 {
243 log.debug() << "ignoring invokedynamic at " << method_identifier
244 << " address " << instruction_address << " with type "
245 << functional_interface_tag.get_identifier() << " which "
246 << e.message << "." << messaget::eom;
247 return {};
248 }
249}
250
256{
258 // Tag = name without 'java::' prefix, matching the convention used by
259 // java_bytecode_convert_class.cpp
260 synthetic_class_type.set_tag(
263 synthetic_class_type.set_synthetic(true);
265 struct_tag_typet base_tag("java::java.lang.Object");
268
269 // Add the class fields:
270
271 {
273 const irep_idt base_field_name("@java.lang.Object");
274 base_field.set_name(base_field_name);
275 base_field.set_base_name(base_field_name);
276 base_field.set_pretty_name(base_field_name);
277 base_field.set_access(ID_private);
278 base_field.type() = base_tag;
279 synthetic_class_type.components().emplace_back(std::move(base_field));
280
281 std::size_t field_idx = 0;
282 for(const auto &param : dynamic_method_type.parameters())
283 {
284 irep_idt field_basename = "capture_" + std::to_string(field_idx++);
285
287 new_field.set_name(field_basename);
288 new_field.set_base_name(field_basename);
289 new_field.set_pretty_name(field_basename);
290 new_field.set_access(ID_private);
291 new_field.type() = param.type();
292 synthetic_class_type.components().emplace_back(std::move(new_field));
293 }
294 }
295
300}
301
303 synthetic_methods_mapt &synthetic_methods,
305 java_method_typet constructor_type) // dynamic_method_type
306{
310 constructor_symbol.pretty_name = constructor_symbol.name;
311 constructor_symbol.base_name = "<init>";
313
314 synthetic_methods[constructor_name] =
316
317 constructor_type.set_is_constructor();
318 constructor_type.return_type() = empty_typet();
319
320 size_t field_idx = 0;
321 for(auto &param : constructor_type.parameters())
322 {
323 irep_idt param_basename = "param_" + std::to_string(field_idx++);
324 param.set_base_name(param_basename);
325 param.set_identifier(
327 }
328
331 constructor_this_param.set_this();
332 constructor_this_param.set_base_name("this");
333 constructor_this_param.set_identifier(id2string(constructor_name) + "::this");
334
335 constructor_type.parameters().insert(
336 constructor_type.parameters().begin(), constructor_this_param);
337
338 constructor_symbol.type = constructor_type;
340 return constructor_symbol;
341}
342
344 synthetic_methods_mapt &synthetic_methods,
347{
348 const std::string implemented_method_name =
350 id2string(method_to_implement.get_base_name()) + ":" +
351 id2string(method_to_implement.get_descriptor());
352
355 synthetic_methods[implemented_method_symbol.name] =
358 implemented_method_symbol.base_name = method_to_implement.get_base_name();
362 implemented_method_type.parameters()[0].type() =
364
365 size_t field_idx = 0;
366 for(auto &param : implemented_method_type.parameters())
367 {
369 field_idx == 0 ? "this" : "param_" + std::to_string(field_idx);
370 param.set_base_name(param_basename);
371 param.set_identifier(
373
374 ++field_idx;
375 }
376
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.
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());
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 }
430 symbol_table,
433 instruction.address,
434 log);
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;
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(
452 }
453}
454
456 const irep_idt &identifier,
457 const irep_idt &base_name,
458 const irep_idt &pretty_name,
459 const typet &type,
461 symbol_table_baset &symbol_table,
462 message_handlert &log)
463{
464 const auto *existing_symbol = symbol_table.lookup(identifier);
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
492
494 parameters.at(0).get_identifier(), parameters.at(0).type());
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");
502 jlo_this_param.set_this();
503
508 "<init>",
511 jlo,
512 symbol_table,
513 message_handler);
515 jlo_constructor_symbol.symbol_expr(),
516 code_function_callt::argumentst{typecast_exprt(this_param, jlo_reference)});
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:
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
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
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);
557 new_instance_var_symbol.type = type;
558 bool add_failed = symbol_table.add(new_instance_var_symbol);
562
563 return new_instance_var;
564}
565
577 const irep_idt &function_id,
579 symbol_table_baset &symbol_table,
580 code_blockt &result)
581{
582 // We must instantiate the object, then call the requested constructor
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();
590
591 // Call static init if it exists:
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:
600 function_id,
601 "newinvokespecial_instance",
603 symbol_table,
604 result);
605
606 // Instantiate the object:
609
610 return new_instance_var;
611}
612
624
630 const symbol_tablet &symbol_table)
631{
633 if(!method_type.has_this())
634 return function_symbol.symbol_expr();
636 to_struct_tag_type(method_type.get_this()->type().subtype())
638 const auto &this_symbol = symbol_table.lookup_ref(declared_on_class_id);
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
651 mangled_method_name,
653 function_symbol.base_name};
654}
655
686 exprt expr,
687 const typet &required_type,
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();
696
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
707 INVARIANT(
708 primitive_type_info != nullptr,
709 "A Java non-pointer type involved in a type disagreement should"
710 " be a primitive");
711
713 role + (original_is_pointer ? "_unboxed" : "_boxed");
714
716 function_id, fresh_local_name, required_type, symbol_table, code_block);
717
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
725 symbol_table.lookup_ref(transform_function_id);
726
729 const exprt cast_expr =
731
735 {expr}});
736
737 return std::move(fresh_local);
738}
739
744 exprt expr,
745 const typet &required_type,
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),
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
792
794 parameters.at(0).get_identifier(), parameters.at(0).type());
796
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:
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 =
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
837 {
839 function_id, lambda_method_symbol, symbol_table, result);
840
841 // Prepend the newly created object to the lambda arg list:
843 }
844
845 const auto &lambda_method_descriptor =
846 lambda_method_handle.get_lambda_method_descriptor();
850 else
851 callee = lambda_method_symbol.symbol_expr();
852
853 // Adjust boxing if required:
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 {
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 {
874 function_id, "return_value", callee_return_type, symbol_table, result);
878 function_type.return_type(),
879 result,
880 symbol_table,
881 function_id,
882 "retval");
884 }
885 else
886 {
888 }
889
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}
struct bytecode_infot const bytecode_info[]
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:147
An expression describing a method on a class.
Definition std_expr.h:3272
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 codet representing the declaration of a local variable.
A codet representing an assignment in the program.
Definition std_code.h:24
codet representation of a function call statement.
codet representation of a "return from a function" statement.
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:37
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
Represents a lambda call to a method.
Definition java_types.h:482
bool get_final() const
Definition java_types.h:383
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:2667
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:171
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
Expression to hold a symbol (variable)
Definition std_expr.h:80
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.
The symbol table.
Symbol table entry.
Definition symbol.h:28
irep_idt name
The unique identifier.
Definition symbol.h:40
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:133
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
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)
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 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 std::string escape_symbol_special_chars(std::string input)
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)
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.
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.
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...
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...
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)
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)
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...
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)
Java lambda code synthesis.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is 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
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
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.