33 exprt::operandst::const_iterator next_it=it;
36 if(next_it!=operands.end() && *next_it < *it)
46 std::sort(operands.begin(), operands.end());
66 { ID_plus, {ID_integer ,
75 { ID_mult, {ID_integer ,
90 { ID_bitand, {ID_unsignedbv ,
95 { ID_bitor, {ID_unsignedbv ,
100 { ID_bitxor, {ID_unsignedbv ,
137 bool no_change =
true;
156 new_ops.reserve(
as_const(expr).operands().size());
160 if(it->id()==expr.
id())
162 new_ops.reserve(new_ops.capacity()+it->operands().size()-1);
165 new_ops.push_back(*it2);
170 new_ops.push_back(*it);
194 const std::string &bits,
203 !type_bits.has_value() ||
204 (type.
id() != ID_union && type.
id() != ID_union_tag &&
205 *type_bits != bits.
size()) ||
206 ((type.
id() == ID_union || type.
id() == ID_union_tag) &&
207 *type_bits < bits.size()))
213 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
214 type.
id() == ID_floatbv || type.
id() == ID_fixedbv ||
215 type.
id() == ID_c_bit_field || type.
id() == ID_pointer ||
216 type.
id() == ID_bv || type.
id() == ID_c_bool)
220 bits.find(
'1') == std::string::npos)
227 std::string tmp = bits;
231 std::reverse(tmp.begin(), tmp.end());
236 else if(type.
id() == ID_c_enum)
248 else if(type.
id() == ID_c_enum_tag)
260 else if(type.
id() == ID_union)
275 else if(type.
id() == ID_union_tag)
287 else if(type.
id() == ID_struct)
301 std::string comp_bits = std::string(
303 numeric_cast_v<std::size_t>(m_offset_bits),
304 numeric_cast_v<std::size_t>(*m_size));
307 if(!comp.has_value())
309 result.add_to_operands(std::move(*comp));
311 m_offset_bits += *m_size;
314 return std::move(result);
316 else if(type.
id() == ID_struct_tag)
328 else if(type.
id() == ID_array)
331 const auto &size_expr = array_type.
size();
335 const std::size_t number_of_elements =
339 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
341 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
346 for(std::size_t i = 0; i < number_of_elements; ++i)
348 std::string el_bits = std::string(bits, i * el_size, el_size);
352 result.add_to_operands(std::move(*el));
355 return std::move(result);
357 else if(type.
id() == ID_vector)
361 const std::size_t n_el = numeric_cast_v<std::size_t>(vector_type.
size());
364 CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
366 const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
371 for(std::size_t i = 0; i < n_el; ++i)
373 std::string el_bits = std::string(bits, i * el_size, el_size);
377 result.add_to_operands(std::move(*el));
380 return std::move(result);
382 else if(type.
id() == ID_complex)
387 CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0);
389 const std::size_t sub_size = numeric_cast_v<std::size_t>(*sub_size_opt);
392 bits.substr(0, sub_size), complex_type.
subtype(), little_endian, ns);
394 bits.substr(sub_size), complex_type.
subtype(), little_endian, ns);
395 if(!real.has_value() || !imag.has_value())
410 if(expr.
id() == ID_constant)
415 type.
id() == ID_unsignedbv || type.
id() == ID_signedbv ||
416 type.
id() == ID_floatbv || type.
id() == ID_fixedbv ||
417 type.
id() == ID_c_bit_field || type.
id() == ID_bv ||
418 type.
id() == ID_c_bool)
424 std::string result(width,
' ');
431 else if(type.
id() == ID_pointer)
438 else if(type.
id() == ID_c_enum_tag)
443 else if(type.
id() == ID_c_enum)
451 else if(expr.
id() == ID_string_constant)
456 else if(expr.
id() == ID_union)
461 expr.
id() == ID_struct || expr.
id() == ID_array || expr.
id() == ID_vector ||
462 expr.
id() == ID_complex)
467 auto tmp =
expr2bits(*it, little_endian, ns);
470 result += tmp.value();
482 if(content.
id() != ID_address_of)
489 if(array_pointer.object().id() != ID_index)
494 const auto &array_start =
to_index_expr(array_pointer.object());
497 array_start.array().id() != ID_symbol ||
498 array_start.array().type().id() != ID_array)
505 const symbolt *symbol_ptr =
nullptr;
508 ns.
lookup(array.get_identifier(), symbol_ptr) ||
509 symbol_ptr->
value.
id() != ID_array)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Expression classes for byte-level operators.
unsignedbv_typet size_type()
Array constructor from list of elements.
const exprt & size() const
std::size_t get_width() const
Complex constructor from a pair of numbers.
Complex numbers made of pair of given subtype.
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Maps a big-endian offset to a little-endian offset.
size_t map_bit(size_t bit) const
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
void reserve_operands(operandst::size_type n)
typet & type()
Return the type of the expression.
const irep_idt & id() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
exprt value
Initial value of symbol.
The type of an expression, extends irept.
const typet & subtype() const
Union constructor from single element.
Vector constructor from list of elements.
const constant_exprt & size() const
#define forall_operands(it, expr)
#define forall_expr(it, expr)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
nonstd::optional< T > optionalt
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
struct saj_tablet saj_table[]
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
static const struct saj_tablet & get_sort_and_join_table_entry(const irep_idt &id, const irep_idt &type_id)
static bool is_associative_and_commutative_for_type(const struct saj_tablet &saj_entry, const irep_idt &type_id)
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
optionalt< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
static bool sort_and_join(exprt &expr, bool do_sort)
bool join_operands(exprt &expr)
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.
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const string_constantt & to_string_constant(const exprt &expr)
produce canonical ordering for associative and commutative binary operators
const irep_idt type_ids[10]