CBMC
|
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>
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_descriptort > | methods_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_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 method). More... | |
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 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::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) |
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 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... | |
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_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. 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... | |
Java lambda code synthesis.
Definition in file lambda_synthesis.cpp.
typedef 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.e.
true if defined with a default method, false if abstract)
Definition at line 125 of file lambda_synthesis.cpp.
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.
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.
|
static |
Definition at line 298 of file lambda_synthesis.cpp.
|
static |
Definition at line 541 of file lambda_synthesis.cpp.
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.
|
static |
Definition at line 27 of file lambda_synthesis.cpp.
|
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.
|
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 55 of file lambda_synthesis.cpp.
|
static |
Definition at line 451 of file lambda_synthesis.cpp.
|
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.
|
static |
Definition at line 337 of file lambda_synthesis.cpp.
|
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.
function_id | ID of the function that result falls within |
lambda_method_symbol | the constructor that will be called, and so whose this parameter we should instantiate. |
symbol_table | symbol table, will gain a local variable |
result | will gain instructions instantiating the required type |
Definition at line 572 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 475 of file lambda_synthesis.cpp.
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.
function_id | synthetic 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_table | will gain local variable symbols |
message_handler | log |
function_id
Definition at line 773 of file lambda_synthesis.cpp.
|
static |
Definition at line 77 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.
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.
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.
|
static |
Definition at line 204 of file lambda_synthesis.cpp.