29 result.reserve(src.size());
31 for(std::size_t i=0; i<src.size(); i++)
33 const size_t mapped_index = map.
map_bit(i);
35 result.push_back(src[mapped_index]);
62 if(expr.
id()==ID_byte_extract_big_endian &&
63 expr.
type().
id()==ID_c_bit_field &&
84 (!index.has_value() || !op_bytes_opt.has_value() ||
85 *index < 0 || *index >= *op_bytes_opt) &&
86 (expr.
op().
id() == ID_member ||
87 expr.
op().
id() == ID_index ||
88 expr.
op().
id() == ID_byte_extract_big_endian ||
89 expr.
op().
id() == ID_byte_extract_little_endian))
108 expr.
id() == ID_byte_extract_little_endian ||
109 expr.
id() == ID_byte_extract_big_endian);
110 const bool little_endian = expr.
id() == ID_byte_extract_little_endian;
122 unsigned byte_width=8;
124 if(index.has_value())
126 const mp_integer offset = *index * byte_width;
128 for(std::size_t i=0; i<width; i++)
130 if(offset + i < 0 || offset + i >= op_bv.size())
133 bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
137 std::size_t bytes=op_bv.size()/byte_width;
142 for(std::size_t i=0; i<width; i++)
153 equal_bv.resize(width);
155 for(std::size_t i=0; i<bytes; i++)
159 std::size_t offset=i*byte_width;
161 for(std::size_t j=0; j<width; j++)
162 if(offset+j<op_bv.size())
163 equal_bv[j]=
prop.
lequal(bv[j], op_bv[offset+j]);
178 for(std::size_t i=0; i<bytes; i++)
184 std::size_t offset=i*byte_width;
186 for(std::size_t j=0; j<width; j++)
190 if(offset+j<op_bv.size())
205 bv=
map_bv(result_map, bv);
The type of an expression, extends irept.
literalt convert(const exprt &expr) override
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
bool is_unbounded_array(const typet &type) const override
typet & type()
Return the type of the expression.
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
#define CHECK_RETURN(CONDITION)
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
virtual literalt new_variable()=0
Expression classes for byte-level operators.
void util_throw_with_nested(T &&t)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Exceptions that can be raised in bv_conversion.
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
#define PRECONDITION(CONDITION)
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
Map bytes according to the configured endianness.
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt equality(const exprt &e1, const exprt &e2)
literalt const_literal(bool value)
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...
size_t number_of_bits() const
Base class for all expressions.
const exprt & root_object() const
virtual bool has_set_to() const
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
std::vector< literalt > bvt