cprover
|
#include "object_factory_parameters.h"
#include "select_pointer_type.h"
#include "synthetic_methods_map.h"
#include <unordered_set>
#include <util/symbol_table.h>
#include <util/std_code.h>
Go to the source code of this file.
Classes | |
class | stub_global_initializer_factoryt |
Functions | |
irep_idt | clinit_wrapper_name (const irep_idt &class_name) |
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initialization has already been done before invoking the real static initializer if not). More... | |
bool | is_clinit_wrapper_function (const irep_idt &function_id) |
Check if function_id is a clinit wrapper. More... | |
void | create_static_initializer_wrappers (symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe) |
Create static initializer wrappers for all classes that need them. More... | |
codet | get_thread_safe_clinit_wrapper_body (const irep_idt &function_id, symbol_table_baset &symbol_table) |
Thread safe version of the static initialiser. More... | |
codet | get_clinit_wrapper_body (const irep_idt &function_id, symbol_table_baset &symbol_table) |
Produces the static initialiser wrapper body for the given function. More... | |
void | create_stub_global_initializers (symbol_tablet &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) |
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initialization has already been done before invoking the real static initializer if not).
Doesn't check whether the symbol actually exists
class_name | class symbol name |
Definition at line 60 of file java_static_initializers.cpp.
References clinit_wrapper_suffix, and id2string().
Referenced by clinit_wrapper_do_recursive_calls(), create_clinit_wrapper_symbols(), java_bytecode_convert_methodt::get_clinit_call(), get_thread_safe_clinit_wrapper_body(), and needs_clinit_wrapper().
void create_static_initializer_wrappers | ( | symbol_tablet & | symbol_table, |
synthetic_methods_mapt & | synthetic_methods, | ||
const bool | thread_safe | ||
) |
Create static initializer wrappers for all classes that need them.
symbol_table | global symbol table |
synthetic_methods | synthetic methods map. Will be extended noting that any wrapper belongs to this code, and so get_clinit_wrapper_body should be used to produce the method body when required. |
thread_safe | if true state variables required to make the clinit_wrapper thread safe will be created. |
Definition at line 627 of file java_static_initializers.cpp.
References create_clinit_wrapper_symbols(), needs_clinit_wrapper(), class_hierarchy_grapht::populate(), and grapht< N >::topsort().
Referenced by java_bytecode_languaget::typecheck().
void create_stub_global_initializers | ( | symbol_tablet & | symbol_table, |
const std::unordered_set< irep_idt > & | stub_globals_set, | ||
const object_factory_parameterst & | object_factory_parameters, | ||
const select_pointer_typet & | pointer_type_selector | ||
) |
codet get_clinit_wrapper_body | ( | const irep_idt & | function_id, |
symbol_table_baset & | symbol_table | ||
) |
Produces the static initialiser wrapper body for the given function.
Note: this version of the clinit wrapper is not thread safe.
function_id | clinit wrapper function id (the wrapper_method_symbol name created by create_clinit_wrapper_symbols ) |
symbol_table | global symbol table |
Definition at line 566 of file java_static_initializers.cpp.
References clinit_already_run_variable_name(), clinit_wrapper_do_recursive_calls(), code_ifthenelset::cond(), dstringt::empty(), irept::get(), INVARIANT, symbol_table_baset::lookup_ref(), exprt::move_to_operands(), and symbolt::type.
Referenced by java_bytecode_languaget::convert_single_method().
codet get_thread_safe_clinit_wrapper_body | ( | const irep_idt & | function_id, |
symbol_table_baset & | symbol_table | ||
) |
Thread safe version of the static initialiser.
Produces the static initialiser wrapper body for the given function. This static initializer implements (a simplification of) the algorithm defined in Section 5.5 of the JVM Specs. This function, or wrapper, checks whether static init has already taken place, calls the actual <clinit>
method if not, and possibly recursively initializes super-classes and interfaces. Assume that C is the class to be initialized and that C extends C' and implements interfaces I1 ... In, then the algorithm is as follows:
Note: The current implementation does not deal with exceptions.
function_id | clinit wrapper function id (the wrapper_method_symbol name created by create_clinit_wrapper_symbols ) |
symbol_table | global symbol table |
Definition at line 386 of file java_static_initializers.cpp.
References code_blockt::add(), add_new_variable_symbol(), exprt::add_source_location(), code_blockt::append(), clinit_local_init_complete_var_name(), clinit_state_var_name(), clinit_thread_local_state_var_name(), clinit_wrapper_do_recursive_calls(), clinit_wrapper_name(), comment(), code_ifthenelset::cond(), code_ifthenelset::else_case(), dstringt::empty(), gen_clinit_assign(), gen_clinit_eqexpr(), irept::get(), IN_PROGRESS, INIT_COMPLETE, INVARIANT, symbol_table_baset::lookup_ref(), NOT_INIT, source_locationt::set_file(), source_locationt::set_function(), source_locationt::set_line(), symbolt::symbol_expr(), code_ifthenelset::then_case(), and symbolt::type.
Referenced by java_bytecode_languaget::convert_single_method().
bool is_clinit_wrapper_function | ( | const irep_idt & | function_id | ) |
Check if function_id is a clinit wrapper.
function_id | some function identifier |
Definition at line 68 of file java_static_initializers.cpp.
References clinit_wrapper_suffix, has_suffix(), and id2string().