cprover
|
#include "java_object_factory.h"
#include <util/expr_initializer.h>
#include <util/fresh_symbol.h>
#include <util/nondet_bool.h>
#include <util/pointer_offset_size.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_functions.h>
#include "generic_parameter_specialization_map_keys.h"
#include "java_root_class.h"
Go to the source code of this file.
Classes | |
class | java_object_factoryt |
class | recursion_set_entryt |
Recursion-set entry owner class. More... | |
Functions | |
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. 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... | |
static mp_integer | max_value (const typet &type) |
Get max value for an integer type. More... | |
static codet | make_allocate_code (const symbol_exprt &lhs, const exprt &size) |
Create code allocating object of size size and assigning it to lhs More... | |
bool | initialize_nondet_string_fields (struct_exprt &struct_expr, code_blockt &code, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable) |
Check if a structure is a nondeterministic String structure, and if it is initialize its length and data fields. More... | |
static void | declare_created_symbols (const std::vector< const symbolt *> &symbols_created, const source_locationt &loc, code_blockt &init_code) |
Add code_declt instructions to init_code for every non-static symbol in symbols_created More... | |
exprt | object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, 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. 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 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... | |
exprt | object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_tablet &symbol_table, const 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 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 | ||
) |
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 |
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 166 of file java_object_factory.cpp.
References exprt::add_source_location(), exprt::copy_to_operands(), get_fresh_aux_symbol(), irept::id(), id2string(), INVARIANT, irept::is_nil(), loc, object_size(), pointer_type(), size_of_expr(), symbolt::symbol_expr(), to_pointer_type(), and exprt::type().
Referenced by allocate_dynamic_object_with_decl(), and java_object_factoryt::allocate_object().
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 |
output_code | code block to which the necessary code is added |
Definition at line 229 of file java_object_factory.cpp.
References code_blockt::add(), exprt::add_source_location(), allocate_dynamic_object(), dynamic_object(), loc, exprt::operands(), typet::subtype(), to_code(), and exprt::type().
Referenced by java_string_library_preprocesst::allocate_fresh_array(), java_string_library_preprocesst::allocate_fresh_string(), and java_string_library_preprocesst::make_argument_for_format().
|
static |
Add code_declt instructions to init_code
for every non-static symbol in symbols_created
symbols_created | list of symbols | |
loc | source location for new code_declt instances | |
[out] | init_code | gets code_declt for each symbol |
Definition at line 1419 of file java_object_factory.cpp.
References code_blockt::add(), exprt::add_source_location(), and loc.
Referenced by gen_nondet_init(), and object_factory().
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 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 1539 of file java_object_factory.cpp.
References code_blockt::append(), declare_created_symbols(), java_object_factoryt::gen_nondet_init(), and loc.
Referenced by java_simple_method_stubst::create_method_stub(), java_simple_method_stubst::create_method_stub_at(), gen_nondet_init(), get_gen_nondet_init_instructions(), stub_global_initializer_factoryt::get_stub_initializer_body(), and java_static_lifetime_init().
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 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 1600 of file java_object_factory.cpp.
References gen_nondet_init(), and loc.
bool initialize_nondet_string_fields | ( | struct_exprt & | struct_expr, |
code_blockt & | code, | ||
const std::size_t & | max_nondet_string_length, | ||
const source_locationt & | loc, | ||
const irep_idt & | function_id, | ||
symbol_table_baset & | symbol_table, | ||
bool | printable | ||
) |
Check if a structure is a nondeterministic String structure, and if it is initialize its length and data fields.
struct_expr | [out]: struct that we may initialize |
code | block to add pre-requisite declarations (e.g. to allocate a data array) |
max_nondet_string_length | maximum length of strings to initialize |
loc | location in the source |
function_id | function ID to associate with auxiliary variables |
symbol_table | the symbol table |
printable | if true, the nondet string must consist of printable characters only |
The code produced is of the form:
Unit tests in unit/java_bytecode/java_object_factory/
ensure it is the case.
Definition at line 556 of file java_object_factory.cpp.
References code_blockt::add(), add_array_to_length_association(), add_character_set_constraint(), add_pointer_to_array_association(), struct_union_typet::component_number(), namespace_baset::follow(), from_integer(), get_fresh_aux_symbol(), struct_union_typet::get_tag(), struct_union_typet::has_component(), id2string(), java_string_library_preprocesst::implements_java_char_sequence(), java_char_type(), java_int_type(), loc, make_allocate_code(), make_nondet_infinite_char_array(), max_value(), exprt::operands(), pointer_type(), set_class_identifier(), symbolt::symbol_expr(), to_struct_type(), and exprt::type().
Referenced by java_object_factoryt::gen_nondet_struct_init().
|
static |
Create code allocating object of size size
and assigning it to lhs
lhs | : pointer which will be allocated |
size | : size of the object |
lhs
Definition at line 511 of file java_object_factory.cpp.
References exprt::copy_to_operands(), exprt::source_location(), and exprt::type().
Referenced by initialize_nondet_string_fields().
|
static |
Get max value for an integer type.
type | Type to find maximum value for |
Definition at line 498 of file java_object_factory.cpp.
References irept::id(), unsignedbv_typet::largest(), signedbv_typet::largest(), to_signedbv_type(), to_unsignedbv_type(), and UNREACHABLE.
Referenced by c_typecheck_baset::enum_constant_type(), c_typecheck_baset::enum_underlying_type(), initialize_nondet_string_fields(), and c_typecheck_baset::typecheck_c_enum_type().
exprt object_factory | ( | const typet & | type, |
const irep_idt | base_name, | ||
code_blockt & | init_code, | ||
symbol_table_baset & | symbol_table, | ||
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 1448 of file java_object_factory.cpp.
References code_blockt::append(), symbolt::base_name, CHECK_RETURN, declare_created_symbols(), goto_functionst::entry_point(), object_factory_parameterst::function_id, java_object_factoryt::gen_nondet_init(), id2string(), symbolt::is_static_lifetime, loc, symbolt::location, symbolt::mode, symbol_table_baset::move(), symbolt::name, NO_UPDATE_IN_PLACE, symbolt::symbol_expr(), and symbolt::type.
Referenced by java_build_arguments(), and object_factory().
exprt object_factory | ( | const typet & | type, |
const irep_idt | base_name, | ||
code_blockt & | init_code, | ||
symbol_tablet & | symbol_table, | ||
const 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 1578 of file java_object_factory.cpp.
References object_factory().