cprover
java_object_factoryt Class Reference
+ Collaboration diagram for java_object_factoryt:

Public Member Functions

 java_object_factoryt (const source_locationt &loc, const java_object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector, message_handlert &log)
 
void gen_nondet_array_init (code_blockt &assignments, const exprt &expr, size_t depth, update_in_placet, const source_locationt &location)
 Create code to initialize a Java array whose size will be at most max_nondet_array_length. More...
 
bool gen_nondet_enum_init (code_blockt &assignments, const exprt &expr, const java_class_typet &java_class_type, const source_locationt &location)
 We nondet-initialize enums to be equal to one of the constants defined for their type: int i = nondet(int); assume(0 < = i < $VALUES.length); expr = $VALUES[i]; where $VALUES is a variable generated by the Java compiler and which gives the possible values of a particular enum subtype (this is the same array that is returned by Enum.values()). More...
 
void gen_nondet_init (code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, const optionalt< typet > &override_type, size_t depth, update_in_placet, const source_locationt &location)
 Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects as necessary and nondet-initializing their members, or if MUST_UPDATE_IN_PLACE is set, re-initializing already-allocated objects. More...
 
void add_created_symbol (const symbolt *symbol)
 
void declare_created_symbols (code_blockt &init_code)
 

Private Member Functions

void gen_pointer_target_init (code_blockt &assignments, const exprt &expr, const typet &target_type, lifetimet lifetime, size_t depth, update_in_placet update_in_place, const source_locationt &location)
 Initializes the pointer-typed lvalue expression expr to point to an object of type target_type, recursively nondet-initializing the members of that object. More...
 
void allocate_nondet_length_array (code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type, const source_locationt &location)
 Allocates a fresh array and emits an assignment writing to lhs the address of the new array. More...
 
void gen_nondet_pointer_init (code_blockt &assignments, const exprt &expr, lifetimet lifetime, const pointer_typet &pointer_type, size_t depth, const update_in_placet &update_in_place, const source_locationt &location)
 Initializes a pointer expr of type pointer_type to a primitive-typed value or an object tree. More...
 
void gen_nondet_struct_init (code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, const struct_typet &struct_type, size_t depth, const update_in_placet &update_in_place, const source_locationt &location)
 Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE is set, re-initializes already-allocated objects. More...
 
symbol_exprt gen_nondet_subtype_pointer_init (code_blockt &assignments, lifetimet lifetime, const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location)
 Generate codet assignments to initalize the selected concrete type. More...
 
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)
 Create code to nondeterministically initialize arrays of primitive type. More...
 
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, size_t depth, update_in_placet update_in_place, const source_locationt &location)
 Create code to nondeterministically initialize each element of an array in a loop. More...
 

Private Attributes

const java_object_factory_parameterst object_factory_parameters
 
std::unordered_set< irep_idtrecursion_set
 This is employed in conjunction with the depth above. More...
 
generic_parameter_specialization_mapt generic_parameter_specialization_map
 Every time the non-det generator visits a type and the type is generic (either a struct or a pointer), the following map is used to store and look up the concrete types of the generic parameters in the current scope. More...
 
symbol_table_basetsymbol_table
 The symbol table. More...
 
const select_pointer_typetpointer_type_selector
 Resolves pointer types potentially using some heuristics, for example to replace pointers to interface types with pointers to concrete implementations. More...
 
allocate_objectst allocate_objects
 
messaget log
 Log for reporting warnings and errors in object creation. More...
 

Detailed Description

Definition at line 26 of file java_object_factory.cpp.

Constructor & Destructor Documentation

◆ java_object_factoryt()

java_object_factoryt::java_object_factoryt ( const source_locationt loc,
const java_object_factory_parameterst  _object_factory_parameters,
symbol_table_baset _symbol_table,
const select_pointer_typet pointer_type_selector,
message_handlert log 
)
inline

Definition at line 76 of file java_object_factory.cpp.

Member Function Documentation

◆ add_created_symbol()

void java_object_factoryt::add_created_symbol ( const symbolt symbol)

Definition at line 1038 of file java_object_factory.cpp.

◆ allocate_nondet_length_array()

void java_object_factoryt::allocate_nondet_length_array ( code_blockt assignments,
const exprt lhs,
const exprt max_length_expr,
const typet element_type,
const source_locationt location 
)
private

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]assignmentsCode is emitted here.
lhsSymbol to assign the new array structure.
max_length_exprMaximum length of the new array (minimum is fixed at zero for now).
element_typeActual 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).
locationSource location associated with nondet-initialization.
Returns
Appends instructions to assignments

Definition at line 1063 of file java_object_factory.cpp.

◆ array_loop_init_code()

void java_object_factoryt::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,
size_t  depth,
update_in_placet  update_in_place,
const source_locationt location 
)
private

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_typetype of array elements
max_length_expr: max length, as specified by max-nondet-array-length
depthNumber of times that a pointer has been dereferenced from the root of the object tree that we are initializing.
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
locationSource location associated with nondet-initialization.

