cprover
java_static_initializers.h File Reference
#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>
Include dependency graph for java_static_initializers.h:
This graph shows which files directly or indirectly include this file:

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)
 

Function Documentation

◆ clinit_wrapper_name()

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).

Doesn't check whether the symbol actually exists

Parameters
class_nameclass symbol name
Returns
static initializer wrapper 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().

◆ 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.

Parameters
symbol_tableglobal symbol table
synthetic_methodssynthetic 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_safeif 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().

◆ create_stub_global_initializers()

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_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.

Parameters
function_idclinit wrapper function id (the wrapper_method_symbol name created by create_clinit_wrapper_symbols)
symbol_tableglobal symbol table
Returns
the body of the static initialiser wrapper/

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().

◆ get_thread_safe_clinit_wrapper_body()

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:

bool init_complete;
if(java::C::__CPROVER_PREFIX_clinit_thread_local_state == INIT_COMPLETE)
{
return;
}
java::C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
// This thread atomically checks and sets the global variable
// 'clinit_state' in order to ensure that only this thread runs the
// static initializer. The assume() statement below will prevent the SAT
// solver from producing a thread schedule where more than 1 thread is
// running the initializer. At the end of this function the only
// thread that runs the static initializer will update the variable.
// Alternatively we could have done a busy wait / spin-lock, but that
// would achieve the same effect and blow up the size of the SAT formula.
assume(java::C::__CPROVER_PREFIX_clinit_state != IN_PROGRESS)
if(java::C::__CPROVER_PREFIX_clinit_state == NOT_INIT)
{
java::C::__CPROVER_PREFIX_clinit_state = IN_PROGRESS
init_complete = false;
}
else if(java::C::__CPROVER_PREFIX_clinit_state == INIT_COMPLETE)
{
init_complete = true;
}
if(init_complete)
return;
java::C'::clinit_wrapper();
java::I1::clinit_wrapper();
java::I2::clinit_wrapper();
// ...
java::In::clinit_wrapper();
java::C::<clinit>();
// Setting this variable to INIT_COMPLETE will let other threads "cross"
// beyond the assume() statement above in this function.
ATOMIC_START
C::__CPROVER_PREFIX_clinit_state = INIT_COMPLETE;
ATOMIC_END
return;

Note: The current implementation does not deal with exceptions.

Parameters
function_idclinit wrapper function id (the wrapper_method_symbol name created by create_clinit_wrapper_symbols)
symbol_tableglobal symbol table
Returns
the body of the static initialiser wrapper

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().

◆ is_clinit_wrapper_function()

bool is_clinit_wrapper_function ( const irep_idt function_id)

Check if function_id is a clinit wrapper.

Parameters
function_idsome function identifier
Returns
true if the passed identifier is a clinit wrapper

Definition at line 68 of file java_static_initializers.cpp.

References clinit_wrapper_suffix, has_suffix(), and id2string().