#include "java_object_factory.h"
#include <util/arith_tools.h>
#include <util/array_element_from_pointer.h>
#include <util/expr_initializer.h>
#include <util/fresh_symbol.h>
#include <util/message.h>
#include <util/nondet_bool.h>
#include <util/prefix.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_functions.h>
#include <util/interval_constraint.h>
#include "generic_parameter_specialization_map_keys.h"
#include "java_object_factory_parameters.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "java_string_literals.h"
#include "java_utils.h"
#include "select_pointer_type.h"

Include dependency graph for java_object_factory.cpp:

Classes
class	java_object_factoryt

class	recursion_set_entryt
	Recursion-set entry owner class. More...

Functions
static irep_idt	integer_interval_to_string (const integer_intervalt &interval)
	Converts and integer_intervalt to a a string of the for [lower]-[upper]. More...

void	initialize_nondet_string_fields (struct_exprt &struct_expr, code_blockt &code, const std::size_t &min_nondet_string_length, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable, allocate_objectst &allocate_objects)
	Initialise length and data fields for a nondeterministic String structure. More...

alternate_casest	get_string_input_values_code (const exprt &expr, const std::list< std::string > &string_input_values, symbol_table_baset &symbol_table)
	Creates an alternate_casest vector in which each item contains an assignment of a string from `string_input_values` (or more precisely the literal symbol corresponding to the string) to `expr`. More...

static code_blockt	assume_expr_integral (const exprt &expr, const typet &type, const source_locationt &location, const allocate_local_symbolt &allocate_local_symbol)
	Generate code block that verifies that an expression of type float or double has integral value. More...

static void	allocate_nondet_length_array (code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type, const allocate_local_symbolt &allocate_local_symbol, const source_locationt &location)
	Allocates a fresh array and emits an assignment writing to `lhs` the address of the new array. More...

static void	array_primitive_init_code (code_blockt &assignments, const exprt &init_array_expr, const typet &element_type, const exprt &max_length_expr, const source_locationt &location, const allocate_local_symbolt &allocate_local_symbol)
	Create code to nondeterministically initialize arrays of primitive type. More...

static void	array_loop_init_code (code_blockt &assignments, const exprt &init_array_expr, const exprt &length_expr, const typet &element_type, const exprt &max_length_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_tablet &symbol_table)
	Create code to nondeterministically initialize each element of an array in a loop. 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_tablet &symbol_table, const size_t max_nondet_array_length)
	Synthesize GOTO for generating a array of nondet length to be stored in the `expr`. More...

static void	assert_type_consistency (const code_blockt &assignments)

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

exprt	object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_tablet &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, update_in_placet update_in_place, message_handlert &log)
	Call gen_nondet_init() above with a default (identity) pointer_type_selector. More...

Variables
const integer_intervalt	printable_char_range (' ', '~')
	Interval that represents the printable character range range U+0020-U+007E, i.e. More...

Function Documentation

◆ allocate_nondet_length_array()

static void allocate_nondet_length_array	(	code_blockt &	assignments,
		const exprt &	lhs,
		const exprt &	max_length_expr,
		const typet &	element_type,
		const allocate_local_symbolt &	allocate_local_symbol,
		const source_locationt &	location
	)

static

Allocates a fresh array and emits an assignment writing to lhs the address of the new array.

Single-use at the moment, but useful to keep as a separate function for downstream branches.

Parameters

[out]	assignments	Code is emitted here.
	lhs	Symbol to assign the new array structure.
	max_length_expr	Maximum length of the new array (minimum is fixed at zero for now).
	element_type	Actual element type of the array (the array for all reference types will have void* type, but this will be annotated as the true member type).
	allocate_local_symbol	A function to generate a new local symbol and add it to the symbol table
	location	Source location associated with nondet-initialization.

Returns: Appends instructions to assignments

Definition at line 1142 of file java_object_factory.cpp.

◆ array_loop_init_code()

static void array_loop_init_code	(	code_blockt &	assignments,
		const exprt &	init_array_expr,
		const exprt &	length_expr,
		const typet &	element_type,
		const exprt &	max_length_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_tablet &	symbol_table
	)

static

Create code to nondeterministically initialize each element of an array in a loop.

The code produced is of the form (supposing an array of type OBJ):

   struct OBJ **array_data_init;
   int array_init_iter;
   array_data_init = (struct OBJ **)init_array_expr;
   array_init_iter = 0;
2: IF array_init_iter == length_expr THEN GOTO 5
   IF array_init_iter == max_length_expr THEN GOTO 5
   IF !NONDET(__CPROVER_bool) THEN GOTO 3
   array_data_init[array_init_iter] = null;
   GOTO 4
3: malloc_site = ALLOCATE(...);
   array_data_init[array_init_iter] = (struct OBJ *)malloc_site;
   *malloc_site = {...};
   malloc_site->value = NONDET(int);
4: array_init_iter = array_init_iter + 1;
   GOTO 2
5: ...

Parameters

[out]	assignments	: Code block to which the initializing assignments will be appended.
	init_array_expr	: array data
	length_expr	: array length
	element_type	type of array elements
	max_length_expr	: max length, as specified by max-nondet-array-length
	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.
	element_generator	A function for generating the body of the loop which creates and assigns the element at the position.
	allocate_local_symbol	A function to generate a new local symbol and add it to the symbol table
	symbol_table	The symbol table.

Definition at line 1330 of file java_object_factory.cpp.

◆ array_primitive_init_code()

static void array_primitive_init_code	(	code_blockt &	assignments,
		const exprt &	init_array_expr,
		const typet &	element_type,
		const exprt &	max_length_expr,
		const source_locationt &	location,
		const allocate_local_symbolt &	allocate_local_symbol
	)

