java_object_factory.cpp File Reference

#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/interval_constraint.h>
#include <util/message.h>
#include <util/nondet_bool.h>
#include <util/symbol_table_base.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_functions.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:

Go to the source code of this file.

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_table_baset &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_table_baset &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_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, 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.

Definition at line 1141 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_table_baset &  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 1329 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 1185 of file java_object_factory.cpp.

assert_type_consistency()

static void assert_type_consistency ( const code_blockt &  assignments )

static

Definition at line 1519 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_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()`

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.

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

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