cprover
java_object_factory.cpp File Reference
+ 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

exprt allocate_dynamic_object (const exprt &target_expr, const typet &allocate_type, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code, std::vector< const symbolt * > &symbols_created, bool cast_needed)
 Generates code for allocating a dynamic object. More...
 
exprt allocate_dynamic_object_with_decl (const exprt &target_expr, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code)
 Generates code for allocating a dynamic object. More...
 
static mp_integer max_value (const typet &type)
 Get max value for an integer type. 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)
 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 void declare_created_symbols (const std::vector< const symbolt * > &symbols_created, const source_locationt &loc, code_blockt &init_code)
 Add code_declt instructions to init_code for every non-static symbol in symbols_created More...
 
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, allocation_typet alloc_type, const source_locationt &loc, const select_pointer_typet &pointer_type_selector)
 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, allocation_typet alloc_type, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
 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, allocation_typet alloc_type, const source_locationt &location)
 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, allocation_typet alloc_type, const java_object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place)
 Call gen_nondet_init() above with a default (identity) pointer_type_selector. More...
 

Function Documentation

◆ allocate_dynamic_object()

exprt allocate_dynamic_object ( const exprt target_expr,
const typet allocate_type,
symbol_table_baset symbol_table,
const source_locationt loc,
const irep_idt function_id,
code_blockt output_code,
std::vector< const symbolt * > &  symbols_created,
bool  cast_needed 
)

Generates code for allocating a dynamic object.

This is used in allocate_object() and also in the library preprocessing for allocating strings.

Parameters
target_exprexpression to which the necessary memory will be allocated, its type should be pointer to allocate_type
allocate_typetype of the object allocated
symbol_tablesymbol table
loclocation in the source
function_idfunction ID to associate with auxiliary variables
output_codecode block to which the necessary code is added
symbols_createdcreated symbols to be declared by the caller
cast_neededBoolean flags saying where we need to cast the malloc site
Returns
Expression representing the malloc site allocated.

Definition at line 187 of file java_object_factory.cpp.

◆ allocate_dynamic_object_with_decl()

exprt allocate_dynamic_object_with_decl ( const exprt target_expr,
symbol_table_baset symbol_table,
const source_locationt loc,
const irep_idt function_id,
code_blockt output_code 
)

Generates code for allocating a dynamic object.

This is a static version of allocate_dynamic_object that can be called from outside java_object_factory and which takes care of creating the associated declarations.

Parameters
target_exprexpression to which the necessary memory will be allocated
symbol_tablesymbol table
loclocation in the source
function_idfunction ID to associate with auxiliary variables
output_codecode block to which the necessary code is added
Returns
the dynamic object created

Definition at line 251 of file java_object_factory.cpp.

◆ declare_created_symbols()

static void declare_created_symbols ( const std::vector< const symbolt * > &  symbols_created,
const source_locationt loc,
code_blockt init_code 
)
static

Add code_declt instructions to init_code for every non-static symbol in symbols_created

Parameters
symbols_createdlist of symbols
locsource location for new code_declt instances
[out]init_codegets code_declt for each symbol

Definition at line 1561 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,
allocation_typet  alloc_type,
const java_object_factory_parameterst object_factory_parameters,
const select_pointer_typet pointer_type_selector,
update_in_placet  update_in_place 
)

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
exprLvalue expression to initialize.
[out]init_codeA 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_tableThe 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.
locSource location to which all generated code will be associated to.
skip_classidIf true, skip initializing field @class_identifier.
alloc_typeAllocate new objects as global objects (GLOBAL) or as local variables (LOCAL) or using malloc (DYNAMIC).
object_factory_parametersParameters for the generation of non deterministic objects.
pointer_type_selectorThe pointer_selector to use to resolve pointer types where required.
update_in_placeNO_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
Returns
init_code gets an instruction sequence to initialize or reinitialize expr and child objects it refers to. symbol_table is modified with any new symbols created. This includes any necessary temporaries, and if create_dyn_objs is false, any allocated objects.

Definition at line 1681 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,
allocation_typet  alloc_type,
const java_object_factory_parameterst object_factory_parameters,
update_in_placet  update_in_place 
)

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

Definition at line 1742 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
exprStruct-typed lvalue expression to which we want to assign the strings.
string_input_valuesStrings to assign.
symbol_tableThe symbol table in which we'll lool up literal symbol
Returns
A vector that can be passed to generate_nondet_switch

Definition at line 952 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 
)

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
struct_expr[out]: struct that we initialize
codeblock to add pre-requisite declarations (e.g. to allocate a data array)
min_nondet_string_lengthminimum length of strings to initialize
max_nondet_string_lengthmaximum length of strings to initialize
loclocation in the source
function_idfunction ID to associate with auxiliary variables
symbol_tablethe symbol table
printableif true, the nondet string must consist of printable characters only

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 568 of file java_object_factory.cpp.

◆ max_value()

static mp_integer max_value ( const typet type)
static

Get max value for an integer type.

Parameters
typeType to find maximum value for
Returns
Maximum integer value

Definition at line 522 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,
allocation_typet  alloc_type,
const source_locationt loc,
const select_pointer_typet pointer_type_selector 
)

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 requried to initialize either the returned value or its child objects

Definition at line 1590 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,
allocation_typet  alloc_type,
const source_locationt location 
)

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

Definition at line 1720 of file java_object_factory.cpp.