Collaboration diagram for java_object_factoryt:

Public Member Functions
	java_object_factoryt (const source_locationt &loc, const java_object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector, message_handlert &log)

bool	gen_nondet_enum_init (code_blockt &assignments, const exprt &expr, const java_class_typet &java_class_type, const source_locationt &location)
	We nondet-initialize enums to be equal to one of the constants defined for their type: int i = nondet(int); assume(0 < = i < $VALUES.length); expr = $VALUES[i]; where $VALUES is a variable generated by the Java compiler and which gives the possible values of a particular enum subtype (this is the same array that is returned by Enum.values()). More...

void	gen_nondet_init (code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, const std::optional< typet > &override_type, size_t depth, update_in_placet, const source_locationt &location)
	Initializes a primitive-typed or reference-typed object tree rooted at `expr`, allocating child objects as necessary and nondet-initializing their members, or if MUST_UPDATE_IN_PLACE is set, re-initializing already-allocated objects. More...

void	add_created_symbol (const symbolt &symbol)

void	declare_created_symbols (code_blockt &init_code)

Private Member Functions
void	gen_pointer_target_init (code_blockt &assignments, const exprt &expr, const typet &target_type, lifetimet lifetime, size_t depth, update_in_placet update_in_place, const source_locationt &location)
	Initializes the pointer-typed lvalue expression `expr` to point to an object of type `target_type`, recursively nondet-initializing the members of that object. More...

void	gen_nondet_pointer_init (code_blockt &assignments, const exprt &expr, lifetimet lifetime, const pointer_typet &pointer_type, size_t depth, const update_in_placet &update_in_place, const source_locationt &location)
	Initializes a pointer `expr` of type `pointer_type` to a primitive-typed value or an object tree. More...

void	gen_nondet_struct_init (code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, const struct_typet &struct_type, size_t depth, const update_in_placet &update_in_place, const source_locationt &location)
	Initializes an object tree rooted at `expr`, allocating child objects as necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE is set, re-initializes already-allocated objects. More...

symbol_exprt	gen_nondet_subtype_pointer_init (code_blockt &assignments, lifetimet lifetime, const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location)
	Generate codet assignments to initalize the selected concrete type. More...

code_blockt	assign_element (const exprt &element, update_in_placet update_in_place, const typet &element_type, size_t depth, const source_locationt &location)
	Generate codet for assigning an individual element inside the array. More...

Private Attributes
const java_object_factory_parameterst	object_factory_parameters

std::unordered_set< irep_idt >	recursion_set
	This is employed in conjunction with the depth above. More...

generic_parameter_specialization_mapt	generic_parameter_specialization_map
	Every time the non-det generator visits a type and the type is generic (either a struct or a pointer), the following map is used to store and look up the concrete types of the generic parameters in the current scope. More...

symbol_table_baset &	symbol_table
	The symbol table. More...

const select_pointer_typet &	pointer_type_selector
	Resolves pointer types potentially using some heuristics, for example to replace pointers to interface types with pointers to concrete implementations. More...

allocate_objectst	allocate_objects

messaget	log
	Log for reporting warnings and errors in object creation. More...

Detailed Description

Definition at line 31 of file java_object_factory.cpp.

Constructor & Destructor Documentation

◆ java_object_factoryt()

java_object_factoryt::java_object_factoryt	(	const source_locationt &	loc,
		const java_object_factory_parameterst	_object_factory_parameters,
		symbol_table_baset &	_symbol_table,
		const select_pointer_typet &	pointer_type_selector,
		message_handlert &	log
	)

inline

Definition at line 73 of file java_object_factory.cpp.

Member Function Documentation

◆ add_created_symbol()

void java_object_factoryt::add_created_symbol ( const symbolt & symbol )

Definition at line 1115 of file java_object_factory.cpp.

◆ assign_element()

code_blockt java_object_factoryt::assign_element	(	const exprt &	element,
		update_in_placet	update_in_place,
		const typet &	element_type,
		size_t	depth,
		const source_locationt &	location
	)

private

Generate codet for assigning an individual element inside the array.

Parameters

element	The lhs expression that will be assigned the new element.
update_in_place	Should the code allow for the object to updated in place.
element_type	The type of the element to create.
depth	The depth in the object tree.
location	Source location to use for synthesized code

Returns: Synthesized code using the object factory to create an element of the type and assign it into element.

Definition at line 1230 of file java_object_factory.cpp.

◆ declare_created_symbols()

void java_object_factoryt::declare_created_symbols ( code_blockt & init_code )

Definition at line 1120 of file java_object_factory.cpp.

◆ gen_nondet_enum_init()

