Go to the documentation of this file.
31 if(c ==
'$' || c ==
':' || c ==
'.')
39 std::size_t instruction_address)
41 return "java::lambda_synthetic_class$" +
63 if(index >= lambda_method_handles.size())
65 const irept &lambda_method_handle = lambda_method_handles.at(index);
68 if(!lambda_method_handle.
id().
empty())
69 return symbol_table.
lookup_ref(lambda_method_handle.
id());
79 const auto &method_symbol = ns.
lookup(method_identifier);
80 const auto &declaring_class_symbol =
84 const auto &lambda_method_handles = class_type.lambda_method_handles();
85 auto lambda_handle_index =
86 dynamic_method_type.
get_int(ID_java_lambda_method_handle_index);
88 symbol_table, lambda_method_handles, lambda_handle_index);
89 if(lambda_method_symbol)
90 return lambda_method_symbol->name;
98 const int instruction_address,
103 const symbolt &implemented_interface_symbol =
110 log.
debug() <<
"ignoring invokedynamic at " << method_identifier
111 <<
" address " << instruction_address
112 <<
" which produces a stub type "
116 else if(implemented_interface_type.
methods().size() != 1)
119 <<
"ignoring invokedynamic at " << method_identifier <<
" address "
120 << instruction_address <<
" which produces type "
122 <<
" which should have exactly one abstract method but actually has "
123 << implemented_interface_type.
methods().size()
124 <<
". Note default methods are not supported yet."
125 <<
"Also note methods declared in an inherited interface are not "
129 return implemented_interface_type.
methods().at(0).get_name();
133 const irep_idt &synthetic_class_name,
143 synthetic_class_type.
set_name(synthetic_class_name);
145 synthetic_class_type.
set(
148 synthetic_class_type.
add_base(base_tag);
149 synthetic_class_type.
add_base(functional_interface_tag);
155 const irep_idt base_field_name(
"@java.lang.Object");
156 base_field.set_name(base_field_name);
157 base_field.set_base_name(base_field_name);
158 base_field.set_pretty_name(base_field_name);
159 base_field.set_access(ID_private);
160 base_field.type() = base_tag;
161 synthetic_class_type.
components().emplace_back(std::move(base_field));
163 std::size_t field_idx = 0;
164 for(
const auto ¶m : dynamic_method_type.
parameters())
169 new_field.set_name(field_basename);
170 new_field.set_base_name(field_basename);
171 new_field.set_pretty_name(field_basename);
172 new_field.set_access(ID_private);
173 new_field.type() = param.type();
174 synthetic_class_type.
components().emplace_back(std::move(new_field));
186 const irep_idt &synthetic_class_name,
196 synthetic_methods[constructor_name] =
202 size_t field_idx = 0;
203 for(
auto ¶m : constructor_type.
parameters())
206 param.set_base_name(param_basename);
207 param.set_identifier(
215 constructor_this_param.
type() =
219 constructor_type.
parameters().begin(), constructor_this_param);
228 const symbolt &interface_method_symbol,
230 const irep_idt &synthetic_class_name)
232 const std::string implemented_method_name = [&] {
233 std::string implemented_method_name =
235 const std::string &functional_interface_tag_str =
238 has_prefix(implemented_method_name, functional_interface_tag_str),
239 "method names should be prefixed by their defining type");
240 implemented_method_name.replace(
242 functional_interface_tag_str.length(),
244 return implemented_method_name;
256 implemented_method_type.parameters()[0].type() =
259 size_t field_idx = 0;
260 for(
auto ¶m : implemented_method_type.parameters())
264 param.set_base_name(param_basename);
265 param.set_identifier(
304 const messaget log{message_handler};
306 for(
const auto &instruction : instructions)
310 const auto &dynamic_method_type =
313 symbol_table, method_identifier, dynamic_method_type);
316 log.debug() <<
"ignoring invokedynamic at " << method_identifier
317 <<
" address " << instruction.address
325 functional_interface_tag,
331 log.debug() <<
"identified invokedynamic at " << method_identifier
332 <<
" address " << instruction.address
334 const irep_idt synthetic_class_name =
337 synthetic_methods, synthetic_class_name, dynamic_method_type));
341 functional_interface_tag,
342 synthetic_class_name));
344 synthetic_class_name,
346 functional_interface_tag,
347 dynamic_method_type));
360 const auto *existing_symbol = symbol_table.
lookup(identifier);
362 return *existing_symbol;
390 parameters.at(0).get_identifier(), parameters.at(0).type());
394 const irep_idt jlo(
"java::java.lang.Object");
406 jlo_constructor_type,
411 jlo_constructor_symbol.symbol_expr(),
413 result.
add(super_constructor_call);
416 auto field_iterator = std::next(class_type.
components().begin());
417 for(
const auto ¶meter : parameters)
421 param_symbol.
name = parameter.get_identifier();
422 param_symbol.
base_name = parameter.get_base_name();
423 param_symbol.
mode = ID_java;
424 param_symbol.
type = parameter.type();
425 symbol_table.
add(param_symbol);
427 if(parameter.get_this())
432 symbol_exprt(parameter.get_identifier(), parameter.type()));
433 result.
add(assign_field);
438 return std::move(result);
456 const auto ¶meters = function_type.parameters();
457 const auto &return_type = function_type.return_type();
463 parameters.at(0).get_identifier(), parameters.at(0).type());
467 for(
const auto &field : class_type.
components())
469 if(field.get_name() ==
"@java.lang.Object")
471 lambda_method_args.push_back(
475 for(
const auto ¶meter : parameters)
479 param_symbol.
name = parameter.get_identifier();
480 param_symbol.
base_name = parameter.get_base_name();
481 param_symbol.
mode = ID_java;
482 param_symbol.
type = parameter.type();
483 symbol_table.
add(param_symbol);
485 if(parameter.get_this())
488 lambda_method_args.push_back(param_symbol.
symbol_expr());
491 const auto &lambda_method_symbol =
492 ns.
lookup(class_type.
get(ID_java_lambda_method_identifier));
497 lambda_method_symbol.symbol_expr(),
505 lambda_method_symbol.symbol_expr(), lambda_method_args));
508 return std::move(result);
Class that provides messages with a built-in verbosity 'level'.
const irep_idt & get_identifier() const
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
signed int get_int(const irep_namet &name) const
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
codet invokedynamic_synthetic_method(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic method.
reference_typet java_reference_type(const typet &subtype)
void set_synthetic(bool synthetic)
marks class synthetic
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.
The type of an expression, extends irept.
std::vector< parametert > parameterst
std::vector< instructiont > instructionst
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
typet type
Type of symbol.
Operator to dereference a pointer.
A side_effect_exprt representation of a function call side effect.
void set_identifier(const irep_idt &identifier)
void add_base(const struct_tag_typet &base)
Add a base class/struct.
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)
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
@ INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR
A generated constructor for a class capturing the parameters of an invokedynamic instruction.
@ INVOKEDYNAMIC_METHOD
A generated method for a class capturing the parameters of an invokedynamic instruction.
irep_idt base_name
Base (non-scoped) name.
A struct tag type, i.e., struct_typet with an identifier.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const methodst & methods() const
static optionalt< irep_idt > lambda_method_name(const symbol_tablet &symbol_table, const irep_idt &method_identifier, const java_method_typet &dynamic_method_type)
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Expression to hold a symbol (variable)
irep_idt pretty_name
Language-specific display name.
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
symbolt implemented_method_symbol(synthetic_methods_mapt &synthetic_methods, const symbolt &interface_method_symbol, const struct_tag_typet &functional_interface_tag, const irep_idt &synthetic_class_name)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
irep_idt mode
Language mode.
struct_tag_typet & subtype()
const std::string & id2string(const irep_idt &d)
void set_tag(const irep_idt &tag)
void set_is_constructor()
The symbol table base class interface.
const java_reference_typet & to_java_reference_type(const typet &type)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const irep_idt & id() const
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)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
exprt::operandst argumentst
void add(const codet &code)
const parameterst & parameters() const
nonstd::optional< T > optionalt
static std::string escape_symbol_special_chars(std::string input)
void set_base_name(const irep_idt &name)
irept::subt java_lambda_method_handlest
codet invokedynamic_synthetic_constructor(const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Create invokedynamic synthetic constructor.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Extract member of struct or union.
const componentst & components() const
codet representation of a "return from a function" statement.
static optionalt< symbolt > get_lambda_method_symbol(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...
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
symbolt synthetic_class_symbol(const irep_idt &synthetic_class_name, const irep_idt &lambda_method_name, const struct_tag_typet &functional_interface_tag, const java_method_typet &dynamic_method_type)
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.
Symbol table entry describing a data type.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
bool has_prefix(const std::string &s, const std::string &prefix)
There are a large number of kinds of tree structured or tree-like data in CPROVER.
static symbolt constructor_symbol(synthetic_methods_mapt &synthetic_methods, const irep_idt &synthetic_class_name, java_method_typet constructor_type)
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)
const java_class_typet & to_java_class_type(const typet &type)
Symbol table entry of function parameter.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const java_method_typet & to_java_method_type(const typet &type)
struct bytecode_infot const bytecode_info[]
A codet representing an assignment in the program.
irep_idt lambda_synthetic_class_name(const irep_idt &method_identifier, std::size_t instruction_address)
irep_idt name
The unique identifier.
Data structure for representing an arbitrary statement in a program.
static optionalt< irep_idt > interface_method_id(const symbol_tablet &symbol_table, const struct_tag_typet &functional_interface_tag, const irep_idt &method_identifier, const int instruction_address, const messaget &log)