71 const typet &target_type,
80 const exprt &max_length_expr,
81 const typet &element_type,
86 std::vector<const symbolt *> &_symbols_created,
126 const typet &override_type,
162 const std::string &basename_prefix,
163 const exprt &min_length_expr,
164 const exprt &max_length_expr,
169 const exprt &instance_expr,
188 const exprt &target_expr,
189 const typet &allocate_type,
194 std::vector<const symbolt *> &symbols_created,
200 if(allocate_type.
id()!=ID_empty)
218 symbols_created.push_back(&malloc_sym);
221 output_code.
add(assign);
226 code.add_source_location()=
loc;
227 output_code.
add(code);
236 output_code.
add(code);
252 const exprt &target_expr,
258 std::vector<const symbolt *> symbols_created;
273 for(
const symbolt *
const symbol_ptr : symbols_created)
277 output_code.
add(decl);
280 for(
const auto &code : tmp_block.
statements())
281 output_code.
add(code);
299 const exprt &target_expr,
300 const typet &allocate_type,
303 const typet &allocate_type_resolved=
ns.
follow(allocate_type);
305 bool cast_needed=allocate_type_resolved!=target_type;
314 "tmp_object_factory",
327 code.add_source_location()=
loc;
328 assignments.
add(code);
404 const typet &target_type,
413 if(target_type.
id() == ID_struct)
419 assignments, expr, depth + 1, update_in_place, location);
422 if(target_class_type.get_base(
"java::java.lang.Enum"))
440 target.
type().
id() == ID_pointer,
"Pointer-typed expression expected");
450 if(target.
id() == ID_address_of)
451 init_expr = target.
op0();
506 "insert_entry should only be called once");
524 if(type.
id() == ID_signedbv)
526 else if(type.
id() == ID_unsignedbv)
571 const std::size_t &min_nondet_string_length,
572 const std::size_t &max_nondet_string_length,
580 ::implements_java_char_sequence(struct_expr.
type()));
601 if(struct_type.
get_tag() ==
"java.lang.CharSequence")
615 "tmp_object_factory",
625 const exprt min_length =
630 if(max_nondet_string_length <=
max_value(length_expr.
type()))
638 const exprt data_expr =
646 array_pointer, data_expr, symbol_table,
loc, code);
649 data_expr, length_expr, symbol_table,
loc, code);
657 array_pointer, length_expr,
" -~", symbol_table,
loc, code);
707 generic_parameter_specialization_map_keys(
710 replacement_pointer_type,
ns.
follow(replacement_pointer_type.subtype()));
713 assignments, alloc_type, replacement_pointer_type, depth, location);
740 if(subtype.
id()==ID_struct)
778 if(
const auto class_type = type_try_dynamic_cast<java_class_typet>(subtype))
780 if(class_type->get_base(
"java::java.lang.Enum") && !must_be_null)
782 const irep_idt &class_name = class_type->get_name();
798 update_in_place_assignments,
811 assignments.
append(update_in_place_assignments);
837 new_object_assignments.
add(set_null_inst);
843 new_object_assignments.
append(non_null_inst);
858 std::move(set_null_inst),
859 std::move(non_null_inst));
861 new_object_assignments.
add(std::move(null_check));
868 assignments.
append(new_object_assignments);
873 "No-update and must-update should have already been resolved");
877 std::move(update_in_place_assignments),
878 std::move(new_object_assignments));
880 assignments.
add(std::move(update_check));
920 "tmp_object_factory",
954 const std::list<std::string> &string_input_values,
958 for(
const auto &val : string_input_values)
960 exprt name_literal(ID_java_string_literal);
961 name_literal.
set(ID_value, val);
1018 const componentst &components=struct_type.
components();
1027 bool skip_special_string_fields =
false;
1033 class_identifier = struct_tag;
1035 const bool is_char_sequence =
1038 const bool has_length_and_data =
1040 const bool has_string_input_values =
1043 if(is_char_sequence && has_length_and_data && has_string_input_values)
1045 skip_special_string_fields =
true;
1070 auto initial_object =
1080 if(is_char_sequence && has_length_and_data)
1082 skip_special_string_fields =
true;
1105 if(name==
"@class_identifier")
1109 else if(name ==
"cproverMonitorCount")
1119 assignments.
add(code);
1121 else if(skip_special_string_fields && (name ==
"length" || name ==
"data"))
1128 INVARIANT(!name.
empty(),
"Each component of a struct must have a name");
1130 bool _is_sub=name[0]==
'@';
1161 "java::" +
id2string(struct_tag) +
".cproverNondetInitialize:()V";
1208 const typet &override_type,
1217 if(type.
id()==ID_pointer)
1225 generic_parameter_specialization_map_keys(
1239 else if(type.
id()==ID_struct)
1247 generic_parameter_specialization_map_keys(
1251 const typet &symbol = override_ ? override_type : expr.
type();
1278 assignments.
add(assign);
1294 const std::string &basename_prefix,
1295 const exprt &min_value_expr,
1296 const exprt &max_value_expr,
1302 min_value_expr.
type(),
1309 const auto &int_symbol_expr = int_symbol.symbol_expr();
1326 const auto min_assume_expr =
1328 const auto max_assume_expr =
1333 return int_symbol_expr;
1354 const exprt &max_length_expr,
1355 const typet &element_type,
1360 "nondet_array_length",
1367 java_new_array.set(ID_length_upper_bound, max_length_expr);
1368 java_new_array.type().subtype().set(ID_element_type, element_type);
1371 assignments.
add(assign);
1393 const typet &element_type =
1394 static_cast<const typet &>(expr.
type().
subtype().
find(ID_element_type));
1404 assignments, expr, max_length_expr, element_type, location);
1412 "Java struct array does not conform to expectations");
1416 const member_exprt length_expr(deref_expr,
"length", comps[1].type());
1426 init_array_expr.
type(),
1433 const auto &array_init_symexpr=array_init_symbol.
symbol_expr();
1434 code_assignt data_assign(array_init_symexpr, init_array_expr);
1436 assignments.
add(data_assign);
1457 assignments.
add(std::move(init_head_label));
1464 equal_exprt(counter_expr, length_expr), goto_done);
1466 assignments.
add(std::move(done_test));
1473 equal_exprt(counter_expr, max_length_expr), std::move(goto_done));
1475 assignments.
add(std::move(max_test));
1479 plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.
type()),
1500 child_update_in_place,
1506 assignments.
add(std::move(incr));
1507 assignments.
add(std::move(goto_head));
1508 assignments.
add(std::move(init_done_label));
1528 "The $VALUES array (populated by clinit_wrapper) should be in the " 1536 const auto &comps = deref_struct_type.components();
1537 const member_exprt length_expr(deref_expr,
"length", comps[1].type());
1550 plus_exprt plus(enum_array_expr, index_expr);
1553 assignments.
add(enum_assign);
1562 const std::vector<const symbolt *> &symbols_created,
1568 for(
const symbolt *
const symbol_ptr : symbols_created)
1570 if(!symbol_ptr->is_static_lifetime)
1574 init_code.
add(decl);
1604 main_symbol.
mode=ID_java;
1606 main_symbol.
name=identifier;
1608 main_symbol.
type=type;
1615 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
1618 std::vector<const symbolt *> symbols_created;
1619 symbols_created.push_back(main_symbol_ptr);
1625 pointer_type_selector);
1642 init_code.
append(assignments);
1692 std::vector<const symbolt *> symbols_created;
1697 object_factory_parameters,
1699 pointer_type_selector);
1716 init_code.
append(assignments);
1735 object_factory_parameters,
1738 pointer_type_selector);
1760 object_factory_parameters,
1761 pointer_type_selector,
1773 const exprt &instance_expr,
1782 assignments.
add(fun_call);
The type of an expression, extends irept.
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)
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...
Semantic type conversion.
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 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 java_object_factory_parameterst object_factory_parameters
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a 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.
java_object_factoryt(std::vector< const symbolt * > &_symbols_created, const source_locationt &loc, const java_object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Goto Programs with Functions.
code_operandst & statements()
symbol_table_baset & symbol_table
The symbol table.
std::vector< componentt > componentst
Fresh auxiliary symbol creation.
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.
const symbol_exprt gen_nondet_int_init(code_blockt &assignments, const std::string &basename_prefix, const exprt &min_length_expr, const exprt &max_length_expr, const source_locationt &location)
Nondeterministically initializes an int i in the range min <= i <= max, where min is the integer repr...
A struct tag type, i.e., struct_typet with an identifier.
codet representation of a goto statement.
typet & type()
Return the type of the expression.
const irep_idt & get_name() const
Get the name of the struct, which can be used to look up its symbol in the symbol table.
#define CHECK_RETURN(CONDITION)
Structure type, corresponds to C style structs.
std::list< std::string > string_input_values
Force one of finitely many explicitly given input strings.
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
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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
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 insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type t...
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.
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Expression Initialization.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
void add(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
code_blockt generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
Pick nondeterministically between imperative actions 'switch_cases'.
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
A codet representing the declaration of a local variable.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
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.
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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 ...
codet representation of 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_exprt that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::unordered_set< irep_idt > & recursion_set
Recursion set to modify.
codet representation of a function call statement.
The plus expression Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
mp_integer largest() const
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void gen_method_call_if_present(code_blockt &assignments, const exprt &instance_expr, const irep_idt &method_name)
Adds a call for the given method to the end of assignments if the method exists in the symbol table.
Operator to return the address of an object.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
void gen_nondet_enum_init(code_blockt &assignments, const exprt &expr, const java_class_typet &java_class_type, const source_locationt &location)
We nondet-initialize enums to be equal to one of the constants defined for their type: int i = nondet...
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
The Boolean constant false.
bool has_component(const irep_idt &component_name) const
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.
namespacet ns
A namespace built from exclusively one symbol table - the one above.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a 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)
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.
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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.
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.
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
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(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 reference-typed object tree rooted at expr, allocating child objects...
const source_locationt & source_location() const
#define UNREACHABLE
This should be used to mark dead code.
static mp_integer max_value(const typet &type)
Get max value for an integer type.
size_t min_nondet_string_length
Minimum value for the non-deterministically-chosen length of a string.
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 th...
symbol_exprt get_or_create_string_literal_symbol(const exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
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.
alternate_casest get_string_input_values_code(const exprt &expr, const std::list< std::string > &string_input_values, symbol_table_baset &symbol_table)
Creates an alternate_casest vector in which each item contains an assignment of a string from string_...
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...
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...
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()
A codet representing sequential composition of program statements.
A codet representing a skip statement.
codet representation of an if-then-else statement.
Expression to hold a symbol (variable)
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
exprt dynamic_object(const exprt &pointer)
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.
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...
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
const irept & find(const irep_namet &name) const
void initialize_nondet_string_fields(struct_exprt &struct_expr, code_blockt &code, const std::size_t &min_nondet_string_length, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable)
Initialise length and data fields for a nondeterministic String structure.
const source_locationt & loc
The source location for new statements emitted during the operation of the methods in this class.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const java_class_typet & to_java_class_type(const typet &type)
A codet representing an assignment in the program.
void set(const irep_namet &name, const irep_idt &value)
std::vector< codet > alternate_casest
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.