24 result.reserve(src.size());
26 for(std::size_t i=0; i<src.size(); i++)
28 const size_t mapped_index = map.
map_bit(i);
30 result.push_back(src[mapped_index]);
50 if(expr.
id()==ID_byte_extract_big_endian &&
51 expr.
type().
id()==ID_c_bit_field &&
69 auto index = numeric_cast<mp_integer>(expr.
offset());
72 (!index.has_value() || !op_bytes_opt.has_value() ||
73 *index < 0 || *index >= *op_bytes_opt) &&
74 (expr.
op().
id() == ID_member ||
75 expr.
op().
id() == ID_index ||
76 expr.
op().
id() == ID_byte_extract_big_endian ||
77 expr.
op().
id() == ID_byte_extract_little_endian))
97 expr.
id() == ID_byte_extract_little_endian ||
98 expr.
id() == ID_byte_extract_big_endian);
99 const bool little_endian = expr.
id() == ID_byte_extract_little_endian;
111 unsigned byte_width=8;
113 if(index.has_value())
115 const mp_integer offset = *index * byte_width;
117 for(std::size_t i=0; i<width; i++)
119 if(offset + i < 0 || offset + i >= op_bv.size())
122 bv[i] = op_bv[numeric_cast_v<std::size_t>(offset + i)];
126 std::size_t bytes=op_bv.size()/byte_width;
131 for(std::size_t i=0; i<width; i++)
140 equal_bv.resize(width);
142 for(std::size_t i=0; i<bytes; i++)
144 std::size_t offset=i*byte_width;
146 for(std::size_t j=0; j<width; j++)
147 if(offset+j<op_bv.size())
148 equal_bv[j]=
prop.
lequal(bv[j], op_bv[offset+j]);
162 for(std::size_t i=0; i<bytes; i++)
167 std::size_t offset=i*byte_width;
169 for(std::size_t j=0; j<width; j++)
173 if(offset+j<op_bv.size())
188 bv=
map_bv(result_map, bv);
Expression classes for byte-level operators.
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...
void conversion_failed(const exprt &expr, bvt &bv)
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.
const exprt & root_object() const
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...
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 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.
Deprecated expression utility functions.
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.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.