69 const typet &target_type,
77 const exprt &max_length_expr,
78 const typet &element_type);
82 std::vector<const symbolt *> &_symbols_created,
115 const typet &override_type,
161 const exprt &target_expr,
162 const typet &allocate_type,
167 std::vector<const symbolt *> &symbols_created,
173 if(allocate_type.
id()!=ID_empty)
190 symbols_created.push_back(&malloc_sym);
198 code.add_source_location()=
loc;
223 const exprt &target_expr,
229 std::vector<const symbolt *> symbols_created;
244 for(
const symbolt *
const symbol_ptr : symbols_created)
248 output_code.
add(decl);
269 const exprt &target_expr,
270 const typet &allocate_type,
273 const typet &allocate_type_resolved=
ns.
follow(allocate_type);
275 bool cast_needed=allocate_type_resolved!=target_type;
284 "tmp_object_factory",
297 code.add_source_location()=
loc;
372 const typet &target_type,
380 if(target_type.
id()==ID_struct &&
408 target.
type().
id()==ID_pointer,
409 "Pointer-typed expression expected");
419 if(target.
id()==ID_address_of)
420 init_expr=target.
op0();
476 "insert_entry should only be called once");
494 if(type.
id() == ID_signedbv)
496 else if(type.
id() == ID_unsignedbv)
547 const std::size_t &max_nondet_string_length,
569 struct_type.
get_tag() ==
"java.lang.CharSequence" 570 ?
"java::java.lang.String" 574 const symbol_typet jlo_symbol(
"java::java.lang.Object");
592 "tmp_object_factory",
608 if(max_nondet_string_length <=
max_value(length_expr.
type()))
621 data_ptr_type,
"",
"string_data_pointer",
loc, ID_java, symbol_table);
622 const auto data_pointer = data_pointer_sym.
symbol_expr();
631 const exprt nondet_array =
635 struct_expr.copy_to_operands(length_expr);
641 array_pointer, data_expr, symbol_table,
loc, code);
644 data_expr, length_expr, symbol_table,
loc, code);
646 struct_expr.copy_to_operands(array_pointer);
652 array_pointer, length_expr,
" -~", symbol_table,
loc, code);
674 const std::size_t &max_nondet_string_length,
687 if(struct_type.get_bool(ID_incomplete_class))
691 expr, symbol_table,
loc, function_id, code);
696 max_nondet_string_length,
751 generic_parameter_specialization_map_keys(
754 replacement_pointer_type,
ns.
follow(replacement_pointer_type.subtype()));
757 assignments, alloc_type, replacement_pointer_type, depth);
784 if(subtype.
id()==ID_struct)
814 update_in_place_assignments,
826 assignments.
append(update_in_place_assignments);
838 bool string_init_succeeded =
false;
843 string_init_succeeded =
854 if(!string_init_succeeded)
867 const bool allow_null =
878 new_object_assignments.
add(set_null_inst);
884 new_object_assignments.
append(non_null_inst);
902 new_object_assignments.
add(null_check);
909 assignments.
append(new_object_assignments);
914 "No-update and must-update should have already been resolved");
918 update_check.
then_case()=update_in_place_assignments;
919 update_check.
else_case()=new_object_assignments;
921 assignments.
add(update_check);
958 "tmp_object_factory",
1025 const componentst &components=struct_type.
components();
1038 class_identifier = struct_tag;
1057 for(
const auto &component : components)
1059 const typet &component_type=component.type();
1060 irep_idt name=component.get_name();
1064 if(name==
"@class_identifier")
1068 else if(name==
"@lock")
1074 INVARIANT(!name.
empty(),
"Each component of a struct must have a name");
1076 bool _is_sub=name[0]==
'@';
1095 substruct_in_place);
1106 "java::" +
id2string(struct_tag) +
".cproverNondetInitialize:()V";
1112 fun_call.
function() = func->symbol_expr();
1116 assignments.
add(fun_call);
1161 const typet &override_type,
1169 if(type.
id()==ID_pointer)
1177 generic_parameter_specialization_map_keys(
1191 else if(type.
id()==ID_struct)
1199 generic_parameter_specialization_map_keys(
1203 const typet &symbol = override_ ? override_type : expr.
type();
1224 exprt rhs=type.
id()==ID_c_bool?
1250 const exprt &max_length_expr,
1251 const typet &element_type)
1256 "nondet_array_length",
1261 const auto &length_sym_expr=length_sym.
symbol_expr();
1280 assume2(length_sym_expr, ID_le, max_length_expr);
1288 java_new_array.set(ID_length_upper_bound, max_length_expr);
1289 java_new_array.type().subtype().set(ID_C_element_type, element_type);
1313 const typet &element_type=
1335 "Java struct array does not conform to expectations");
1339 const member_exprt length_expr(deref_expr,
"length", comps[1].type());
1349 init_array_expr.
type(),
1356 const auto &array_init_symexpr=array_init_symbol.
symbol_expr();
1404 plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.
type()),
1425 child_update_in_place);
1441 const std::vector<const symbolt *> &symbols_created,
1447 for(
const symbolt *
const symbol_ptr : symbols_created)
1449 if(!symbol_ptr->is_static_lifetime)
1453 init_code.
add(decl);
1483 main_symbol.
mode=ID_java;
1485 main_symbol.
name=identifier;
1487 main_symbol.
type=type;
1494 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
1497 std::vector<const symbolt *> symbols_created;
1498 symbols_created.push_back(main_symbol_ptr);
1504 pointer_type_selector);
1520 init_code.
append(assignments);
1570 std::vector<const symbolt *> symbols_created;
1575 object_factory_parameters,
1577 pointer_type_selector);
1593 init_code.
append(assignments);
1612 object_factory_parameters,
1615 pointer_type_selector);
1637 object_factory_parameters,
1638 pointer_type_selector,
The type of an expression.
irep_idt name
The unique identifier.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
allocation_typet
Selects the kind of allocation used by java_object_factory et al.
exprt size_of_expr(const typet &type, const namespacet &ns)
const codet & then_case() const
const object_factory_parameterst object_factory_parameters
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)...
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
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.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
const select_pointer_typet & pointer_type_selector
Resolves pointer types potentially using some heuristics, for example to replace pointers to interfac...
irep_idt mode
Language mode.
static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating object of size size and assigning it to lhs
const exprt & cond() const
irep_idt get_tag(const typet &type)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void copy_to_operands(const exprt &expr)
Goto Programs with Functions.
symbol_table_baset & symbol_table
The symbol table.
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
Fresh auxiliary symbol creation.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
recursion_set_entryt(std::unordered_set< irep_idt > &_recursion_set)
Initialize a recursion-set entry owner operating on a given set.
Allocate local stacked objects.
const componentst & components() const
Nondeterministic boolean helper.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
#define CHECK_RETURN(CONDITION)
exprt get_nondet_bool(const typet &type)
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const symbol_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct...
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
#define INVARIANT(CONDITION, REASON)
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_set, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
Extract member of struct or union.
void gen_nondet_pointer_init(code_blockt &assignments, const exprt &expr, const irep_idt &class_identifier, allocation_typet alloc_type, const pointer_typet &pointer_type, size_t depth, const update_in_placet &update_in_place)
Initializes a pointer expr of type pointer_type to a primitive-typed value or an object tree...
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
Expression Initialization.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
An expression denoting infinity.
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr, size_t depth, update_in_placet)
Create code to initialize a Java array whose size will be at most max_nondet_array_length.
A reference into the symbol table.
size_t max_nondet_tree_depth
Maximum depth for object hierarchy on input.
static bool add_nondet_string_pointer_initialization(const exprt &expr, const std::size_t &max_nondet_string_length, bool printable, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add code for the initialization of a string using a nondeterministic content and association of its a...
A declaration of a local variable.
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 ...
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 ...
bool string_printable
Force string content to be ASCII printable characters when set to true.
Operator to dereference a pointer.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A label for branch targets.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
#define PRECONDITION(CONDITION)
A side effect that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
std::unordered_set< irep_idt > & recursion_set
Recursion set to modify.
const typet & follow(const typet &) const
mp_integer largest() const
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)
Initializes a primitive-typed or referece-typed object tree rooted at expr, allocating child objects ...
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Operator to return the address of an object.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
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)
Initializes the pointer-typed lvalue expression expr to point to an object of type target_type...
The boolean constant false.
bool has_component(const irep_idt &component_name) const
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const bool lock, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
const void insert_pairs_for_pointer(const pointer_typet &pointer_type, const typet &pointer_subtype_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic pointer type ...
namespacet ns
A namespace built from exclusively one symbol table - the one above.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
An assumption, which must hold in subsequent code.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
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.
Allocate dynamic objects (using MALLOC)
mp_integer largest() const
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
static irep_idt entry_point()
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 th...
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)
Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializ...
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
irep_idt erase_entry
Entry to erase on destruction, if non-empty.
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.
Base class for all expressions.
size_t max_nondet_string_length
Maximum value for the non-deterministically-chosen length of a string.
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
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...
void allocate_nondet_length_array(code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type)
Allocates a fresh array and emits an assignment writing to lhs the address of the new array...
static mp_integer max_value(const typet &type)
Get max value for an integer type.
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
Recursion-set entry owner class.
std::unordered_set< irep_idt > recursion_set
This is employed in conjunction with the depth above.
source_locationt & add_source_location()
static bool implements_java_char_sequence_pointer(const typet &type)
const codet & to_code(const exprt &expr)
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)
Expression to hold a symbol (variable)
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
exprt dynamic_object(const exprt &pointer)
A statement in a programming language.
recursion_set_entryt & operator=(const recursion_set_entryt &)=delete
~recursion_set_entryt()
Removes erase_entry (if set) from the controlled set.
codet initialize_nondet_string_struct(const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable)
Initialize a nondeterministic String structure.
static bool implements_java_char_sequence(const typet &type)
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
const typet & subtype() const
symbol_exprt gen_nondet_subtype_pointer_init(code_blockt &assignments, allocation_typet alloc_type, const pointer_typet &substitute_pointer_type, size_t depth)
Generate codet assignments to initalize the selected concrete type.
An expression containing a side effect.
bool insert_entry(const irep_idt &entry)
Try to add an entry to the controlled set.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual pointer_typet convert_pointer_type(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, const namespacet &ns) const
Select what type should be used for a given pointer type.
struct constructor from list of elements
const codet & else_case() const
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 symb...
const irept & find(const irep_namet &name) const
const source_locationt & loc
The source location for new statements emitted during the operation of the methods in this class...
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.
const void insert_pairs_for_symbol(const symbol_typet &symbol_type, const typet &symbol_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type t...