cprover
java_object_factoryt Class Reference
Collaboration diagram for java_object_factoryt:
[legend]

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_locationtloc
 
std::unordered_set< irep_idt, irep_id_hashrecursion_set
 
bool assume_non_null
 
size_t max_nondet_array_length
 
symbol_tabletsymbol_table
 
namespacet ns
 

Detailed Description

Definition at line 54 of file java_object_factory.cpp.

Constructor & Destructor Documentation

§ java_object_factoryt()

java_object_factoryt::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 
)
inline

Member Function Documentation

§ 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 
)
private

Allocates a fresh array.

Single-use at the moment, but useful to keep as a separate function for downstream branches.

parameters: 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)
Returns
Appends instructions to 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().

§ allocate_object()

exprt java_object_factoryt::allocate_object ( code_blockt assignments,
const exprt target_expr,
const typet allocate_type,
bool  create_dynamic_objects 
)
Parameters
assignmentsThe code block to add code to
target_exprThe expression which we are allocating a symbol for
allocate_type
create_dynamic_objectsWhether 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().

§ gen_nondet_array_init()

§ gen_nondet_init()

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.

Parameters
exprThe expression which we are generating a non-determinate value for
is_sub
class_identifier
create_dynamic_objectsIf true, allocate variables on the heap
overrideIgnore 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_typeType 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().

§ gen_nondet_pointer_init()

void java_object_factoryt::gen_nondet_pointer_init ( code_blockt assignments,
const exprt expr,
const irep_idt class_identifier,
bool  create_dynamic_objects,
const pointer_typet pointer_type 
)
private

Initialises a primitive or object tree rooted at expr, of type pointer.

It allocates child objects as necessary and nondet-initialising their members,

Parameters
assignments- the code block we are building with initilisation code
exprlvalue 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_objectsif 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().

§ gen_nondet_struct_init()

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

Initialises an object tree rooted at expr, allocating child objects as necessary and nondet-initialising their members.

Parameters
assignmentsThe code block to append the new instructions to
exprpointer-typed lvalue expression to initialise
is_subIf 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_identifierclsid to initialise .lang.Object.
create_dynamic_objectsif 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().

§ gen_pointer_target_init()

void java_object_factoryt::gen_pointer_target_init ( code_blockt assignments,
const exprt expr,
const typet target_type,
bool  create_dynamic_objects 
)
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.

parameters: expr: pointer-typed lvalue expression to initialise
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().

§ get_null_assignment()

code_assignt java_object_factoryt::get_null_assignment ( const exprt expr,
const pointer_typet ptr_type 
)
private

Adds an instruction to init_code null-initialising expr.

parameters: expr: pointer-typed lvalue expression to initialise
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().

Member Data Documentation

§ assume_non_null

bool java_object_factoryt::assume_non_null
private

Definition at line 59 of file java_object_factory.cpp.

Referenced by gen_nondet_pointer_init().

§ loc

§ max_nondet_array_length

size_t java_object_factoryt::max_nondet_array_length
private

Definition at line 60 of file java_object_factory.cpp.

Referenced by gen_nondet_array_init().

§ ns

namespacet java_object_factoryt::ns
private

§ recursion_set

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

Definition at line 58 of file java_object_factory.cpp.

Referenced by gen_nondet_pointer_init(), and gen_nondet_struct_init().

§ symbol_table

symbol_tablet& java_object_factoryt::symbol_table
private

§ symbols_created

std::vector<const symbolt *>& java_object_factoryt::symbols_created
private

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