Go to the documentation of this file.
67 const typet &target_type,
140 const exprt &element,
142 const typet &element_type,
192 const typet &target_type,
199 PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
202 const typet &followed_target_type = ns.
follow(target_type);
212 [
this, update_in_place, depth, location](
215 element, update_in_place, element_type, depth + 1, location);
219 type, basename_prefix);
225 if(target_class_type.get_base(
"java::java.lang.Enum"))
238 if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
241 assignments, expr, target_type, lifetime,
"tmp_object_factory");
245 if(expr.
id() == ID_address_of)
319 result += numeric_cast_v<char>(interval.
lower);
321 result += numeric_cast_v<char>(interval.
upper);
367 const std::size_t &min_nondet_string_length,
368 const std::size_t &max_nondet_string_length,
387 if(struct_type.
get_tag() ==
"java.lang.CharSequence")
405 const exprt min_length =
411 max_nondet_string_length <=
420 const exprt data_expr =
428 array_pointer, data_expr, symbol_table, loc, function_id, code);
431 data_expr, length_expr, symbol_table, loc, function_id, code);
485 const typet &followed_subtype = ns.
follow(subtype);
500 generic_parameter_specialization_map_keys(
502 generic_parameter_specialization_map_keys.
insert(
503 replacement_pointer_type, ns.
follow(replacement_pointer_type.
subtype()));
506 assignments, lifetime, replacement_pointer_type, depth, location);
540 if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
565 const auto class_type =
566 type_try_dynamic_cast<java_class_typet>(followed_subtype))
568 if(class_type->get_base(
"java::java.lang.Enum"))
570 const irep_idt &class_name = class_type->get_name();
584 if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
587 update_in_place_assignments,
600 assignments.
append(update_in_place_assignments);
615 update_in_placet::NO_UPDATE_IN_PLACE,
627 new_object_assignments.
append(non_null_inst);
642 std::move(set_null_inst),
643 std::move(non_null_inst));
645 new_object_assignments.
add(std::move(null_check));
650 if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
652 assignments.
append(new_object_assignments);
656 INVARIANT(update_in_place==update_in_placet::MAY_UPDATE_IN_PLACE,
657 "No-update and must-update should have already been resolved");
661 std::move(update_in_place_assignments),
662 std::move(new_object_assignments));
664 assignments.
add(std::move(update_check));
700 replacement_pointer,
"tmp_object_factory");
711 update_in_placet::NO_UPDATE_IN_PLACE,
714 return new_symbol_expr;
729 const std::list<std::string> &string_input_values,
733 for(
const auto &val : string_input_values)
780 const componentst &components=struct_type.
components();
793 const bool has_string_input_values =
813 (!is_sub && !skip_classid &&
860 else if(name ==
"cproverMonitorCount")
870 assignments.
add(code);
880 INVARIANT(!name.
empty(),
"Each component of a struct must have a name");
882 bool _is_sub=name[0]==
'@';
889 update_in_placet::MAY_UPDATE_IN_PLACE :
912 cprover_nondet_initialize = resolve_inherited_component(
913 "java::" +
id2string(struct_tag),
"cproverNondetInitialize:()V",
true);
915 if(cprover_nondet_initialize)
917 const symbolt &cprover_nondet_initialize_symbol =
918 ns.
lookup(cprover_nondet_initialize->get_full_component_identifier());
949 const auto &aux_int =
950 allocate_local_symbol(
java_int_type(),
"assume_integral_tmp");
955 assignments.
add(aux_assign);
1008 const typet &type = override_type.has_value() ? *override_type : expr.
type();
1012 if(type.
id()==ID_pointer)
1020 generic_parameter_specialization_map_keys(
1022 generic_parameter_specialization_map_keys.
insert(
1034 else if(followed_type.
id() == ID_struct)
1042 generic_parameter_specialization_map_keys(
1046 const typet &symbol =
1047 override_type.has_value() ? *override_type : expr.
type();
1049 generic_parameter_specialization_map_keys.
insert(
1068 exprt rhs = type.
id() == ID_c_bool
1074 assignments.
add(assign);
1084 if(
auto singleton = interval.as_singleton())
1091 exprt within_bounds = interval.make_contains_expr(expr);
1107 type, basename_prefix);
1144 const exprt &max_length_expr,
1145 const typet &element_type,
1152 "nondet_array_length",
1154 allocate_local_symbol,
1159 java_new_array.
set(ID_length_upper_bound, max_length_expr);
1160 java_new_array.
type().
subtype().
set(ID_element_type, element_type);
1163 assignments.
add(assign);
1185 const exprt &init_array_expr,
1186 const typet &element_type,
1187 const exprt &max_length_expr,
1191 const array_typet array_type(element_type, max_length_expr);
1195 allocate_local_symbol(
pointer_type(array_type),
"array_data_init");
1200 tmp_finite_array_pointer,
1202 assignments.
statements().back().add_source_location() = location;
1207 assignments.
add(
code_assignt(data_pointer_deref, std::move(nondet_data)));
1208 assignments.
statements().back().add_source_location() = location;
1213 assignments.
add(
code_assignt(init_array_expr, std::move(tmp_nondet_pointer)));
1214 assignments.
statements().back().add_source_location() = location;
1227 const exprt &element,
1229 const typet &element_type,
1234 bool new_item_is_primitive = element.
type().
id() != ID_pointer;
1242 if(new_item_is_primitive)
1244 init_expr = element;
1249 element.
type(),
"new_array_item");
1253 if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
1262 ? update_in_placet::MAY_UPDATE_IN_PLACE
1273 child_update_in_place,
1276 if(!new_item_is_primitive)
1327 const exprt &init_array_expr,
1328 const exprt &length_expr,
1329 const typet &element_type,
1330 const exprt &max_length_expr,
1338 allocate_local_symbol(init_array_expr.
type(),
"array_data_init");
1340 code_assignt data_assign(array_init_symexpr, init_array_expr);
1342 assignments.
add(data_assign);
1345 allocate_local_symbol(length_expr.
type(),
"array_init_iter");
1355 loop_body.
add(std::move(max_test));
1361 loop_body.
append(element_generator(element_at_counter, element_type));
1367 std::move(loop_body),
1378 const size_t max_nondet_array_length)
1382 PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
1389 const typet &element_type =
1396 if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
1403 allocate_local_symbol,
1412 "Java struct array does not conform to expectations");
1415 const auto &comps = struct_type.
components();
1416 const member_exprt length_expr(deref_expr,
"length", comps[1].type());
1423 if(element_type.
id() == ID_pointer || element_type.
id() == ID_c_bool)
1436 allocate_local_symbol,
1451 allocate_local_symbol);
1480 <<
" is missing, so the corresponding Enum "
1481 "type will nondet initialised"
1493 const auto &comps = deref_struct_type.components();
1494 const member_exprt length_expr(deref_expr,
"length", comps[1].type());
1509 assignments.
add(enum_assign);
1519 for(
const auto &code : assignments.
statements())
1521 if(code.get_statement() != ID_assign)
1525 assignment.lhs().type() == assignment.rhs().type(),
1526 "object factory should produce type-consistent assignments");
1556 main_symbol.
mode=ID_java;
1558 main_symbol.
name=identifier;
1560 main_symbol.
type=type;
1567 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
1571 loc, parameters, symbol_table, pointer_type_selector, log);
1581 update_in_placet::NO_UPDATE_IN_PLACE,
1588 init_code.
append(assignments);
1637 loc, object_factory_parameters, symbol_table, pointer_type_selector, log);
1653 init_code.
append(assignments);
1673 object_factory_parameters,
1676 pointer_type_selector,
1700 object_factory_parameters,
1701 pointer_type_selector,
const java_object_factory_parameterst object_factory_parameters
Class that provides messages with a built-in verbosity 'level'.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
recursion_set_entryt & operator=(const recursion_set_entryt &)=delete
const componentst & components() const
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
bool insert_entry(const irep_idt &entry)
Try to add an entry to the controlled set.
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'.
const typet & subtype() const
symbol_table_baset & symbol_table
The symbol table.
static void array_primitive_init_code(code_blockt &assignments, const exprt &init_array_expr, const typet &element_type, const exprt &max_length_expr, const source_locationt &location, const allocate_local_symbolt &allocate_local_symbol)
Create code to nondeterministically initialize arrays of primitive type.
static void allocate_nondet_length_array(code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type, const allocate_local_symbolt &allocate_local_symbol, const source_locationt &location)
Allocates a fresh array and emits an assignment writing to lhs the address of the new array.
void insert(const pointer_typet &pointer_type, const typet &pointer_subtype_struct)
Author: Diffblue Ltd.
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
recursion_set_entryt(std::unordered_set< irep_idt > &_recursion_set)
Initialize a recursion-set entry owner operating on a given set.
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
symbol_exprt generate_nondet_int(const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)
Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value,...
#define CHECK_RETURN(CONDITION)
void gen_nondet_pointer_init(code_blockt &assignments, const exprt &expr, lifetimet lifetime, 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.
The type of an expression, extends irept.
typet type
Type of symbol.
Operator to dereference a pointer.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
code_blockt gen_nondet_array_init(const exprt &expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_tablet &symbol_table, const size_t max_nondet_array_length)
Synthesize GOTO for generating a array of nondet length to be stored in the expr.
void add_created_symbol(const symbolt *symbol_ptr)
Add a pointer to a symbol to the list of pointers to symbols created so far.
const irept & find(const irep_namet &name) const
Recursion-set entry owner class.
A codet representing the declaration of a local variable.
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...
Base class for all expressions.
std::vector< componentt > componentst
Produce code for simple implementation of String Java libraries.
irep_idt base_name
Base (non-scoped) name.
A struct tag type, i.e., struct_typet with an identifier.
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_...
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const select_pointer_typet & pointer_type_selector
Resolves pointer types potentially using some heuristics, for example to replace pointers to interfac...
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
bool is_true() const
Return whether the expression is a constant representing true.
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.
const integer_intervalt printable_char_range(' ', '~')
Interval that represents the printable character range range U+0020-U+007E, i.e.
Expression to hold a symbol (variable)
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_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.
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
codet representation of an if-then-else statement.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
static void assert_type_consistency(const code_blockt &assignments)
size_t max_nondet_tree_depth
Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.
Struct constructor from list of elements.
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.
code_operandst & statements()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
recursion_set_entryt(const recursion_set_entryt &)=delete
bool string_printable
Force string content to be ASCII printable characters when set to true.
java_object_factoryt(const source_locationt &loc, const java_object_factory_parameterst _object_factory_parameters, symbol_table_baset &_symbol_table, const select_pointer_typet &pointer_type_selector, message_handlert &log)
interval_uniont assume_inputs_interval
Force numerical primitive inputs to fall within the interval.
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.
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
Expression Initialization.
irep_idt mode
Language mode.
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
std::vector< codet > alternate_casest
bool has_prefix(const std::string &s, const std::string &prefix)
bool is_java_string_type(const struct_typet &struct_type)
Returns true iff the argument represents a string type (CharSequence, StringBuilder,...
The null pointer constant.
codet representation of a break statement (within a for or while loop).
const std::string & id2string(const irep_idt &d)
void gen_nondet_struct_init(code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, 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...
symbol_exprt gen_nondet_subtype_pointer_init(code_blockt &assignments, lifetimet lifetime, const pointer_typet &substitute_pointer_type, size_t depth, const source_locationt &location)
Generate codet assignments to initalize the selected concrete type.
#define PRECONDITION(CONDITION)
The symbol table base class interface.
std::unordered_set< irep_idt > & recursion_set
Recursion set to modify.
An assumption, which must hold in subsequent code.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
~recursion_set_entryt()
Removes erase_entry (if set) from the controlled set.
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, lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const lifetimet lifetime, const irep_idt &basename_prefix="tmp")
Allocates a new object, either by creating a local variable with automatic lifetime,...
dereference_exprt array_element_from_pointer(const exprt &pointer, const exprt &index)
Generate statement using pointer arithmetic to access the element at the given index of a pointer arr...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
allocate_objectst allocate_objects
bool assume_inputs_integral
Force double and float inputs to be integral.
pointer_typet pointer_type(const typet &subtype)
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
messaget log
Log for reporting warnings and errors in object creation.
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void add(const codet &code)
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, allocate_objectst &allocate_objects)
Initialise length and data fields for a nondeterministic String structure.
void gen_pointer_target_init(code_blockt &assignments, const exprt &expr, const typet &target_type, lifetimet lifetime, 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,...
signedbv_typet java_int_type()
nonstd::optional< T > optionalt
irep_idt erase_entry
Entry to erase on destruction, if non-empty.
static irep_idt integer_interval_to_string(const integer_intervalt &interval)
Converts and integer_intervalt to a a string of the for [lower]-[upper].
size_t max_nondet_array_length
Maximum value for the non-deterministically-chosen length of an array.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
lifetimet
Selects the kind of objects allocated.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
A side_effect_exprt that returns a non-deterministically chosen value.
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.
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
void add_created_symbol(const symbolt *symbol)
Extract member of struct or union.
void declare_created_symbols(code_blockt &init_code)
size_t max_nondet_string_length
Maximum value for the non-deterministically-chosen length of a string.
static code_blockt assume_expr_integral(const exprt &expr, const typet &type, const source_locationt &location, const allocate_local_symbolt &allocate_local_symbol)
Generate code block that verifies that an expression of type float or double has integral value.
Structure type, corresponds to C style structs.
exprt interval_constraint(const exprt &expr, const integer_intervalt &interval)
Given an exprt and an integer interval return an exprt that represents restricting the expression to ...
floatbv_typet java_double_type()
size_t min_nondet_string_length
Minimum value for the non-deterministically-chosen length of a string.
const code_assignt & to_code_assign(const codet &code)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
source_locationt location
Source code location of definition of symbol.
void gen_nondet_init(code_blockt &assignments, const exprt &expr, bool is_sub, bool skip_classid, lifetimet lifetime, const optionalt< 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...
void set(const irep_namet &name, const irep_idt &value)
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
unsignedbv_typet java_char_type()
A base class for relations, i.e., binary predicates whose two operands have the same type.
Goto Programs with Functions.
code_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
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...
Extract class identifier.
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
mp_integer largest() const
Return the largest value that can be represented using this type.
c_bool_typet java_boolean_type()
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
exprt get_nondet_bool(const typet &type, const source_locationt &source_location)
static void array_loop_init_code(code_blockt &assignments, const exprt &init_array_expr, const exprt &length_expr, const typet &element_type, const exprt &max_length_expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_tablet &symbol_table)
Create code to nondeterministically initialize each element of an array in a loop.
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)...
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const java_class_typet & to_java_class_type(const typet &type)
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A codet representing an assignment in the program.
std::function< code_blockt(const exprt &element_at_counter, const typet &element_type)> array_element_generatort
mstreamt & warning() const
const source_locationt & source_location() const
bool 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...
irep_idt name
The unique identifier.
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_range, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
An expression containing a side effect.
floatbv_typet java_float_type()
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
code_blockt assign_element(const exprt &element, update_in_placet update_in_place, const typet &element_type, size_t depth, const source_locationt &location)
Generate codet for assigning an individual element inside the array.
Nondeterministic boolean helper.
std::unordered_set< irep_idt > recursion_set
This is employed in conjunction with the depth above.