Go to the documentation of this file.
34 exprt::operandst::const_iterator next_it=it;
37 if(next_it!=operands.end() && *next_it < *it)
47 std::sort(operands.begin(), operands.end());
67 { ID_plus, {ID_integer ,
76 { ID_mult, {ID_integer ,
91 { ID_bitand, {ID_unsignedbv ,
96 { ID_bitor, {ID_unsignedbv ,
101 { ID_bitxor, {ID_unsignedbv ,
138 bool no_change =
true;
157 new_ops.reserve(
as_const(expr).operands().size());
161 if(it->id()==expr.
id())
163 new_ops.reserve(new_ops.capacity()+it->operands().size()-1);
166 new_ops.push_back(*it2);
171 new_ops.push_back(*it);
195 const std::string &bits,
204 !type_bits.has_value() ||
205 (type.
id() != ID_union && type.
id() != ID_union_tag &&
206 *type_bits != bits.
size()) ||
207 ((type.
id() == ID_union || type.
id() == ID_union_tag) &&
208 *type_bits < bits.size()))
214 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
215 type.
id() == ID_floatbv || type.
id() == ID_fixedbv ||
216 type.
id() == ID_c_bit_field || type.
id() == ID_pointer ||
217 type.
id() == ID_bv || type.
id() == ID_c_bool)
221 bits.find(
'1') == std::string::npos)
228 std::string tmp = bits;
232 std::reverse(tmp.begin(), tmp.end());
237 else if(type.
id() == ID_c_enum)
249 else if(type.
id() == ID_c_enum_tag)
261 else if(type.
id() == ID_union)
276 else if(type.
id() == ID_union_tag)
288 else if(type.
id() == ID_struct)
302 std::string comp_bits = std::string(
304 numeric_cast_v<std::size_t>(m_offset_bits),
305 numeric_cast_v<std::size_t>(*m_size));
308 if(!comp.has_value())
310 result.add_to_operands(std::move(*comp));
312 m_offset_bits += *m_size;
315 return std::move(result);
317 else if(type.
id() == ID_struct_tag)
329 else if(type.
id() == ID_array)
332 const auto &size_expr = array_type.
size();
336 const std::size_t number_of_elements =
340 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
342 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
347 for(std::size_t i = 0; i < number_of_elements; ++i)
349 std::string el_bits = std::string(bits, i * el_size, el_size);
353 result.add_to_operands(std::move(*el));
356 return std::move(result);
358 else if(type.
id() == ID_vector)
362 const std::size_t n_el = numeric_cast_v<std::size_t>(vector_type.
size());
365 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
367 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
372 for(std::size_t i = 0; i < n_el; ++i)
374 std::string el_bits = std::string(bits, i * el_size, el_size);
378 result.add_to_operands(std::move(*el));
381 return std::move(result);
383 else if(type.
id() == ID_complex)
388 CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0);
390 const std::size_t sub_size = numeric_cast_v<std::size_t>(*sub_size_opt);
393 bits.substr(0, sub_size), complex_type.
subtype(), little_endian, ns);
395 bits.substr(sub_size), complex_type.
subtype(), little_endian, ns);
396 if(!real.has_value() || !imag.has_value())
411 if(expr.
id() == ID_constant)
416 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
417 type.
id() == ID_floatbv || type.
id() == ID_fixedbv ||
418 type.
id() == ID_c_bit_field || type.
id() == ID_bv ||
419 type.
id() == ID_c_bool)
425 std::string result(width,
' ');
432 else if(type.
id() == ID_pointer)
439 else if(type.
id() == ID_c_enum_tag)
444 else if(type.
id() == ID_c_enum)
452 else if(expr.
id() == ID_string_constant)
457 else if(expr.
id() == ID_union)
462 expr.
id() == ID_struct || expr.
id() == ID_array || expr.
id() == ID_vector ||
463 expr.
id() == ID_complex)
468 auto tmp =
expr2bits(*it, little_endian, ns);
471 result += tmp.value();
483 if(content.
id() != ID_address_of)
490 if(array_pointer.object().id() != ID_index)
495 const auto &array_start =
to_index_expr(array_pointer.object());
498 array_start.array().id() != ID_symbol ||
499 array_start.array().type().id() != ID_array)
506 const symbolt *symbol_ptr =
nullptr;
509 ns.
lookup(array.get_identifier(), symbol_ptr) ||
510 symbol_ptr->
value.
id() != ID_array)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const typet & subtype() const
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Union constructor from single element.
const string_constantt & to_string_constant(const exprt &expr)
produce canonical ordering for associative and commutative binary operators
Base class for all expressions.
std::vector< componentt > componentst
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Complex numbers made of pair of given subtype.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
static bool is_associative_and_commutative_for_type(const struct saj_tablet &saj_entry, const irep_idt &type_id)
Vector constructor from list of elements.
struct configt::ansi_ct ansi_c
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
Struct constructor from list of elements.
const exprt & size() const
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().
Expression classes for byte-level operators.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
bool has_operands() const
Return true if there is at least one operand.
The null pointer constant.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
#define forall_operands(it, expr)
#define PRECONDITION(CONDITION)
const irep_idt type_ids[10]
struct saj_tablet saj_table[]
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
size_t map_bit(size_t bit) const
static bool sort_and_join(exprt &expr, bool do_sort)
bool join_operands(exprt &expr)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< exprt > operandst
Complex constructor from a pair of numbers.
nonstd::optional< T > optionalt
const constant_exprt & size() const
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
std::size_t get_width() const
exprt value
Initial value of symbol.
Structure type, corresponds to C style structs.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Maps a big-endian offset to a little-endian offset.
static const struct saj_tablet & get_sort_and_join_table_entry(const irep_idt &id, const irep_idt &type_id)
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define forall_expr(it, expr)
unsignedbv_typet size_type()
A constant literal expression.
void reserve_operands(operandst::size_type n)
API to expression classes.
const irep_idt & get_value() const
Array constructor from list of elements.
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.