cprover
java_object_factory.h File Reference

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

Enumerations

enum  allocation_typet { allocation_typet::GLOBAL, allocation_typet::LOCAL, allocation_typet::DYNAMIC }
 Selects the kind of allocation used by java_object_factory et al. More...
 
enum  update_in_placet { update_in_placet::NO_UPDATE_IN_PLACE, update_in_placet::MAY_UPDATE_IN_PLACE, update_in_placet::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, object_factory_parameterst parameters, allocation_typet alloc_type, const source_locationt &location, 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...
 
exprt object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_tablet &symbol_table, const 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 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...
 
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 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...
 
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=false)
 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...
 
codet initialize_nondet_string_struct (const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable)
 Initialize a nondeterministic String structure. 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(), at the bottom of the file. Their purpose is very similar. 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.

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.

Enumeration Type Documentation

◆ allocation_typet

enum allocation_typet
strong

Selects the kind of allocation used by java_object_factory et al.

Enumerator
GLOBAL 

Allocate global objects.

LOCAL 

Allocate local stacked objects.

DYNAMIC 

Allocate dynamic objects (using MALLOC)

Definition at line 79 of file java_object_factory.h.

◆ update_in_placet

enum update_in_placet
strong
Enumerator
NO_UPDATE_IN_PLACE 
MAY_UPDATE_IN_PLACE 
MUST_UPDATE_IN_PLACE 

Definition at line 108 of file java_object_factory.h.

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

References exprt::add_source_location(), exprt::copy_to_operands(), get_fresh_aux_symbol(), irept::id(), id2string(), INVARIANT, irept::is_nil(), loc, object_size(), pointer_type(), size_of_expr(), symbolt::symbol_expr(), to_pointer_type(), and exprt::type().

Referenced by allocate_dynamic_object_with_decl(), and java_object_factoryt::allocate_object().

◆ 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
output_codecode block to which the necessary code is added
Returns
the dynamic object created

Definition at line 222 of file java_object_factory.cpp.

References code_blockt::add(), exprt::add_source_location(), allocate_dynamic_object(), dynamic_object(), loc, exprt::operands(), typet::subtype(), to_code(), and exprt::type().

Referenced by add_nondet_string_pointer_initialization(), java_string_library_preprocesst::allocate_fresh_array(), java_string_library_preprocesst::allocate_fresh_string(), and java_string_library_preprocesst::make_argument_for_format().

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

References code_blockt::append(), declare_created_symbols(), java_object_factoryt::gen_nondet_init(), and loc.

Referenced by java_simple_method_stubst::create_method_stub(), java_simple_method_stubst::create_method_stub_at(), gen_nondet_init(), stub_global_initializer_factoryt::get_stub_initializer_body(), insert_nondet_init_code(), and java_static_lifetime_init().

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

References gen_nondet_init(), and loc.

◆ initialize_nondet_string_struct()

codet initialize_nondet_string_struct ( const exprt obj,
const std::size_t &  max_nondet_string_length,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
bool  printable 
)

Initialize a nondeterministic String structure.

Parameters
objstruct to initialize, must have been declared using code of the form:
struct java.lang.String { struct \@java.lang.Object;
int length; char *data; } tmp_object_factory$1;
max_nondet_string_lengthmaximum length of strings to initialize
loclocation in the source
symbol_tablethe symbol table
Returns
code for initialization of the strings
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);
arg = { .@java.lang.Object={
.@class_identifier=\"java::java.lang.String\", .@lock=false },
.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 545 of file java_object_factory.cpp.

References code_blockt::add(), add_array_to_length_association(), add_character_set_constraint(), add_pointer_to_array_association(), exprt::copy_to_operands(), namespace_baset::follow(), from_integer(), get_fresh_aux_symbol(), struct_union_typet::get_tag(), struct_union_typet::has_component(), id2string(), java_string_library_preprocesst::implements_java_char_sequence(), java_char_type(), java_int_type(), java_root_class_init(), loc, make_allocate_code(), make_nondet_infinite_char_array(), max_value(), pointer_type(), PRECONDITION, symbolt::symbol_expr(), to_struct_type(), and exprt::type().

Referenced by add_nondet_string_pointer_initialization().

◆ object_factory() [1/2]

exprt object_factory ( const typet type,
const irep_idt  base_name,
code_blockt init_code,
symbol_table_baset symbol_table,
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 1469 of file java_object_factory.cpp.

References code_blockt::append(), symbolt::base_name, CHECK_RETURN, declare_created_symbols(), goto_functionst::entry_point(), object_factory_parameterst::function_id, java_object_factoryt::gen_nondet_init(), id2string(), symbolt::is_static_lifetime, loc, symbolt::location, symbolt::mode, symbol_table_baset::move(), symbolt::name, NO_UPDATE_IN_PLACE, symbolt::symbol_expr(), and symbolt::type.

Referenced by java_build_arguments(), and object_factory().

◆ object_factory() [2/2]

exprt object_factory ( const typet type,
const irep_idt  base_name,
code_blockt init_code,
symbol_tablet symbol_table,
const 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 1597 of file java_object_factory.cpp.

References object_factory().