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)
206 if(src.
id()==ID_byte_extract_little_endian)
208 else if(src.
id()==ID_byte_extract_big_endian)
229 if(type.id()==ID_array)
238 if(element_width>0 && element_width%8==0 &&
259 else if(type.id()==ID_struct)
267 for(
const auto &comp : components)
272 if(element_width<=0 || element_width%8!=0)
285 tmp.
type()=comp.type();
295 const exprt &root=unpacked.
op();
302 "offset bits are byte aligned");
317 size_bits/8+((size_bits%8==0)?0:1);
324 op.reserve(width_bytes);
326 for(std::size_t i=0; i<width_bytes; i++)
329 std::size_t offset_int=
330 little_endian?(width_bytes-i-1):i;
334 op.push_back(index_expr);
350 bool negative_offset)
357 throw "byte_update of unknown width:\n"+src.
pretty();
367 if(subtype.
id()==ID_unsignedbv ||
368 subtype.
id()==ID_signedbv ||
369 subtype.
id()==ID_floatbv ||
370 subtype.
id()==ID_c_bool ||
371 subtype.
id()==ID_pointer)
376 throw "can't flatten byte_update for sub-type without size";
390 if(i==0 && element_size==1)
393 if(new_value.
type()!=subtype)
399 src.
id()==ID_byte_update_little_endian?
400 ID_byte_extract_little_endian:
401 src.
id()==ID_byte_update_big_endian?
402 ID_byte_extract_big_endian:
403 throw "unexpected src.id() in flatten_byte_update",
406 byte_extract_expr.
op()=src.
op2();
407 byte_extract_expr.offset()=i_expr;
414 with_exprt with_expr(result, where, new_value);
415 with_expr.type()=src.
type();
417 result.
swap(with_expr);
428 element_size/sub_size+((element_size%sub_size==0)?1:2);
442 mult_exprt cell_offset(cell_index, sub_size_expr);
444 bool is_first_cell=i==0;
445 bool is_last_cell=i==num_elements-1;
448 exprt stored_value_offset;
449 if(element_size<=sub_size)
452 stored_value_offset=zero_offset;
460 stored_value_offset=zero_offset;
461 else if(is_last_cell)
468 src.
id()==ID_byte_update_little_endian ?
469 ID_byte_extract_little_endian :
470 src.
id()==ID_byte_update_big_endian ?
471 ID_byte_extract_big_endian :
472 throw "unexpected src.id() in flatten_byte_update";
475 element_size<sub_size ? src.
op2().
type() : subtype);
477 byte_extract_expr.
op()=src.
op2();
478 byte_extract_expr.offset()=stored_value_offset;
487 exprt overwrite_offset;
490 else if(is_last_cell)
497 stored_value_offset);
500 overwrite_offset=zero_offset;
510 exprt flattened_byte_update_expr=
514 result, cell_index, flattened_byte_update_expr);
525 "flatten_byte_update can only do arrays of scalars right now, " 529 else if(t.
id()==ID_signedbv ||
530 t.
id()==ID_unsignedbv ||
531 t.
id()==ID_floatbv ||
537 assert(type_width>0);
540 if(element_size*8>width)
541 throw "flatten_byte_update to update element that is too large";
548 exprt value_extended;
557 value_extended=src.
op2();
575 mask_shifted=
lshr_exprt(mask, offset_times_eight);
576 value_shifted=
lshr_exprt(value_extended, offset_times_eight);
580 mask_shifted=
shl_exprt(mask, offset_times_eight);
581 value_shifted=
shl_exprt(value_extended, offset_times_eight);
588 bitor_exprt bitor_expr(bitand_expr, value_shifted);
594 throw "flatten_byte_update can only do array and scalars " 608 if(src.
id()==ID_byte_update_little_endian ||
609 src.
id()==ID_byte_update_big_endian ||
610 src.
id()==ID_byte_extract_little_endian ||
611 src.
id()==ID_byte_extract_big_endian)
634 if(src.
id()==ID_byte_update_little_endian ||
635 src.
id()==ID_byte_update_big_endian)
637 else if(src.
id()==ID_byte_extract_little_endian ||
638 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)
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)