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...
 
static codet make_allocate_code (const symbol_exprt &lhs, const exprt &size)
 Create code allocating object of size size and assigning it to lhs 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...
 
static bool add_nondet_string_pointer_initialization (const exprt &expr, const std::size_t &max_nondet_string_length, bool printable, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
 Add code for the initialization of a string using a nondeterministic content and association of its address to the pointer 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, 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 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 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, update_in_placet update_in_place)
 Call gen_nondet_init() above with a default (identity) pointer_type_selector. More...
 

Function Documentation

◆ add_nondet_string_pointer_initialization()

static bool add_nondet_string_pointer_initialization ( const exprt expr,
const std::size_t &  max_nondet_string_length,
bool  printable,
symbol_table_baset symbol_table,
const source_locationt loc,
const irep_idt function_id,
code_blockt code 
)
static

Add code for the initialization of a string using a nondeterministic content and association of its address to the pointer expr.

Parameters
exprpointer to be affected
max_nondet_string_lengthmaximum length of strings to initialize
printableBoolean, true to force content to be printable
symbol_tablethe symbol table
loclocation in the source
[out]codecode block in which initialization code is added
Returns
false if code was added, true to signal an error when the given object does not implement CharSequence or does not have data and length fields, in which case it should be initialized another way.

Definition at line 672 of file java_object_factory.cpp.

References code_blockt::add(), allocate_dynamic_object_with_decl(), namespace_baset::follow(), initialize_nondet_string_struct(), loc, typet::subtype(), to_struct_type(), to_symbol_type(), and exprt::type().

Referenced by java_object_factoryt::gen_nondet_pointer_init().

◆ 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().

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

References code_blockt::add(), exprt::add_source_location(), and loc.

Referenced by gen_nondet_init(), and object_factory().

◆ 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().

◆ make_allocate_code()

static codet make_allocate_code ( const symbol_exprt lhs,
const exprt size 
)
static

Create code allocating object of size size and assigning it to lhs

Parameters
lhs: pointer which will be allocated
size: size of the object
Returns
code allocation object and assigning lhs

Definition at line 505 of file java_object_factory.cpp.

References exprt::copy_to_operands(), and exprt::type().

Referenced by initialize_nondet_string_struct().

◆ max_value()

static mp_integer max_value ( const typet type)
static

◆ 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().