Go to the documentation of this file.
14 std::ostringstream buf;
15 buf <<
"string_refinement#" << prefix <<
"#" << ++
symbol_count;
19 created_symbols.push_back(result);
26 if(
const auto &if_expr = expr_try_dynamic_cast<if_exprt>((
exprt)s))
36 if(emplace_result.second)
38 emplace_result.first->second =
42 return emplace_result.first->second;
50 return find_result->second;
73 const exprt &char_pointer,
74 const typet &char_array_type)
79 char_array_type.
subtype().
id() == ID_unsignedbv ||
80 char_array_type.
subtype().
id() == ID_signedbv);
82 if(char_pointer.
id() == ID_if)
102 const bool is_constant_array =
103 char_pointer.
id() == ID_address_of &&
108 if(is_constant_array)
113 const std::string symbol_name =
"char_array_" +
id2string(char_pointer.
id());
114 const auto array_sym =
116 const auto insert_result =
135 std::unordered_map<array_string_exprt, exprt, irep_hash> &length_of_array,
139 array_expr.
id() != ID_if,
140 "attempt_assign_length_from_type does not handle if exprts");
145 const exprt &size_to_assign =
148 : symbol_generator(
"string_length", array_expr.
length_type());
150 const auto emplace_result =
151 length_of_array.emplace(array_expr, size_to_assign);
153 emplace_result.second,
154 "attempt_assign_length_from_type should only be called when no entry"
155 "for the array_string_exprt exists in the length_of_array map");
159 const exprt &pointer_expr,
166 it_bool.second,
"should not associate two arrays to the same pointer");
176 const std::unordered_map<array_string_exprt, exprt, irep_hash> &
192 const auto string_argument = expr_checked_cast<struct_exprt>(arg);
193 return array_pool.
find(string_argument.op1(), string_argument.op0());
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const std::unordered_map< array_string_exprt, exprt, irep_hash > & created_strings() const
Return a map mapping all array_string_exprt of the array_pool to their length.
const typet & length_type() const
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
Generate a new symbol expression of the given type with some prefix.
const typet & subtype() const
static void attempt_assign_length_from_type(const array_string_exprt &array_expr, std::unordered_map< array_string_exprt, exprt, irep_hash > &length_of_array, symbol_generatort &symbol_generator)
Given an array_string_exprt, get the size of the underlying array.
Associates arrays and length to pointers, so that the string refinement can transform builtin functio...
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
refined_string_exprt & to_string_expr(exprt &expr)
The type of an expression, extends irept.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Correspondance between arrays and pointers string representations.
The trinary if-then-else operator.
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
Base class for all expressions.
Expression to hold a symbol (variable)
bitvector_typet index_type()
An expression denoting infinity.
const exprt & length() const
const exprt & size() const
typet & type()
Return the type of the expression.
Generation of fresh symbols of a given type.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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)
#define PRECONDITION(CONDITION)
const irep_idt & id() const
array_string_exprt & to_array_string_expr(exprt &expr)
nonstd::optional< T > optionalt
bitvector_typet char_type()
const exprt & content() const
optionalt< exprt > get_length_if_exists(const array_string_exprt &s) const
As opposed to get_length(), do not create a new symbol if the length of the array_string_exprt does n...
symbol_generatort & fresh_symbol
Generate fresh symbols.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
bool is_refined_string_type(const typet &type)
std::unordered_map< array_string_exprt, exprt, irep_hash > length_of_array
Associate length to arrays of infinite size.
array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
Converts a struct containing a length and pointer to an array.
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
Helper function for find.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void insert(const exprt &pointer_expr, const array_string_exprt &array)
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
Associate arrays to char pointers Invariant: Each array_string_exprt in this map has a corresponding ...
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.