cprover
|
#include "lambda_synthesis.h"
#include "java_bytecode_convert_method.h"
#include "java_bytecode_parse_tree.h"
#include "java_types.h"
#include "java_utils.h"
#include "synthetic_methods_map.h"
#include <util/message.h>
#include <util/namespace.h>
#include <util/prefix.h>
#include <util/symbol_table.h>
#include <string.h>
Go to the source code of this file.
Functions | |
static std::string | escape_symbol_special_chars (std::string input) |
irep_idt | lambda_synthetic_class_name (const irep_idt &method_identifier, std::size_t instruction_address) |
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 method). More... | |
static optionalt< irep_idt > | lambda_method_name (const symbol_tablet &symbol_table, const irep_idt &method_identifier, const java_method_typet &dynamic_method_type) |
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) |
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) |
static symbolt | constructor_symbol (synthetic_methods_mapt &synthetic_methods, const irep_idt &synthetic_class_name, java_method_typet constructor_type) |
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) |
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 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) |
codet | invokedynamic_synthetic_constructor (const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) |
Create invokedynamic synthetic constructor. More... | |
codet | invokedynamic_synthetic_method (const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) |
Create invokedynamic synthetic method. More... | |
Java lambda code synthesis
Definition in file lambda_synthesis.cpp.
|
static |
Definition at line 184 of file lambda_synthesis.cpp.
void create_invokedynamic_synthetic_classes | ( | const irep_idt & | method_identifier, |
const java_bytecode_parse_treet::methodt::instructionst & | instructions, | ||
symbol_tablet & | symbol_table, | ||
synthetic_methods_mapt & | synthetic_methods, | ||
message_handlert & | message_handler | ||
) |
Definition at line 297 of file lambda_synthesis.cpp.
|
static |
Definition at line 27 of file lambda_synthesis.cpp.
|
static |
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap method).
symbol_table | global symbol table |
lambda_method_handles | Vector of lambda method handles (bootstrap methods) of the class where the lambda is called |
index | Index of the lambda method handle in the vector |
Definition at line 54 of file lambda_synthesis.cpp.
|
static |
Definition at line 351 of file lambda_synthesis.cpp.
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 | ||
) |
Definition at line 226 of file lambda_synthesis.cpp.
|
static |
Definition at line 94 of file lambda_synthesis.cpp.
codet invokedynamic_synthetic_constructor | ( | const irep_idt & | function_id, |
symbol_table_baset & | symbol_table, | ||
message_handlert & | message_handler | ||
) |
Create invokedynamic synthetic constructor.
Definition at line 375 of file lambda_synthesis.cpp.
codet invokedynamic_synthetic_method | ( | const irep_idt & | function_id, |
symbol_table_baset & | symbol_table, | ||
message_handlert & | message_handler | ||
) |
Create invokedynamic synthetic method.
Definition at line 441 of file lambda_synthesis.cpp.
|
static |
Definition at line 73 of file lambda_synthesis.cpp.
irep_idt lambda_synthetic_class_name | ( | const irep_idt & | method_identifier, |
std::size_t | instruction_address | ||
) |
Definition at line 37 of file lambda_synthesis.cpp.
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 | ||
) |
Definition at line 132 of file lambda_synthesis.cpp.