31 const exprt &max_bytes,
33 bool unpack_byte_array=
false)
44 if(type.
id()==ID_array)
53 throw "cannot unpack array with non-constant element width:\n"+
55 else if(element_width%8!=0)
56 throw "cannot unpack array of non-byte aligned elements:\n"+
60 if(!unpack_byte_array && element_width==8)
66 throw "cannot unpack array of non-const size:\n"+type.
pretty();
78 replace.
insert(ID_C_incomplete, index);
89 else if(type.
id()==ID_struct)
94 for(
const auto &comp : components)
99 if(element_width<=0 || element_width%8!=0)
100 throw "cannot unpack struct with non-byte aligned components:\n"+
106 for(
const auto& op : sub.operands())
110 else if(type.
id()!=ID_empty)
118 throw "cannot unpack object of non-constant width:\n"+
200 if(src.
id()==ID_byte_extract_little_endian)
202 else if(src.
id()==ID_byte_extract_big_endian)
223 if(type.id()==ID_array)
232 if(element_width>0 && element_width%8==0 &&
253 else if(type.id()==ID_struct)
261 for(
const auto &comp : components)
266 if(element_width<=0 || element_width%8!=0)
279 tmp.
type()=comp.type();
289 const exprt &root=unpacked.
op();
302 throw "byte_extract flatting with non-constant size:\n"+
309 size_bits/8+((size_bits%8==0)?0:1);
316 op.reserve(width_bytes);
318 for(std::size_t i=0; i<width_bytes; i++)
321 std::size_t offset_int=
322 little_endian?(width_bytes-i-1):i;
326 op.push_back(index_expr);
335 return concatenation;
342 bool negative_offset)
349 throw "byte_update of unknown width:\n"+src.
pretty();
359 if(subtype.
id()==ID_unsignedbv ||
360 subtype.
id()==ID_signedbv ||
361 subtype.
id()==ID_floatbv ||
362 subtype.
id()==ID_c_bool ||
363 subtype.
id()==ID_pointer)
368 throw "can't flatten byte_update for sub-type without size";
382 if(i==0 && element_size==1)
385 if(new_value.
type()!=subtype)
391 src.
id()==ID_byte_update_little_endian?
392 ID_byte_extract_little_endian:
393 src.
id()==ID_byte_update_big_endian?
394 ID_byte_extract_big_endian:
395 throw "unexpected src.id() in flatten_byte_update",
398 byte_extract_expr.
op()=src.
op2();
399 byte_extract_expr.offset()=i_expr;
408 with_expr.old()=result;
409 with_expr.where()=where;
410 with_expr.new_value()=new_value;
412 result.
swap(with_expr);
423 element_size/sub_size+((element_size%sub_size==0)?1:2);
437 mult_exprt cell_offset(cell_index, sub_size_expr);
439 bool is_first_cell=i==0;
440 bool is_last_cell=i==num_elements-1;
443 exprt stored_value_offset;
444 if(element_size<=sub_size)
447 stored_value_offset=zero_offset;
455 stored_value_offset=zero_offset;
456 else if(is_last_cell)
463 src.
id()==ID_byte_update_little_endian ?
464 ID_byte_extract_little_endian :
465 src.
id()==ID_byte_update_big_endian ?
466 ID_byte_extract_big_endian :
467 throw "unexpected src.id() in flatten_byte_update";
470 element_size<sub_size ? src.
op2().
type() : subtype);
472 byte_extract_expr.
op()=src.
op2();
473 byte_extract_expr.offset()=stored_value_offset;
482 exprt overwrite_offset;
485 else if(is_last_cell)
492 stored_value_offset);
495 overwrite_offset=zero_offset;
505 exprt flattened_byte_update_expr=
509 result, cell_index, flattened_byte_update_expr);
520 "flatten_byte_update can only do arrays of scalars right now, " 524 else if(t.
id()==ID_signedbv ||
525 t.
id()==ID_unsignedbv ||
526 t.
id()==ID_floatbv ||
532 assert(type_width>0);
535 if(element_size*8>width)
536 throw "flatten_byte_update to update element that is too large";
543 exprt value_extended;
552 value_extended=src.
op2();
570 mask_shifted=
lshr_exprt(mask, offset_times_eight);
571 value_shifted=
lshr_exprt(value_extended, offset_times_eight);
575 mask_shifted=
shl_exprt(mask, offset_times_eight);
576 value_shifted=
shl_exprt(value_extended, offset_times_eight);
583 bitor_exprt bitor_expr(bitand_expr, value_shifted);
589 throw "flatten_byte_update can only do array and scalars " 603 if(src.
id()==ID_byte_update_little_endian ||
604 src.
id()==ID_byte_update_big_endian ||
605 src.
id()==ID_byte_extract_little_endian ||
606 src.
id()==ID_byte_extract_big_endian)
629 if(src.
id()==ID_byte_update_little_endian ||
630 src.
id()==ID_byte_update_big_endian)
632 else if(src.
id()==ID_byte_extract_little_endian ||
633 src.
id()==ID_byte_extract_big_endian)
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
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)
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
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
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)
API to expression classes.
const exprt & size() const
#define forall_operands(it, expr)
bitvector_typet index_type()
std::vector< exprt > operandst
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
unsigned integer2unsigned(const mp_integer &n)
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
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)