33 const exprt &max_bytes,
35 bool unpack_byte_array=
false)
46 if(type.
id()==ID_array)
55 throw "cannot unpack array with non-constant element width:\n"+
57 else if(element_width%8!=0)
58 throw "cannot unpack array of non-byte aligned elements:\n"+
62 if(!unpack_byte_array && element_width==8)
82 replace.
insert(ID_C_incomplete, index);
93 else if(type.
id()==ID_struct)
98 for(
const auto &comp : components)
103 if(element_width<=0 || element_width%8!=0)
111 for(
const auto& op : sub.operands())
115 else if(type.
id()!=ID_empty)
205 src.
id() == ID_byte_extract_little_endian ||
206 src.
id() == ID_byte_extract_big_endian);
207 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
225 if(type.id()==ID_array)
234 if(element_width>0 && element_width%8==0 &&
255 else if(type.id()==ID_struct)
263 for(
const auto &comp : components)
268 if(element_width<=0 || element_width%8!=0)
281 tmp.
type()=comp.type();
291 const exprt &root=unpacked.
op();
298 "offset bits are byte aligned");
313 size_bits/8+((size_bits%8==0)?0:1);
320 op.reserve(width_bytes);
322 for(std::size_t i=0; i<width_bytes; i++)
325 std::size_t offset_int=
326 little_endian?(width_bytes-i-1):i;
330 op.push_back(index_expr);
346 bool negative_offset)
353 throw "byte_update of unknown width:\n"+src.
pretty();
363 if(subtype.
id()==ID_unsignedbv ||
364 subtype.
id()==ID_signedbv ||
365 subtype.
id()==ID_floatbv ||
366 subtype.
id()==ID_c_bool ||
367 subtype.
id()==ID_pointer)
372 throw "can't flatten byte_update for sub-type without size";
386 if(i==0 && element_size==1)
389 if(new_value.
type()!=subtype)
395 src.
id()==ID_byte_update_little_endian?
396 ID_byte_extract_little_endian:
397 src.
id()==ID_byte_update_big_endian?
398 ID_byte_extract_big_endian:
399 throw "unexpected src.id() in flatten_byte_update",
402 byte_extract_expr.
op()=src.
op2();
403 byte_extract_expr.offset()=i_expr;
410 with_exprt with_expr(result, where, new_value);
411 with_expr.type()=src.
type();
413 result.
swap(with_expr);
424 element_size/sub_size+((element_size%sub_size==0)?1:2);
438 mult_exprt cell_offset(cell_index, sub_size_expr);
440 bool is_first_cell=i==0;
441 bool is_last_cell=i==num_elements-1;
444 exprt stored_value_offset;
445 if(element_size<=sub_size)
448 stored_value_offset=zero_offset;
456 stored_value_offset=zero_offset;
457 else if(is_last_cell)
464 src.
id()==ID_byte_update_little_endian ?
465 ID_byte_extract_little_endian :
466 src.
id()==ID_byte_update_big_endian ?
467 ID_byte_extract_big_endian :
468 throw "unexpected src.id() in flatten_byte_update";
471 element_size<sub_size ? src.
op2().
type() : subtype);
473 byte_extract_expr.
op()=src.
op2();
474 byte_extract_expr.offset()=stored_value_offset;
483 exprt overwrite_offset;
486 else if(is_last_cell)
493 stored_value_offset);
496 overwrite_offset=zero_offset;
506 exprt flattened_byte_update_expr=
510 result, cell_index, flattened_byte_update_expr);
521 "flatten_byte_update can only do arrays of scalars right now, " 525 else if(t.
id()==ID_signedbv ||
526 t.
id()==ID_unsignedbv ||
527 t.
id()==ID_floatbv ||
533 assert(type_width>0);
536 if(element_size*8>width)
537 throw "flatten_byte_update to update element that is too large";
544 exprt value_extended;
553 value_extended=src.
op2();
571 mask_shifted=
lshr_exprt(mask, offset_times_eight);
572 value_shifted=
lshr_exprt(value_extended, offset_times_eight);
576 mask_shifted=
shl_exprt(mask, offset_times_eight);
577 value_shifted=
shl_exprt(value_extended, offset_times_eight);
584 bitor_exprt bitor_expr(bitand_expr, value_shifted);
590 throw "flatten_byte_update can only do array and scalars " 604 if(src.
id()==ID_byte_update_little_endian ||
605 src.
id()==ID_byte_update_big_endian ||
606 src.
id()==ID_byte_extract_little_endian ||
607 src.
id()==ID_byte_extract_big_endian)
630 if(src.
id()==ID_byte_update_little_endian ||
631 src.
id()==ID_byte_update_big_endian)
633 else if(src.
id()==ID_byte_extract_little_endian ||
634 src.
id()==ID_byte_extract_big_endian)
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
Fixed-width bit-vector with unsigned binary interpretation.
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
exprt flatten_byte_update(const byte_update_exprt &src, const namespacet &ns, bool negative_offset)
void copy_to_operands(const exprt &expr)
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
const componentst & components() const
exprt flatten_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...
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
unsignedbv_typet size_type()
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Extract member of struct or union.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Concatenation of bit-vector operands.
const irep_idt & id() const
Expression classes for byte-level operators.
division (integer and real)
static exprt unpack_rec(const exprt &src, bool little_endian, const exprt &max_bytes, const namespacet &ns, bool unpack_byte_array=false)
rewrite an object into its individual bytes
exprt flatten_byte_operators(const exprt &src, const namespacet &ns)
#define PRECONDITION(CONDITION)
const exprt & size() const
#define forall_operands(it, expr)
const typet & follow(const typet &) const
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
std::vector< exprt > operandst
unsigned integer2unsigned(const mp_integer &n)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
Operator to update elements in structs and arrays.
const std::string & id_string() const
#define Forall_operands(it, expr)
void insert(const irep_idt &identifier, const exprt &expr)
Expression to hold a symbol (variable)
bool has_byte_operator(const exprt &src)
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
Bit-wise negation of bit-vectors.
struct constructor from list of elements
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
void make_typecast(const typet &_type)
array constructor from list of elements
bool simplify(exprt &expr, const namespacet &ns)