Definition at line 1171 of file java_object_factory.cpp.

◆ array_primitive_init_code()

void java_object_factoryt::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 
)
private

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_typetype of array elements
max_length_expr: the (constant) size to which initialise the array
locationSource location associated with nondet-initialization.

Definition at line 1102 of file java_object_factory.cpp.

◆ declare_created_symbols()

void java_object_factoryt::declare_created_symbols ( code_blockt init_code)

Definition at line 1043 of file java_object_factory.cpp.

◆ gen_nondet_array_init()

void java_object_factoryt::gen_nondet_array_init ( code_blockt assignments,
const exprt expr,
size_t  depth,
update_in_placet  update_in_place,
const source_locationt location 
)

Create code to initialize a Java array whose size will be at most max_nondet_array_length.

The code is emitted to assignments does as follows:

  1. non-deterministically choose a length for the array
  2. assume that such length is >=0 and <= max_length
  3. loop through all elements of the array and initialize them

Definition at line 1289 of file java_object_factory.cpp.

◆ gen_nondet_enum_init()

bool java_object_factoryt::gen_nondet_enum_init ( code_blockt assignments,
const exprt expr,
const java_class_typet java_class_type,
const source_locationt location 
)

We nondet-initialize enums to be equal to one of the constants defined for their type: int i = nondet(int); assume(0 < = i < $VALUES.length); expr = $VALUES[i]; where $VALUES is a variable generated by the Java compiler and which gives the possible values of a particular enum subtype (this is the same array that is returned by Enum.values()).

This may fail if the $VALUES static field is not present. Ensuring that field is in the symbol table when this method may be applicable is the driver program's responsibility: for example, ci_lazy_methods.cpp makes some effort to retain this field when a stub method might refer to it.

Returns
true on success

Definition at line 1375 of file java_object_factory.cpp.

◆ gen_nondet_init()

void java_object_factoryt::gen_nondet_init ( code_blockt assignments,
const exprt expr,
bool  is_sub,
bool  skip_classid,
lifetimet  lifetime,
const optionalt< typet > &  override_type,
size_t  depth,
update_in_placet  update_in_place,
const source_locationt location 
)

Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects as necessary and nondet-initializing their members, or if MUST_UPDATE_IN_PLACE is set, re-initializing already-allocated objects.

Parameters
assignmentsA code block where the initializing assignments will be appended to.
exprLvalue expression to initialize.
is_subIf true, expr is a substructure of a larger object, which in Java necessarily means a base class.
skip_classidIf true, skip initializing @class_identifier.
lifetimeLifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
depthNumber of times that a pointer has been dereferenced from the root of the object tree that we are initializing.
override_typeIf not empty, initialize with override_type instead of expr.type(). Used at the moment for reference arrays, which are implemented as void* arrays but should be init'd as their true type with appropriate casts.
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
locationSource location associated with nondet-initialization.

Definition at line 936 of file java_object_factory.cpp.

◆ gen_nondet_pointer_init()

void java_object_factoryt::gen_nondet_pointer_init ( code_blockt assignments,
const exprt expr,
lifetimet  lifetime,
const pointer_typet pointer_type,
size_t  depth,
const update_in_placet update_in_place,
const source_locationt location 
)
private

Initializes a pointer expr of type pointer_type to a primitive-typed value or an object tree.

It allocates child objects as necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE is set, re-initializes already-allocated objects.

Parameters
assignmentsThe code block we are building with initialization code.
exprPointer-typed lvalue expression to initialize.
lifetimeLifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
depthNumber of times that a pointer has been dereferenced from the root of the object tree that we are initializing.
pointer_typeThe type of the pointer we are initalizing
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
locationSource location associated with nondet-initialization.

Definition at line 460 of file java_object_factory.cpp.

◆ gen_nondet_struct_init()

void java_object_factoryt::gen_nondet_struct_init ( code_blockt assignments,
const exprt expr,
bool  is_sub,
bool  skip_classid,
lifetimet  lifetime,
const struct_typet struct_type,
size_t  depth,
const update_in_placet update_in_place,
const source_locationt location 
)
private

Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializes their members, or if MUST_UPDATE_IN_PLACE is set, re-initializes already-allocated objects.

After initialization calls validation method expr.cproverNondetInitialize() if it was provided by the user.

Parameters
assignmentsThe code block to append the new instructions to
exprStruct-typed lvalue expression to initialize
is_subIf true, expr is a substructure of a larger object, which in Java necessarily means a base class
skip_classidIf true, skip initializing @class_identifier
lifetimeLifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
struct_typeThe type of the struct we are initializing
depthNumber of times that a pointer has been dereferenced from the root of the object tree that we are initializing
update_in_placeEnum instance with the following meaning. NO_UPDATE_IN_PLACE: initialize expr from scratch MUST_UPDATE_IN_PLACE: reinitialize an existing object MAY_UPDATE_IN_PLACE: invalid input
locationSource location associated with nondet-initialization

