25 const exprt &bitvector_expr,
26 const typet &target_type,
39 std::size_t lower_bound,
40 std::size_t upper_bound)
43 result.
lb = lower_bound;
44 result.
ub = upper_bound;
52 if(result.
ub < result.
lb)
65 const exprt &bitvector_expr,
73 operands.reserve(components.size());
75 for(
const auto &comp : components)
78 std::size_t component_bits;
79 if(component_bits_opt.has_value())
80 component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
85 if(component_bits == 0)
102 if(component_bits_opt.has_value())
112 const exprt &bitvector_expr,
117 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
120 const std::size_t total_bits =
122 if(!num_elements.has_value())
124 if(!subtype_bits.has_value() || *subtype_bits == 0)
125 num_elements = total_bits;
127 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
130 !num_elements.has_value() || !subtype_bits.has_value() ||
131 *subtype_bits * *num_elements == total_bits,
132 "subtype width times array size should be total bitvector width");
135 operands.reserve(*num_elements);
136 for(std::size_t i = 0; i < *num_elements; ++i)
138 if(subtype_bits.has_value())
140 const std::size_t subtype_bits_int =
141 numeric_cast_v<std::size_t>(*subtype_bits);
143 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
147 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
159 return array_exprt{std::move(operands), array_type};
165 const exprt &bitvector_expr,
170 const std::size_t num_elements =
171 numeric_cast_v<std::size_t>(vector_type.
size());
174 !subtype_bits.has_value() ||
175 *subtype_bits * num_elements ==
177 "subtype width times vector size should be total bitvector width");
180 operands.reserve(num_elements);
181 for(std::size_t i = 0; i < num_elements; ++i)
183 if(subtype_bits.has_value())
185 const std::size_t subtype_bits_int =
186 numeric_cast_v<std::size_t>(*subtype_bits);
188 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
192 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
210 const exprt &bitvector_expr,
215 const std::size_t total_bits =
218 std::size_t subtype_bits;
219 if(subtype_bits_opt.has_value())
221 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
223 subtype_bits * 2 == total_bits,
224 "subtype width should be half of the total bitvector width");
227 subtype_bits = total_bits / 2;
229 const auto bounds_real =
map_bounds(endianness_map, 0, subtype_bits - 1);
230 const auto bounds_imag =
231 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
263 const exprt &bitvector_expr,
264 const typet &target_type,
272 target_type.
id() == ID_c_enum || target_type.
id() == ID_c_enum_tag ||
273 target_type.
id() == ID_string)
282 if(target_type.
id() == ID_struct)
287 else if(target_type.
id() == ID_struct_tag)
294 result.
type() = target_type;
295 return std::move(result);
297 else if(target_type.
id() == ID_array)
300 bitvector_expr,
to_array_type(target_type), endianness_map, ns);
302 else if(target_type.
id() == ID_vector)
307 else if(target_type.
id() == ID_complex)
315 false,
"bv_to_expr does not yet support ", target_type.
id_string());
325 bool unpack_byte_array =
false);
335 std::size_t lower_bound,
336 std::size_t upper_bound,
341 if(src.
id() == ID_array)
345 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
346 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
350 bytes.reserve(upper_bound - lower_bound);
351 for(std::size_t i = lower_bound; i < upper_bound; ++i)
381 const std::size_t el_bytes =
382 numeric_cast_v<std::size_t>((element_bits + 7) / 8);
384 if(!src_size.has_value() && !max_bytes.has_value())
388 static std::size_t array_comprehension_index_counter = 0;
389 ++array_comprehension_index_counter;
391 "$array_comprehension_index_a_v" +
404 exprt body = sub_operands.front();
406 array_comprehension_index,
407 from_integer(el_bytes, array_comprehension_index.type())};
408 for(std::size_t i = 1; i < el_bytes; ++i)
418 if(src.
type().
id() == ID_vector)
430 std::move(array_comprehension_index),
444 if(element_bits > 0 && element_bits % 8 == 0)
446 if(!num_elements.has_value())
449 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
452 if(offset_bytes.has_value())
455 first_element = *offset_bytes / el_bytes;
457 byte_operands.resize(
458 numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
467 num_elements = *max_bytes;
471 for(
mp_integer i = first_element; i < *num_elements; ++i)
476 (src_simp.
id() == ID_array || src_simp.
id() == ID_vector) &&
479 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
480 element = src_simp.
operands()[index_int];
489 exprt sub =
unpack_rec(element, little_endian, {}, max_bytes, ns,
true);
492 byte_operands.insert(
493 byte_operands.end(), sub_operands.begin(), sub_operands.end());
496 const std::size_t size = byte_operands.size();
498 std::move(byte_operands),
514 std::size_t total_bits,
525 unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns,
true);
529 std::make_move_iterator(sub.
operands().begin()),
530 std::make_move_iterator(sub.
operands().end()));
558 for(
auto it = components.begin(); it != components.end(); ++it)
560 const auto &comp = *it;
569 component_bits.has_value() ||
570 (std::next(it) == components.end() && !bit_fields.has_value()),
571 "members of non-constant width should come last in a struct");
574 if(src.
id() == ID_struct)
580 if(bit_fields.has_value())
583 std::move(bit_fields->first),
593 if(offset_bytes.has_value())
598 if(*offset_in_member < 0)
599 offset_in_member.reset();
602 if(max_bytes.has_value())
605 if(*max_bytes_left < 0)
612 (component_bits.has_value() && *component_bits % 8 != 0))
614 if(!bit_fields.has_value())
617 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
618 bit_fields->first.insert(
619 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
621 bit_fields->second += bits_int;
629 !bit_fields.has_value(),
630 "all preceding members should have been processed");
633 member, little_endian, offset_in_member, max_bytes_left, ns,
true);
635 byte_operands.insert(
637 std::make_move_iterator(sub.
operands().begin()),
638 std::make_move_iterator(sub.
operands().end()));
640 if(component_bits.has_value())
644 if(bit_fields.has_value())
646 std::move(bit_fields->first),
654 const std::size_t size = byte_operands.size();
690 byte_operands.insert(
692 std::make_move_iterator(sub_imag.
operands().begin()),
693 std::make_move_iterator(sub_imag.
operands().end()));
695 const std::size_t size = byte_operands.
size();
717 bool unpack_byte_array)
719 if(src.
type().
id()==ID_array)
727 if(!unpack_byte_array && *element_bits == 8)
730 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.
size());
740 else if(src.
type().
id() == ID_vector)
748 if(!unpack_byte_array && *element_bits == 8)
753 numeric_cast_v<mp_integer>(vector_type.
size()),
760 else if(src.
type().
id() == ID_complex)
764 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
766 return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
768 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
777 for(
const auto &comp : components)
781 if(!element_width.has_value() || *element_width <= max_width)
784 max_width = *element_width;
785 max_comp_type = comp.type();
786 max_comp_name = comp.get_name();
793 member, little_endian, offset_bytes, max_bytes, ns,
true);
796 else if(src.
type().
id() == ID_pointer)
806 else if(src.
id() == ID_string_constant)
816 else if(src.
id() == ID_constant && src.
type().
id() == ID_string)
826 else if(src.
type().
id()!=ID_empty)
831 DATA_INVARIANT(bits_opt.has_value(),
"basic type should have a fixed size");
839 src,
bv_typet{numeric_cast_v<std::size_t>(bits)}),
848 byte_operands.push_back(extractbits);
850 byte_operands.insert(byte_operands.begin(), extractbits);
853 const std::size_t size = byte_operands.
size();
855 std::move(byte_operands),
880 if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
885 real.
type() = subtype;
891 imag.
type() = subtype;
950 src.
id() == ID_byte_extract_little_endian ||
951 src.
id() == ID_byte_extract_big_endian);
952 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
956 if(upper_bound_opt.has_value())
960 upper_bound_opt.value(),
962 src.
offset(), upper_bound_opt.value().
type())),
965 else if(src.
type().
id() == ID_empty)
968 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.
offset());
969 const auto upper_bound_int_opt =
970 numeric_cast<mp_integer>(upper_bound_opt.value_or(
nil_exprt()));
974 src.
op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
976 if(src.
type().
id()==ID_array)
985 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
987 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
988 if(!num_elements.has_value() && unpacked.
op().
id() == ID_array)
989 num_elements = unpacked.
op().
operands().size();
991 if(num_elements.has_value())
994 operands.reserve(*num_elements);
995 for(std::size_t i = 0; i < *num_elements; ++i)
1002 tmp.
type() = subtype;
1003 tmp.
offset() = new_offset;
1014 static std::size_t array_comprehension_index_counter = 0;
1015 ++array_comprehension_index_counter;
1017 "$array_comprehension_index_a" +
1026 *element_bits / 8, array_comprehension_index.type())},
1030 body.
type() = subtype;
1031 body.
offset() = std::move(new_offset);
1039 else if(src.
type().
id() == ID_vector)
1048 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1050 const std::size_t num_elements =
1051 numeric_cast_v<std::size_t>(vector_type.
size());
1054 operands.reserve(num_elements);
1055 for(std::size_t i = 0; i < num_elements; ++i)
1062 tmp.
type() = subtype;
1071 else if(src.
type().
id() == ID_complex)
1074 if(result.has_value())
1075 return std::move(*result);
1079 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
1087 for(
const auto &comp : components)
1093 !component_bits.has_value() || *component_bits == 0 ||
1094 *component_bits % 8 != 0)
1100 auto member_offset_opt =
1103 if(!member_offset_opt.has_value())
1112 member_offset_opt.value(), unpacked.
offset().
type()));
1115 tmp.
type()=comp.type();
1124 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
1130 typet max_comp_type;
1133 for(
const auto &comp : components)
1137 if(!element_width.has_value() || *element_width <= max_width)
1140 max_width = *element_width;
1141 max_comp_type = comp.type();
1142 max_comp_name = comp.get_name();
1148 tmp.
type() = max_comp_type;
1155 const exprt &root=unpacked.
op();
1159 if(root.
type().
id() == ID_vector)
1167 subtype_bits.has_value() && *subtype_bits == 8,
1168 "offset bits are byte aligned");
1171 if(!size_bits.has_value())
1176 op0_bits.has_value(),
1177 "the extracted width or the source width must be known");
1178 size_bits = op0_bits;
1182 (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1185 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_elements);
1187 op.reserve(width_bytes);
1189 for(std::size_t i=0; i<width_bytes; i++)
1192 std::size_t offset_int=
1193 little_endian?(width_bytes-i-1):i;
1200 offset_i.is_constant() &&
1201 (root.
id() == ID_array || root.
id() == ID_vector) &&
1203 index < root.
operands().size() && index >= 0)
1206 op.push_back(root.
operands()[numeric_cast_v<std::size_t>(index)]);
1231 const exprt &value_as_byte_array,
1246 const typet &subtype,
1247 const exprt &value_as_byte_array,
1248 const exprt &non_const_update_bound,
1253 static std::size_t array_comprehension_index_counter = 0;
1254 ++array_comprehension_index_counter;
1256 "$array_comprehension_index_u_a_v" +
1262 array_comprehension_index, src.
offset().
type()),
1267 array_comprehension_index, non_const_update_bound.
type()),
1270 src.
offset(), non_const_update_bound.
type()),
1271 non_const_update_bound}};
1274 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1278 value_as_byte_array,
1281 src.
offset(), array_comprehension_index.
type())}},
1286 std::move(array_comprehension_body),
1302 const typet &subtype,
1310 for(std::size_t i = 0; i < value_as_byte_array.
operands().size(); ++i)
1320 if(e.id() == ID_index)
1323 if(index_expr.
array() == src.
op() && index_expr.
index() == where)
1328 if(non_const_update_bound.has_value())
1334 *non_const_update_bound},
1342 if(result.
id() != ID_with)
1343 result =
with_exprt{result, where, update_value};
1368 const typet &subtype,
1369 const exprt &subtype_size,
1370 const exprt &value_as_byte_array,
1371 const exprt &non_const_update_bound,
1372 const exprt &initial_bytes,
1373 const exprt &first_index,
1374 const exprt &first_update_value,
1377 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1378 ? ID_byte_extract_little_endian
1379 : ID_byte_extract_big_endian;
1383 static std::size_t array_comprehension_index_counter = 0;
1384 ++array_comprehension_index_counter;
1386 "$array_comprehension_index_u_a_v_u" +
1398 array_comprehension_index, first_index.
type()),
1407 array_comprehension_index, first_index.
type()),
1411 extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1420 non_const_update_bound, subtype_size.
type()),
1432 non_const_update_bound, initial_bytes.
type()),
1440 array_comprehension_index, last_index.type()),
1453 value_as_byte_array,
1455 last_index, subtype_size.
type()),
1461 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1465 array_comprehension_index, first_index.
type()),
1469 array_comprehension_index, last_index.type()),
1471 std::move(last_update_value),
1472 std::move(update_value)}}};
1476 std::move(array_comprehension_body),
1493 const typet &subtype,
1494 const exprt &value_as_byte_array,
1498 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1499 ? ID_byte_extract_little_endian
1500 : ID_byte_extract_big_endian;
1509 subtype_size_opt.value(), src.
offset().
type()),
1524 if(non_const_update_bound.has_value())
1527 *non_const_update_bound, subtype_size.
type());
1532 value_as_byte_array.
id() == ID_array,
1533 "value should be an array expression if the update bound is constant");
1551 value_as_byte_array,
1556 if(value_as_byte_array.
id() != ID_array)
1562 value_as_byte_array,
1563 *non_const_update_bound,
1575 std::size_t step_size = 1;
1582 std::size_t offset = 0;
1586 with_exprt result{src.
op(), first_index, first_update_value};
1589 for(; offset + step_size <= value_as_byte_array.
operands().size();
1590 offset += step_size, ++i)
1607 value_as_byte_array,
1608 std::move(offset_expr),
1616 if(offset < value_as_byte_array.
operands().size())
1618 const std::size_t tail_size =
1619 value_as_byte_array.
operands().size() - offset;
1631 value_as_byte_array,
1653 const typet &subtype,
1654 const exprt &value_as_byte_array,
1658 const bool is_array = src.
type().
id() == ID_array;
1670 !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1671 non_const_update_bound.has_value() || value_as_byte_array.
id() != ID_array)
1674 src, subtype, value_as_byte_array, non_const_update_bound, ns);
1677 std::size_t num_elements =
1683 elements.reserve(num_elements);
1687 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1691 for(; i < num_elements &&
1693 (offset_bytes + value_as_byte_array.operands().size()) * 8;
1696 mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1697 mp_integer update_elements = *subtype_bits / 8;
1698 exprt::operandst::const_iterator first =
1699 value_as_byte_array.operands().begin();
1700 exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1701 if(update_offset < 0)
1704 value_as_byte_array.operands().size() > -update_offset,
1705 "indices past the update should be handled above");
1706 first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1710 update_elements -= update_offset;
1712 update_elements > 0,
1713 "indices before the update should be handled above");
1716 if(std::distance(first, end) > update_elements)
1717 end = first + numeric_cast_v<std::ptrdiff_t>(update_elements);
1719 const std::size_t update_size = update_values.size();
1724 from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1726 std::move(update_values),
1732 for(; i < num_elements; ++i)
1733 elements.push_back(
index_exprt{src.op(), from_integer(i, index_type())});
1755 const exprt &value_as_byte_array,
1759 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1760 ? ID_byte_extract_little_endian
1761 : ID_byte_extract_big_endian;
1764 elements.reserve(struct_type.
components().size());
1767 for(
const auto &comp : struct_type.
components())
1779 auto offset_bytes = numeric_cast<mp_integer>(offset);
1786 offset_bytes.has_value() &&
1787 (*offset_bytes * 8 >= *element_width ||
1788 (value_as_byte_array.
id() == ID_array && *offset_bytes < 0 &&
1789 -*offset_bytes >= value_as_byte_array.
operands().size())))
1791 elements.push_back(std::move(member));
1795 else if(!offset_bytes.has_value())
1818 bu, value_as_byte_array, non_const_update_bound, ns),
1828 mp_integer update_elements = (*element_width + 7) / 8;
1829 std::size_t first = 0;
1830 if(*offset_bytes < 0)
1834 value_as_byte_array.
id() != ID_array ||
1835 value_as_byte_array.
operands().size() > -*offset_bytes,
1836 "members past the update should be handled above");
1837 first = numeric_cast_v<std::size_t>(-*offset_bytes);
1841 update_elements -= *offset_bytes;
1843 update_elements > 0,
1844 "members before the update should be handled above");
1850 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1851 if(value_as_byte_array.
id() == ID_array)
1852 end = std::min(end, value_as_byte_array.
operands().size());
1855 const std::size_t update_size = update_values.size();
1864 if(non_const_update_bound.has_value())
1872 *non_const_update_bound,
1884 remaining_update_bytes};
1886 member_update_bound = std::move(update_size_expr);
1891 const std::size_t shift =
1893 const std::size_t element_bits_int =
1894 numeric_cast_v<std::size_t>(*element_width);
1896 const bool little_endian = src.
id() == ID_byte_update_little_endian;
1902 bv_typet{shift + element_bits_int}};
1911 exprt updated_element =
1915 elements.push_back(updated_element);
1920 element_bits_int - 1 + (little_endian ? shift : 0),
1921 (little_endian ? shift : 0),
1944 const exprt &value_as_byte_array,
1951 typet max_comp_type;
1954 for(
const auto &comp : components)
1958 if(!element_width.has_value() || *element_width <= max_width)
1961 max_width = *element_width;
1962 max_comp_type = comp.type();
1963 max_comp_name = comp.get_name();
1968 "lower_byte_update of union of unknown size is not supported");
1972 bu.
type() = max_comp_type;
1990 const exprt &value_as_byte_array,
1994 if(src.
type().
id() == ID_array || src.
type().
id() == ID_vector)
1997 if(src.
type().
id() == ID_vector)
2007 if(*element_width == 8)
2009 if(value_as_byte_array.
id() != ID_array)
2012 non_const_update_bound.has_value(),
2013 "constant update bound should yield an array expression");
2015 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2022 non_const_update_bound,
2027 src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2029 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
2034 value_as_byte_array,
2035 non_const_update_bound,
2040 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
2045 value_as_byte_array,
2046 non_const_update_bound,
2053 src.
type().
id() == ID_c_enum || src.
type().
id() == ID_c_enum_tag)
2058 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2059 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2062 if(value_as_byte_array.
id() == ID_array)
2063 update_bytes = value_as_byte_array.
operands();
2070 if(non_const_update_bound.has_value())
2074 src.
id() == ID_byte_update_little_endian,
2080 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2086 *non_const_update_bound},
2092 const std::size_t update_size = update_bytes.size();
2093 const std::size_t width = std::max(type_bits, update_size * 8);
2095 const bool is_little_endian = src.
id() == ID_byte_update_little_endian;
2099 if(is_little_endian)
2111 offset_times_eight, ID_ge,
from_integer(0, offset_type)};
2113 if_exprt mask_shifted{offset_ge_zero,
2116 if(!is_little_endian)
2117 mask_shifted.true_case().
swap(mask_shifted.false_case());
2122 if(width > type_bits)
2129 if(!is_little_endian)
2138 if(is_little_endian)
2139 std::reverse(value.operands().begin(), value.operands().end());
2141 exprt zero_extended;
2142 if(width > update_size * 8)
2149 if(!is_little_endian)
2155 zero_extended = value;
2158 if_exprt value_shifted{offset_ge_zero,
2159 shl_exprt{zero_extended, offset_times_eight},
2160 lshr_exprt{zero_extended, offset_times_eight}};
2161 if(!is_little_endian)
2162 value_shifted.true_case().
swap(value_shifted.false_case());
2165 bitor_exprt bitor_expr{bitand_expr, value_shifted};
2167 if(!is_little_endian && width > type_bits)
2172 bitor_expr, width - 1, width - type_bits,
bv_typet{type_bits}},
2183 false,
"lower_byte_update does not yet support ", src.
type().
id_string());
2190 src.
id() == ID_byte_update_little_endian ||
2191 src.
id() == ID_byte_update_big_endian,
2192 "byte update expression should either be little or big endian");
2211 simplify(update_size_expr_opt.value(), ns);
2213 if(!update_size_expr_opt.value().is_constant())
2214 non_const_update_bound = *update_size_expr_opt;
2216 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
2217 ? ID_byte_extract_little_endian
2218 : ID_byte_extract_big_endian;
2235 if(src.
id()==ID_byte_update_little_endian ||
2236 src.
id()==ID_byte_update_big_endian ||
2237 src.
id()==ID_byte_extract_little_endian ||
2238 src.
id()==ID_byte_extract_big_endian)
2258 if(src.
id()==ID_byte_update_little_endian ||
2259 src.
id()==ID_byte_update_big_endian)
2261 else if(src.
id()==ID_byte_extract_little_endian ||
2262 src.
id()==ID_byte_extract_big_endian)