23 result.reserve(src.size());
25 for(std::size_t i=0; i<src.size(); i++)
27 const size_t mapped_index = map.
map_bit(i);
29 result.push_back(src[mapped_index]);
49 if(expr.
id()==ID_byte_extract_big_endian &&
50 expr.
type().
id()==ID_c_bit_field &&
68 auto index = numeric_cast<mp_integer>(expr.
offset());
71 (!index.has_value() || !op_bytes_opt.has_value() ||
72 *index < 0 || *index >= *op_bytes_opt) &&
73 (expr.
op().
id() == ID_member ||
74 expr.
op().
id() == ID_index ||
75 expr.
op().
id() == ID_byte_extract_big_endian ||
76 expr.
op().
id() == ID_byte_extract_little_endian))
96 expr.
id() == ID_byte_extract_little_endian ||
97 expr.
id() == ID_byte_extract_big_endian);
98 const bool little_endian = expr.
id() == ID_byte_extract_little_endian;
110 unsigned byte_width=8;
112 if(index.has_value())
114 const mp_integer offset = *index * byte_width;
116 for(std::size_t i=0; i<width; i++)
118 if(offset + i < 0 || offset + i >= op_bv.size())
121 bv[i] = op_bv[numeric_cast_v<std::size_t>(offset + i)];
125 std::size_t bytes=op_bv.size()/byte_width;
138 equal_bv.resize(width);
140 for(std::size_t i=0; i<bytes; i++)
142 std::size_t offset=i*byte_width;
144 for(std::size_t j=0; j<width; j++)
145 if(offset+j<op_bv.size())
146 equal_bv[j]=
prop.
lequal(bv[j], op_bv[offset+j]);
160 for(std::size_t i=0; i<bytes; i++)
165 std::size_t offset=i*byte_width;
167 for(std::size_t j=0; j<width; j++)
171 if(offset+j<op_bv.size())
186 bv=
map_bv(result_map, bv);
Expression classes for byte-level operators.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
void set_width(std::size_t width)
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
bool is_unbounded_array(const typet &type) const override
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
virtual std::size_t boolbv_width(const typet &type) const
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.
typet & type()
Return the type of the expression.
const irep_idt & id() const
Split an expression into a base object and a (byte) offset.
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
The plus expression Associativity is not specified.
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual bool has_set_to() const
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
std::vector< literalt > bvt
literalt const_literal(bool value)
API to expression classes for Pointers.
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.
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...
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
API to expression classes.