cprover
|
#include "java_static_initializers.h"
#include "java_object_factory.h"
#include "java_utils.h"
#include <goto-programs/class_hierarchy.h>
#include <util/std_types.h>
#include <util/std_expr.h>
#include <util/std_code.h>
#include <util/suffix.h>
#include <util/arith_tools.h>
Go to the source code of this file.
Enumerations | |
enum | clinit_statest { clinit_statest::NOT_INIT, clinit_statest::IN_PROGRESS, clinit_statest::INIT_COMPLETE } |
The three states in which a <clinit> method for a class can be before, after, and during static class initialization. More... | |
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... | |
static symbolt | add_new_variable_symbol (symbol_table_baset &symbol_table, const irep_idt &name, const typet &type, const exprt &value, const bool is_thread_local, const bool is_static_lifetime) |
Add a new symbol to the symbol table. More... | |
static irep_idt | clinit_already_run_variable_name (const irep_idt &class_name) |
Get name of the static-initialization-already-done global variable for a given class. More... | |
static irep_idt | clinit_function_name (const irep_idt &class_name) |
Get name of the real static initializer for a given class. More... | |
static irep_idt | clinit_state_var_name (const irep_idt &class_name) |
Get name of the static-initialization-state global variable for a given class. More... | |
static irep_idt | clinit_thread_local_state_var_name (const irep_idt &class_name) |
Get name of the static-initialization-state local state variable for a given class. More... | |
static irep_idt | clinit_local_init_complete_var_name (const irep_idt &class_name) |
Get name of the static-initialization local variable for a given class. More... | |
static code_assignt | gen_clinit_assign (const exprt &expr, const clinit_statest state) |
Generates a code_assignt for clinit_statest /param expr: expression to be used as the LHS of generated assignment. More... | |
static equal_exprt | gen_clinit_eqexpr (const exprt &expr, const clinit_statest state) |
Generates an equal_exprt for clinit_statest /param expr: expression to be used as the LHS of generated eqaul exprt. More... | |
static void | clinit_wrapper_do_recursive_calls (const symbol_tablet &symbol_table, const irep_idt &class_name, code_blockt &init_body) |
Generates codet that iterates through the base types of the class specified by class_name, C, and recursively adds calls to their clinit wrapper. More... | |
static bool | needs_clinit_wrapper (const irep_idt &class_name, const symbol_tablet &symbol_table) |
Checks whether a static initializer wrapper is needed for a given class, i.e. More... | |
static void | create_clinit_wrapper_symbols (const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe) |
Creates a static initializer wrapper symbol for the given class, along with a global boolean that tracks if it has been run already. 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_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... | |
template<class itertype > | |
static itertype | advance_to_next_key (itertype in, itertype end) |
Advance map iterator to next distinct key. More... | |
Variables | |
const typet | clinit_states_type = java_byte_type() |
const std::string | clinit_wrapper_suffix = "::clinit_wrapper" |
const std::string | clinit_function_suffix = ".<clinit>:()V" |
|
strong |
The three states in which a <clinit>
method for a class can be before, after, and during static class initialization.
These states are only used when the thread safe version of the clinit wrapper is generated.
According to the JVM Spec document (section 5.5), the JVM needs to maintain, for every class initializer, a state indicating whether the initializer has been executed, is being executed, or has raised errors. The spec mandates that the JVM consider 4 different states (not initialized, being initialized, ready for use, and initialization error). The clinit_statet
is a simplification of those 4 states where:
NOT_INIT
corresponds to "not initialized" IN_PROGRESS
corresponds to "some thread is currently running the
`<clinit>` and no other thread should run it" INIT_COMPLETE
corresponds to "the `<clinit>` has been executed and the
class is ready to be used, or it has errored"
The last state corresponds to a fusion of the two original states "ready for use" and "initialization error". The basis for fusing these states is that for simplification reasons both implementations of the clinit wrapper do not handle exceptions, hence the error state is not possible.
Enumerator | |
---|---|
NOT_INIT | |
IN_PROGRESS | |
INIT_COMPLETE |
Definition at line 40 of file java_static_initializers.cpp.
|
static |
Add a new symbol to the symbol table.
Note: assumes that a symbol with this name does not exist. /param name: name of the symbol to be generated /param type: type of the symbol to be generated /param value: initial value of the symbol to be generated /param is_thread_local: if true this symbol will be set as thread local /param is_static_lifetime: if true this symbol will be set as static /return returns new symbol.
Definition at line 81 of file java_static_initializers.cpp.
References symbol_table_baset::add(), symbolt::base_name, symbolt::is_lvalue, symbolt::is_state_var, symbolt::is_static_lifetime, symbolt::is_thread_local, symbolt::mode, symbolt::name, symbolt::pretty_name, symbolt::type, and symbolt::value.
Referenced by create_clinit_wrapper_symbols(), and get_thread_safe_clinit_wrapper_body().
|
static |
Advance map iterator to next distinct key.
in | iterator to advance |
end | end of container iterator |
Definition at line 654 of file java_static_initializers.cpp.
References PRECONDITION.
Referenced by stub_global_initializer_factoryt::create_stub_global_initializer_symbols().
Get name of the static-initialization-already-done global variable for a given class.
class_name | class symbol name |
Definition at line 108 of file java_static_initializers.cpp.
References id2string().
Referenced by create_clinit_wrapper_symbols(), and get_clinit_wrapper_body().
Get name of the real static initializer for a given class.
Doesn't check if a static initializer actually exists.
class_name | class symbol name |
Definition at line 117 of file java_static_initializers.cpp.
References clinit_function_suffix, and id2string().
Referenced by clinit_wrapper_do_recursive_calls(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), and needs_clinit_wrapper().
Get name of the static-initialization local variable for a given class.
class_name | class symbol name |
Definition at line 143 of file java_static_initializers.cpp.
References CPROVER_PREFIX, and id2string().
Referenced by get_thread_safe_clinit_wrapper_body().
Get name of the static-initialization-state global variable for a given class.
class_name | class symbol name |
Definition at line 126 of file java_static_initializers.cpp.
References CPROVER_PREFIX, and id2string().
Referenced by create_clinit_wrapper_symbols(), and get_thread_safe_clinit_wrapper_body().
Get name of the static-initialization-state local state variable for a given class.
class_name | class symbol name |
Definition at line 135 of file java_static_initializers.cpp.
References CPROVER_PREFIX, and id2string().
Referenced by create_clinit_wrapper_symbols(), and get_thread_safe_clinit_wrapper_body().
|
static |
Generates codet that iterates through the base types of the class specified by class_name, C, and recursively adds calls to their clinit wrapper.
Finally a call to the clinint wrapper of C is made.
symbol_table | symbol table | |
class_name | name of the class to generate clinit wrapper calls for | |
[out] | init_body | appended with calls to clinit wrapper |
Definition at line 186 of file java_static_initializers.cpp.
References class_typet::bases(), clinit_function_name(), clinit_wrapper_name(), code_function_callt::function(), symbol_table_baset::lookup_ref(), exprt::move_to_operands(), symbol_table_baset::symbols, to_class_type(), to_symbol_type(), and symbolt::type.
Referenced by get_clinit_wrapper_body(), and get_thread_safe_clinit_wrapper_body().
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().
|
static |
Creates a static initializer wrapper symbol for the given class, along with a global boolean that tracks if it has been run already.
class_name | class symbol name |
symbol_table | global symbol table; will gain a clinit_wrapper symbol and a corresponding has-run-already global. |
synthetic_methods | synthetic method type map. The new clinit wrapper symbol will be recorded, such that we get a callback to produce its body if and when required. |
thread_safe | if true state variables required to make the clinit_wrapper thread safe will be created. |
Definition at line 250 of file java_static_initializers.cpp.
References symbol_table_baset::add(), add_new_variable_symbol(), symbolt::base_name, clinit_already_run_variable_name(), clinit_state_var_name(), clinit_states_type, clinit_thread_local_state_var_name(), clinit_wrapper_name(), from_integer(), INVARIANT, symbolt::mode, symbolt::name, NOT_INIT, symbolt::pretty_name, irept::set(), STATIC_INITIALIZER_WRAPPER, and symbolt::type.
Referenced by create_static_initializer_wrappers().
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 626 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().
|
static |
Generates a code_assignt for clinit_statest /param expr: expression to be used as the LHS of generated assignment.
/param state: execution state of the clint_wrapper, used as the RHS of the generated assignment. /return returns a code_assignt, assigning expr
to the integer representation of state
Definition at line 157 of file java_static_initializers.cpp.
References clinit_states_type, and from_integer().
Referenced by get_thread_safe_clinit_wrapper_body().
|
static |
Generates an equal_exprt for clinit_statest /param expr: expression to be used as the LHS of generated eqaul exprt.
/param state: execution state of the clint_wrapper, used as the RHS of the generated equal exprt. /return returns a equal_exprt, equating expr
to the integer representation of state
Definition at line 173 of file java_static_initializers.cpp.
References clinit_states_type, and from_integer().
Referenced by get_thread_safe_clinit_wrapper_body().
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 565 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 385 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().
|
static |
Checks whether a static initializer wrapper is needed for a given class, i.e.
if the given class or any superclass has a static initializer.
class_name | class symbol name |
symbol_table | global symbol table |
Definition at line 219 of file java_static_initializers.cpp.
References class_typet::bases(), clinit_function_name(), clinit_wrapper_name(), symbol_table_baset::has_symbol(), symbol_table_baset::lookup_ref(), to_class_type(), to_symbol_type(), and symbolt::type.
Referenced by create_static_initializer_wrappers().
const std::string clinit_function_suffix = ".<clinit>:()V" |
Definition at line 52 of file java_static_initializers.cpp.
Referenced by clinit_function_name().
const typet clinit_states_type = java_byte_type() |
Definition at line 47 of file java_static_initializers.cpp.
Referenced by create_clinit_wrapper_symbols(), gen_clinit_assign(), and gen_clinit_eqexpr().
const std::string clinit_wrapper_suffix = "::clinit_wrapper" |
Definition at line 51 of file java_static_initializers.cpp.
Referenced by clinit_wrapper_name(), and is_clinit_wrapper_function().