cprover
|
#include "java_bytecode_language.h"
#include "select_pointer_type.h"
#include <util/message.h>
#include <util/std_code.h>
#include <util/symbol_table.h>
Go to the source code of this file.
Enumerations | |
enum | allocation_typet { allocation_typet::GLOBAL, allocation_typet::LOCAL, allocation_typet::DYNAMIC } |
Selects the kind of allocation used by java_object_factory et al. More... | |
enum | update_in_placet { update_in_placet::NO_UPDATE_IN_PLACE, update_in_placet::MAY_UPDATE_IN_PLACE, update_in_placet::MUST_UPDATE_IN_PLACE } |
Functions | |
exprt | object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, allocation_typet alloc_type, const source_locationt &location, 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... | |
exprt | object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_tablet &symbol_table, const java_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 java_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... | |
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 java_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... | |
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=false) |
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... | |
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) that can allocate and initialize non-deterministically both primitive Java types and objects. The non-deterministic initialization of one object triggers the non-deterministic initialization of all its fields, which in turn could be references to other objects. We thus speak about an object tree.
This is useful for, e.g., the creation of a verification harness (non-det initialization of the parameters of the method to verify), mocking methods that are called but for which we don't have a body (overapproximating the return value and possibly side effects).
The two main APIs are gen_nondet_init() and object_factory() (which calls gen_nondet_init()), at the bottom of the file. A call to
gen_nondet_init(expr, code, ..., update_in_place)
appends to code
(a code_blockt) a sequence of statements that non-deterministically initialize the expr
(which is expected to be an l-value exprt) with a primitive or reference value of type equal to or compatible with expr.type()
– see documentation for the argument pointer_type_selector
for additional details. gen_nondet_init() is the starting point of a recursive algorithm, and most other functions in this file are different (recursive or base) cases depending on the type of expr.
The code generated mainly depends on the parameter update_in_place
. Assume that expr
is a reference to an object (in our IR, that means a pointer to a struct).
When update_in_place == NO_UPDATE_IN_PLACE, the following code is generated:
When update_in_place == MUST_UPDATE_IN_PLACE, the following code is generated (assuming that MyClass has fields "int x" and "OtherClass y"):
When update_in_place == MAY_UPDATE_IN_PLACE, the following code is generated:
Definition in file java_object_factory.h.
|
strong |
Selects the kind of allocation used by java_object_factory et al.
Enumerator | |
---|---|
GLOBAL | Allocate global objects. |
LOCAL | Allocate local stacked objects. |
DYNAMIC | Allocate dynamic objects (using MALLOC) |
Definition at line 82 of file java_object_factory.h.
|
strong |
Enumerator | |
---|---|
NO_UPDATE_IN_PLACE | |
MAY_UPDATE_IN_PLACE | |
MUST_UPDATE_IN_PLACE |
Definition at line 111 of file java_object_factory.h.
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.
target_expr | expression to which the necessary memory will be allocated, its type should be pointer to allocate_type |
allocate_type | type of the object allocated |
symbol_table | symbol table |
loc | location in the source |
function_id | function ID to associate with auxiliary variables |
output_code | code block to which the necessary code is added |
symbols_created | created symbols to be declared by the caller |
cast_needed | Boolean flags saying where we need to cast the malloc site |
Definition at line 187 of file java_object_factory.cpp.
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.
target_expr | expression to which the necessary memory will be allocated |
symbol_table | symbol table |
loc | location in the source |
function_id | function ID to associate with auxiliary variables |
output_code | code block to which the necessary code is added |
Definition at line 251 of file java_object_factory.cpp.
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 java_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.
expr | Lvalue expression to initialize. | |
[out] | init_code | A 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_table | The 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. | |
loc | Source location to which all generated code will be associated to. | |
skip_classid | If true, skip initializing field @class_identifier . | |
alloc_type | Allocate new objects as global objects (GLOBAL) or as local variables (LOCAL) or using malloc (DYNAMIC). | |
object_factory_parameters | Parameters for the generation of non deterministic objects. | |
pointer_type_selector | The pointer_selector to use to resolve pointer types where required. | |
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 |
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 1681 of file java_object_factory.cpp.
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 java_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 1742 of file java_object_factory.cpp.
exprt object_factory | ( | const typet & | type, |
const irep_idt | base_name, | ||
code_blockt & | init_code, | ||
symbol_table_baset & | symbol_table, | ||
java_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.
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 1590 of file java_object_factory.cpp.
exprt object_factory | ( | const typet & | type, |
const irep_idt | base_name, | ||
code_blockt & | init_code, | ||
symbol_tablet & | symbol_table, | ||
const java_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 1720 of file java_object_factory.cpp.