#include "java_static_initializers.h"
#include <util/arith_tools.h>
#include <util/cprover_prefix.h>
#include <util/json.h>
#include <util/std_code.h>
#include <util/suffix.h>
#include <util/symbol_table_base.h>
#include <goto-programs/class_hierarchy.h>
#include <goto-programs/goto_instruction_code.h>
#include "assignments_from_json.h"
#include "ci_lazy_methods_needed.h"
#include "java_object_factory.h"
#include "java_object_factory_parameters.h"
#include "java_types.h"
#include "java_utils.h"

Include dependency graph for java_static_initializers.cpp:

Enumerations
enum class	clinit_statest { NOT_INIT , IN_PROGRESS , INIT_COMPLETE }
	The three states in which a `<clinit>` method for a class can be before, after, and during static class initialization. More...

Functions
static typet	clinit_states_type ()

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

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

bool	is_clinit_function (const irep_idt &function_id)
	Check if function_id is a clinit. More...

bool	is_user_specified_clinit_function (const irep_idt &function_id)
	Check if function_id is a user-specified clinit. 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_frontend_assignt	gen_clinit_assign (const exprt &expr, const clinit_statest state)
	Generates a code_frontend_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 (symbol_table_baset &symbol_table, const irep_idt &class_name, code_blockt &init_body, 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)
	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_table_baset &symbol_table)
	Checks whether a static initializer wrapper is needed for a given class, i.e. More...

static void	create_function_symbol (const irep_idt &class_name, const irep_idt &function_name, const irep_idt &function_base_name, const synthetic_method_typet &synthetic_method_type, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods)

static void	create_clinit_wrapper_function_symbol (const irep_idt &class_name, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods)

static void	create_user_specified_clinit_function_symbol (const irep_idt &class_name, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods)

static void	create_clinit_wrapper_symbols (const irep_idt &class_name, symbol_table_baset &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...

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

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

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

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

template<class itertype >
static itertype	advance_to_next_key (itertype in, itertype end)
	Advance map iterator to next distinct key. More...

Variables
const std::string	clinit_wrapper_suffix = ".<clinit_wrapper>"

const std::string	user_specified_clinit_suffix = ".<user_specified_clinit>"

const std::string	clinit_function_suffix = ".<clinit>:()V"

Enumeration Type Documentation

◆ clinit_statest

enum clinit_statest

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 49 of file java_static_initializers.cpp.

Function Documentation

◆ add_new_variable_symbol()

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
	)

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 115 of file java_static_initializers.cpp.

◆ advance_to_next_key()

template<class itertype >

static itertype advance_to_next_key	(	itertype	in,
		itertype	end
	)

static

Advance map iterator to next distinct key.

Parameters

in	iterator to advance
end	end of container iterator

Definition at line 908 of file java_static_initializers.cpp.

◆ 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_already_run_variable_name()

static irep_idt clinit_already_run_variable_name ( const irep_idt & class_name )

static

Get name of the static-initialization-already-done global variable for a given class.

Parameters

class_name class symbol name

Returns: static initializer wrapper-already run global name

Definition at line 140 of file java_static_initializers.cpp.

◆ clinit_function_name()

static irep_idt clinit_function_name ( const irep_idt & class_name )

static

Get name of the real static initializer for a given class.

Doesn't check if a static initializer actually exists.

Parameters

class_name class symbol name

Returns: Static initializer symbol name

Definition at line 149 of file java_static_initializers.cpp.

◆ clinit_local_init_complete_var_name()

static irep_idt clinit_local_init_complete_var_name ( const irep_idt & class_name )

static

Get name of the static-initialization local variable for a given class.

Parameters

class_name class symbol name

Returns: static initializer wrapper-state local variable

Definition at line 175 of file java_static_initializers.cpp.

◆ clinit_state_var_name()

static irep_idt clinit_state_var_name ( const irep_idt & class_name )

static

Get name of the static-initialization-state global variable for a given class.

Parameters

class_name class symbol name

Returns: static initializer wrapper-state variable global name

Definition at line 158 of file java_static_initializers.cpp.

◆ clinit_states_type()

static typet clinit_states_type ( )

static

Definition at line 56 of file java_static_initializers.cpp.

◆ clinit_thread_local_state_var_name()

static irep_idt clinit_thread_local_state_var_name ( const irep_idt & class_name )

static

Get name of the static-initialization-state local state variable for a given class.

Parameters

class_name class symbol name

Returns: static initializer wrapper-state local state variable name

Definition at line 167 of file java_static_initializers.cpp.

◆ clinit_wrapper_do_recursive_calls()

static void clinit_wrapper_do_recursive_calls	(	symbol_table_baset &	symbol_table,
		const irep_idt &	class_name,
		code_blockt &	init_body,
		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
	)

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 clinit of C is made. If nondet-static option was given then all static variables that are not constants (i.e. final) are then re-assigned to a nondet value.

Parameters

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

Definition at line 229 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_clinit_wrapper_function_symbol()

static void create_clinit_wrapper_function_symbol	(	const irep_idt &	class_name,
		symbol_table_baset &	symbol_table,
		synthetic_methods_mapt &	synthetic_methods
	)

