Go to the documentation of this file.
63 const typet &target_type,
136 const exprt &element,
138 const typet &element_type,
188 const typet &target_type,
198 const typet &followed_target_type = ns.
follow(target_type);
208 [
this, update_in_place, depth, location](
211 element, update_in_place, element_type, depth + 1, location);
215 type, basename_prefix);
221 if(target_class_type.get_base(
"java::java.lang.Enum"))
237 assignments, expr, target_type, lifetime,
"tmp_object_factory");
241 if(expr.
id() == ID_address_of)
315 result += numeric_cast_v<char>(interval.
lower);
317 result += numeric_cast_v<char>(interval.
upper);
363 const std::size_t &min_nondet_string_length,
364 const std::size_t &max_nondet_string_length,
383 if(struct_type.
get_tag() ==
"java.lang.CharSequence")
401 const exprt min_length =
407 max_nondet_string_length <=
416 const exprt data_expr =
424 array_pointer, data_expr, symbol_table, loc, function_id, code);
427 data_expr, length_expr, symbol_table, loc, function_id, code);
481 const typet &followed_subtype = ns.
follow(subtype);
496 generic_parameter_specialization_map_keys(
498 generic_parameter_specialization_map_keys.
insert(
499 replacement_pointer_type, ns.
follow(replacement_pointer_type.
subtype()));
502 assignments, lifetime, replacement_pointer_type, depth, location);
561 const auto class_type =
562 type_try_dynamic_cast<java_class_typet>(followed_subtype))
564 if(class_type->get_base(
"java::java.lang.Enum"))
566 const irep_idt &class_name = class_type->get_name();
583 update_in_place_assignments,
596 assignments.
append(update_in_place_assignments);
623 new_object_assignments.
append(non_null_inst);
638 std::move(set_null_inst),
639 std::move(non_null_inst));
641 new_object_assignments.
add(std::move(null_check));
648 assignments.
append(new_object_assignments);
653 "No-update and must-update should have already been resolved");
657 std::move(update_in_place_assignments),
658 std::move(new_object_assignments));
660 assignments.
add(std::move(update_check));
696 replacement_pointer,
"tmp_object_factory");
710 return new_symbol_expr;
725 const std::list<std::string> &string_input_values,
729 for(
const auto &val : string_input_values)
776 const componentst &components=struct_type.
components();
789 const bool has_string_input_values =
809 (!is_sub && !skip_classid &&
856 else if(name ==
"cproverMonitorCount")
866 assignments.
add(code);
876 INVARIANT(!name.
empty(),
"Each component of a struct must have a name");
878 bool _is_sub=name[0]==
'@';
908 cprover_nondet_initialize = resolve_inherited_component(
909 "java::" +
id2string(struct_tag),
"cproverNondetInitialize:()V",
true);
911 if(cprover_nondet_initialize)
913 const symbolt &cprover_nondet_initialize_symbol =
914 ns.
lookup(cprover_nondet_initialize->get_full_component_identifier());
945 const auto &aux_int =
946 allocate_local_symbol(
java_int_type(),
"assume_integral_tmp");
951 assignments.
add(aux_assign);
1004 const typet &type = override_type.has_value() ? *override_type : expr.
type();
1008 if(type.
id()==ID_pointer)
1016 generic_parameter_specialization_map_keys(
1018 generic_parameter_specialization_map_keys.
insert(
1030 else if(followed_type.
id() == ID_struct)
1038 generic_parameter_specialization_map_keys(
1042 const typet &symbol =
1043 override_type.has_value() ? *override_type : expr.
type();
1045 generic_parameter_specialization_map_keys.
insert(
1064 exprt rhs = type.
id() == ID_c_bool
1070 assignments.
add(assign);
1080 if(
auto singleton = interval.as_singleton())
1087 exprt within_bounds = interval.make_contains_expr(expr);
1103 type, basename_prefix);
1140 const exprt &max_length_expr,
1141 const typet &element_type,
1148 "nondet_array_length",
1150 allocate_local_symbol,
1155 java_new_array.
set(ID_length_upper_bound, max_length_expr);
1156 java_new_array.
type().
subtype().
set(ID_element_type, element_type);
1159 assignments.
add(assign);
1181 const exprt &init_array_expr,
1182 const typet &element_type,
1183 const exprt &max_length_expr,
1187 const array_typet array_type(element_type, max_length_expr);
1191 allocate_local_symbol(
pointer_type(array_type),
"array_data_init");
1196 tmp_finite_array_pointer,
1198 assignments.
statements().back().add_source_location() = location;
1203 assignments.
add(
code_assignt(data_pointer_deref, std::move(nondet_data)));
1204 assignments.
statements().back().add_source_location() = location;
1209 assignments.
add(
code_assignt(init_array_expr, std::move(tmp_nondet_pointer)));
1210 assignments.
statements().back().add_source_location() = location;
1223 const exprt &element,
1225 const typet &element_type,
1230 bool new_item_is_primitive = element.
type().
id() != ID_pointer;
1238 if(new_item_is_primitive)
1240 init_expr = element;
1245 element.
type(),
"new_array_item");
1269 child_update_in_place,
1272 if(!new_item_is_primitive)
1323 const exprt &init_array_expr,
1324 const exprt &length_expr,
1325 const typet &element_type,
1326 const exprt &max_length_expr,
1334 allocate_local_symbol(init_array_expr.
type(),
"array_data_init");
1336 code_assignt data_assign(array_init_symexpr, init_array_expr);
1338 assignments.
add(data_assign);
1341 allocate_local_symbol(length_expr.
type(),
"array_init_iter");
1351 loop_body.
add(std::move(max_test));
1357 loop_body.
append(element_generator(element_at_counter, element_type));
1363 std::move(loop_body),
1374 const size_t max_nondet_array_length)
1385 const typet &element_type =
1399 allocate_local_symbol,
1408 "Java struct array does not conform to expectations");
1411 const auto &comps = struct_type.
components();
1412 const member_exprt length_expr(deref_expr,
"length", comps[1].type());
1419 if(element_type.
id() == ID_pointer || element_type.
id() == ID_c_bool)
1432 allocate_local_symbol,
1447 allocate_local_symbol);
1476 <<
" is missing, so the corresponding Enum "
1477 "type will nondet initialised"
1489 const auto &comps = deref_struct_type.components();
1490 const member_exprt length_expr(deref_expr,
"length", comps[1].type());
1505 assignments.
add(enum_assign);
1515 for(
const auto &code : assignments.
statements())
1517 if(code.get_statement() != ID_assign)
1521 assignment.lhs().type() == assignment.rhs().type(),
1522 "object factory should produce type-consistent assignments");
1552 main_symbol.
mode=ID_java;
1554 main_symbol.
name=identifier;
1556 main_symbol.
type=type;
1563 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
1567 loc, parameters, symbol_table, pointer_type_selector, log);
1584 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...
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
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.
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
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 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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
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...
allocate_objectst allocate_objects
bool assume_inputs_integral
Force double and float inputs to be integral.
pointer_typet pointer_type(const typet &subtype)
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
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()
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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()
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
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)
bool has_prefix(const std::string &s, const std::string &prefix)
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 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.