24 const exprt &bitvector_expr,
25 const typet &target_type,
38 std::size_t lower_bound,
39 std::size_t upper_bound)
42 result.
lb = lower_bound;
43 result.
ub = upper_bound;
51 if(result.
ub < result.
lb)
52 std::swap(result.
lb, result.
ub);
61 if(src.
id() == ID_unsignedbv)
63 else if(src.
id() == ID_signedbv)
65 else if(src.
id() == ID_bv)
67 else if(src.
id() == ID_c_enum)
69 else if(src.
id() == ID_c_bit_field)
79 const exprt &bitvector_expr,
87 operands.reserve(components.size());
89 for(
const auto &comp : components)
92 std::size_t component_bits;
93 if(component_bits_opt.has_value())
94 component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
99 if(component_bits == 0)
118 if(component_bits_opt.has_value())
128 const exprt &bitvector_expr,
135 if(components.empty())
140 std::size_t component_bits;
141 if(widest_member.has_value())
142 component_bits = numeric_cast_v<std::size_t>(widest_member->second);
146 if(component_bits == 0)
149 components.front().get_name(),
150 bv_to_expr(bitvector_expr, components.front().
type(), endianness_map, ns),
154 const auto bounds =
map_bounds(endianness_map, 0, component_bits - 1);
156 const irep_idt &component_name = widest_member.has_value()
157 ? widest_member->first.get_name()
158 : components.front().get_name();
159 const typet &component_type = widest_member.has_value()
160 ? widest_member->first.type()
161 : components.front().type();
176 const exprt &bitvector_expr,
181 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
184 const std::size_t total_bits =
186 if(!num_elements.has_value())
188 if(!subtype_bits.has_value() || *subtype_bits == 0)
189 num_elements = total_bits;
191 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
194 !num_elements.has_value() || !subtype_bits.has_value() ||
195 *subtype_bits * *num_elements == total_bits,
196 "subtype width times array size should be total bitvector width");
199 operands.reserve(*num_elements);
200 for(std::size_t i = 0; i < *num_elements; ++i)
202 if(subtype_bits.has_value())
204 const std::size_t subtype_bits_int =
205 numeric_cast_v<std::size_t>(*subtype_bits);
207 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
213 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
221 bitvector_expr, array_type.
element_type(), endianness_map, ns));
225 return array_exprt{std::move(operands), array_type};
231 const exprt &bitvector_expr,
236 const std::size_t num_elements =
237 numeric_cast_v<std::size_t>(vector_type.
size());
240 !subtype_bits.has_value() ||
241 *subtype_bits * num_elements ==
243 "subtype width times vector size should be total bitvector width");
246 operands.reserve(num_elements);
247 for(std::size_t i = 0; i < num_elements; ++i)
249 if(subtype_bits.has_value())
251 const std::size_t subtype_bits_int =
252 numeric_cast_v<std::size_t>(*subtype_bits);
254 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
260 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
268 bitvector_expr, vector_type.
element_type(), endianness_map, ns));
278 const exprt &bitvector_expr,
283 const std::size_t total_bits =
286 std::size_t subtype_bits;
287 if(subtype_bits_opt.has_value())
289 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
291 subtype_bits * 2 == total_bits,
292 "subtype width should be half of the total bitvector width");
295 subtype_bits = total_bits / 2;
297 const auto bounds_real =
map_bounds(endianness_map, 0, subtype_bits - 1);
298 const auto bounds_imag =
299 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
333 const exprt &bitvector_expr,
334 const typet &target_type,
340 if(target_type.
id() == ID_floatbv)
350 target_type.
id() == ID_c_enum || target_type.
id() == ID_c_enum_tag ||
351 target_type.
id() == ID_string)
357 if(target_type.
id() == ID_struct)
362 else if(target_type.
id() == ID_struct_tag)
369 result.
type() = target_type;
370 return std::move(result);
372 else if(target_type.
id() == ID_union)
375 bitvector_expr,
to_union_type(target_type), endianness_map, ns);
377 else if(target_type.
id() == ID_union_tag)
384 result.
type() = target_type;
387 else if(target_type.
id() == ID_array)
390 bitvector_expr,
to_array_type(target_type), endianness_map, ns);
392 else if(target_type.
id() == ID_vector)
397 else if(target_type.
id() == ID_complex)
405 false,
"bv_to_expr does not yet support ", target_type.
id_string());
412 const std::optional<mp_integer> &offset_bytes,
413 const std::optional<mp_integer> &max_bytes,
414 const std::size_t bits_per_byte,
416 bool unpack_byte_array =
false);
427 std::size_t lower_bound,
428 std::size_t upper_bound,
429 const std::size_t bits_per_byte,
434 if(src.
id() == ID_array)
438 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
439 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
442 const typet &element_type = src.
type().
id() == ID_array
445 const typet index_type = src.
type().
id() == ID_array
452 bytes.reserve(upper_bound - lower_bound);
453 for(std::size_t i = lower_bound; i < upper_bound; ++i)
471 std::size_t el_bytes,
473 const std::size_t bits_per_byte,
476 const typet index_type = src.
type().
id() == ID_array
482 static std::size_t array_comprehension_index_counter = 0;
483 ++array_comprehension_index_counter;
485 "$array_comprehension_index_a_v" +
494 unpack_rec(element, little_endian, {}, {}, bits_per_byte, ns,
false);
498 exprt body = sub_operands.front();
500 array_comprehension_index,
501 from_integer(el_bytes, array_comprehension_index.type())};
502 for(std::size_t i = 1; i < el_bytes; ++i)
510 const exprt array_vector_size = src.
type().
id() == ID_vector
515 std::move(array_comprehension_index),
540 const std::optional<mp_integer> &src_size,
543 const std::optional<mp_integer> &offset_bytes,
544 const std::optional<mp_integer> &max_bytes,
545 const std::size_t bits_per_byte,
548 const std::size_t el_bytes = numeric_cast_v<std::size_t>(
549 (element_bits + bits_per_byte - 1) / bits_per_byte);
551 if(!src_size.has_value() && !max_bytes.has_value())
554 el_bytes > 0 && element_bits % bits_per_byte == 0,
555 "unpacking of arrays with non-byte-aligned elements is not supported");
557 src, el_bytes, little_endian, bits_per_byte, ns);
565 std::optional<mp_integer> num_elements = src_size;
566 if(element_bits > 0 && element_bits % bits_per_byte == 0)
568 if(!num_elements.has_value())
571 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
574 if(offset_bytes.has_value())
577 first_element = *offset_bytes / el_bytes;
579 byte_operands.resize(
580 numeric_cast_v<std::size_t>(std::min(
581 *offset_bytes - (*offset_bytes % el_bytes),
582 *num_elements * el_bytes)),
591 num_elements = *max_bytes;
594 const typet index_type = src_simp.
type().
id() == ID_array
598 for(
mp_integer i = first_element; i < *num_elements; ++i)
603 (src_simp.
id() == ID_array || src_simp.
id() == ID_vector) &&
606 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
607 element = src_simp.
operands()[index_int];
617 const std::optional<mp_integer> element_max_bytes =
619 ? std::min(
mp_integer{el_bytes}, *max_bytes - byte_operands.size())
620 : std::optional<mp_integer>{};
621 const std::size_t element_max_bytes_int =
622 element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
626 element, little_endian, {}, element_max_bytes, bits_per_byte, ns,
true);
629 byte_operands.insert(
630 byte_operands.end(), sub_operands.begin(), sub_operands.end());
632 if(max_bytes && byte_operands.size() >= *max_bytes)
636 const std::size_t size = byte_operands.size();
638 std::move(byte_operands),
655 std::size_t total_bits,
658 const std::optional<mp_integer> &offset_bytes,
659 const std::optional<mp_integer> &max_bytes,
660 const std::size_t bits_per_byte,
664 std::move(bit_fields),
bv_typet{total_bits}};
677 std::make_move_iterator(sub.
operands().begin()),
678 std::make_move_iterator(sub.
operands().end()));
694 const std::optional<mp_integer> &offset_bytes,
695 const std::optional<mp_integer> &max_bytes,
696 const std::size_t bits_per_byte,
700 src.
type().
id() == ID_struct_tag
705 std::optional<mp_integer> offset_in_member;
706 std::optional<mp_integer> max_bytes_left;
707 std::optional<std::pair<exprt::operandst, std::size_t>> bit_fields;
711 for(
auto it = components.begin(); it != components.end(); ++it)
713 const auto &comp = *it;
722 component_bits.has_value() ||
723 (std::next(it) == components.end() && !bit_fields.has_value()),
724 "members of non-constant width should come last in a struct");
727 if(src.
id() == ID_struct)
733 if(bit_fields.has_value())
736 std::move(bit_fields->first),
747 if(offset_bytes.has_value())
752 if(*offset_in_member < 0)
753 offset_in_member.reset();
756 if(max_bytes.has_value())
759 if(*max_bytes_left < 0)
766 (component_bits.has_value() && *component_bits % bits_per_byte != 0))
768 if(!bit_fields.has_value())
771 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
772 bit_fields->first.insert(
773 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
775 bit_fields->second += bits_int;
783 !bit_fields.has_value(),
784 "all preceding members should have been processed");
787 component_bits.has_value() && offset_in_member.has_value() &&
788 *offset_in_member * bits_per_byte >= *component_bits)
792 byte_operands.resize(
793 byte_operands.size() +
794 numeric_cast_v<std::size_t>(*component_bits / bits_per_byte),
808 byte_operands.insert(
810 std::make_move_iterator(sub.
operands().begin()),
811 std::make_move_iterator(sub.
operands().end()));
814 if(component_bits.has_value())
819 if(bit_fields.has_value())
822 std::move(bit_fields->first),
832 const std::size_t size = byte_operands.size();
834 std::move(byte_operands),
847 const std::size_t bits_per_byte,
861 *subtype_bits / bits_per_byte,
871 *subtype_bits / bits_per_byte,
875 byte_operands.insert(
877 std::make_move_iterator(sub_imag.
operands().begin()),
878 std::make_move_iterator(sub_imag.
operands().end()));
880 const std::size_t size = byte_operands.size();
882 std::move(byte_operands),
901 const std::optional<mp_integer> &offset_bytes,
902 const std::optional<mp_integer> &max_bytes,
903 const std::size_t bits_per_byte,
905 bool unpack_byte_array)
907 if(src.
type().
id() == ID_array)
916 !unpack_byte_array && *element_bits == bits_per_byte &&
922 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.
size());
933 else if(src.
type().
id() == ID_vector)
942 !unpack_byte_array && *element_bits == bits_per_byte &&
950 numeric_cast_v<mp_integer>(vector_type.
size()),
958 else if(src.
type().
id() == ID_complex)
962 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
965 src, little_endian, offset_bytes, max_bytes, bits_per_byte, ns);
967 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
970 src.
type().
id() == ID_union_tag
976 if(widest_member.has_value())
979 src, widest_member->first.get_name(), widest_member->first.
type()};
984 widest_member->second,
1002 else if(src.
type().
id() == ID_pointer)
1013 else if(src.
id() == ID_string_constant)
1035 else if(src.
type().
id() != ID_empty)
1040 DATA_INVARIANT(bits_opt.has_value(),
"basic type should have a fixed size");
1046 if(max_bytes.has_value())
1048 const auto max_bits = *max_bytes * bits_per_byte;
1051 last_bit = std::min(last_bit, max_bits);
1055 bit_offset = std::max(
mp_integer{0}, last_bit - max_bits);
1060 src,
bv_typet{numeric_cast_v<std::size_t>(total_bits)});
1061 auto const byte_type =
bv_typet{bits_per_byte};
1066 for(; bit_offset < last_bit; bit_offset += bits_per_byte)
1072 from_integer(bit_offset + bits_per_byte - 1, array_type.index_type()),
1080 byte_operands.push_back(extractbits);
1082 byte_operands.insert(byte_operands.begin(), extractbits);
1085 const std::size_t size = byte_operands.size();
1087 return array_exprt{std::move(byte_operands), std::move(array_type)};
1107 const typet &subtype,
1111 std::optional<std::size_t> num_elements;
1112 if(src.
type().
id() == ID_array)
1117 if(num_elements.has_value())
1120 operands.reserve(*num_elements);
1121 for(std::size_t i = 0; i < *num_elements; ++i)
1130 tmp.
type() = subtype;
1131 tmp.
offset() = new_offset;
1137 if(src.
type().
id() == ID_array)
1150 static std::size_t array_comprehension_index_counter = 0;
1151 ++array_comprehension_index_counter;
1153 "$array_comprehension_index_a" +
1161 array_comprehension_index,
1164 array_comprehension_index.type())},
1168 body.
type() = subtype;
1169 body.
offset() = std::move(new_offset);
1172 std::move(array_comprehension_index),
1199 real.
type() = subtype;
1206 imag.
type() = subtype;
1265 src.
id() == ID_byte_extract_little_endian ||
1266 src.
id() == ID_byte_extract_big_endian);
1267 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
1271 if(upper_bound_opt.has_value())
1275 upper_bound_opt.value(),
1277 src.
offset(), upper_bound_opt.value().
type())),
1280 else if(src.
type().
id() == ID_empty)
1283 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.
offset());
1284 const auto upper_bound_int_opt =
1285 numeric_cast<mp_integer>(upper_bound_opt.value_or(
nil_exprt()));
1291 lower_bound_int_opt,
1292 upper_bound_int_opt,
1299 if(src.
type().
id() == ID_array || src.
type().
id() == ID_vector)
1308 element_bits.has_value() && *element_bits >= 1 &&
1312 src, unpacked, subtype, *element_bits, ns);
1315 else if(src.
type().
id() == ID_complex)
1318 if(result.has_value())
1319 return std::move(*result);
1323 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
1326 src.
type().
id() == ID_struct_tag
1334 for(
const auto &comp : components)
1340 !component_bits.has_value() ||
1347 auto member_offset_opt =
1350 if(!member_offset_opt.has_value())
1359 member_offset_opt.value(), unpacked.
offset().
type()));
1362 tmp.
type() = comp.type();
1363 tmp.
offset() = new_offset;
1371 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
1374 src.
type().
id() == ID_union_tag
1380 if(widest_member.has_value())
1383 tmp.
type() = widest_member->first.type();
1386 widest_member->first.get_name(),
1392 const exprt &root = unpacked.
op();
1395 std::optional<typet> subtype;
1396 std::optional<typet> index_type;
1397 if(root.
type().
id() == ID_vector)
1412 "offset bits are byte aligned");
1415 if(!size_bits.has_value())
1420 op0_bits.has_value(),
1421 "the extracted width or the source width must be known");
1422 size_bits = op0_bits;
1430 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1432 op.reserve(width_bytes);
1434 for(std::size_t i = 0; i < width_bytes; i++)
1437 std::size_t offset_int = little_endian ? (width_bytes - i - 1) : i;
1446 offset_i.is_constant() &&
1447 (root.
id() == ID_array || root.
id() == ID_vector) &&
1449 index < root.
operands().size() && index >= 0)
1452 op.push_back(root.
operands()[numeric_cast_v<std::size_t>(index)]);
1460 if(width_bytes == 1)
1478 const exprt &value_as_byte_array,
1479 const std::optional<exprt> &non_const_update_bound,
1493 const typet &subtype,
1494 const exprt &value_as_byte_array,
1495 const exprt &non_const_update_bound,
1500 static std::size_t array_comprehension_index_counter = 0;
1501 ++array_comprehension_index_counter;
1503 "$array_comprehension_index_u_a_v" +
1509 array_comprehension_index, src.
offset().
type()),
1514 array_comprehension_index, non_const_update_bound.
type()),
1518 src.
offset(), non_const_update_bound.
type()),
1519 non_const_update_bound}};
1522 src.
id() == ID_byte_update_little_endian ||
1523 src.
id() == ID_byte_update_big_endian);
1524 const bool little_endian = src.
id() == ID_byte_update_little_endian;
1530 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1534 value_as_byte_array,
1536 array_comprehension_index,
1538 src.
offset(), array_comprehension_index.
type())}},
1545 array_comprehension_index,
1546 std::move(array_comprehension_body),
1562 const typet &subtype,
1564 const std::optional<exprt> &non_const_update_bound,
1568 src.
id() == ID_byte_update_little_endian ||
1569 src.
id() == ID_byte_update_big_endian);
1570 const bool little_endian = src.
id() == ID_byte_update_little_endian;
1572 const typet index_type = src.
type().
id() == ID_array
1579 for(std::size_t i = 0; i < value_as_byte_array.
operands().size(); ++i)
1592 if(e.id() == ID_index)
1595 if(index_expr.
array() == src.
op() && index_expr.
index() == where)
1601 if(non_const_update_bound.has_value())
1607 *non_const_update_bound},
1612 if(result.
id() != ID_with)
1613 result =
with_exprt{result, std::move(where), std::move(update_value)};
1638 const typet &subtype,
1639 const exprt &subtype_size,
1640 const exprt &value_as_byte_array,
1641 const exprt &non_const_update_bound,
1642 const exprt &initial_bytes,
1643 const exprt &first_index,
1644 const exprt &first_update_value,
1647 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1648 ? ID_byte_extract_little_endian
1649 : ID_byte_extract_big_endian;
1653 static std::size_t array_comprehension_index_counter = 0;
1654 ++array_comprehension_index_counter;
1656 "$array_comprehension_index_u_a_v_u" +
1669 array_comprehension_index, first_index.
type()),
1680 array_comprehension_index, first_index.
type()),
1685 value_as_byte_array,
1686 std::move(offset_expr),
1698 non_const_update_bound, subtype_size.
type()),
1713 non_const_update_bound, initial_bytes.
type()),
1715 subtype_size.
type()),
1722 array_comprehension_index, last_index.type()),
1737 value_as_byte_array,
1742 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1747 array_comprehension_index, first_index.
type()),
1753 array_comprehension_index, last_index.type()),
1755 std::move(last_update_value),
1756 std::move(update_value)}}};
1760 array_comprehension_index,
1761 std::move(array_comprehension_body),
1778 const typet &subtype,
1779 const exprt &value_as_byte_array,
1780 const std::optional<exprt> &non_const_update_bound,
1790 subtype_size_opt.value(), src.
offset().
type()),
1805 const exprt update_size =
1809 if(non_const_update_bound.has_value())
1812 *non_const_update_bound, subtype_size.
type());
1817 value_as_byte_array.
id() == ID_array,
1818 "value should be an array expression if the update bound is constant");
1819 update_bound = update_size;
1835 value_as_byte_array,
1839 if(value_as_byte_array.
id() != ID_array)
1845 value_as_byte_array,
1846 *non_const_update_bound,
1858 std::size_t step_size = 1;
1865 std::size_t offset = 0;
1869 with_exprt result{src.
op(), first_index, first_update_value};
1871 auto lower_byte_update_array_vector_non_const_one_element =
1876 &value_as_byte_array,
1878 &result](std::size_t i) ->
void {
1893 value_as_byte_array,
1901 for(; offset + step_size <= value_as_byte_array.
operands().size();
1902 offset += step_size, ++i)
1904 lower_byte_update_array_vector_non_const_one_element(i);
1908 if(offset < value_as_byte_array.
operands().size())
1909 lower_byte_update_array_vector_non_const_one_element(i);
1929 const exprt &element_to_update,
1932 const exprt &value_as_byte_array,
1933 const std::optional<exprt> &non_const_update_bound,
1941 std::size_t first = 0;
1948 mp_integer offset_bits_in_target_element = offset_bits - bits_already_set;
1950 if(offset_bits_in_target_element < 0)
1953 value_as_byte_array.
id() != ID_array ||
1955 -offset_bits_in_target_element,
1956 "indices past the update should be handled below");
1957 first += numeric_cast_v<std::size_t>(
1959 offset_bits_in_target_element +=
1962 if(offset_bits_in_target_element < 0)
1969 update_elements > 0,
"indices before the update should be handled above");
1972 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1973 if(value_as_byte_array.
id() == ID_array)
1974 end = std::min(end, value_as_byte_array.
operands().size());
1977 const std::size_t update_size = update_values.size();
1986 offset_bits_in_target_element >= 0 &&
1989 new_value =
array_exprt{update_values, update_type};
1993 if(src.
id() == ID_byte_update_little_endian)
1994 std::reverse(update_values.begin(), update_values.end());
1995 if(offset_bits_in_target_element < 0)
1997 if(src.
id() == ID_byte_update_little_endian)
2002 numeric_cast_v<std::size_t>(-offset_bits_in_target_element)};
2009 numeric_cast_v<std::size_t>(-offset_bits_in_target_element)};
2014 const std::size_t offset_bits_int =
2015 numeric_cast_v<std::size_t>(offset_bits_in_target_element);
2016 const std::size_t subtype_bits_int =
2017 numeric_cast_v<std::size_t>(subtype_bits);
2021 subtype_bits_int - 1,
2022 subtype_bits_int - offset_bits_int,
2035 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
2036 ? ID_byte_extract_little_endian
2037 : ID_byte_extract_big_endian;
2048 offset_bits_in_target_element = 0;
2063 std::optional<exprt> update_bound;
2064 if(non_const_update_bound.has_value())
2072 *non_const_update_bound,
2076 *non_const_update_bound,
2086 remaining_update_bytes},
2105 const typet &subtype,
2106 const std::optional<mp_integer> &subtype_bits,
2107 const exprt &value_as_byte_array,
2108 const std::optional<exprt> &non_const_update_bound,
2111 const bool is_array = src.
type().
id() == ID_array;
2128 !subtype_bits.has_value() || value_as_byte_array.
id() != ID_array)
2131 src, subtype, value_as_byte_array, non_const_update_bound, ns);
2134 std::size_t num_elements =
2141 elements.reserve(num_elements);
2145 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bits; ++i)
2151 i * *subtype_bits < offset_bits + value_as_byte_array.operands().size() *
2152 src.get_bits_per_byte();
2161 value_as_byte_array,
2162 non_const_update_bound,
2167 for(; i < num_elements; ++i)
2190 const exprt &value_as_byte_array,
2191 const std::optional<exprt> &non_const_update_bound,
2195 elements.reserve(struct_type.
components().size());
2198 for(
const auto &comp : struct_type.
components())
2211 auto offset_bits = numeric_cast<mp_integer>(offset);
2212 if(!offset_bits.has_value() || !element_width.has_value())
2219 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
2220 ? ID_byte_extract_little_endian
2221 : ID_byte_extract_big_endian;
2241 bu, value_as_byte_array, non_const_update_bound, ns),
2256 *offset_bits >= *element_width ||
2257 (value_as_byte_array.
id() == ID_array && *offset_bits < 0 &&
2261 elements.push_back(member);
2272 value_as_byte_array,
2273 non_const_update_bound,
2294 const exprt &value_as_byte_array,
2295 const std::optional<exprt> &non_const_update_bound,
2301 widest_member.has_value(),
2302 "lower_byte_update of union of unknown size is not supported");
2306 src.
op(), widest_member->first.get_name(), widest_member->first.
type()});
2307 bu.
type() = widest_member->first.type();
2310 widest_member->first.get_name(),
2325 const exprt &value_as_byte_array,
2326 const std::optional<exprt> &non_const_update_bound,
2329 if(src.
type().
id() == ID_array || src.
type().
id() == ID_vector)
2331 std::optional<typet> subtype;
2332 if(src.
type().
id() == ID_vector)
2341 if(value_as_byte_array.
id() != ID_array)
2344 non_const_update_bound.has_value(),
2345 "constant update bound should yield an array expression");
2347 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2354 non_const_update_bound,
2363 value_as_byte_array,
2364 non_const_update_bound,
2368 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
2371 src.
type().
id() == ID_struct_tag
2375 src, struct_type, value_as_byte_array, non_const_update_bound, ns);
2379 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
2382 src.
type().
id() == ID_union_tag
2386 src, union_type, value_as_byte_array, non_const_update_bound, ns);
2392 src.
type().
id() == ID_c_enum || src.
type().
id() == ID_c_enum_tag)
2397 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2398 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2401 if(value_as_byte_array.
id() == ID_array)
2402 update_bytes = value_as_byte_array.
operands();
2406 value_as_byte_array,
2413 const std::size_t update_size_bits =
2415 const std::size_t bit_width = std::max(type_bits, update_size_bits);
2417 const bool is_little_endian = src.
id() == ID_byte_update_little_endian;
2421 if(bit_width > type_bits)
2428 if(!is_little_endian)
2434 if(non_const_update_bound.has_value())
2438 src.
id() == ID_byte_update_little_endian,
2445 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2451 *non_const_update_bound},
2459 if(is_little_endian)
2464 power(2, bit_width) -
power(2, bit_width - update_size_bits),
2479 if(!is_little_endian)
2481 mask_shifted.true_case().
swap(mask_shifted.false_case());
2492 if(is_little_endian)
2493 std::reverse(value.operands().begin(), value.operands().end());
2495 exprt zero_extended;
2496 if(bit_width > update_size_bits)
2503 if(!is_little_endian)
2509 zero_extended = value;
2514 shl_exprt{zero_extended, offset_in_bits},
2516 if(!is_little_endian)
2518 value_shifted.true_case().
swap(value_shifted.false_case());
2525 bitor_exprt bitor_expr{bitand_expr, value_shifted};
2527 if(bit_width > type_bits)
2530 bitor_expr.type(), src.
id() == ID_byte_update_little_endian, ns);
2531 const auto bounds =
map_bounds(endianness_map, 0, type_bits - 1);
2537 bitor_expr, bounds.ub, bounds.lb,
bv_typet{type_bits}},
2548 false,
"lower_byte_update does not yet support ", src.
type().
id_string());
2555 src.
id() == ID_byte_update_little_endian ||
2556 src.
id() == ID_byte_update_big_endian,
2557 "byte update expression should either be little or big endian");
2573 std::optional<exprt> non_const_update_bound;
2578 simplify(update_size_expr_opt.value(), ns);
2580 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
2581 ? ID_byte_extract_little_endian
2582 : ID_byte_extract_big_endian;
2585 if(!update_size_expr_opt.value().is_constant())
2586 non_const_update_bound = *update_size_expr_opt;
2594 update_bits.has_value(),
"constant size-of should imply fixed bit width");
2595 const size_t update_bits_int = numeric_cast_v<size_t>(*update_bits);
2597 if(update_bits_int % bits_per_byte != 0)
2601 "non-byte aligned type expected to be a bitvector type");
2612 const exprt overlapping_byte =
2615 size_t n_extra_bits = bits_per_byte - update_bits_int % bits_per_byte;
2617 overlapping_byte, n_extra_bits - 1, 0,
bv_typet{n_extra_bits}};
2621 update_value,
bv_typet{update_bits_int}),
2628 update_bits_int / bits_per_byte, update_size_expr_opt->type());
2657 src.
id() == ID_byte_update_little_endian ||
2658 src.
id() == ID_byte_update_big_endian)
2663 src.
id() == ID_byte_extract_little_endian ||
2664 src.
id() == ID_byte_extract_big_endian)
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Expression to define a mapping from an argument (index) to elements.
Array constructor from list of elements.
typet index_type() const
The type of the index expressions into any instance of this type.
const typet & element_type() const
The type of the elements of the array.
const exprt & size() const
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Bit-wise negation of bit-vectors.
Base class of fixed-width bit-vector types.
std::size_t get_width() const
Fixed-width bit-vector without numerical interpretation.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & value() const
const exprt & offset() const
std::size_t get_bits_per_byte() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Complex constructor from a pair of numbers.
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Complex numbers made of pair of given subtype.
Concatenation of bit-vector operands.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Union constructor to support unions without any member (a GCC/Clang feature).
Maps a big-endian offset to a little-endian offset.
size_t number_of_bits() const
size_t map_bit(size_t bit) const
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
Fixed-width bit-vector with two's complement interpretation.
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const typet & subtype() const
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
The unary minus expression.
Union constructor from single element.
std::optional< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
typet index_type() const
The type of any index expression into an instance of this type.
Operator to update elements in structs and arrays.
#define Forall_operands(it, expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update v...
static exprt lower_byte_update_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as updat...
static exprt bv_to_expr(const exprt &bitvector_expr, const typet &target_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an expression of type target_type.
static exprt bv_to_union_expr(const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a union-typed expression.
static complex_exprt bv_to_complex_expr(const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.
static array_exprt unpack_struct(const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const std::size_t bits_per_byte, const namespacet &ns)
Build the individual bytes to be used in an update.
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...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
static vector_exprt bv_to_vector_expr(const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.
static void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
static struct_exprt bv_to_struct_expr(const exprt &bitvector_expr, const struct_typet &struct_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a struct-typed expression.
static array_exprt unpack_complex(const exprt &src, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const std::optional< mp_integer > &subtype_bits, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as ...
static exprt lower_byte_update_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
static array_exprt bv_to_array_expr(const exprt &bitvector_expr, const array_typet &array_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an array-typed expression.
static boundst map_bounds(const endianness_mapt &endianness_map, std::size_t lower_bound, std::size_t upper_bound)
Map bit boundaries according to endianness.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
static exprt lower_byte_extract_array_vector(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const typet &subtype, const mp_integer &element_bits, const namespacet &ns)
Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual compon...
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
static exprt unpack_array_vector(const exprt &src, const std::optional< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
static exprt unpack_rec(const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
static exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update ...
static exprt lower_byte_update_byte_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_by...
static exprt lower_byte_update_single_element(const byte_update_exprt &src, const mp_integer &offset_bits, const exprt &element_to_update, const mp_integer &subtype_bits, const mp_integer &bits_already_set, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Byte update a struct/array/vector element.
static std::optional< exprt > lower_byte_extract_complex(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components t...
static exprt lower_byte_update_array_vector_unbounded(const byte_update_exprt &src, const typet &subtype, const exprt &subtype_size, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const exprt &initial_bytes, const exprt &first_index, const exprt &first_update_value, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)