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);
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)