cprover
|
#include "java_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... | |
code_blockt | get_thread_safe_clinit_wrapper_body (const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) |
Thread safe version of the static initializer. More... | |
code_ifthenelset | get_clinit_wrapper_body (const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) |
Produces the static initializer 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 java_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.
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 701 of file java_static_initializers.cpp.
void create_stub_global_initializers | ( | symbol_tablet & | symbol_table, |
const std::unordered_set< irep_idt > & | stub_globals_set, | ||
const java_object_factory_parameterst & | object_factory_parameters, | ||
const select_pointer_typet & | pointer_type_selector | ||
) |
code_ifthenelset get_clinit_wrapper_body | ( | const irep_idt & | function_id, |
symbol_table_baset & | symbol_table, | ||
const bool | nondet_static, | ||
const java_object_factory_parameterst & | object_factory_parameters, | ||
const select_pointer_typet & | pointer_type_selector | ||
) |
Produces the static initializer 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 |
nondet_static | true if nondet-static option was given |
object_factory_parameters | object factory parameters used to populate nondet-initialized globals and objects reachable from them (only needed if nondet-static is true) |
pointer_type_selector | used to choose concrete types for abstract- typed globals and fields (only needed if nondet-static is true) |
Definition at line 638 of file java_static_initializers.cpp.
code_blockt get_thread_safe_clinit_wrapper_body | ( | const irep_idt & | function_id, |
symbol_table_baset & | symbol_table, | ||
const bool | nondet_static, | ||
const java_object_factory_parameterst & | object_factory_parameters, | ||
const select_pointer_typet & | pointer_type_selector | ||
) |
Thread safe version of the static initializer.
Produces the static initializer 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 |
nondet_static | true if nondet-static option was given |
object_factory_parameters | object factory parameters used to populate nondet-initialized globals and objects reachable from them (only needed if nondet-static is true) |
pointer_type_selector | used to choose concrete types for abstract- typed globals and fields (only needed if nondet-static is true) |
Definition at line 448 of file java_static_initializers.cpp.
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.