static

Create code to nondeterministically initialize arrays of primitive type.

The code produced is of the form (for an array of type TYPE):

TYPE (*array_data_init)[max_length_expr];
array_data_init =
  ALLOCATE(TYPE [max_length_expr], max_length_expr, false);
*array_data_init = NONDET(TYPE [max_length_expr]);
init_array_expr = *array_data_init;

Parameters

[out]	assignments	: Code block to which the initializing assignments will be appended.
	init_array_expr	: array data
	element_type	type of array elements
	max_length_expr	: the (constant) size to which initialise the array
	location	Source location associated with nondet-initialization.
	allocate_local_symbol	A function to generate a new local symbol and add it to the symbol table

Definition at line 1186 of file java_object_factory.cpp.

◆ assert_type_consistency()

static void assert_type_consistency ( const code_blockt & assignments )

static

Definition at line 1520 of file java_object_factory.cpp.

◆ assume_expr_integral()

static code_blockt assume_expr_integral	(	const exprt &	expr,
		const typet &	type,
		const source_locationt &	location,
		const allocate_local_symbolt &	allocate_local_symbol
	)

static

Generate code block that verifies that an expression of type float or double has integral value.

For example, for a float expression floatVal we generate: int assume_integral_tmp; assume_integral_tmp = NONDET(int); ASSUME FLOAT_TYPECAST(assume_integral_tmp, float, __CPROVER_rounding_mode) == floatVal

Parameters

expr	The expression we want to make an assumption on
type	The type of the expression
location	Source location associated with the expression
allocate_local_symbol	A function to generate a new local symbol and add it to the symbol table

Returns: Code block constructing the auxiliary nondet integer and an assume statement that the integer is equal to the value of the expression

Definition at line 940 of file java_object_factory.cpp.

◆ 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_tablet &	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() ```

Definition at line 1376 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 1624 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 1681 of file java_object_factory.cpp.

◆ get_string_input_values_code()

alternate_casest get_string_input_values_code	(	const exprt &	expr,
		const std::list< std::string > &	string_input_values,
		symbol_table_baset &	symbol_table
	)

Creates an alternate_casest vector in which each item contains an assignment of a string from string_input_values (or more precisely the literal symbol corresponding to the string) to expr.

Parameters

expr	Struct-typed lvalue expression to which we want to assign the strings.
string_input_values	Strings to assign.
symbol_table	The symbol table in which we'll lool up literal symbol

Returns: A vector that can be passed to generate_nondet_switch

Definition at line 728 of file java_object_factory.cpp.

◆ initialize_nondet_string_fields()

void initialize_nondet_string_fields	(	struct_exprt &	struct_expr,
		code_blockt &	code,
		const std::size_t &	min_nondet_string_length,
		const std::size_t &	max_nondet_string_length,
		const source_locationt &	loc,
		const irep_idt &	function_id,
		symbol_table_baset &	symbol_table,
		bool	printable,
		allocate_objectst &	allocate_objects
	)

Initialise length and data fields for a nondeterministic String structure.

If the structure is not a nondeterministic structure, the call results in a precondition violation.

Parameters

[out]	struct_expr	struct that we initialize
	code	block to add pre-requisite declarations (e.g. to allocate a data array)
	min_nondet_string_length	minimum length of strings to initialize
	max_nondet_string_length	maximum length of strings to initialize
	loc	location in the source
	function_id	function ID to associate with auxiliary variables
	symbol_table	the symbol table
	printable	if true, the nondet string must consist of printable characters only
	allocate_objects	manages memory allocation and keeps track of the newly created symbols

The code produced is of the form:

int tmp_object_factory$1;
tmp_object_factory$1 = NONDET(int);
__CPROVER_assume(tmp_object_factory$1 >= 0);
__CPROVER_assume(tmp_object_factory$1 <= max_nondet_string_length);
char (*string_data_pointer)[INFINITY()];
string_data_pointer = ALLOCATE(char [INFINITY()], INFINITY(), false);
char nondet_infinite_array$2[INFINITY()];
nondet_infinite_array$2 = NONDET(char [INFINITY()]);
*string_data_pointer = nondet_infinite_array$2;
cprover_associate_array_to_pointer_func(
  *string_data_pointer, *string_data_pointer);
cprover_associate_length_to_array_func(
  *string_data_pointer, tmp_object_factory);
 
struct_expr is then adjusted to set
  .length=tmp_object_factory,
  .data=*string_data_pointer

Unit tests in unit/java_bytecode/java_object_factory/ ensure it is the case.

Definition at line 364 of file java_object_factory.cpp.

◆ integer_interval_to_string()

static irep_idt integer_interval_to_string ( const integer_intervalt & interval )

static

Converts and integer_intervalt to a a string of the for [lower]-[upper].

Definition at line 316 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,
		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 1547 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_tablet &	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 1657 of file java_object_factory.cpp.

Variable Documentation

◆ printable_char_range

const integer_intervalt printable_char_range(' ', '~')

Interval that represents the printable character range range U+0020-U+007E, i.e.

' ' to '~'

Classes

Functions

Variables

Function Documentation

◆ allocate_nondet_length_array()

◆ array_loop_init_code()

◆ array_primitive_init_code()

◆ assert_type_consistency()

◆ assume_expr_integral()

◆ gen_nondet_array_init()

◆ gen_nondet_init() [1/2]

◆ gen_nondet_init() [2/2]

◆ get_string_input_values_code()

◆ initialize_nondet_string_fields()

◆ integer_interval_to_string()

◆ object_factory() [1/2]

◆ object_factory() [2/2]

Variable Documentation

◆ printable_char_range