bool java_object_factoryt::gen_nondet_enum_init	(	code_blockt &	assignments,
		const exprt &	expr,
		const java_class_typet &	java_class_type,
		const source_locationt &	location
	)

We nondet-initialize enums to be equal to one of the constants defined for their type: int i = nondet(int); assume(0 < = i < $VALUES.length); expr = $VALUES[i]; where $VALUES is a variable generated by the Java compiler and which gives the possible values of a particular enum subtype (this is the same array that is returned by Enum.values()).

This may fail if the $VALUES static field is not present. Ensuring that field is in the symbol table when this method may be applicable is the driver program's responsibility: for example, ci_lazy_methods.cpp makes some effort to retain this field when a stub method might refer to it.

Returns: true on success

Definition at line 1473 of file java_object_factory.cpp.

◆ gen_nondet_init()

void java_object_factoryt::gen_nondet_init	(	code_blockt &	assignments,
		const exprt &	expr,
		bool	is_sub,
		bool	skip_classid,
		lifetimet	lifetime,
		const std::optional< typet > &	override_type,
		size_t	depth,
		update_in_placet	update_in_place,
		const source_locationt &	location
	)

Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects as necessary and nondet-initializing their members, or if MUST_UPDATE_IN_PLACE is set, re-initializing already-allocated objects.

Extra constraints might be added to initialized objects, based on options recorded in object_factory_parameters.

Parameters

assignments	A code block where the initializing assignments will be appended to.
expr	Lvalue expression to initialize.
is_sub	If true, `expr` is a substructure of a larger object, which in Java necessarily means a base class.
skip_classid	If true, skip initializing `@class_identifier`.
lifetime	Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
depth	Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing.
override_type	If not empty, initialize with `override_type` instead of `expr.type()`. Used at the moment for reference arrays, which are implemented as void* arrays but should be init'd as their true type with appropriate casts.
update_in_place	NO_UPDATE_IN_PLACE: initialize `expr` from scratch MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ and MUST_ cases. MUST_UPDATE_IN_PLACE: reinitialize an existing object
location	Source location associated with nondet-initialization.

Definition at line 998 of file java_object_factory.cpp.

◆ gen_nondet_pointer_init()

void java_object_factoryt::gen_nondet_pointer_init	(	code_blockt &	assignments,
		const exprt &	expr,
		lifetimet	lifetime,
		const pointer_typet &	pointer_type,
		size_t	depth,
		const update_in_placet &	update_in_place,
		const source_locationt &	location
	)

private

Initializes a pointer expr of type pointer_type to a primitive-typed value or an object tree.

It allocates child objects as necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE is set, re-initializes already-allocated objects.

Parameters

assignments	The code block we are building with initialization code.
expr	Pointer-typed lvalue expression to initialize.
lifetime	Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
depth	Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing.
pointer_type	The type of the pointer we are initalizing
update_in_place	NO_UPDATE_IN_PLACE: initialize `expr` from scratch MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ and MUST_ cases. MUST_UPDATE_IN_PLACE: reinitialize an existing object
location	Source location associated with nondet-initialization.

Definition at line 473 of file java_object_factory.cpp.

◆ gen_nondet_struct_init()

void java_object_factoryt::gen_nondet_struct_init	(	code_blockt &	assignments,
		const exprt &	expr,
		bool	is_sub,
		bool	skip_classid,
		lifetimet	lifetime,
		const struct_typet &	struct_type,
		size_t	depth,
		const update_in_placet &	update_in_place,
		const source_locationt &	location
	)

private

Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE is set, re-initializes already-allocated objects.

After initialization calls validation method expr.cproverNondetInitialize() if it was provided by the user.

Parameters

assignments	The code block to append the new instructions to
expr	Struct-typed lvalue expression to initialize
is_sub	If true, `expr` is a substructure of a larger object, which in Java necessarily means a base class
skip_classid	If true, skip initializing `@class_identifier`
lifetime	Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
struct_type	The type of the struct we are initializing
depth	Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing
update_in_place	Enum instance with the following meaning. NO_UPDATE_IN_PLACE: initialize `expr` from scratch MUST_UPDATE_IN_PLACE: reinitialize an existing object MAY_UPDATE_IN_PLACE: invalid input
location	Source location associated with nondet-initialization

Definition at line 764 of file java_object_factory.cpp.

◆ gen_nondet_subtype_pointer_init()

symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init	(	code_blockt &	assignments,
		lifetimet	lifetime,
		const pointer_typet &	replacement_pointer,
		size_t	depth,
		const source_locationt &	location
	)

private

Generate codet assignments to initalize the selected concrete type.

Generated code looks as follows (here A = replacement_pointer.subtype()):

// allocate memory for a new object, depends on lifetime A { ... } tmp_object;

