35 const exprt &max_bytes,
37 bool unpack_byte_array=
false)
48 if(type.
id()==ID_array)
60 "element width of array should be constant",
64 element_width % 8 == 0,
65 "elements in array should be byte-aligned",
69 if(!unpack_byte_array && *element_width == 8)
100 else if(type.
id()==ID_struct)
105 for(
const auto &comp : components)
111 !element_width.has_value() || *element_width == 0 ||
112 *element_width % 8 != 0)
120 for(
const auto& op : sub.operands())
124 else if(type.
id()!=ID_empty)
131 if(bits_opt.has_value())
161 return std::move(array);
214 src.
id() == ID_byte_extract_little_endian ||
215 src.
id() == ID_byte_extract_big_endian);
216 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
234 if(type.id()==ID_array)
244 element_width.has_value() && *element_width >= 1 &&
245 *element_width % 8 == 0 &&
to_integer(array_type.
size(), num_elements))
265 else if(type.id()==ID_struct)
273 for(
const auto &comp : components)
279 !element_width.has_value() || *element_width == 0 ||
280 *element_width % 8 != 0)
293 tmp.
type()=comp.type();
303 const exprt &root=unpacked.
op();
312 subtype_bits.has_value() && *subtype_bits == 8,
313 "offset bits are byte aligned");
316 if(!size_bits.has_value())
319 if(op0_bits.has_value())
328 (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
333 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_elements);
335 op.reserve(width_bytes);
337 for(std::size_t i=0; i<width_bytes; i++)
340 std::size_t offset_int=
341 little_endian?(width_bytes-i-1):i;
345 op.push_back(index_expr);
361 bool negative_offset)
366 element_size_opt.has_value(),
367 "size of type in bytes must be known",
370 const mp_integer &element_size = *element_size_opt;
380 if(subtype.
id()==ID_unsignedbv ||
381 subtype.
id()==ID_signedbv ||
382 subtype.
id()==ID_floatbv ||
383 subtype.
id()==ID_c_bool ||
384 subtype.
id()==ID_pointer)
389 sub_size_opt.has_value(),
390 "bit width (rounded to full bytes) of subtype must be known");
406 if(i==0 && element_size==1)
408 new_value = src.
value();
409 if(new_value.
type()!=subtype)
415 src.
id() == ID_byte_update_little_endian ||
416 src.
id() == ID_byte_update_big_endian,
417 "byte update expression should either be little or big endian");
420 src.
id() == ID_byte_update_little_endian
421 ? ID_byte_extract_little_endian
422 : ID_byte_extract_big_endian,
425 byte_extract_expr.
op() = src.
value();
426 byte_extract_expr.offset()=i_expr;
433 with_exprt with_expr(result, where, new_value);
434 with_expr.type()=src.
type();
436 result.
swap(with_expr);
447 element_size/sub_size+((element_size%sub_size==0)?1:2);
461 mult_exprt cell_offset(cell_index, sub_size_expr);
463 bool is_first_cell=i==0;
464 bool is_last_cell=i==num_elements-1;
467 exprt stored_value_offset;
468 if(element_size<=sub_size)
470 new_value = src.
value();
471 stored_value_offset=zero_offset;
479 stored_value_offset=zero_offset;
480 else if(is_last_cell)
487 src.
id() == ID_byte_update_little_endian ||
488 src.
id() == ID_byte_update_big_endian,
489 "byte update expression should either be little or big endian");
492 src.
id() == ID_byte_update_little_endian
493 ? ID_byte_extract_little_endian
494 : ID_byte_extract_big_endian,
495 element_size < sub_size ? src.
value().
type() : subtype);
497 byte_extract_expr.
op() = src.
value();
498 byte_extract_expr.offset()=stored_value_offset;
507 exprt overwrite_offset;
510 else if(is_last_cell)
518 overwrite_offset=zero_offset;
528 exprt flattened_byte_update_expr=
532 result, cell_index, flattened_byte_update_expr);
544 "flatten_byte_update can only do arrays of scalars right now",
548 else if(t.
id()==ID_signedbv ||
549 t.
id()==ID_unsignedbv ||
550 t.
id()==ID_floatbv ||
556 CHECK_RETURN(type_width.has_value() && *type_width > 0);
557 const std::size_t width = numeric_cast_v<std::size_t>(*type_width);
560 element_size * 8 <= width,
561 "element bit width must not be larger than width indicated by type");
568 exprt value_extended;
570 if(width > element_size * 8)
575 width - numeric_cast_v<std::size_t>(element_size) * 8)),
579 value_extended = src.
value();
597 mask_shifted=
lshr_exprt(mask, offset_times_eight);
598 value_shifted=
lshr_exprt(value_extended, offset_times_eight);
602 mask_shifted=
shl_exprt(mask, offset_times_eight);
603 value_shifted=
shl_exprt(value_extended, offset_times_eight);
610 bitor_exprt bitor_expr(bitand_expr, value_shifted);
618 "flatten_byte_update can only do arrays and scalars right now",
632 if(src.
id()==ID_byte_update_little_endian ||
633 src.
id()==ID_byte_update_big_endian ||
634 src.
id()==ID_byte_extract_little_endian ||
635 src.
id()==ID_byte_extract_big_endian)
656 if(src.
id()==ID_byte_update_little_endian ||
657 src.
id()==ID_byte_update_big_endian)
659 else if(src.
id()==ID_byte_extract_little_endian ||
660 src.
id()==ID_byte_extract_big_endian)
The type of an expression, extends irept.
exprt size_of_expr(const typet &type, const namespacet &ns)
Fixed-width bit-vector with unsigned binary interpretation.
Semantic type conversion.
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
static exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns, bool negative_offset)
exprt simplify_expr(const exprt &src, const namespacet &ns)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
const componentst & components() const
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
#define CHECK_RETURN(CONDITION)
Structure type, corresponds to C style structs.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.
Replace expression or type symbols by an expression or type, respectively.
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
const exprt & size() const
#define forall_operands(it, expr)
The plus expression Associativity is not specified.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
std::vector< exprt > operandst
Binary multiplication Associativity is not specified.
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...
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
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
Operator to update elements in structs and arrays.
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
bool has_byte_operator(const exprt &src)
const std::string & id_string() const
#define Forall_operands(it, expr)
Expression to hold a symbol (variable)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
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)
Create a typecast_exprt to the given type.
Array constructor from list of elements.
bool simplify(exprt &expr, const namespacet &ns)