CBMC
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
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

 
 

Typedefs

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

Functions

static std::string  escape_symbol_special_chars (std::string input)
 
 
  Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap method).
 
 
  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.
 
 
 
 
 
 
 
  Create invokedynamic synthetic constructor.
 
 
  Instantiates an object suitable for calling a given constructor (but does not actually call it).
 
  If maybe_boxed_type is a boxed primitive return its unboxing method; otherwise return empty.
 
  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)
 
  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.
 
  Box or unbox expr as per box_or_unbox_type_if_necessary, then cast the result to required_type.
 
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.
 

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 typetrequired_type,
code_blocktcode_block,
symbol_table_basetsymbol_table,
const irep_idtfunction_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 typetrequired_type,
code_blocktcode_block,
symbol_table_basetsymbol_table,
const irep_idtfunction_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_maptsynthetic_methods,
const irep_idtsynthetic_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_idtfunction_id,
const irep_idtbasename,
const typettype,
symbol_table_basetsymbol_table,
code_blocktmethod 
)
static

Definition at line 541 of file lambda_synthesis.cpp.

◆  create_invokedynamic_synthetic_classes()

void create_invokedynamic_synthetic_classes ( const irep_idtmethod_identifier,
symbol_table_basetsymbol_table,
synthetic_methods_maptsynthetic_methods,
message_handlertmessage_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_idtinterface_id,
const namespacetns 
)
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_basetsymbol_table,
const size_t  index 
)
static

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

Parameters
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
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_idtidentifier,
const irep_idtbase_name,
const irep_idtpretty_name,
const typettype,
const irep_idtdeclaring_class,
symbol_table_basetsymbol_table,
message_handlertlog 
)
static

Definition at line 451 of file lambda_synthesis.cpp.

◆  get_unboxing_method()

static std::optional< irep_idt > get_unboxing_method ( const pointer_typetmaybe_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_maptsynthetic_methods,
const java_class_typet::methodtmethod_to_implement,
const irep_idtsynthetic_class_name 
)
static

Definition at line 337 of file lambda_synthesis.cpp.

◆  instantiate_new_object()

static symbol_exprt instantiate_new_object ( const irep_idtfunction_id,
const symboltlambda_method_symbol,
symbol_table_basetsymbol_table,
code_blocktresult 
)
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_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
Returns
the newly instantiated symbol

Definition at line 572 of file lambda_synthesis.cpp.

◆  invokedynamic_synthetic_constructor()

codet invokedynamic_synthetic_constructor ( const irep_idtfunction_id,
symbol_table_basetsymbol_table,
message_handlertmessage_handler 
)

Create invokedynamic synthetic constructor.

Definition at line 475 of file lambda_synthesis.cpp.

◆  invokedynamic_synthetic_method()

codet invokedynamic_synthetic_method ( const irep_idtfunction_id,
symbol_table_basetsymbol_table,
message_handlertmessage_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_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
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_basetsymbol_table,
const irep_idtmethod_identifier,
const java_method_typetdynamic_method_type 
)
static

Definition at line 77 of file lambda_synthesis.cpp.

◆  lambda_synthetic_class_name()

irep_idt lambda_synthetic_class_name ( const irep_idtmethod_identifier,
std::size_t  instruction_address 
)

Definition at line 37 of file lambda_synthesis.cpp.

◆  make_function_expr()

exprt make_function_expr ( const symboltfunction_symbol,
const symbol_table_basetsymbol_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_idtsynthetic_class_name,
const struct_tag_typetfunctional_interface_tag,
const java_method_typetdynamic_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_basetsymbol_table,
const struct_tag_typetfunctional_interface_tag,
const irep_idtmethod_identifier,
const int  instruction_address,
const messagetlog 
)
static

Definition at line 204 of file lambda_synthesis.cpp.

AltStyle によって変換されたページ (->オリジナル) /