// non-det init all the fields of A A.x = NONDET(...) A.y = NONDET(...)

// assign expr with a suitably casted pointer to new_object A * p = &tmp_object

Parameters

assignments	A block of code where we append the generated code
lifetime	Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
replacement_pointer	The type of the pointer we actually want to create
depth	Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing
location	Source location associated with nondet-initialization

Returns: A symbol expression of type replacement_pointer corresponding to a pointer to object tmp_object (see above)

Definition at line 692 of file java_object_factory.cpp.

◆ gen_pointer_target_init()

void java_object_factoryt::gen_pointer_target_init	(	code_blockt &	assignments,
		const exprt &	expr,
		const typet &	target_type,
		lifetimet	lifetime,
		size_t	depth,
		update_in_placet	update_in_place,
		const source_locationt &	location
	)

private

Initializes the pointer-typed lvalue expression expr to point to an object of type target_type, recursively nondet-initializing the members of that object.

Code emitted mainly depends on update_in_place:

When in NO_UPDATE_IN_PLACE mode, the code emitted looks like:

struct new_object obj; // depends on lifetime
<expr> := &obj
// recursive initialization of obj in NO_UPDATE_IN_PLACE mode

When in MUST_UPDATE_IN_PLACE mode, all code is emitted by a recursive call to gen_nondet_init in MUST_UPDATE_IN_PLACE mode, and looks like:

(*<expr>).some_int := NONDET(int)

(*<expr>).some_char := NONDET(char)

It is illegal to call the function with MAY_UPDATE_IN_PLACE.

Parameters

[out]	assignments	A code_blockt where the initialization code will be emitted to.
	expr	Pointer-typed lvalue expression to initialize. The pointed type equals `target_type`.
	target_type	Structure type to initialize, which may not match `expr` (for example, `expr` might be have type void). It cannot be a pointer to a primitive type because Java does not allow so.
	lifetime	Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
	depth	Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing.
	update_in_place	NO_UPDATE_IN_PLACE: initialize `expr` from scratch MUST_UPDATE_IN_PLACE: reinitialize an existing object MAY_UPDATE_IN_PLACE: invalid input
	location	Source location associated with nondet-initialization.

Definition at line 189 of file java_object_factory.cpp.

Member Data Documentation

◆ allocate_objects

allocate_objectst java_object_factoryt::allocate_objects

private

Definition at line 59 of file java_object_factory.cpp.

◆ generic_parameter_specialization_map

generic_parameter_specialization_mapt java_object_factoryt::generic_parameter_specialization_map

private

Every time the non-det generator visits a type and the type is generic (either a struct or a pointer), the following map is used to store and look up the concrete types of the generic parameters in the current scope.

Note that not all generic parameters need to have a concrete type, e.g., the method under test is generic. The types are removed from the map when the scope changes. Note that in different depths of the scope the parameters can be specialized with different types so we keep a stack of types for each parameter.

Definition at line 49 of file java_object_factory.cpp.

◆ log

messaget java_object_factoryt::log

private

Log for reporting warnings and errors in object creation.

Definition at line 62 of file java_object_factory.cpp.

◆ object_factory_parameters

const java_object_factory_parameterst java_object_factoryt::object_factory_parameters

private

Definition at line 33 of file java_object_factory.cpp.

◆ pointer_type_selector

const select_pointer_typet& java_object_factoryt::pointer_type_selector

private

Resolves pointer types potentially using some heuristics, for example to replace pointers to interface types with pointers to concrete implementations.

Definition at line 57 of file java_object_factory.cpp.

◆ recursion_set

std::unordered_set<irep_idt> java_object_factoryt::recursion_set

private

This is employed in conjunction with the depth above.

Every time the non-det generator visits a type, the type is added to this set. We forbid the non-det initialization when we see the type for the second time in this set AND the tree depth becomes >= than the maximum value above.

Definition at line 39 of file java_object_factory.cpp.

◆ symbol_table

symbol_table_baset& java_object_factoryt::symbol_table

private

The symbol table.

Definition at line 52 of file java_object_factory.cpp.

The documentation for this class was generated from the following file:

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_object_factory.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ java_object_factoryt()

Member Function Documentation

◆ add_created_symbol()

◆ assign_element()

◆ declare_created_symbols()

◆ gen_nondet_enum_init()

◆ gen_nondet_init()

◆ gen_nondet_pointer_init()

◆ gen_nondet_struct_init()

◆ gen_nondet_subtype_pointer_init()

◆ gen_pointer_target_init()

Member Data Documentation

◆ allocate_objects

◆ generic_parameter_specialization_map

◆ log

◆ object_factory_parameters

◆ pointer_type_selector

◆ recursion_set

◆ symbol_table