Loading...

Searching...

No Matches

Classes | Functions

java_static_initializers.h File Reference

#include "synthetic_methods_map.h"
#include <unordered_set>
#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).

irep_idt user_specified_clinit_name (const irep_idt &class_name)

bool is_clinit_wrapper_function (const irep_idt &function_id)

Check if function_id is a clinit wrapper.

bool is_clinit_function (const irep_idt &function_id)

Check if function_id is a clinit.

bool is_user_specified_clinit_function (const irep_idt &function_id)

Check if function_id is a user-specified clinit.

void create_static_initializer_symbols (symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe, const bool is_user_clinit_needed)

Create static initializer wrappers and possibly user-specified functions for initial static field value assignments for all classes that need them.

code_blockt get_thread_safe_clinit_wrapper_body (const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)

Thread safe version of the static initializer.

code_ifthenelset get_clinit_wrapper_body (const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)

Produces the static initializer wrapper body for the given function.

std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols (const symbol_table_baset &symbol_table)

code_blockt get_user_specified_clinit_body (const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references, const std::unordered_multimap< irep_idt, symbolt > &class_to_declared_symbols_map)

Create the body of a user_specified_clinit function for a given class, which includes assignments for all static fields of the class to values read from an input file.

void create_stub_global_initializers (symbol_table_baset &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)

Function Documentation

◆ class_to_declared_symbols()

std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols ( const symbol_table_baset & symbol_table )

Returns: map associating classes to the symbols they declare

Definition at line 779 of file java_static_initializers.cpp.

◆ 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_name class symbol name

Returns: static initializer wrapper name

Definition at line 73 of file java_static_initializers.cpp.

◆ create_static_initializer_symbols()

void create_static_initializer_symbols ( symbol_table_baset & symbol_table,

synthetic_methods_mapt & synthetic_methods,

const bool thread_safe,

const bool is_user_clinit_needed

)

Create static initializer wrappers and possibly user-specified functions for initial static field value assignments for all classes that need them.

For each class that will require a static initializer wrapper, create a function named package.classname.<clinit_wrapper>, and a corresponding global tracking whether it has run or not. If a file containing initial static values is given, also create a function named package.classname::user_specified_clinit.

Parameters: 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.

is_user_clinit_needed determines whether or not a symbol for the synthetic user_specified_clinit function should be created. This is true if a file was given with the –static-values option and false otherwise.

Definition at line 874 of file java_static_initializers.cpp.

◆ create_stub_global_initializers()

void create_stub_global_initializers ( symbol_table_baset & 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_clinit_wrapper_body()

code_ifthenelset get_clinit_wrapper_body ( const irep_idt & function_id,

symbol_table_baset & symbol_table,

const bool nondet_static,

const bool replace_clinit,

const java_object_factory_parameterst & object_factory_parameters,

const select_pointer_typet & pointer_type_selector,

message_handlert & message_handler

)

Produces the static initializer wrapper body for the given function.

Note: this version of the clinit wrapper is not thread safe.

Parameters: 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

replace_clinit true iff calls to clinit are replaced with calls to user_specified_clinit.

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)

message_handler log output

Returns: the body of the static initializer wrapper

Definition at line 718 of file java_static_initializers.cpp.

◆ get_thread_safe_clinit_wrapper_body()

code_blockt get_thread_safe_clinit_wrapper_body ( const irep_idt & function_id,

symbol_table_baset & symbol_table,

const bool nondet_static,

const bool replace_clinit,

const java_object_factory_parameterst & object_factory_parameters,

const select_pointer_typet & pointer_type_selector,

message_handlert & message_handler

)

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:

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.

ATOMIC_BEGIN

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;

}

ATOMIC_END

if(init_complete)

return;

java::C'.<clinit_wrapper>();

java::I1.<clinit_wrapper>();

java::I2.<clinit_wrapper>();

// ...

java::In.<clinit_wrapper>();

java::C.<clinit>(); // or nondet-initialization of all static

// variables of C if nondet-static is true

// 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;

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

ATOMIC_END

@ ATOMIC_END

Definition goto_program.h:43

ATOMIC_BEGIN

@ ATOMIC_BEGIN

Definition goto_program.h:42

clinit_statest::INIT_COMPLETE

@ INIT_COMPLETE

clinit_statest::NOT_INIT

@ NOT_INIT

clinit_statest::IN_PROGRESS

@ IN_PROGRESS

Note: The current implementation does not deal with exceptions.

Parameters: 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

replace_clinit true iff calls to clinit are replaced with calls to user_specified_clinit.

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)

message_handler log output

Returns: the body of the static initializer wrapper

Definition at line 520 of file java_static_initializers.cpp.

◆ get_user_specified_clinit_body()

code_blockt get_user_specified_clinit_body ( const irep_idt & class_id,

const json_objectt & static_values_json,

symbol_table_baset & symbol_table,

std::optional< ci_lazy_methods_neededt > needed_lazy_methods,

size_t max_user_array_length,

std::unordered_map< std::string, object_creation_referencet > & references,

const std::unordered_multimap< irep_idt, symbolt > & class_to_declared_symbols_map

)

Create the body of a user_specified_clinit function for a given class, which includes assignments for all static fields of the class to values read from an input file.

If the file could not be parsed or an entry for this class could not be found in it, the user_specified_clinit function will only contain a call to the "real" clinit function, and not include any assignments itself. If an entry for this class is found but some of its static fields are not mentioned in the input file, those fields will be assigned default values (zero or null).

Parameters: class_id the id of the class to create a user_specified_clinit function body for.

static_values_json JSON object containing values of static fields. The format is expected to be a map whose keys are class names, and whose values are maps from static field names to values.

symbol_table used to look up and create new symbols

needed_lazy_methods used to mark any runtime types given in the input file as needed

max_user_array_length maximum value for constant or variable length arrays. Any arrays that were specified to be of nondeterministic length in the input file will be limited by this value.

references map to keep track of reference-equal objets.

class_to_declared_symbols_map map classes to the symbols that they declare.