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)
53 std::swap(result.
lb, result.
ub);
62 if(src.
id() == ID_unsignedbv)
64 else if(src.
id() == ID_signedbv)
66 else if(src.
id() == ID_bv)
68 else if(src.
id() == ID_c_enum)
70 else if(src.
id() == ID_c_bit_field)
80 const exprt &bitvector_expr,
88 operands.reserve(components.size());
90 for(
const auto &comp : components)
93 std::size_t component_bits;
94 if(component_bits_opt.has_value())
95 component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
100 if(component_bits == 0)
117 if(component_bits_opt.has_value())
127 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)
153 const auto bounds =
map_bounds(endianness_map, 0, component_bits - 1);
155 const irep_idt &component_name = widest_member.has_value()
156 ? widest_member->first.get_name()
157 : components.front().get_name();
158 const typet &component_type = widest_member.has_value()
159 ? widest_member->first.type()
160 : components.front().type();
174 const exprt &bitvector_expr,
179 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
182 const std::size_t total_bits =
184 if(!num_elements.has_value())
186 if(!subtype_bits.has_value() || *subtype_bits == 0)
187 num_elements = total_bits;
189 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
192 !num_elements.has_value() || !subtype_bits.has_value() ||
193 *subtype_bits * *num_elements == total_bits,
194 "subtype width times array size should be total bitvector width");
197 operands.reserve(*num_elements);
198 for(std::size_t i = 0; i < *num_elements; ++i)
200 if(subtype_bits.has_value())
202 const std::size_t subtype_bits_int =
203 numeric_cast_v<std::size_t>(*subtype_bits);
205 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
210 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
218 bitvector_expr, array_type.
element_type(), endianness_map, ns));
222 return array_exprt{std::move(operands), array_type};
228 const exprt &bitvector_expr,
233 const std::size_t num_elements =
234 numeric_cast_v<std::size_t>(vector_type.
size());
237 !subtype_bits.has_value() ||
238 *subtype_bits * num_elements ==
240 "subtype width times vector size should be total bitvector width");
243 operands.reserve(num_elements);
244 for(std::size_t i = 0; i < num_elements; ++i)
246 if(subtype_bits.has_value())
248 const std::size_t subtype_bits_int =
249 numeric_cast_v<std::size_t>(*subtype_bits);
251 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
256 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
264 bitvector_expr, vector_type.
element_type(), endianness_map, ns));
274 const exprt &bitvector_expr,
279 const std::size_t total_bits =
282 std::size_t subtype_bits;
283 if(subtype_bits_opt.has_value())
285 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
287 subtype_bits * 2 == total_bits,
288 "subtype width should be half of the total bitvector width");
291 subtype_bits = total_bits / 2;
293 const auto bounds_real =
map_bounds(endianness_map, 0, subtype_bits - 1);
294 const auto bounds_imag =
295 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
328 const exprt &bitvector_expr,
329 const typet &target_type,
337 target_type.
id() == ID_c_enum || target_type.
id() == ID_c_enum_tag ||
338 target_type.
id() == ID_string)
347 if(target_type.
id() == ID_struct)
352 else if(target_type.
id() == ID_struct_tag)
359 result.
type() = target_type;
360 return std::move(result);
362 else if(target_type.
id() == ID_union)
365 bitvector_expr,
to_union_type(target_type), endianness_map, ns);
367 else if(target_type.
id() == ID_union_tag)
374 result.
type() = target_type;
375 return std::move(result);
377 else if(target_type.
id() == ID_array)
380 bitvector_expr,
to_array_type(target_type), endianness_map, ns);
382 else if(target_type.
id() == ID_vector)
387 else if(target_type.
id() == ID_complex)
395 false,
"bv_to_expr does not yet support ", target_type.
id_string());
405 bool unpack_byte_array =
false);
415 std::size_t lower_bound,
416 std::size_t upper_bound,
421 if(src.
id() == ID_array)
425 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
426 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
436 bytes.reserve(upper_bound - lower_bound);
437 for(std::size_t i = lower_bound; i < upper_bound; ++i)
454 std::size_t el_bytes,
460 static std::size_t array_comprehension_index_counter = 0;
461 ++array_comprehension_index_counter;
463 "$array_comprehension_index_a_v" +
474 exprt body = sub_operands.front();
476 array_comprehension_index,
477 from_integer(el_bytes, array_comprehension_index.type())};
478 for(std::size_t i = 1; i < el_bytes; ++i)
486 const exprt array_vector_size = src.
type().
id() == ID_vector
491 std::move(array_comprehension_index),
520 const std::size_t el_bytes =
521 numeric_cast_v<std::size_t>((element_bits + 7) / 8);
523 if(!src_size.has_value() && !max_bytes.has_value())
526 el_bytes > 0 && element_bits % 8 == 0,
527 "unpacking of arrays with non-byte-aligned elements is not supported");
529 src, el_bytes, little_endian, ns);
538 if(element_bits > 0 && element_bits % 8 == 0)
540 if(!num_elements.has_value())
543 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
546 if(offset_bytes.has_value())
549 first_element = *offset_bytes / el_bytes;
551 byte_operands.resize(
552 numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
561 num_elements = *max_bytes;
565 for(
mp_integer i = first_element; i < *num_elements; ++i)
570 (src_simp.
id() == ID_array || src_simp.
id() == ID_vector) &&
573 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
574 element = src_simp.
operands()[index_int];
586 ? std::min(
mp_integer{el_bytes}, *max_bytes - byte_operands.size())
588 const std::size_t element_max_bytes_int =
589 element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
593 unpack_rec(element, little_endian, {}, element_max_bytes, ns,
true);
596 byte_operands.insert(
597 byte_operands.end(), sub_operands.begin(), sub_operands.end());
599 if(max_bytes && byte_operands.size() >= *max_bytes)
603 const std::size_t size = byte_operands.size();
605 std::move(byte_operands),
621 std::size_t total_bits,
632 unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns,
true);
636 std::make_move_iterator(sub.
operands().begin()),
637 std::make_move_iterator(sub.
operands().end()));
665 for(
auto it = components.begin(); it != components.end(); ++it)
667 const auto &comp = *it;
676 component_bits.has_value() ||
677 (std::next(it) == components.end() && !bit_fields.has_value()),
678 "members of non-constant width should come last in a struct");
681 if(src.
id() == ID_struct)
687 if(bit_fields.has_value())
690 std::move(bit_fields->first),
700 if(offset_bytes.has_value())
705 if(*offset_in_member < 0)
706 offset_in_member.reset();
709 if(max_bytes.has_value())
712 if(*max_bytes_left < 0)
719 (component_bits.has_value() && *component_bits % 8 != 0))
721 if(!bit_fields.has_value())
724 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
725 bit_fields->first.insert(
726 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
728 bit_fields->second += bits_int;
736 !bit_fields.has_value(),
737 "all preceding members should have been processed");
740 member, little_endian, offset_in_member, max_bytes_left, ns,
true);
742 byte_operands.insert(
744 std::make_move_iterator(sub.
operands().begin()),
745 std::make_move_iterator(sub.
operands().end()));
747 if(component_bits.has_value())
751 if(bit_fields.has_value())
753 std::move(bit_fields->first),
761 const std::size_t size = byte_operands.size();
797 byte_operands.insert(
799 std::make_move_iterator(sub_imag.
operands().begin()),
800 std::make_move_iterator(sub_imag.
operands().end()));
802 const std::size_t size = byte_operands.size();
824 bool unpack_byte_array)
826 if(src.
type().
id()==ID_array)
834 if(!unpack_byte_array && *element_bits == 8)
837 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.
size());
847 else if(src.
type().
id() == ID_vector)
855 if(!unpack_byte_array && *element_bits == 8)
860 numeric_cast_v<mp_integer>(vector_type.
size()),
867 else if(src.
type().
id() == ID_complex)
871 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
873 return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
875 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
881 if(widest_member.has_value())
884 src, widest_member->first.get_name(), widest_member->first.
type()};
886 member, little_endian, offset_bytes, widest_member->second, ns,
true);
889 else if(src.
type().
id() == ID_pointer)
899 else if(src.
id() == ID_string_constant)
909 else if(src.
id() == ID_constant && src.
type().
id() == ID_string)
919 else if(src.
type().
id()!=ID_empty)
924 DATA_INVARIANT(bits_opt.has_value(),
"basic type should have a fixed size");
930 if(max_bytes.has_value())
932 const auto max_bits = *max_bytes * 8;
935 last_bit = std::min(last_bit, max_bits);
939 bit_offset = std::max(
mp_integer{0}, last_bit - max_bits);
944 src,
bv_typet{numeric_cast_v<std::size_t>(total_bits)});
947 for(; bit_offset < last_bit; bit_offset += 8)
959 byte_operands.push_back(extractbits);
961 byte_operands.insert(byte_operands.begin(), extractbits);
964 const std::size_t size = byte_operands.size();
966 std::move(byte_operands),
987 const typet &subtype,
992 if(src.
type().
id() == ID_array)
997 if(num_elements.has_value())
1000 operands.reserve(*num_elements);
1001 for(std::size_t i = 0; i < *num_elements; ++i)
1008 tmp.
type() = subtype;
1009 tmp.
offset() = new_offset;
1015 if(src.
type().
id() == ID_array)
1028 static std::size_t array_comprehension_index_counter = 0;
1029 ++array_comprehension_index_counter;
1031 "$array_comprehension_index_a" +
1039 array_comprehension_index,
1040 from_integer(element_bits / 8, array_comprehension_index.type())},
1044 body.
type() = subtype;
1045 body.
offset() = std::move(new_offset);
1069 if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
1074 real.
type() = subtype;
1080 imag.
type() = subtype;
1139 src.
id() == ID_byte_extract_little_endian ||
1140 src.
id() == ID_byte_extract_big_endian);
1141 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
1145 if(upper_bound_opt.has_value())
1149 upper_bound_opt.value(),
1151 src.
offset(), upper_bound_opt.value().
type())),
1154 else if(src.
type().
id() == ID_empty)
1157 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.
offset());
1158 const auto upper_bound_int_opt =
1159 numeric_cast<mp_integer>(upper_bound_opt.value_or(
nil_exprt()));
1163 src.
op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
1168 if(src.
type().
id() == ID_array || src.
type().
id() == ID_vector)
1176 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1179 src, unpacked, subtype, *element_bits, ns);
1182 else if(src.
type().
id() == ID_complex)
1185 if(result.has_value())
1186 return std::move(*result);
1190 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
1198 for(
const auto &comp : components)
1204 !component_bits.has_value() || *component_bits == 0 ||
1205 *component_bits % 8 != 0)
1211 auto member_offset_opt =
1214 if(!member_offset_opt.has_value())
1223 member_offset_opt.value(), unpacked.
offset().
type()));
1226 tmp.
type()=comp.type();
1235 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
1241 if(widest_member.has_value())
1244 tmp.
type() = widest_member->first.type();
1247 widest_member->first.get_name(),
1253 const exprt &root=unpacked.
op();
1257 if(root.
type().
id() == ID_vector)
1265 subtype_bits.has_value() && *subtype_bits == 8,
1266 "offset bits are byte aligned");
1269 if(!size_bits.has_value())
1274 op0_bits.has_value(),
1275 "the extracted width or the source width must be known");
1276 size_bits = op0_bits;
1279 mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1282 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1284 op.reserve(width_bytes);
1286 for(std::size_t i=0; i<width_bytes; i++)
1289 std::size_t offset_int=
1290 little_endian?(width_bytes-i-1):i;
1297 offset_i.is_constant() &&
1298 (root.
id() == ID_array || root.
id() == ID_vector) &&
1300 index < root.
operands().size() && index >= 0)
1303 op.push_back(root.
operands()[numeric_cast_v<std::size_t>(index)]);
1319 std::move(op),
adjust_width(*subtype, width_bytes * 8));
1328 const exprt &value_as_byte_array,
1343 const typet &subtype,
1344 const exprt &value_as_byte_array,
1345 const exprt &non_const_update_bound,
1350 static std::size_t array_comprehension_index_counter = 0;
1351 ++array_comprehension_index_counter;
1353 "$array_comprehension_index_u_a_v" +
1359 array_comprehension_index, src.
offset().
type()),
1364 array_comprehension_index, non_const_update_bound.
type()),
1367 src.
offset(), non_const_update_bound.
type()),
1368 non_const_update_bound}};
1371 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1375 value_as_byte_array,
1378 src.
offset(), array_comprehension_index.
type())}},
1383 std::move(array_comprehension_body),
1399 const typet &subtype,
1407 for(std::size_t i = 0; i < value_as_byte_array.
operands().size(); ++i)
1417 if(e.id() == ID_index)
1420 if(index_expr.
array() == src.
op() && index_expr.
index() == where)
1425 if(non_const_update_bound.has_value())
1431 *non_const_update_bound},
1439 if(result.
id() != ID_with)
1440 result =
with_exprt{result, where, update_value};
1465 const typet &subtype,
1466 const exprt &subtype_size,
1467 const exprt &value_as_byte_array,
1468 const exprt &non_const_update_bound,
1469 const exprt &initial_bytes,
1470 const exprt &first_index,
1471 const exprt &first_update_value,
1474 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1475 ? ID_byte_extract_little_endian
1476 : ID_byte_extract_big_endian;
1480 static std::size_t array_comprehension_index_counter = 0;
1481 ++array_comprehension_index_counter;
1483 "$array_comprehension_index_u_a_v_u" +
1495 array_comprehension_index, first_index.
type()),
1504 array_comprehension_index, first_index.
type()),
1509 extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1518 non_const_update_bound, subtype_size.
type()),
1530 non_const_update_bound, initial_bytes.
type()),
1538 array_comprehension_index, last_index.type()),
1551 value_as_byte_array,
1553 last_index, subtype_size.
type()),
1559 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1563 array_comprehension_index, first_index.
type()),
1567 array_comprehension_index, last_index.type()),
1569 std::move(last_update_value),
1570 std::move(update_value)}}};
1574 std::move(array_comprehension_body),
1591 const typet &subtype,
1592 const exprt &value_as_byte_array,
1596 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1597 ? ID_byte_extract_little_endian
1598 : ID_byte_extract_big_endian;
1607 subtype_size_opt.value(), src.
offset().
type()),
1622 if(non_const_update_bound.has_value())
1625 *non_const_update_bound, subtype_size.
type());
1630 value_as_byte_array.
id() == ID_array,
1631 "value should be an array expression if the update bound is constant");
1649 value_as_byte_array,
1654 if(value_as_byte_array.
id() != ID_array)
1660 value_as_byte_array,
1661 *non_const_update_bound,
1673 std::size_t step_size = 1;
1680 std::size_t offset = 0;
1684 with_exprt result{src.
op(), first_index, first_update_value};
1687 for(; offset + step_size <= value_as_byte_array.
operands().size();
1688 offset += step_size, ++i)
1705 value_as_byte_array,
1706 std::move(offset_expr),
1714 if(offset < value_as_byte_array.
operands().size())
1716 const std::size_t tail_size =
1717 value_as_byte_array.
operands().size() - offset;
1729 value_as_byte_array,
1751 const typet &subtype,
1752 const exprt &value_as_byte_array,
1756 const bool is_array = src.
type().
id() == ID_array;
1768 !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1769 non_const_update_bound.has_value() || value_as_byte_array.
id() != ID_array)
1772 src, subtype, value_as_byte_array, non_const_update_bound, ns);
1775 std::size_t num_elements =
1781 elements.reserve(num_elements);
1785 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1789 for(; i < num_elements &&
1791 (offset_bytes + value_as_byte_array.operands().size()) * 8;
1794 mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1795 mp_integer update_elements = *subtype_bits / 8;
1796 exprt::operandst::const_iterator first =
1797 value_as_byte_array.operands().begin();
1798 exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1799 if(update_offset < 0)
1802 value_as_byte_array.operands().size() > -update_offset,
1803 "indices past the update should be handled above");
1804 first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1808 update_elements -= update_offset;
1810 update_elements > 0,
1811 "indices before the update should be handled above");
1814 if(std::distance(first, end) > update_elements)
1815 end = first + numeric_cast_v<std::ptrdiff_t>(update_elements);
1817 const std::size_t update_size = update_values.size();
1822 from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1824 std::move(update_values),
1830 for(; i < num_elements; ++i)
1831 elements.push_back(
index_exprt{src.op(), from_integer(i, c_index_type())});
1853 const exprt &value_as_byte_array,
1857 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1858 ? ID_byte_extract_little_endian
1859 : ID_byte_extract_big_endian;
1862 elements.reserve(struct_type.
components().size());
1865 for(
const auto &comp : struct_type.
components())
1877 auto offset_bytes = numeric_cast<mp_integer>(offset);
1884 offset_bytes.has_value() &&
1885 (*offset_bytes * 8 >= *element_width ||
1886 (value_as_byte_array.
id() == ID_array && *offset_bytes < 0 &&
1887 -*offset_bytes >= value_as_byte_array.
operands().size())))
1889 elements.push_back(std::move(member));
1893 else if(!offset_bytes.has_value())
1916 bu, value_as_byte_array, non_const_update_bound, ns),
1926 mp_integer update_elements = (*element_width + 7) / 8;
1927 std::size_t first = 0;
1928 if(*offset_bytes < 0)
1932 value_as_byte_array.
id() != ID_array ||
1933 value_as_byte_array.
operands().size() > -*offset_bytes,
1934 "members past the update should be handled above");
1935 first = numeric_cast_v<std::size_t>(-*offset_bytes);
1939 update_elements -= *offset_bytes;
1941 update_elements > 0,
1942 "members before the update should be handled above");
1948 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1949 if(value_as_byte_array.
id() == ID_array)
1950 end = std::min(end, value_as_byte_array.
operands().size());
1953 const std::size_t update_size = update_values.size();
1962 if(non_const_update_bound.has_value())
1970 *non_const_update_bound,
1982 remaining_update_bytes};
1984 member_update_bound = std::move(update_size_expr);
1989 const std::size_t shift =
1991 const std::size_t element_bits_int =
1992 numeric_cast_v<std::size_t>(*element_width);
1994 const bool little_endian = src.
id() == ID_byte_update_little_endian;
2000 bv_typet{shift + element_bits_int}};
2009 exprt updated_element =
2013 elements.push_back(updated_element);
2018 element_bits_int - 1 + (little_endian ? shift : 0),
2019 (little_endian ? shift : 0),
2042 const exprt &value_as_byte_array,
2049 widest_member.has_value(),
2050 "lower_byte_update of union of unknown size is not supported");
2054 src.
op(), widest_member->first.get_name(), widest_member->first.
type()});
2055 bu.
type() = widest_member->first.type();
2058 widest_member->first.get_name(),
2073 const exprt &value_as_byte_array,
2077 if(src.
type().
id() == ID_array || src.
type().
id() == ID_vector)
2080 if(src.
type().
id() == ID_vector)
2090 if(*element_width == 8)
2092 if(value_as_byte_array.
id() != ID_array)
2095 non_const_update_bound.has_value(),
2096 "constant update bound should yield an array expression");
2098 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2105 non_const_update_bound,
2110 src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2112 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
2117 value_as_byte_array,
2118 non_const_update_bound,
2123 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
2128 value_as_byte_array,
2129 non_const_update_bound,
2136 src.
type().
id() == ID_c_enum || src.
type().
id() == ID_c_enum_tag)
2141 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2142 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2145 if(value_as_byte_array.
id() == ID_array)
2146 update_bytes = value_as_byte_array.
operands();
2153 const std::size_t update_size_bits = update_bytes.size() * 8;
2154 const std::size_t bit_width = std::max(type_bits, update_size_bits);
2156 const bool is_little_endian = src.
id() == ID_byte_update_little_endian;
2160 if(bit_width > type_bits)
2167 if(!is_little_endian)
2173 if(non_const_update_bound.has_value())
2177 src.
id() == ID_byte_update_little_endian,
2183 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2189 *non_const_update_bound},
2197 if(is_little_endian)
2202 power(2, bit_width) -
power(2, bit_width - update_size_bits),
2210 offset_times_eight, ID_ge,
from_integer(0, offset_type)};
2212 if_exprt mask_shifted{offset_ge_zero,
2215 if(!is_little_endian)
2216 mask_shifted.true_case().
swap(mask_shifted.false_case());
2223 if(is_little_endian)
2224 std::reverse(value.operands().begin(), value.operands().end());
2226 exprt zero_extended;
2227 if(bit_width > update_size_bits)
2234 if(!is_little_endian)
2240 zero_extended = value;
2243 if_exprt value_shifted{offset_ge_zero,
2244 shl_exprt{zero_extended, offset_times_eight},
2245 lshr_exprt{zero_extended, offset_times_eight}};
2246 if(!is_little_endian)
2247 value_shifted.true_case().
swap(value_shifted.false_case());
2250 bitor_exprt bitor_expr{bitand_expr, value_shifted};
2252 if(bit_width > type_bits)
2255 bitor_expr.type(), src.
id() == ID_byte_update_little_endian, ns);
2256 const auto bounds =
map_bounds(endianness_map, 0, type_bits - 1);
2261 bitor_expr, bounds.ub, bounds.lb,
bv_typet{type_bits}},
2272 false,
"lower_byte_update does not yet support ", src.
type().
id_string());
2279 src.
id() == ID_byte_update_little_endian ||
2280 src.
id() == ID_byte_update_big_endian,
2281 "byte update expression should either be little or big endian");
2302 simplify(update_size_expr_opt.value(), ns);
2304 if(!update_size_expr_opt.value().is_constant())
2305 non_const_update_bound = *update_size_expr_opt;
2313 update_bits.has_value(),
"constant size-of should imply fixed bit width");
2314 const size_t update_bits_int = numeric_cast_v<size_t>(*update_bits);
2316 if(update_bits_int % 8 != 0)
2320 "non-byte aligned type expected to be a bitvector type");
2321 size_t n_extra_bits = 8 - update_bits_int % 8;
2324 src.
op().
type(), src.
id() == ID_byte_update_little_endian, ns);
2326 endianness_map, update_bits_int, update_bits_int + n_extra_bits - 1);
2328 src.
op(), bounds.ub, bounds.lb,
bv_typet{n_extra_bits}};
2332 update_value,
bv_typet{update_bits_int}),
2338 update_size_expr_opt =
2339 from_integer(update_bits_int / 8, update_size_expr_opt->type());
2343 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
2344 ? ID_byte_extract_little_endian
2345 : ID_byte_extract_big_endian;
2362 if(src.
id()==ID_byte_update_little_endian ||
2363 src.
id()==ID_byte_update_big_endian ||
2364 src.
id()==ID_byte_extract_little_endian ||
2365 src.
id()==ID_byte_extract_big_endian)
2385 if(src.
id()==ID_byte_update_little_endian ||
2386 src.
id()==ID_byte_update_big_endian)
2388 else if(src.
id()==ID_byte_extract_little_endian ||
2389 src.
id()==ID_byte_extract_big_endian)
API to expression classes for bitvectors.
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)
unsignedbv_typet size_type()
bitvector_typet c_index_type()
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Expression to define a mapping from an argument (index) to elements.
Array constructor from list of elements.
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
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 & offset() const
const exprt & value() 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.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
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 typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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.
Union constructor from single element.
optionalt< 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.
Operator to update elements in structs and arrays.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
nonstd::optional< T > optionalt
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, 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_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const optionalt< 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 array_exprt unpack_struct(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
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 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 exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const optionalt< 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 ...
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...
static optionalt< 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...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
static array_exprt unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
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 exprt lower_byte_update_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< 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 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 union_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.
bool has_byte_operator(const exprt &src)
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.
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const optionalt< 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...
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 unpack_array_vector(const exprt &src, const optionalt< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
static exprt unpack_rec(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const namespacet &ns)
Build the individual bytes to be used in an 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(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< 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 lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< 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_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...
static void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
#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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_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)