cprover
|
Public Member Functions | |
java_object_factoryt (std::vector< const symbolt *> &_symbols_created, const source_locationt &loc, bool _assume_non_null, size_t _max_nondet_array_length, symbol_tablet &_symbol_table) | |
exprt | allocate_object (code_blockt &assignments, const exprt &, const typet &, bool create_dynamic_objects) |
void | gen_nondet_array_init (code_blockt &assignments, const exprt &expr) |
create code to initialize a Java array with size max_nondet_array_length , loop over elements and initialize them More... | |
void | gen_nondet_init (code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool create_dynamic_objects, bool override=false, const typet &override_type=empty_typet()) |
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point to if expr is a pointer or struct. More... | |
Private Member Functions | |
code_assignt | get_null_assignment (const exprt &expr, const pointer_typet &ptr_type) |
Adds an instruction to init_code null-initialising expr . More... | |
void | gen_pointer_target_init (code_blockt &assignments, const exprt &expr, const typet &target_type, bool create_dynamic_objects) |
Initialises an object tree rooted at expr , allocating child objects as necessary and nondet-initialising their members, or if MUST_UPDATE_IN_PLACE is set, re-initialising already-allocated objects. More... | |
void | allocate_nondet_length_array (code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type) |
Allocates a fresh array. More... | |
void | gen_nondet_pointer_init (code_blockt &assignments, const exprt &expr, const irep_idt &class_identifier, bool create_dynamic_objects, const pointer_typet &pointer_type) |
Initialises a primitive or object tree rooted at expr , of type pointer. More... | |
void | gen_nondet_struct_init (code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool create_dynamic_objects, const struct_typet &struct_type) |
Initialises an object tree rooted at expr , allocating child objects as necessary and nondet-initialising their members. More... | |
Private Attributes | |
std::vector< const symbolt * > & | symbols_created |
const source_locationt & | loc |
std::unordered_set< irep_idt, irep_id_hash > | recursion_set |
bool | assume_non_null |
size_t | max_nondet_array_length |
symbol_tablet & | symbol_table |
namespacet | ns |
Definition at line 54 of file java_object_factory.cpp.
|
inline |
Definition at line 81 of file java_object_factory.cpp.
References allocate_object(), gen_nondet_array_init(), gen_nondet_init(), gen_nondet_pointer_init(), gen_nondet_struct_init(), and pointer_type().
|
private |
Allocates a fresh array.
Single-use at the moment, but useful to keep as a separate function for downstream branches.
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 473 of file java_object_factory.cpp.
References exprt::add_source_location(), exprt::copy_to_operands(), from_integer(), gen_nondet_init(), java_int_type(), loc, exprt::move_to_operands(), new_tmp_symbol(), 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, | ||
bool | create_dynamic_objects | ||
) |
assignments | The code block to add code to |
target_expr | The expression which we are allocating a symbol for |
allocate_type | |
create_dynamic_objects | Whether to create a symbol with static lifetime or |
Definition at line 136 of file java_object_factory.cpp.
References exprt::add_source_location(), exprt::copy_to_operands(), namespace_baset::follow(), irept::id(), irept::is_nil(), loc, new_tmp_symbol(), ns, object_size(), pointer_type(), size_of_expr(), typet::subtype(), symbolt::symbol_expr(), symbol_table, symbols_created, to_pointer_type(), and exprt::type().
Referenced by gen_pointer_target_init(), and java_object_factoryt().
void java_object_factoryt::gen_nondet_array_init | ( | code_blockt & | assignments, |
const exprt & | expr | ||
) |
create code to initialize a Java array with size max_nondet_array_length
, loop over elements and initialize them
Definition at line 511 of file java_object_factory.cpp.
References exprt::add_source_location(), allocate_nondet_length_array(), as_string(), symbolt::base_name, struct_union_typet::components(), code_ifthenelset::cond(), exprt::copy_to_operands(), irept::find(), namespace_baset::follow(), from_integer(), gen_nondet_init(), irept::id(), java_int_type(), loc, max_nondet_array_length, exprt::move_to_operands(), new_tmp_symbol(), ns, pointer_type(), 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(), and java_object_factoryt().
void java_object_factoryt::gen_nondet_init | ( | code_blockt & | assignments, |
const exprt & | expr, | ||
bool | is_sub, | ||
irep_idt | class_identifier, | ||
bool | create_dynamic_objects, | ||
bool | override = false , |
||
const typet & | override_type = empty_typet() |
||
) |
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point to if expr is a pointer or struct.
expr | The expression which we are generating a non-determinate value for |
is_sub | |
class_identifier | |
create_dynamic_objects | If true, allocate variables on the heap |
override | Ignore the LHS' real 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. |
override_type | Type to use if ignoring the LHS' real type |
Definition at line 418 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(), get_nondet_bool(), irept::id(), loc, ns, pointer_type(), to_pointer_type(), to_struct_type(), and exprt::type().
Referenced by allocate_nondet_length_array(), gen_nondet_array_init(), gen_nondet_struct_init(), gen_pointer_target_init(), java_object_factoryt(), and object_factory().
|
private |
Initialises a primitive or object tree rooted at expr
, of type pointer.
It allocates child objects as necessary and nondet-initialising their members,
assignments | - the code block we are building with initilisation code |
expr | lvalue expression to initialise |
class_identifier | - the name of the class so we can identify special cases where a null pointer is not applicable. |
create_dynamic_objects | if true, use malloc to allocate objects; otherwise generate fresh static symbols. |
pointer_type | - The type of the pointer we are initalising |
Definition at line 279 of file java_object_factory.cpp.
References code_blockt::add(), code_blockt::append(), assume_non_null, code_ifthenelset::cond(), exprt::copy_to_operands(), code_ifthenelset::else_case(), namespace_baset::follow(), gen_pointer_target_init(), get_null_assignment(), struct_union_typet::get_tag(), irept::id(), ns, recursion_set, typet::subtype(), code_ifthenelset::then_case(), and to_struct_type().
Referenced by gen_nondet_init(), and java_object_factoryt().
|
private |
Initialises an object tree rooted at expr
, allocating child objects as necessary and nondet-initialising their members.
assignments | The code block to append the new instructions to |
expr | pointer-typed lvalue expression to initialise |
is_sub | If true, expr is a substructure of a larger object, which in Java necessarily means a base class. not match expr (for example, expr might be void) |
class_identifier | clsid to initialise .lang.Object. |
create_dynamic_objects | if true, use malloc to allocate objects; otherwise generate fresh static symbols. |
struct_type | - The type of the struct we are initalising |
Definition at line 350 of file java_object_factory.cpp.
References exprt::add_source_location(), as_string(), struct_union_typet::components(), exprt::copy_to_operands(), dstringt::empty(), from_integer(), gen_nondet_init(), struct_union_typet::get_tag(), INVARIANT, loc, recursion_set, and exprt::type().
Referenced by gen_nondet_init(), and java_object_factoryt().
|
private |
Initialises an object tree rooted at expr
, allocating child objects as necessary and nondet-initialising their members, or if MUST_UPDATE_IN_PLACE is set, re-initialising already-allocated objects.
target_type
: structure type to initialise, which may not match expr (for example, expr might be void) create_dynamic_objects
: if true, use malloc to allocate objects; otherwise generate fresh static symbols. update_in_place
: NO_UPDATE_IN_PLACE: initialise expr
from scratch MUST_UPDATE_IN_PLACE: reinitialise an existing object MAY_UPDATE_IN_PLACE: invalid input Definition at line 229 of file java_object_factory.cpp.
References allocate_object(), gen_nondet_array_init(), gen_nondet_init(), has_prefix(), irept::id(), id2string(), exprt::op0(), typet::subtype(), to_struct_type(), and exprt::type().
Referenced by gen_nondet_pointer_init().
|
private |
Adds an instruction to init_code
null-initialising expr
.
ptr_type
: pointer type to write Definition at line 208 of file java_object_factory.cpp.
References exprt::add_source_location(), and loc.
Referenced by gen_nondet_pointer_init().
|
private |
Definition at line 59 of file java_object_factory.cpp.
Referenced by gen_nondet_pointer_init().
|
private |
Definition at line 57 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(), get_null_assignment(), and object_factory().
|
private |
Definition at line 60 of file java_object_factory.cpp.
Referenced by gen_nondet_array_init().
|
private |
Definition at line 62 of file java_object_factory.cpp.
Referenced by allocate_object(), gen_nondet_array_init(), gen_nondet_init(), and gen_nondet_pointer_init().
|
private |
Definition at line 58 of file java_object_factory.cpp.
Referenced by gen_nondet_pointer_init(), and gen_nondet_struct_init().
|
private |
Definition at line 61 of file java_object_factory.cpp.
Referenced by allocate_nondet_length_array(), allocate_object(), and gen_nondet_array_init().
|
private |
Definition at line 56 of file java_object_factory.cpp.
Referenced by allocate_nondet_length_array(), allocate_object(), gen_nondet_array_init(), and object_factory().