This module is responsible for the synthesis of code (in the form of a sequence of codet statements) that can allocate and initialize non-deterministically both primitive Java types and objects. More...

#include "nondet.h"
#include <goto-programs/allocate_objects.h>
#include <util/std_code.h>

Include dependency graph for java_object_factory.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs
using	array_element_generatort = std::function< code_blockt(const exprt &element_at_counter, const typet &element_type)>

Enumerations
enum class	update_in_placet { NO_UPDATE_IN_PLACE , MAY_UPDATE_IN_PLACE , MUST_UPDATE_IN_PLACE }

Functions
exprt	object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, lifetimet lifetime, const source_locationt &location, const select_pointer_typet &pointer_type_selector, message_handlert &log)
	Similar to `gen_nondet_init` below, but instead of allocating and non-deterministically initializing the the argument `expr` passed to that function, we create a static global object of type `type` and non-deterministically initialize it. More...

exprt	object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, const java_object_factory_parameterst &object_factory_parameters, lifetimet lifetime, const source_locationt &location, message_handlert &log)
	Call object_factory() above with a default (identity) pointer_type_selector. More...

void	gen_nondet_init (const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
	Initializes a primitive-typed or reference-typed object tree rooted at `expr`, allocating child objects as necessary and nondet-initializing their members, or if MAY_ or MUST_UPDATE_IN_PLACE is set, re-initializing already-allocated objects. More...

void	gen_nondet_init (const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place, message_handlert &log)
	Call gen_nondet_init() above with a default (identity) pointer_type_selector. More...

code_blockt	gen_nondet_array_init (const exprt &expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_table_baset &symbol_table, size_t max_nondet_array_length)
	Synthesize GOTO for generating a array of nondet length to be stored in the `expr`. More...

Detailed Description

This module is responsible for the synthesis of code (in the form of a sequence of codet statements) that can allocate and initialize non-deterministically both primitive Java types and objects.

The non-deterministic initialization of one object triggers the non-deterministic initialization of all its fields, which in turn could be references to other objects. We thus speak about an object tree.

This is useful for, e.g., the creation of a verification harness (non-det initialization of the parameters of the method to verify), mocking methods that are called but for which we don't have a body (overapproximating the return value and possibly side effects).

The two main APIs are gen_nondet_init() and object_factory() (which calls gen_nondet_init()), at the bottom of the file. A call to

gen_nondet_init(expr, code, ..., update_in_place)

appends to code (a code_blockt) a sequence of statements that non-deterministically initialize the expr (which is expected to be an l-value exprt) with a primitive or reference value of type equal to or compatible with expr.type() – see documentation for the argument pointer_type_selector for additional details. gen_nondet_init() is the starting point of a recursive algorithm, and most other functions in this file are different (recursive or base) cases depending on the type of expr.

The code generated mainly depends on the parameter update_in_place. Assume that expr is a reference to an object (in our IR, that means a pointer to a struct).

When update_in_place == NO_UPDATE_IN_PLACE, the following code is generated:

struct MyClass object;
if (NONDET(bool))
  expr = NULL;
else
  expr = &object;
  ... // non-det initialization of `object` in NO_UPDATE_IN_PLACE mode

When update_in_place == MUST_UPDATE_IN_PLACE, the following code is generated (assuming that MyClass has fields "int x" and "OtherClass y"):

expr->x = NONDET(int);

expr->y = ... // non-det initialization in MUST_UPDATE_IN_PLACE mode

When update_in_place == MAY_UPDATE_IN_PLACE, the following code is generated:

if (NONDET(bool))
  ... // non-det initialization of `expr` in MUST_UPDATE_IN_PLACE
else
  ... // non-det initialization of `expr` in NO_UPDATE_IN_PLACE

Definition in file java_object_factory.h.

Typedef Documentation

◆ array_element_generatort

using array_element_generatort = std::function< code_blockt(const exprt &element_at_counter, const typet &element_type)>

Definition at line 136 of file java_object_factory.h.

Enumeration Type Documentation

◆ update_in_placet

enum update_in_placet

strong

Enumerator
NO_UPDATE_IN_PLACE
MAY_UPDATE_IN_PLACE
MUST_UPDATE_IN_PLACE

Definition at line 106 of file java_object_factory.h.

Function Documentation

◆ gen_nondet_array_init()

code_blockt gen_nondet_array_init	(	const exprt &	expr,
		update_in_placet	update_in_place,
		const source_locationt &	location,
		const array_element_generatort &	element_generator,
		const allocate_local_symbolt &	allocate_local_symbol,
		const symbol_table_baset &	symbol_table,
		size_t	max_nondet_array_length
	)

Synthesize GOTO for generating a array of nondet length to be stored in the expr.

Parameters

expr	The array expression to initialize.
update_in_place	Should the code allow the solver the freedom to leave the array as is.
location	Source location to use for all synthesized code.
element_generator	A function that creates a new element and assigns it to the provided expression.
allocate_local_symbol	A function that creates a local symbol in the symbol table. See java_object_factoryt::assign_element for an example implementation.
symbol_table	The symbol table.
max_nondet_array_length	The maximum size the array can be.

Returns: The GOTO that approximates:
array_length = NONDET(int)

ASSUME(array_length < max_nondet_array_length)

expr = java_new_array(max_nondet_array_length)

expr->length = array_length

for (int i = 0; i < array_length; ++i)

`element_generator()`

ASSUME
@ ASSUME
Definition: goto_program.h:35

Definition at line 1375 of file java_object_factory.cpp.

◆ gen_nondet_init() [1/2]

void gen_nondet_init	(	const exprt &	expr,
		code_blockt &	init_code,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		bool	skip_classid,
		lifetimet	lifetime,
		const java_object_factory_parameterst &	object_factory_parameters,
		const select_pointer_typet &	pointer_type_selector,
		update_in_placet	update_in_place,
		message_handlert &	log
	)

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

Parameters

	expr	Lvalue expression to initialize.
[out]	init_code	A code block where the initializing assignments will be appended to. It gets an instruction sequence to initialize or reinitialize `expr` and child objects it refers to.
	symbol_table	The symbol table, where new variables created as a result of emitting code to `init_code` will be inserted to. This includes any necessary temporaries, and if `create_dyn_objs` is false, any allocated objects.
	loc	Source location to which all generated code will be associated to.
	skip_classid	If true, skip initializing field `@class_identifier`.
	lifetime	Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
	object_factory_parameters	Parameters for the generation of non deterministic objects.
	pointer_type_selector	The pointer_selector to use to resolve pointer types where required.
	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
	log	used to report object construction warnings and failures

Definition at line 1623 of file java_object_factory.cpp.

◆ gen_nondet_init() [2/2]

void gen_nondet_init	(	const exprt &	expr,
		code_blockt &	init_code,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		bool	skip_classid,
		lifetimet	lifetime,
		const java_object_factory_parameterst &	object_factory_parameters,
		update_in_placet	update_in_place,
		message_handlert &	log
	)

Call gen_nondet_init() above with a default (identity) pointer_type_selector.

Definition at line 1680 of file java_object_factory.cpp.

◆ object_factory() [1/2]

exprt object_factory	(	const typet &	type,
		const irep_idt	base_name,
		code_blockt &	init_code,
		symbol_table_baset &	symbol_table,
		const java_object_factory_parameterst &	object_factory_parameters,
		lifetimet	lifetime,
		const source_locationt &	location,
		message_handlert &	log
	)

Call object_factory() above with a default (identity) pointer_type_selector.

Definition at line 1656 of file java_object_factory.cpp.

◆ object_factory() [2/2]

exprt object_factory	(	const typet &	type,
		const irep_idt	base_name,
		code_blockt &	init_code,
		symbol_table_baset &	symbol_table,
		java_object_factory_parameterst	parameters,
		lifetimet	lifetime,
		const source_locationt &	loc,
		const select_pointer_typet &	pointer_type_selector,
		message_handlert &	log
	)

Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing the the argument expr passed to that function, we create a static global object of type type and non-deterministically initialize it.

See gen_nondet_init for a description of the parameters. The only new one is type, which is the type of the object to create.

Returns: The object created, the symbol_table gains any new symbols created, and init_code gains any instructions required to initialize either the returned value or its child objects

Definition at line 1546 of file java_object_factory.cpp.

Typedefs

Enumerations

Functions