static

Definition at line 356 of file java_static_initializers.cpp.

◆ create_clinit_wrapper_symbols()

static void create_clinit_wrapper_symbols	(	const irep_idt &	class_name,
		symbol_table_baset &	symbol_table,
		synthetic_methods_mapt &	synthetic_methods,
		const bool	thread_safe
	)

static

Creates a static initializer wrapper symbol for the given class, along with a global boolean that tracks if it has been run already.

Parameters

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 395 of file java_static_initializers.cpp.

◆ create_function_symbol()

static void create_function_symbol	(	const irep_idt &	class_name,
		const irep_idt &	function_name,
		const irep_idt &	function_base_name,
		const synthetic_method_typet &	synthetic_method_type,
		symbol_table_baset &	symbol_table,
		synthetic_methods_mapt &	synthetic_methods
	)

static

Definition at line 328 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_user_specified_clinit_function_symbol()

static void create_user_specified_clinit_function_symbol	(	const irep_idt &	class_name,
		symbol_table_baset &	symbol_table,
		synthetic_methods_mapt &	synthetic_methods
	)

static

Definition at line 371 of file java_static_initializers.cpp.

◆ gen_clinit_assign()

static code_frontend_assignt gen_clinit_assign	(	const exprt &	expr,
		const clinit_statest	state
	)

static

Generates a code_frontend_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_frontend_assignt, assigning expr to the integer representation of state

Definition at line 189 of file java_static_initializers.cpp.

◆ gen_clinit_eqexpr()

static equal_exprt gen_clinit_eqexpr	(	const exprt &	expr,
		const clinit_statest	state
	)

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 205 of file java_static_initializers.cpp.

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

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.

Returns: the body of the user_specified_clinit function as a code block.

Definition at line 791 of file java_static_initializers.cpp.

◆ is_clinit_function()

bool is_clinit_function ( const irep_idt & function_id )

Check if function_id is a clinit.

Parameters

function_id some function identifier

Returns: true if the passed identifier is a clinit

Definition at line 94 of file java_static_initializers.cpp.

◆ is_clinit_wrapper_function()

bool is_clinit_wrapper_function ( const irep_idt & function_id )

Check if function_id is a clinit wrapper.

Parameters

function_id some function identifier

Returns: true if the passed identifier is a clinit wrapper

Definition at line 86 of file java_static_initializers.cpp.

◆ is_user_specified_clinit_function()

bool is_user_specified_clinit_function ( const irep_idt & function_id )

Check if function_id is a user-specified clinit.

Parameters

function_id some function identifier

Returns: true if the passed identifier is a clinit

Definition at line 102 of file java_static_initializers.cpp.

◆ needs_clinit_wrapper()

static bool needs_clinit_wrapper	(	const irep_idt &	class_name,
		const symbol_table_baset &	symbol_table
	)

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.

Parameters

class_name	class symbol name
symbol_table	global symbol table

Returns: true if a static initializer wrapper is needed

Definition at line 306 of file java_static_initializers.cpp.

◆ user_specified_clinit_name()

irep_idt user_specified_clinit_name ( const irep_idt & class_name )

Definition at line 78 of file java_static_initializers.cpp.

Variable Documentation

◆ clinit_function_suffix

const std::string clinit_function_suffix = ".<clinit>:()V"

Definition at line 65 of file java_static_initializers.cpp.

◆ clinit_wrapper_suffix

const std::string clinit_wrapper_suffix = ".<clinit_wrapper>"

Definition at line 63 of file java_static_initializers.cpp.

◆ user_specified_clinit_suffix

const std::string user_specified_clinit_suffix = ".<user_specified_clinit>"

Definition at line 64 of file java_static_initializers.cpp.

Enumerations

Functions

Variables

Enumeration Type Documentation

◆ clinit_statest

Function Documentation

◆ add_new_variable_symbol()

◆ advance_to_next_key()

◆ class_to_declared_symbols()

◆ clinit_already_run_variable_name()

◆ clinit_function_name()

◆ clinit_local_init_complete_var_name()

◆ clinit_state_var_name()

◆ clinit_states_type()

◆ clinit_thread_local_state_var_name()

◆ clinit_wrapper_do_recursive_calls()

◆ clinit_wrapper_name()

◆ create_clinit_wrapper_function_symbol()

◆ create_clinit_wrapper_symbols()

◆ create_function_symbol()

◆ create_static_initializer_symbols()

◆ create_user_specified_clinit_function_symbol()

◆ gen_clinit_assign()

◆ gen_clinit_eqexpr()

◆ get_clinit_wrapper_body()

◆ get_thread_safe_clinit_wrapper_body()

◆ get_user_specified_clinit_body()

◆ is_clinit_function()

◆ is_clinit_wrapper_function()

◆ is_user_specified_clinit_function()

◆ needs_clinit_wrapper()

◆ user_specified_clinit_name()

Variable Documentation

◆ clinit_function_suffix

◆ clinit_wrapper_suffix

◆ user_specified_clinit_suffix