31 if(c ==
'$' || c ==
':' || c ==
'.')
39 std::size_t instruction_address)
41 return "java::lambda_synthetic_class$" +
54 static std::optional<java_class_typet::java_lambda_method_handlet>
64 if(index >= lambda_method_handles.size())
76 static std::optional<java_class_typet::java_lambda_method_handlet>
83 const auto &method_symbol = ns.
lookup(method_identifier);
84 const auto &declaring_class_symbol =
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);
111 return a->get_base_name() == b->get_base_name()
115 : a->get_base_name() < b->get_base_name();
137 static const irep_idt jlo =
"java::java.lang.Object";
140 if(jlo == interface_id)
146 if(interface.get_is_stub())
149 "produces a type that inherits the stub type " +
id2string(interface_id));
155 for(
const auto &base : interface.bases())
159 for(
const auto &base_method : base_methods)
161 if(base_method.second)
164 all_methods[base_method.first] =
true;
170 all_methods.emplace(base_method.first,
false);
176 for(
const auto &method : interface.methods())
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";
183 (method.get_base_name() == equals &&
184 method.get_descriptor() == equals_descriptor) ||
185 (method.get_base_name() == hashCode &&
186 method.get_descriptor() == hashCode_descriptor))
197 all_methods[&method] =
198 !ns.
lookup(method.get_name()).type.get_bool(ID_C_abstract);
208 const int instruction_address,
220 for(
const auto &entry : all_methods)
224 if(method_and_descriptor_to_implement !=
nullptr)
227 "produces a type with at least two unimplemented methods");
229 method_and_descriptor_to_implement = entry.first;
233 if(!method_and_descriptor_to_implement)
236 "produces a type with no unimplemented methods");
238 return method_and_descriptor_to_implement;
242 log.debug() <<
"ignoring invokedynamic at " << method_identifier
243 <<
" address " << instruction_address <<
" with type "
251 const irep_idt &synthetic_class_name,
261 synthetic_class_type.
set_name(synthetic_class_name);
265 synthetic_class_type.
add_base(base_tag);
266 synthetic_class_type.
add_base(functional_interface_tag);
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));
280 std::size_t field_idx = 0;
281 for(
const auto ¶m : dynamic_method_type.
parameters())
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));
295 return type_symbolt{synthetic_class_name, synthetic_class_type, ID_java};
300 const irep_idt &synthetic_class_name,
308 synthetic_methods[constructor_name] =
314 size_t field_idx = 0;
315 for(
auto ¶m : constructor_type.
parameters())
318 param.set_base_name(param_basename);
319 param.set_identifier(
330 constructor_type.
parameters().begin(), constructor_this_param);
340 const irep_idt &synthetic_class_name)
342 const std::string implemented_method_name =
344 id2string(method_to_implement.get_base_name()) +
":" +
348 implemented_method_name, method_to_implement.
type(), ID_java};
354 implemented_method_type.parameters()[0].type() =
357 size_t field_idx = 0;
358 for(
auto ¶m : implemented_method_type.parameters())
362 param.set_base_name(param_basename);
363 param.set_identifier(
404 for(
const auto &instruction : instructions)
408 const auto &dynamic_method_type =
411 symbol_table, method_identifier, dynamic_method_type);
414 log.debug() <<
"ignoring invokedynamic at " << method_identifier
415 <<
" address " << instruction.address
423 functional_interface_tag,
427 if(!unimplemented_method)
429 log.debug() <<
"identified invokedynamic at " << method_identifier
430 <<
" address " << instruction.address <<
" for lambda: "
431 << lambda_handle->get_lambda_method_identifier()
433 const irep_idt synthetic_class_name =
436 synthetic_methods, synthetic_class_name, dynamic_method_type));
438 synthetic_methods, *unimplemented_method, synthetic_class_name));
440 synthetic_class_name,
442 functional_interface_tag,
443 dynamic_method_type));
456 const auto *existing_symbol = symbol_table.
lookup(identifier);
458 return *existing_symbol;
486 parameters.at(0).get_identifier(), parameters.at(0).type());
490 const irep_idt jlo(
"java::java.lang.Object");
502 jlo_constructor_type,
507 jlo_constructor_symbol.symbol_expr(),
509 result.
add(super_constructor_call);
512 auto field_iterator = std::next(class_type.
components().begin());
513 for(
const auto ¶meter : parameters)
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);
523 if(parameter.get_this())
528 symbol_exprt(parameter.get_identifier(), parameter.type()));
529 result.
add(assign_field);
534 return std::move(result);
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);
555 return new_instance_var;
570 const symbolt &lambda_method_symbol,
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();
586 if(
const auto *static_init_symbol = symbol_table.
lookup(static_init_name))
594 "newinvokespecial_instance",
603 return new_instance_var;
608 static std::optional<irep_idt>
616 : std::optional<irep_idt>{};
623 const symbolt &function_symbol,
627 if(!method_type.has_this())
629 const irep_idt &declared_on_class_id =
633 const auto &this_symbol = symbol_table.
lookup_ref(declared_on_class_id);
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);
647 declared_on_class_id,
682 const typet &required_type,
686 const std::string &role)
688 const typet &original_type = expr.
type();
692 if(original_is_pointer == required_is_pointer)
701 original_is_pointer ? required_type : original_type);
703 primitive_type_info !=
nullptr,
704 "A Java non-pointer type involved in a type disagreement should"
708 role + (original_is_pointer ?
"_unboxed" :
"_boxed");
711 function_id, fresh_local_name, required_type, symbol_table, code_block);
713 const irep_idt transform_function_id =
717 .value_or(primitive_type_info->unboxing_function_name)
718 : primitive_type_info->boxed_type_factory_method;
720 const symbolt &transform_function_symbol =
721 symbol_table.
lookup_ref(transform_function_id);
723 const typet &transform_function_param_type =
725 const exprt cast_expr =
733 return std::move(fresh_local);
741 const typet &required_type,
745 const std::string &role)
749 expr, required_type, code_block, symbol_table, function_id, role),
784 const auto ¶meters = function_type.parameters();
790 parameters.at(0).get_identifier(), parameters.at(0).type());
794 for(
const auto &field : class_type.
components())
796 if(field.get_name() ==
"@java.lang.Object")
798 lambda_method_args.push_back(
802 for(
const auto ¶meter : parameters)
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);
812 if(parameter.get_this())
815 lambda_method_args.push_back(param_symbol.
symbol_expr());
820 class_type.
find(ID_java_lambda_method_handle));
822 const auto &lambda_method_symbol =
825 const auto is_constructor_lambda =
828 const auto use_virtual_dispatch =
832 if(is_constructor_lambda)
835 function_id, lambda_method_symbol, symbol_table, result);
838 lambda_method_args.insert(lambda_method_args.begin(), new_instance_var);
841 const auto &lambda_method_descriptor =
844 if(use_virtual_dispatch)
845 callee = lambda_method_descriptor;
847 callee = lambda_method_symbol.symbol_expr();
851 const auto &callee_parameters = callee_type.
parameters();
852 const auto &callee_return_type = callee_type.
return_type();
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)
859 std::move(lambda_method_args[i]),
860 callee_parameters[i].type(),
867 if(function_type.return_type() !=
empty_typet() && !is_constructor_lambda)
870 function_id,
"return_value", callee_return_type, symbol_table, result);
874 function_type.return_type(),
886 if(is_constructor_lambda)
890 lambda_method_args.at(0), function_type.return_type())});
893 return std::move(result);
struct bytecode_infot const bytecode_info[]
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
An expression describing a method on a class.
A codet representing sequential composition of program statements.
void add(const codet &code)
A goto_instruction_codet representing the declaration of a local variable.
A codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
goto_instruction_codet representation of a "return from a function" statement.
void set_base_name(const irep_idt &name)
void set_identifier(const irep_idt &identifier)
std::vector< parametert > parameterst
void set_is_constructor()
const typet & return_type() const
const parameterst & parameters() const
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.
Base class for all expressions.
typet & type()
Return the type of the expression.
const irept & find(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
signed int get_int(const irep_idt &name) const
Represents a lambda call to a method.
const irep_idt & get_descriptor() const
Gets the method's descriptor – the mangled form of its type.
const java_method_typet & type() const
void set_synthetic(bool synthetic)
marks class synthetic
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.
const componentst & components() const
std::vector< java_lambda_method_handlet > java_lambda_method_handlest
@ LAMBDA_VIRTUAL_METHOD_HANDLE
Virtual call to the given interface or method.
@ UNKNOWN_HANDLE
Can't be called.
@ LAMBDA_CONSTRUCTOR_HANDLE
Instantiate the needed type then call a constructor.
struct_tag_typet & subtype()
Extract member of struct or union.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const std::string message
no_unique_unimplemented_method_exceptiont(const std::string &s)
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
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.
A struct tag type, i.e., struct_typet with an identifier.
void add_base(const struct_tag_typet &base)
Add a base class/struct.
void set_tag(const irep_idt &tag)
const componentst & components() const
Expression to hold a symbol (variable)
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.
const symbolt & lookup_ref(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.
irep_idt base_name
Base (non-scoped) name.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
irep_idt mode
Language mode.
const irep_idt & get_identifier() const
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
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_class_typet & to_java_class_type(const typet &type)
const java_reference_typet & to_java_reference_type(const typet &type)
const java_method_typet & to_java_method_type(const typet &type)
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.
std::optional< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
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.
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 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...
static std::optional< 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)
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)
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 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 ...
static std::optional< 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...
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)
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 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)
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.
irep_idt lambda_synthetic_class_name(const irep_idt &method_identifier, std::size_t instruction_address)
static std::optional< 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.
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.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
#define POSTCONDITION(CONDITION)
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
int strcmp(const char *s1, const char *s2)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
int operator()(const java_class_typet::methodt *a, const java_class_typet::methodt *b) const
Return type for get_boxed_type_info_by_name.
const irep_idt unboxing_function_name
Name of the function defined on the boxed type that returns the boxed value.
std::vector< instructiont > instructionst
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.