25 const typet &target_type,
38 std::size_t lower_bound,
39 std::size_t upper_bound)
42 result.
lb = lower_bound;
43 result.
ub = upper_bound;
51 if(result.
ub < result.
lb)
52 std::swap(result.
lb, result.
ub);
87 operands.reserve(components.size());
89 for(
const auto &
comp : components)
135 if(components.empty())
149 components.front().get_name(),
158 : components.front().get_name();
161 : components.front().type();
196 "subtype width times array size should be total bitvector width");
243 "subtype width times vector size should be total bitvector width");
292 "subtype width should be half of the total bitvector width");
334 const typet &target_type,
369 result.
type() = target_type;
370 return std::move(result);
384 result.
type() = target_type;
405 false,
"bv_to_expr does not yet support ", target_type.
id_string());
427 std::size_t lower_bound,
428 std::size_t upper_bound,
452 bytes.reserve(upper_bound - lower_bound);
453 for(std::size_t i = lower_bound; i < upper_bound; ++i)
485 "$array_comprehension_index_a_v" +
502 for(std::size_t i = 1; i <
el_bytes; ++i)
555 "unpacking of arrays with non-byte-aligned elements is not supported");
677 std::make_move_iterator(sub.
operands().begin()),
678 std::make_move_iterator(sub.
operands().end()));
708 for(
auto it = components.begin(); it != components.end(); ++it)
710 const auto &
comp = *it;
720 (std::next(it) == components.end() && !
bit_fields.has_value()),
721 "members of non-constant width should come last in a struct");
781 "all preceding members should have been processed");
807 std::make_move_iterator(sub.
operands().begin()),
808 std::make_move_iterator(sub.
operands().end()));
874 std::make_move_iterator(
sub_imag.operands().begin()),
875 std::make_move_iterator(
sub_imag.operands().end()));
1101 const typet &subtype,
1115#pragma GCC diagnostic push
1117# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
1130 tmp.type() = subtype;
1153 "$array_comprehension_index_a" +
1168 body.
type() = subtype;
1199 real.type() = subtype;
1206 imag.type() = subtype;
1318 if(result.has_value())
1319 return std::move(*result);
1331 for(
const auto &
comp : components)
1406 "offset bits are byte aligned");
1415 "the extracted width or the source width must be known");
1443 index < root.
operands().size() && index >= 0)
1487 const typet &subtype,
1497 "$array_comprehension_index_u_a_v" +
1524 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1556 const typet &subtype,
1632 const typet &subtype,
1650 "$array_comprehension_index_u_a_v_u" +
1736 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1772 const typet &subtype,
1812 "value should be an array expression if the update bound is constant");
1859 std::size_t offset = 0;
1872 &result](std::size_t i) ->
void {
1891 result.add_to_operands(std::move(where), std::move(element));
1935 std::size_t first = 0;
1950 "indices past the update should be handled below");
1963 update_elements > 0,
"indices before the update should be handled above");
2099 const typet &subtype,
2146 src.get_bits_per_byte();
2189 elements.reserve(
struct_type.components().size());
2229 bu.type() =
bu.op().type();
2255 elements.push_back(member);
2296 "lower_byte_update of union of unknown size is not supported");
2339 "constant update bound should yield an array expression");
2487 std::reverse(value.operands().begin(), value.operands().end());
2542 false,
"lower_byte_update does not yet support ", src.
type().
id_string());
2551 "byte update expression should either be little or big endian");
2588 update_bits.has_value(),
"constant size-of should imply fixed bit width");
2595 "non-byte aligned type expected to be a bitvector type");
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet index_type()
unsignedbv_typet size_type()
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Expression to define a mapping from an argument (index) to elements.
Array constructor from list of elements.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Bit-wise negation of bit-vectors.
Base class of fixed-width bit-vector types.
Fixed-width bit-vector without numerical interpretation.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
std::size_t get_bits_per_byte() const
const exprt & value() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Complex constructor from a pair of numbers.
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Complex numbers made of pair of given subtype.
Concatenation of bit-vector operands.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Union constructor to support unions without any member (a GCC/Clang feature).
Maps a big-endian offset to a little-endian offset.
size_t number_of_bits() const
size_t map_bit(size_t bit) const
Base class for all expressions.
std::vector< exprt > operandst
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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...
The plus expression Associativity is not specified.
Fixed-width bit-vector with two's complement interpretation.
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
std::vector< componentt > componentst
Expression to hold a symbol (variable)
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
The unary minus expression.
Union constructor from single element.
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Operator to update elements in structs and arrays.
#define Forall_operands(it, expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
static exprt lower_byte_update_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as updat...
static exprt unpack_array_vector(const exprt &src, const optionalt< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
static exprt bv_to_expr(const exprt &bitvector_expr, const typet &target_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an expression of type target_type.
static exprt bv_to_union_expr(const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a union-typed expression.
static complex_exprt bv_to_complex_expr(const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.
static exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update ...
static exprt unpack_rec(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const std::size_t bits_per_byte, const namespacet &ns)
Build the individual bytes to be used in an update.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
static optionalt< exprt > lower_byte_extract_complex(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components t...
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const optionalt< mp_integer > &subtype_bits, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as ...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
static vector_exprt bv_to_vector_expr(const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.
static exprt lower_byte_update_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
static struct_exprt bv_to_struct_expr(const exprt &bitvector_expr, const struct_typet &struct_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a struct-typed expression.
static array_exprt unpack_complex(const exprt &src, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
static exprt lower_byte_update_single_element(const byte_update_exprt &src, const mp_integer &offset_bits, const exprt &element_to_update, const mp_integer &subtype_bits, const mp_integer &bits_already_set, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Byte update a struct/array/vector element.
static array_exprt bv_to_array_expr(const exprt &bitvector_expr, const array_typet &array_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an array-typed expression.
static boundst map_bounds(const endianness_mapt &endianness_map, std::size_t lower_bound, std::size_t upper_bound)
Map bit boundaries according to endianness.
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update v...
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
static exprt lower_byte_extract_array_vector(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const typet &subtype, const mp_integer &element_bits, const namespacet &ns)
Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual compon...
static void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
static array_exprt unpack_struct(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
static exprt lower_byte_update_byte_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_by...
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
static exprt lower_byte_update_array_vector_unbounded(const byte_update_exprt &src, const typet &subtype, const exprt &subtype_size, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const exprt &initial_bytes, const exprt &first_index, const exprt &first_update_value, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const string_constantt & to_string_constant(const exprt &expr)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)