69 const typet &target_type,
78 const exprt &max_length_expr,
79 const typet &element_type,
84 std::vector<const symbolt *> &_symbols_created,
118 const typet &override_type,
167 const exprt &target_expr,
168 const typet &allocate_type,
173 std::vector<const symbolt *> &symbols_created,
179 if(allocate_type.
id()!=ID_empty)
197 symbols_created.push_back(&malloc_sym);
205 code.add_source_location()=
loc;
230 const exprt &target_expr,
236 std::vector<const symbolt *> symbols_created;
251 for(
const symbolt *
const symbol_ptr : symbols_created)
255 output_code.
add(decl);
276 const exprt &target_expr,
277 const typet &allocate_type,
280 const typet &allocate_type_resolved=
ns.
follow(allocate_type);
282 bool cast_needed=allocate_type_resolved!=target_type;
291 "tmp_object_factory",
304 code.add_source_location()=
loc;
379 const typet &target_type,
388 if(target_type.
id()==ID_struct &&
394 assignments, expr, depth + 1, update_in_place, location);
413 target.
type().
id()==ID_pointer,
414 "Pointer-typed expression expected");
424 if(target.
id()==ID_address_of)
425 init_expr=target.
op0();
482 "insert_entry should only be called once");
500 if(type.
id() == ID_signedbv)
502 else if(type.
id() == ID_unsignedbv)
559 const std::size_t &max_nondet_string_length,
590 if(struct_type.
get_tag() ==
"java.lang.CharSequence")
593 struct_expr, ns,
symbol_typet(
"java::java.lang.String"));
604 "tmp_object_factory",
620 if(max_nondet_string_length <=
max_value(length_expr.
type()))
633 data_ptr_type,
"",
"string_data_pointer",
loc, ID_java, symbol_table);
634 const auto data_pointer = data_pointer_sym.
symbol_expr();
643 const exprt nondet_array =
653 array_pointer, data_expr, symbol_table,
loc, code);
656 data_expr, length_expr, symbol_table,
loc, code);
664 array_pointer, length_expr,
" -~", symbol_table,
loc, code);
714 generic_parameter_specialization_map_keys(
717 replacement_pointer_type,
ns.
follow(replacement_pointer_type.subtype()));
720 assignments, alloc_type, replacement_pointer_type, depth, location);
747 if(subtype.
id()==ID_struct)
777 update_in_place_assignments,
790 assignments.
append(update_in_place_assignments);
810 const bool allow_null =
821 new_object_assignments.
add(set_null_inst);
827 new_object_assignments.
append(non_null_inst);
845 new_object_assignments.
add(null_check);
852 assignments.
append(new_object_assignments);
857 "No-update and must-update should have already been resolved");
860 update_check.
cond() =
862 update_check.
then_case()=update_in_place_assignments;
863 update_check.
else_case()=new_object_assignments;
865 assignments.
add(update_check);
903 "tmp_object_factory",
972 const componentst &components=struct_type.
components();
981 bool skip_special_string_fields =
false;
987 class_identifier = struct_tag;
995 exprt initial_object =
1005 skip_special_string_fields =
1019 for(
const auto &component : components)
1021 const typet &component_type=component.type();
1022 irep_idt name=component.get_name();
1026 if(name==
"@class_identifier")
1030 else if(name ==
"cproverMonitorCount")
1042 else if(skip_special_string_fields && (name ==
"length" || name ==
"data"))
1050 INVARIANT(!name.
empty(),
"Each component of a struct must have a name");
1052 bool _is_sub=name[0]==
'@';
1083 "java::" +
id2string(struct_tag) +
".cproverNondetInitialize:()V";
1089 fun_call.
function() = func->symbol_expr();
1093 assignments.
add(fun_call);
1138 const typet &override_type,
1147 if(type.
id()==ID_pointer)
1155 generic_parameter_specialization_map_keys(
1169 else if(type.
id()==ID_struct)
1177 generic_parameter_specialization_map_keys(
1181 const typet &symbol = override_ ? override_type : expr.
type();
1228 const exprt &max_length_expr,
1229 const typet &element_type,
1235 "nondet_array_length",
1240 const auto &length_sym_expr=length_sym.
symbol_expr();
1260 assume2(length_sym_expr, ID_le, max_length_expr);
1268 java_new_array.set(ID_length_upper_bound, max_length_expr);
1269 java_new_array.type().subtype().set(ID_element_type, element_type);
1294 const typet &element_type =
1305 assignments, expr, max_length_expr, element_type, location);
1313 "Java struct array does not conform to expectations");
1317 const member_exprt length_expr(deref_expr,
"length", comps[1].type());
1327 init_array_expr.
type(),
1334 const auto &array_init_symexpr=array_init_symbol.
symbol_expr();
1382 plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.
type()),
1403 child_update_in_place,
1420 const std::vector<const symbolt *> &symbols_created,
1426 for(
const symbolt *
const symbol_ptr : symbols_created)
1428 if(!symbol_ptr->is_static_lifetime)
1432 init_code.
add(decl);
1462 main_symbol.
mode=ID_java;
1464 main_symbol.
name=identifier;
1466 main_symbol.
type=type;
1473 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
1476 std::vector<const symbolt *> symbols_created;
1477 symbols_created.push_back(main_symbol_ptr);
1483 pointer_type_selector);
1500 init_code.
append(assignments);
1550 std::vector<const symbolt *> symbols_created;
1555 object_factory_parameters,
1557 pointer_type_selector);
1574 init_code.
append(assignments);
1593 object_factory_parameters,
1596 pointer_type_selector);
1618 object_factory_parameters,
1619 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.
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, const source_locationt &location)
Initializes the pointer-typed lvalue expression expr to point to an object of type target_type...
exprt size_of_expr(const typet &type, const namespacet &ns)
const codet & then_case() const
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, const source_locationt &location)
Initializes an object tree rooted at expr, allocating child objects as necessary and nondet-initializ...
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)
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.
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.
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 d...
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
A reference into the symbol table.
size_t max_nondet_tree_depth
Maximum depth for object hierarchy on input.
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
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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.
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 gen_nondet_pointer_init(code_blockt &assignments, const exprt &expr, allocation_typet alloc_type, const pointer_typet &pointer_type, size_t depth, const update_in_placet &update_in_place, const source_locationt &location)
Initializes a pointer expr of type pointer_type to a primitive-typed value or an object tree...
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
const java_method_typet & to_java_method_type(const typet &type)
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...
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.
std::size_t component_number(const irep_idt &component_name) const
symbol_exprt gen_nondet_subtype_pointer_init(code_blockt &assignments, allocation_typet alloc_type, const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location)
Generate codet assignments to initalize the selected concrete type.
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 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, const source_locationt &location)
Initializes a primitive-typed or referece-typed object tree rooted at expr, allocating child objects ...
const source_locationt & source_location() const
static mp_integer max_value(const typet &type)
Get max value for an integer type.
void allocate_nondet_length_array(code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type, const source_locationt &location)
Allocates a fresh array and emits an assignment writing to lhs the address of the new array...
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()
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.
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
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...
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr, size_t depth, update_in_placet, const source_locationt &location)
Create code to initialize a Java array whose size will be at most max_nondet_array_length.