CBMC
lambda_synthesis.cpp File Reference

Java lambda code synthesis. More...

#include "lambda_synthesis.h"
#include <util/message.h>
#include <util/namespace.h>
#include <util/symbol_table_base.h>
#include "java_bytecode_convert_method.h"
#include "java_bytecode_parse_tree.h"
#include "java_static_initializers.h"
#include "java_types.h"
#include "java_utils.h"
#include "synthetic_methods_map.h"
#include <string.h>
+ Include dependency graph for lambda_synthesis.cpp:

Go to the source code of this file.

Classes

class  no_unique_unimplemented_method_exceptiont
 
struct  compare_base_name_and_descriptort
 

Typedefs

typedef std::map< const java_class_typet::methodt *, bool, compare_base_name_and_descriptortmethods_by_name_and_descriptort
 Map from method, indexed by name and descriptor but not defining class, onto defined-ness (i.e. More...
 

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 std::optional< java_class_typet::java_lambda_method_handletget_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 method). More...
 
static std::optional< java_class_typet::java_lambda_method_handletlambda_method_handle (const symbol_table_baset &symbol_table, const irep_idt &method_identifier, const java_method_typet &dynamic_method_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_typet::methodt * onto a boolean value which is true if the method is defined (i.e. More...
 
static const java_class_typet::methodttry_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)
 
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)
 
static symbolt constructor_symbol (synthetic_methods_mapt &synthetic_methods, const irep_idt &synthetic_class_name, java_method_typet constructor_type)
 
static symbolt implemented_method_symbol (synthetic_methods_mapt &synthetic_methods, const java_class_typet::methodt &method_to_implement, 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_table_baset &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...
 
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 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). More...
 
static std::optional< irep_idtget_unboxing_method (const pointer_typet &maybe_boxed_type)
 If maybe_boxed_type is a boxed primitive return its unboxing method; otherwise return empty. More...
 
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 virtual dispatch could be required (i.e., if it is non-static and its 'this' parameter is a non-final type) More...
 
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 to code_block, then return an expression giving the adjusted expression. More...
 
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. More...
 
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. More...
 

Detailed Description

Java lambda code synthesis.

Definition in file lambda_synthesis.cpp.

Typedef Documentation

◆ methods_by_name_and_descriptort

Map from method, indexed by name and descriptor but not defining class, onto defined-ness (i.e.

true if defined with a default method, false if abstract)

Definition at line 125 of file lambda_synthesis.cpp.

Function Documentation

◆ adjust_type_if_necessary()

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.

If the source is legal Java that should mean a pointer upcast or primitive widening conversion, but this is not checked.

Definition at line 743 of file lambda_synthesis.cpp.

◆ box_or_unbox_type_if_necessary()

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 to code_block, then return an expression giving the adjusted expression.

Otherwise return expr unchanged. role is a suggested name prefix for any temporary variable needed; function_id is the id of the function any created code it added to.

Regarding the apparent behaviour of the Java compiler / runtime with regard to adapting generic methods to/from primtitive types:

When unboxing, it appears to permit widening numeric conversions at the same time. For example, implementing Consumer<Short> by a function of type long -> void is possible, as the generated function will look like impl(Object o) { realfunc(((Number)o).longValue()); }

On the other hand when boxing to satisfy a generic interface type this is not permitted: in theory we should be able to implement Producer<Long> by a function of type () -> int, generating boxing code like impl() { return Long.valueOf(realfunc()); }

However it appears there is no way to convey to the lambda metafactory that a Long is really required rather than an Integer (the obvious conversion from int), so the compiler forbids this and requires that only simple boxing is performed.

Therefore when unboxing we cast to Number first, while when boxing and the target type is not a specific boxed type (i.e. the target is Object or Number etc) then we use the primitive type as our cue regarding the boxed type to produce.

Definition at line 684 of file lambda_synthesis.cpp.

◆ 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 298 of file lambda_synthesis.cpp.

◆ create_and_declare_local()

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

Definition at line 541 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_table_baset symbol_table,
synthetic_methods_mapt synthetic_methods,
message_handlert message_handler 
)

Definition at line 395 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_interface_methods()

static const methods_by_name_and_descriptort get_interface_methods ( const irep_idt interface_id,
const namespacet ns 
)
static

Find all methods defined by this method and its parent types, returned as a map from const java_class_typet::methodt * onto a boolean value which is true if the method is defined (i.e.

has a default definition) as of this node in the class graph. If there are multiple name-and-descriptor-compatible methods, for example because both If1.f(int) and If2.f(int) are inherited here, only one is stored in the map, chosen arbitrarily.

Definition at line 135 of file lambda_synthesis.cpp.

◆ get_lambda_method_handle()

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 
)
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 55 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 451 of file lambda_synthesis.cpp.

◆ get_unboxing_method()

static std::optional<irep_idt> get_unboxing_method ( const pointer_typet maybe_boxed_type)
static

If maybe_boxed_type is a boxed primitive return its unboxing method; otherwise return empty.

Definition at line 613 of file lambda_synthesis.cpp.

◆ implemented_method_symbol()

static symbolt implemented_method_symbol ( synthetic_methods_mapt synthetic_methods,
const java_class_typet::methodt method_to_implement,
const irep_idt synthetic_class_name 
)
static

Definition at line 337 of file lambda_synthesis.cpp.

◆ instantiate_new_object()

static symbol_exprt instantiate_new_object ( const irep_idt function_id,
const symbolt lambda_method_symbol,
symbol_table_baset symbol_table,
code_blockt result 
)
static

Instantiates an object suitable for calling a given constructor (but does not actually call it).

Adds a local to symbol_table, and code implementing the required operation to result; returns a symbol carrying a reference to the newly instantiated object.

Parameters
function_idID of the function that result falls within
lambda_method_symbolthe constructor that will be called, and so whose this parameter we should instantiate.
symbol_tablesymbol table, will gain a local variable
resultwill gain instructions instantiating the required type
Returns
the newly instantiated symbol

Definition at line 572 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 475 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 the body for the synthetic method implementing an invokedynamic method.

Create invokedynamic synthetic method.

For most lambdas this means creating a simple function body like TR new_synthetic_method(T1 param1, T2 param2, ...) { return target_method(capture1, capture2, ..., param1, param2, ...); }, where the first parameter might be a this parameter. For a constructor method, the generated code will be of the form TNew new_synthetic_method(T1 param1, T2 param2, ...) { return new TNew(capture1, capture2, ..., param1, param2, ...); } i.e. the TNew object will be both instantiated and constructed.

Parameters
function_idsynthetic method whose body should be generated; information about the lambda method to generate has already been stored in the symbol table by create_invokedynamic_synthetic_classes.
symbol_tablewill gain local variable symbols
message_handlerlog
Returns
the method body for function_id

Definition at line 773 of file lambda_synthesis.cpp.

◆ lambda_method_handle()

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

Definition at line 77 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.

◆ make_function_expr()

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 virtual dispatch could be required (i.e., if it is non-static and its 'this' parameter is a non-final type)

Definition at line 626 of file lambda_synthesis.cpp.

◆ synthetic_class_symbol()

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 
)

Definition at line 250 of file lambda_synthesis.cpp.

◆ try_get_unique_unimplemented_method()

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

Definition at line 204 of file lambda_synthesis.cpp.