cprover
lambda_synthesis.cpp File Reference
#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>
+ Include dependency graph for lambda_synthesis.cpp:

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< symboltget_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_idtlambda_method_name (const symbol_tablet &symbol_table, const irep_idt &method_identifier, const java_method_typet &dynamic_method_type)
 
static optionalt< irep_idtinterface_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 symboltget_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...
 

Detailed Description

Java lambda code synthesis

Definition in file lambda_synthesis.cpp.

Function Documentation

◆ constructor_symbol()

static symbolt constructor_symbol ( synthetic_methods_mapt synthetic_methods,
const irep_idt synthetic_class_name,
java_method_typet  constructor_type 
)
static

Definition at line 184 of file lambda_synthesis.cpp.

◆ create_invokedynamic_synthetic_classes()

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.

◆ escape_symbol_special_chars()

static std::string escape_symbol_special_chars ( std::string  input)
static

Definition at line 27 of file lambda_synthesis.cpp.

◆ get_lambda_method_symbol()

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 
)
static

Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap method).

Parameters
symbol_tableglobal symbol table
lambda_method_handlesVector of lambda method handles (bootstrap methods) of the class where the lambda is called
indexIndex of the lambda method handle in the vector
Returns
Symbol of the lambda method if the method handle has a known type

Definition at line 54 of file lambda_synthesis.cpp.

◆ get_or_create_method_symbol()

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 
)
static

Definition at line 351 of file lambda_synthesis.cpp.

◆ implemented_method_symbol()

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.

◆ interface_method_id()

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 
)
static

Definition at line 94 of file lambda_synthesis.cpp.

◆ invokedynamic_synthetic_constructor()

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.

◆ invokedynamic_synthetic_method()

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.

◆ lambda_method_name()

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

Definition at line 73 of file lambda_synthesis.cpp.

◆ lambda_synthetic_class_name()

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.

◆ synthetic_class_symbol()

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.