cprover
|
Public Member Functions | |
java_object_factoryt (std::vector< const symbolt *> &_symbols_created, const source_locationt &loc, const object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector) | |
exprt | allocate_object (code_blockt &assignments, const exprt &, const typet &, allocation_typet alloc_type) |
Installs a new symbol in the symbol table, pushing the corresponding symbolt object to the field symbols_created and emits to assignments a new assignment of the form <target_expr> := address-of(new_object) . More... | |
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... | |
void | gen_nondet_init (code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool skip_classid, allocation_typet alloc_type, bool override_, const typet &override_type, size_t depth, update_in_placet, const source_locationt &location) |
Initializes a primitive-typed or referece-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... | |
Private Member Functions | |
code_assignt | get_null_assignment (const exprt &expr, const pointer_typet &ptr_type) |
Returns a codet that assigns expr , of type ptr_type , a NULL value. More... | |
void | gen_pointer_target_init (code_blockt &assignments, const exprt &expr, const typet &target_type, allocation_typet alloc_type, 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, allocation_typet alloc_type, 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, irep_idt class_identifier, bool skip_classid, allocation_typet alloc_type, 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, allocation_typet alloc_type, const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location) |
Generate codet assignments to initalize the selected concrete type. More... | |
Private Attributes | |
std::vector< const symbolt * > & | symbols_created |
Every new variable initialized by the code emitted by the methods of this class gets a symbol in the symbol table, and such symbols are also added to this vector. More... | |
const source_locationt & | loc |
The source location for new statements emitted during the operation of the methods in this class. More... | |
const object_factory_parameterst | object_factory_parameters |
std::unordered_set< irep_idt > | recursion_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_baset & | symbol_table |
The symbol table. More... | |
namespacet | ns |
A namespace built from exclusively one symbol table - the one above. More... | |
const select_pointer_typet & | pointer_type_selector |
Resolves pointer types potentially using some heuristics, for example to replace pointers to interface types with pointers to concrete implementations. More... | |
Definition at line 22 of file java_object_factory.cpp.
|
inline |
Definition at line 83 of file java_object_factory.cpp.
|
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.
[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). |
assignments
Definition at line 1225 of file java_object_factory.cpp.
References exprt::add_source_location(), exprt::copy_to_operands(), from_integer(), object_factory_parameterst::function_id, gen_nondet_init(), get_fresh_aux_symbol(), id2string(), java_int_type(), loc, LOCAL, exprt::move_to_operands(), NO_UPDATE_IN_PLACE, object_factory_parameters, symbolt::symbol_expr(), symbol_table, symbols_created, and exprt::type().
Referenced by gen_nondet_array_init().
exprt java_object_factoryt::allocate_object | ( | code_blockt & | assignments, |
const exprt & | target_expr, | ||
const typet & | allocate_type, | ||
allocation_typet | alloc_type | ||
) |
Installs a new symbol in the symbol table, pushing the corresponding symbolt object to the field symbols_created
and emits to assignments
a new assignment of the form <target_expr> := address-of(new_object)
.
The allocate_type
may differ from target_expr.type()
, e.g. for target_expr having type int* and allocate_type being an int[10].
assignments | The code block to add code to. |
target_expr | The expression which we are allocating a symbol for. |
allocate_type | |
alloc_type | Allocation type (global, local or dynamic) |
Definition at line 274 of file java_object_factory.cpp.
References allocate_dynamic_object(), exprt::copy_to_operands(), DYNAMIC, namespace_baset::follow(), object_factory_parameterst::function_id, get_fresh_aux_symbol(), GLOBAL, id2string(), symbolt::is_static_lifetime, loc, LOCAL, ns, object_factory_parameters, typet::subtype(), symbolt::symbol_expr(), symbol_table, symbols_created, exprt::type(), and UNREACHABLE.
Referenced by gen_pointer_target_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:
Definition at line 1281 of file java_object_factory.cpp.
References exprt::add_source_location(), allocate_nondet_length_array(), symbolt::base_name, struct_union_typet::components(), code_ifthenelset::cond(), exprt::copy_to_operands(), DYNAMIC, irept::find(), namespace_baset::follow(), from_integer(), object_factory_parameterst::function_id, gen_nondet_init(), get_fresh_aux_symbol(), irept::id(), id2string(), INVARIANT, is_valid_java_array(), java_int_type(), loc, object_factory_parameterst::max_nondet_array_length, MAY_UPDATE_IN_PLACE, exprt::move_to_operands(), MUST_UPDATE_IN_PLACE, NO_UPDATE_IN_PLACE, ns, object_factory_parameters, pointer_type(), PRECONDITION, typet::subtype(), symbolt::symbol_expr(), symbol_table, symbols_created, code_ifthenelset::then_case(), to_struct_type(), and exprt::type().
Referenced by gen_pointer_target_init().
void java_object_factoryt::gen_nondet_init | ( | code_blockt & | assignments, |
const exprt & | expr, | ||
bool | is_sub, | ||
irep_idt | class_identifier, | ||
bool | skip_classid, | ||
allocation_typet | alloc_type, | ||
bool | override_, | ||
const typet & | override_type, | ||
size_t | depth, | ||
update_in_placet | update_in_place, | ||
const source_locationt & | location | ||
) |
Initializes a primitive-typed or referece-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.
assignments | A code block where the initializing assignments will be appended to. |
expr | Lvalue expression to initialize. |
is_sub | If true, expr is a substructure of a larger object, which in Java necessarily means a base class. |
class_identifier | Name of the parent class. Used to initialize the @class_identifier among others. |
skip_classid | If true, skip initializing @class_identifier . |
alloc_type | Allocation type (global, local or dynamic) |
override_ | If true, 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. |
depth | Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing. |
override_type | Override type per above. |
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 |
Definition at line 1130 of file java_object_factory.cpp.
References exprt::add_source_location(), exprt::copy_to_operands(), namespace_baset::follow(), gen_nondet_pointer_init(), gen_nondet_struct_init(), generic_parameter_specialization_map, get_nondet_bool(), irept::id(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(), loc, ns, pointer_type(), PRECONDITION, typet::subtype(), to_pointer_type(), to_struct_type(), to_symbol_type(), and exprt::type().
Referenced by allocate_nondet_length_array(), gen_nondet_array_init(), gen_nondet_init(), gen_nondet_struct_init(), gen_nondet_subtype_pointer_init(), gen_pointer_target_init(), and object_factory().
|
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.
assignments | The code block we are building with initialization code. |
expr | Pointer-typed lvalue expression to initialize. |
alloc_type | Allocation type (global, local or dynamic) |
depth | Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing. |
pointer_type | The type of the pointer we are initalizing |
update_in_place |
|
Definition at line 691 of file java_object_factory.cpp.
References code_blockt::add(), code_blockt::append(), code_ifthenelset::cond(), select_pointer_typet::convert_pointer_type(), exprt::copy_to_operands(), code_ifthenelset::else_case(), equal_java_types(), namespace_baset::follow(), gen_nondet_subtype_pointer_init(), gen_pointer_target_init(), generic_parameter_specialization_map, get_null_assignment(), struct_union_typet::get_tag(), irept::id(), recursion_set_entryt::insert_entry(), generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(), INVARIANT, object_factory_parameterst::max_nondet_tree_depth, object_factory_parameterst::max_nonnull_tree_depth, MAY_UPDATE_IN_PLACE, MUST_UPDATE_IN_PLACE, NO_UPDATE_IN_PLACE, ns, object_factory_parameters, pointer_type(), pointer_type_selector, PRECONDITION, recursion_set, exprt::source_location(), typet::subtype(), code_ifthenelset::then_case(), to_struct_type(), and exprt::type().
Referenced by gen_nondet_init().
|
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.
assignments | The code block to append the new instructions to. |
expr | Struct-typed lvalue expression to initialize. |
is_sub | If true, expr is a substructure of a larger object, which in Java necessarily means a base class. |
class_identifier | Name of the parent class. Used to initialize the @class_identifier among others. |
skip_classid | If true, skip initializing @class_identifier . |
alloc_type | Allocation type (global, local or dynamic) |
struct_type | The type of the struct we are initalizing. |
depth | Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing. |
update_in_place | NO_UPDATE_IN_PLACE: initialize expr from scratch MUST_UPDATE_IN_PLACE: reinitialize an existing object MAY_UPDATE_IN_PLACE: invalid input |
Definition at line 954 of file java_object_factory.cpp.
References code_blockt::add(), exprt::add_source_location(), code_function_callt::arguments(), struct_union_typet::components(), exprt::copy_to_operands(), dstringt::empty(), namespace_baset::follow(), from_integer(), code_function_callt::function(), object_factory_parameterst::function_id, gen_nondet_init(), struct_union_typet::get_tag(), code_typet::has_this(), irept::id(), id2string(), initialize_nondet_string_fields(), INVARIANT, loc, symbol_table_baset::lookup(), object_factory_parameterst::max_nondet_string_length, MAY_UPDATE_IN_PLACE, MUST_UPDATE_IN_PLACE, ns, object_factory_parameters, PRECONDITION, set_class_identifier(), object_factory_parameterst::string_printable, symbol_table, to_java_method_type(), to_struct_expr(), exprt::type(), and zero_initializer().
Referenced by gen_nondet_init().
|
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 alloc_type
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
assignments | A block of code where we append the generated code. |
alloc_type | Allocation type (global, local or dynamic) |
replacement_pointer | The type of the pointer we actually want to to create. |
depth | Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing. |
replacement_pointer
corresponding to a pointer to object tmp_object
(see above). Definition at line 893 of file java_object_factory.cpp.
References object_factory_parameterst::function_id, gen_nondet_init(), get_fresh_aux_symbol(), id2string(), loc, NO_UPDATE_IN_PLACE, object_factory_parameters, symbolt::symbol_expr(), and symbol_table.
Referenced by gen_nondet_pointer_init().
|
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:
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:
It is illegal to call the function with MAY_UPDATE_IN_PLACE.
[out] | assignments | A code_blockt where the initialization code will be emitted to. |
expr | Pointer-typed lvalue expression to initialize. The pointed type equals target_type . | |
target_type | Structure 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. | |
alloc_type | Allocation type (global, local or dynamic) | |
depth | Number of times that a pointer has been dereferenced from the root of the object tree that we are initializing. | |
update_in_place | NO_UPDATE_IN_PLACE: initialize expr from scratch MUST_UPDATE_IN_PLACE: reinitialize an existing object MAY_UPDATE_IN_PLACE: invalid input |
Definition at line 376 of file java_object_factory.cpp.
References allocate_object(), gen_nondet_array_init(), gen_nondet_init(), get_tag(), has_prefix(), irept::id(), id2string(), INVARIANT, MAY_UPDATE_IN_PLACE, NO_UPDATE_IN_PLACE, exprt::op0(), PRECONDITION, typet::subtype(), to_struct_type(), and exprt::type().
Referenced by gen_nondet_pointer_init().
|
private |
Returns a codet that assigns expr
, of type ptr_type
, a NULL value.
Definition at line 327 of file java_object_factory.cpp.
References exprt::add_source_location(), and loc.
Referenced by gen_nondet_pointer_init().
|
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 49 of file java_object_factory.cpp.
Referenced by gen_nondet_init(), and gen_nondet_pointer_init().
|
private |
The source location for new statements emitted during the operation of the methods in this class.
Definition at line 31 of file java_object_factory.cpp.
Referenced by allocate_nondet_length_array(), allocate_object(), gen_nondet_array_init(), gen_nondet_init(), gen_nondet_struct_init(), gen_nondet_subtype_pointer_init(), and get_null_assignment().
|
private |
A namespace built from exclusively one symbol table - the one above.
Definition at line 55 of file java_object_factory.cpp.
Referenced by allocate_object(), gen_nondet_array_init(), gen_nondet_init(), gen_nondet_pointer_init(), and gen_nondet_struct_init().
|
private |
Definition at line 33 of file java_object_factory.cpp.
Referenced by allocate_nondet_length_array(), allocate_object(), gen_nondet_array_init(), gen_nondet_pointer_init(), gen_nondet_struct_init(), and gen_nondet_subtype_pointer_init().
|
private |
Resolves pointer types potentially using some heuristics, for example to replace pointers to interface types with pointers to concrete implementations.
Definition at line 60 of file java_object_factory.cpp.
Referenced by gen_nondet_pointer_init().
|
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 39 of file java_object_factory.cpp.
Referenced by gen_nondet_pointer_init().
|
private |
The symbol table.
Definition at line 52 of file java_object_factory.cpp.
Referenced by allocate_nondet_length_array(), allocate_object(), gen_nondet_array_init(), gen_nondet_struct_init(), and gen_nondet_subtype_pointer_init().
|
private |
Every new variable initialized by the code emitted by the methods of this class gets a symbol in the symbol table, and such symbols are also added to this vector.
Definition at line 27 of file java_object_factory.cpp.
Referenced by allocate_nondet_length_array(), allocate_object(), and gen_nondet_array_init().