Definition at line 750 of file java_object_factory.cpp.

◆ gen_nondet_subtype_pointer_init()

symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init ( code_blockt assignments,
lifetimet  lifetime,
const pointer_typet replacement_pointer,
size_t  depth,
const source_locationt location 
)
private

Generate codet assignments to initalize the selected concrete type.

Generated code looks as follows (here A = replacement_pointer.subtype()):

// allocate memory for a new object, depends on lifetime A { ... } tmp_object;

// non-det init all the fields of A A.x = NONDET(...) A.y = NONDET(...)

// assign expr with a suitably casted pointer to new_object A * p = &tmp_object

Parameters
assignmentsA block of code where we append the generated code
lifetimeLifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
replacement_pointerThe type of the pointer we actually want to create
depthNumber of times that a pointer has been dereferenced from the root of the object tree that we are initializing
locationSource location associated with nondet-initialization
Returns
A symbol expression of type replacement_pointer corresponding to a pointer to object tmp_object (see above)

Definition at line 678 of file java_object_factory.cpp.

◆ gen_pointer_target_init()

void java_object_factoryt::gen_pointer_target_init ( code_blockt assignments,
const exprt expr,
const typet target_type,
lifetimet  lifetime,
size_t  depth,
update_in_placet  update_in_place,
const source_locationt location 
)
private

Initializes the pointer-typed lvalue expression expr to point to an object of type target_type, recursively nondet-initializing the members of that object.

Code emitted mainly depends on update_in_place:

When in NO_UPDATE_IN_PLACE mode, the code emitted looks like:

struct new_object obj; // depends on lifetime
<expr> := &obj
// recursive initialization of obj in NO_UPDATE_IN_PLACE mode

When in MUST_UPDATE_IN_PLACE mode, all code is emitted by a recursive call to gen_nondet_init in MUST_UPDATE_IN_PLACE mode, and looks like:

(*<expr>).some_int := NONDET(int)
(*<expr>).some_char := NONDET(char)

It is illegal to call the function with MAY_UPDATE_IN_PLACE.

Parameters
[out]assignmentsA code_blockt where the initialization code will be emitted to.
exprPointer-typed lvalue expression to initialize. The pointed type equals target_type.
target_typeStructure type to initialize, which may not match *expr (for example, expr might be have type void*). It cannot be a pointer to a primitive type because Java does not allow so.
lifetimeLifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
depthNumber of times that a pointer has been dereferenced from the root of the object tree that we are initializing.
update_in_placeNO_UPDATE_IN_PLACE: initialize expr from scratch MUST_UPDATE_IN_PLACE: reinitialize an existing object MAY_UPDATE_IN_PLACE: invalid input
locationSource location associated with nondet-initialization.

Definition at line 209 of file java_object_factory.cpp.

Member Data Documentation

◆ allocate_objects

allocate_objectst java_object_factoryt::allocate_objects
private

Definition at line 54 of file java_object_factory.cpp.

◆ generic_parameter_specialization_map

generic_parameter_specialization_mapt java_object_factoryt::generic_parameter_specialization_map
private

Every time the non-det generator visits a type and the type is generic (either a struct or a pointer), the following map is used to store and look up the concrete types of the generic parameters in the current scope.

Note that not all generic parameters need to have a concrete type, e.g., the method under test is generic. The types are removed from the map when the scope changes. Note that in different depths of the scope the parameters can be specialized with different types so we keep a stack of types for each parameter.

Definition at line 44 of file java_object_factory.cpp.

◆ log

messaget java_object_factoryt::log
private

Log for reporting warnings and errors in object creation.

Definition at line 57 of file java_object_factory.cpp.

◆ object_factory_parameters

const java_object_factory_parameterst java_object_factoryt::object_factory_parameters
private

Definition at line 28 of file java_object_factory.cpp.

◆ pointer_type_selector

const select_pointer_typet& java_object_factoryt::pointer_type_selector
private

Resolves pointer types potentially using some heuristics, for example to replace pointers to interface types with pointers to concrete implementations.

Definition at line 52 of file java_object_factory.cpp.

◆ recursion_set

std::unordered_set<irep_idt> java_object_factoryt::recursion_set
private

This is employed in conjunction with the depth above.

Every time the non-det generator visits a type, the type is added to this set. We forbid the non-det initialization when we see the type for the second time in this set AND the tree depth becomes >= than the maximum value above.

Definition at line 34 of file java_object_factory.cpp.

◆ symbol_table

symbol_table_baset& java_object_factoryt::symbol_table
private

The symbol table.

Definition at line 47 of file java_object_factory.cpp.


The documentation for this class was generated from the following file: