26 const exprt &bitvector_expr,
27 const typet &target_type,
40 std::size_t lower_bound,
41 std::size_t upper_bound)
44 result.
lb = lower_bound;
45 result.
ub = upper_bound;
53 if(result.
ub < result.
lb)
66 const exprt &bitvector_expr,
74 operands.reserve(components.size());
76 for(
const auto &comp : components)
79 std::size_t component_bits;
80 if(component_bits_opt.has_value())
81 component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
86 if(component_bits == 0)
103 if(component_bits_opt.has_value())
113 const exprt &bitvector_expr,
121 if(components.empty())
126 std::size_t component_bits;
127 if(widest_member.has_value())
128 component_bits = numeric_cast_v<std::size_t>(widest_member->second);
132 if(component_bits == 0)
139 const auto bounds =
map_bounds(endianness_map, 0, component_bits - 1);
141 const irep_idt &component_name = widest_member.has_value()
142 ? widest_member->first.get_name()
143 : components.front().get_name();
144 const typet &component_type = widest_member.has_value()
145 ? widest_member->first.type()
146 : components.front().type();
160 const exprt &bitvector_expr,
165 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
168 const std::size_t total_bits =
170 if(!num_elements.has_value())
172 if(!subtype_bits.has_value() || *subtype_bits == 0)
173 num_elements = total_bits;
175 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
178 !num_elements.has_value() || !subtype_bits.has_value() ||
179 *subtype_bits * *num_elements == total_bits,
180 "subtype width times array size should be total bitvector width");
183 operands.reserve(*num_elements);
184 for(std::size_t i = 0; i < *num_elements; ++i)
186 if(subtype_bits.has_value())
188 const std::size_t subtype_bits_int =
189 numeric_cast_v<std::size_t>(*subtype_bits);
191 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
195 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
207 return array_exprt{std::move(operands), array_type};
213 const exprt &bitvector_expr,
218 const std::size_t num_elements =
219 numeric_cast_v<std::size_t>(vector_type.
size());
222 !subtype_bits.has_value() ||
223 *subtype_bits * num_elements ==
225 "subtype width times vector size should be total bitvector width");
228 operands.reserve(num_elements);
229 for(std::size_t i = 0; i < num_elements; ++i)
231 if(subtype_bits.has_value())
233 const std::size_t subtype_bits_int =
234 numeric_cast_v<std::size_t>(*subtype_bits);
236 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
240 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
258 const exprt &bitvector_expr,
263 const std::size_t total_bits =
266 std::size_t subtype_bits;
267 if(subtype_bits_opt.has_value())
269 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
271 subtype_bits * 2 == total_bits,
272 "subtype width should be half of the total bitvector width");
275 subtype_bits = total_bits / 2;
277 const auto bounds_real =
map_bounds(endianness_map, 0, subtype_bits - 1);
278 const auto bounds_imag =
279 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
311 const exprt &bitvector_expr,
312 const typet &target_type,
320 target_type.
id() == ID_c_enum || target_type.
id() == ID_c_enum_tag ||
321 target_type.
id() == ID_string)
330 if(target_type.
id() == ID_struct)
335 else if(target_type.
id() == ID_struct_tag)
342 result.
type() = target_type;
343 return std::move(result);
345 else if(target_type.
id() == ID_union)
348 bitvector_expr,
to_union_type(target_type), endianness_map, ns);
350 else if(target_type.
id() == ID_union_tag)
357 result.
type() = target_type;
358 return std::move(result);
360 else if(target_type.
id() == ID_array)
363 bitvector_expr,
to_array_type(target_type), endianness_map, ns);
365 else if(target_type.
id() == ID_vector)
370 else if(target_type.
id() == ID_complex)
378 false,
"bv_to_expr does not yet support ", target_type.
id_string());
388 bool unpack_byte_array =
false);
398 std::size_t lower_bound,
399 std::size_t upper_bound,
404 if(src.
id() == ID_array)
408 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
409 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
413 bytes.reserve(upper_bound - lower_bound);
414 for(std::size_t i = lower_bound; i < upper_bound; ++i)
444 const std::size_t el_bytes =
445 numeric_cast_v<std::size_t>((element_bits + 7) / 8);
447 if(!src_size.has_value() && !max_bytes.has_value())
451 static std::size_t array_comprehension_index_counter = 0;
452 ++array_comprehension_index_counter;
454 "$array_comprehension_index_a_v" +
467 exprt body = sub_operands.front();
469 array_comprehension_index,
470 from_integer(el_bytes, array_comprehension_index.type())};
471 for(std::size_t i = 1; i < el_bytes; ++i)
479 const exprt array_vector_size = src.
type().
id() == ID_vector
484 std::move(array_comprehension_index),
498 if(element_bits > 0 && element_bits % 8 == 0)
500 if(!num_elements.has_value())
503 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
506 if(offset_bytes.has_value())
509 first_element = *offset_bytes / el_bytes;
511 byte_operands.resize(
512 numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
521 num_elements = *max_bytes;
525 for(
mp_integer i = first_element; i < *num_elements; ++i)
530 (src_simp.
id() == ID_array || src_simp.
id() == ID_vector) &&
533 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
534 element = src_simp.
operands()[index_int];
546 ? std::min(
mp_integer{el_bytes}, *max_bytes - byte_operands.size())
548 const std::size_t element_max_bytes_int =
549 element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
553 unpack_rec(element, little_endian, {}, element_max_bytes, ns,
true);
556 byte_operands.insert(
557 byte_operands.end(), sub_operands.begin(), sub_operands.end());
559 if(max_bytes && byte_operands.size() >= *max_bytes)
563 const std::size_t size = byte_operands.size();
565 std::move(byte_operands),
581 std::size_t total_bits,
592 unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns,
true);
596 std::make_move_iterator(sub.
operands().begin()),
597 std::make_move_iterator(sub.
operands().end()));
625 for(
auto it = components.begin(); it != components.end(); ++it)
627 const auto &comp = *it;
636 component_bits.has_value() ||
637 (std::next(it) == components.end() && !bit_fields.has_value()),
638 "members of non-constant width should come last in a struct");
641 if(src.
id() == ID_struct)
647 if(bit_fields.has_value())
650 std::move(bit_fields->first),
660 if(offset_bytes.has_value())
665 if(*offset_in_member < 0)
666 offset_in_member.reset();
669 if(max_bytes.has_value())
672 if(*max_bytes_left < 0)
679 (component_bits.has_value() && *component_bits % 8 != 0))
681 if(!bit_fields.has_value())
684 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
685 bit_fields->first.insert(
686 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
688 bit_fields->second += bits_int;
696 !bit_fields.has_value(),
697 "all preceding members should have been processed");
700 member, little_endian, offset_in_member, max_bytes_left, ns,
true);
702 byte_operands.insert(
704 std::make_move_iterator(sub.
operands().begin()),
705 std::make_move_iterator(sub.
operands().end()));
707 if(component_bits.has_value())
711 if(bit_fields.has_value())
713 std::move(bit_fields->first),
721 const std::size_t size = byte_operands.size();
757 byte_operands.insert(
759 std::make_move_iterator(sub_imag.
operands().begin()),
760 std::make_move_iterator(sub_imag.
operands().end()));
762 const std::size_t size = byte_operands.
size();
784 bool unpack_byte_array)
786 if(src.
type().
id()==ID_array)
794 if(!unpack_byte_array && *element_bits == 8)
797 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.
size());
807 else if(src.
type().
id() == ID_vector)
815 if(!unpack_byte_array && *element_bits == 8)
820 numeric_cast_v<mp_integer>(vector_type.
size()),
827 else if(src.
type().
id() == ID_complex)
831 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
833 return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
835 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
844 for(
const auto &comp : components)
848 if(!element_width.has_value() || *element_width <= max_width)
851 max_width = *element_width;
852 max_comp_type = comp.type();
853 max_comp_name = comp.get_name();
860 member, little_endian, offset_bytes, max_bytes, ns,
true);
863 else if(src.
type().
id() == ID_pointer)
873 else if(src.
id() == ID_string_constant)
883 else if(src.
id() == ID_constant && src.
type().
id() == ID_string)
893 else if(src.
type().
id()!=ID_empty)
898 DATA_INVARIANT(bits_opt.has_value(),
"basic type should have a fixed size");
904 if(max_bytes.has_value())
906 const auto max_bits = *max_bytes * 8;
909 last_bit = std::min(last_bit, max_bits);
913 bit_offset = std::max(
mp_integer{0}, last_bit - max_bits);
918 src,
bv_typet{numeric_cast_v<std::size_t>(total_bits)});
921 for(; bit_offset < last_bit; bit_offset += 8)
933 byte_operands.push_back(extractbits);
935 byte_operands.insert(byte_operands.begin(), extractbits);
938 const std::size_t size = byte_operands.size();
940 std::move(byte_operands),
965 if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
970 real.
type() = subtype;
976 imag.
type() = subtype;
1035 src.
id() == ID_byte_extract_little_endian ||
1036 src.
id() == ID_byte_extract_big_endian);
1037 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
1041 if(upper_bound_opt.has_value())
1045 upper_bound_opt.value(),
1047 src.
offset(), upper_bound_opt.value().
type())),
1050 else if(src.
type().
id() == ID_empty)
1053 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.
offset());
1054 const auto upper_bound_int_opt =
1055 numeric_cast<mp_integer>(upper_bound_opt.value_or(
nil_exprt()));
1059 src.
op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
1064 if(src.
type().
id()==ID_array)
1073 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1075 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
1077 if(num_elements.has_value())
1080 operands.reserve(*num_elements);
1081 for(std::size_t i = 0; i < *num_elements; ++i)
1088 tmp.
type() = subtype;
1089 tmp.
offset() = new_offset;
1100 static std::size_t array_comprehension_index_counter = 0;
1101 ++array_comprehension_index_counter;
1103 "$array_comprehension_index_a" +
1112 *element_bits / 8, array_comprehension_index.type())},
1116 body.
type() = subtype;
1117 body.
offset() = std::move(new_offset);
1125 else if(src.
type().
id() == ID_vector)
1134 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1136 const std::size_t num_elements =
1137 numeric_cast_v<std::size_t>(vector_type.
size());
1140 operands.reserve(num_elements);
1141 for(std::size_t i = 0; i < num_elements; ++i)
1148 tmp.
type() = subtype;
1157 else if(src.
type().
id() == ID_complex)
1160 if(result.has_value())
1161 return std::move(*result);
1165 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
1173 for(
const auto &comp : components)
1179 !component_bits.has_value() || *component_bits == 0 ||
1180 *component_bits % 8 != 0)
1186 auto member_offset_opt =
1189 if(!member_offset_opt.has_value())
1198 member_offset_opt.value(), unpacked.
offset().
type()));
1201 tmp.
type()=comp.type();
1210 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
1216 if(widest_member.has_value())
1219 tmp.
type() = widest_member->first.type();
1222 widest_member->first.get_name(),
1228 const exprt &root=unpacked.
op();
1232 if(root.
type().
id() == ID_vector)
1240 subtype_bits.has_value() && *subtype_bits == 8,
1241 "offset bits are byte aligned");
1244 if(!size_bits.has_value())
1249 op0_bits.has_value(),
1250 "the extracted width or the source width must be known");
1251 size_bits = op0_bits;
1254 mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1257 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1259 op.reserve(width_bytes);
1261 for(std::size_t i=0; i<width_bytes; i++)
1264 std::size_t offset_int=
1265 little_endian?(width_bytes-i-1):i;
1272 offset_i.is_constant() &&
1273 (root.
id() == ID_array || root.
id() == ID_vector) &&
1275 index < root.
operands().size() && index >= 0)
1278 op.push_back(root.
operands()[numeric_cast_v<std::size_t>(index)]);
1303 const exprt &value_as_byte_array,
1318 const typet &subtype,
1319 const exprt &value_as_byte_array,
1320 const exprt &non_const_update_bound,
1325 static std::size_t array_comprehension_index_counter = 0;
1326 ++array_comprehension_index_counter;
1328 "$array_comprehension_index_u_a_v" +
1334 array_comprehension_index, src.
offset().
type()),
1339 array_comprehension_index, non_const_update_bound.
type()),
1342 src.
offset(), non_const_update_bound.
type()),
1343 non_const_update_bound}};
1346 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1350 value_as_byte_array,
1353 src.
offset(), array_comprehension_index.
type())}},
1358 std::move(array_comprehension_body),
1374 const typet &subtype,
1382 for(std::size_t i = 0; i < value_as_byte_array.
operands().size(); ++i)
1392 if(e.id() == ID_index)
1395 if(index_expr.
array() == src.
op() && index_expr.
index() == where)
1400 if(non_const_update_bound.has_value())
1406 *non_const_update_bound},
1414 if(result.
id() != ID_with)
1415 result =
with_exprt{result, where, update_value};
1440 const typet &subtype,
1441 const exprt &subtype_size,
1442 const exprt &value_as_byte_array,
1443 const exprt &non_const_update_bound,
1444 const exprt &initial_bytes,
1445 const exprt &first_index,
1446 const exprt &first_update_value,
1449 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1450 ? ID_byte_extract_little_endian
1451 : ID_byte_extract_big_endian;
1455 static std::size_t array_comprehension_index_counter = 0;
1456 ++array_comprehension_index_counter;
1458 "$array_comprehension_index_u_a_v_u" +
1470 array_comprehension_index, first_index.
type()),
1479 array_comprehension_index, first_index.
type()),
1483 extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1492 non_const_update_bound, subtype_size.
type()),
1504 non_const_update_bound, initial_bytes.
type()),
1512 array_comprehension_index, last_index.type()),
1525 value_as_byte_array,
1527 last_index, subtype_size.
type()),
1533 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1537 array_comprehension_index, first_index.
type()),
1541 array_comprehension_index, last_index.type()),
1543 std::move(last_update_value),
1544 std::move(update_value)}}};
1548 std::move(array_comprehension_body),
1565 const typet &subtype,
1566 const exprt &value_as_byte_array,
1570 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1571 ? ID_byte_extract_little_endian
1572 : ID_byte_extract_big_endian;
1581 subtype_size_opt.value(), src.
offset().
type()),
1596 if(non_const_update_bound.has_value())
1599 *non_const_update_bound, subtype_size.
type());
1604 value_as_byte_array.
id() == ID_array,
1605 "value should be an array expression if the update bound is constant");
1623 value_as_byte_array,
1628 if(value_as_byte_array.
id() != ID_array)
1634 value_as_byte_array,
1635 *non_const_update_bound,
1647 std::size_t step_size = 1;
1654 std::size_t offset = 0;
1658 with_exprt result{src.
op(), first_index, first_update_value};
1661 for(; offset + step_size <= value_as_byte_array.
operands().size();
1662 offset += step_size, ++i)
1679 value_as_byte_array,
1680 std::move(offset_expr),
1688 if(offset < value_as_byte_array.
operands().size())
1690 const std::size_t tail_size =
1691 value_as_byte_array.
operands().size() - offset;
1703 value_as_byte_array,
1725 const typet &subtype,
1726 const exprt &value_as_byte_array,
1730 const bool is_array = src.
type().
id() == ID_array;
1742 !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1743 non_const_update_bound.has_value() || value_as_byte_array.
id() != ID_array)
1746 src, subtype, value_as_byte_array, non_const_update_bound, ns);
1749 std::size_t num_elements =
1755 elements.reserve(num_elements);
1759 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1763 for(; i < num_elements &&
1765 (offset_bytes + value_as_byte_array.operands().size()) * 8;
1768 mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1769 mp_integer update_elements = *subtype_bits / 8;
1770 exprt::operandst::const_iterator first =
1771 value_as_byte_array.operands().begin();
1772 exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1773 if(update_offset < 0)
1776 value_as_byte_array.operands().size() > -update_offset,
1777 "indices past the update should be handled above");
1778 first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1782 update_elements -= update_offset;
1784 update_elements > 0,
1785 "indices before the update should be handled above");
1788 if(std::distance(first, end) > update_elements)
1789 end = first + numeric_cast_v<std::ptrdiff_t>(update_elements);
1791 const std::size_t update_size = update_values.size();
1796 from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1798 std::move(update_values),
1804 for(; i < num_elements; ++i)
1805 elements.push_back(
index_exprt{src.op(), from_integer(i, index_type())});
1827 const exprt &value_as_byte_array,
1831 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1832 ? ID_byte_extract_little_endian
1833 : ID_byte_extract_big_endian;
1836 elements.reserve(struct_type.
components().size());
1839 for(
const auto &comp : struct_type.
components())
1851 auto offset_bytes = numeric_cast<mp_integer>(offset);
1858 offset_bytes.has_value() &&
1859 (*offset_bytes * 8 >= *element_width ||
1860 (value_as_byte_array.
id() == ID_array && *offset_bytes < 0 &&
1861 -*offset_bytes >= value_as_byte_array.
operands().size())))
1863 elements.push_back(std::move(member));
1867 else if(!offset_bytes.has_value())
1890 bu, value_as_byte_array, non_const_update_bound, ns),
1900 mp_integer update_elements = (*element_width + 7) / 8;
1901 std::size_t first = 0;
1902 if(*offset_bytes < 0)
1906 value_as_byte_array.
id() != ID_array ||
1907 value_as_byte_array.
operands().size() > -*offset_bytes,
1908 "members past the update should be handled above");
1909 first = numeric_cast_v<std::size_t>(-*offset_bytes);
1913 update_elements -= *offset_bytes;
1915 update_elements > 0,
1916 "members before the update should be handled above");
1922 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1923 if(value_as_byte_array.
id() == ID_array)
1924 end = std::min(end, value_as_byte_array.
operands().size());
1927 const std::size_t update_size = update_values.size();
1936 if(non_const_update_bound.has_value())
1944 *non_const_update_bound,
1956 remaining_update_bytes};
1958 member_update_bound = std::move(update_size_expr);
1963 const std::size_t shift =
1965 const std::size_t element_bits_int =
1966 numeric_cast_v<std::size_t>(*element_width);
1968 const bool little_endian = src.
id() == ID_byte_update_little_endian;
1974 bv_typet{shift + element_bits_int}};
1983 exprt updated_element =
1987 elements.push_back(updated_element);
1992 element_bits_int - 1 + (little_endian ? shift : 0),
1993 (little_endian ? shift : 0),
2016 const exprt &value_as_byte_array,
2023 widest_member.has_value(),
2024 "lower_byte_update of union of unknown size is not supported");
2028 src.
op(), widest_member->first.get_name(), widest_member->first.
type()});
2029 bu.
type() = widest_member->first.type();
2032 widest_member->first.get_name(),
2047 const exprt &value_as_byte_array,
2051 if(src.
type().
id() == ID_array || src.
type().
id() == ID_vector)
2054 if(src.
type().
id() == ID_vector)
2064 if(*element_width == 8)
2066 if(value_as_byte_array.
id() != ID_array)
2069 non_const_update_bound.has_value(),
2070 "constant update bound should yield an array expression");
2072 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2079 non_const_update_bound,
2084 src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2086 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
2091 value_as_byte_array,
2092 non_const_update_bound,
2097 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
2102 value_as_byte_array,
2103 non_const_update_bound,
2110 src.
type().
id() == ID_c_enum || src.
type().
id() == ID_c_enum_tag)
2115 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2116 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2119 if(value_as_byte_array.
id() == ID_array)
2120 update_bytes = value_as_byte_array.
operands();
2127 const std::size_t update_size_bits = update_bytes.size() * 8;
2128 const std::size_t bit_width = std::max(type_bits, update_size_bits);
2130 const bool is_little_endian = src.
id() == ID_byte_update_little_endian;
2134 if(bit_width > type_bits)
2141 if(!is_little_endian)
2147 if(non_const_update_bound.has_value())
2151 src.
id() == ID_byte_update_little_endian,
2157 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2163 *non_const_update_bound},
2171 if(is_little_endian)
2176 power(2, bit_width) -
power(2, bit_width - update_size_bits),
2184 offset_times_eight, ID_ge,
from_integer(0, offset_type)};
2186 if_exprt mask_shifted{offset_ge_zero,
2189 if(!is_little_endian)
2190 mask_shifted.true_case().
swap(mask_shifted.false_case());
2197 if(is_little_endian)
2198 std::reverse(value.operands().begin(), value.operands().end());
2200 exprt zero_extended;
2201 if(bit_width > update_size_bits)
2208 if(!is_little_endian)
2214 zero_extended = value;
2217 if_exprt value_shifted{offset_ge_zero,
2218 shl_exprt{zero_extended, offset_times_eight},
2219 lshr_exprt{zero_extended, offset_times_eight}};
2220 if(!is_little_endian)
2221 value_shifted.true_case().
swap(value_shifted.false_case());
2224 bitor_exprt bitor_expr{bitand_expr, value_shifted};
2226 if(!is_little_endian && bit_width > type_bits)
2232 bit_width - type_bits,
2237 else if(bit_width > type_bits)
2252 false,
"lower_byte_update does not yet support ", src.
type().
id_string());
2259 src.
id() == ID_byte_update_little_endian ||
2260 src.
id() == ID_byte_update_big_endian,
2261 "byte update expression should either be little or big endian");
2280 simplify(update_size_expr_opt.value(), ns);
2282 if(!update_size_expr_opt.value().is_constant())
2283 non_const_update_bound = *update_size_expr_opt;
2285 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
2286 ? ID_byte_extract_little_endian
2287 : ID_byte_extract_big_endian;
2304 if(src.
id()==ID_byte_update_little_endian ||
2305 src.
id()==ID_byte_update_big_endian ||
2306 src.
id()==ID_byte_extract_little_endian ||
2307 src.
id()==ID_byte_extract_big_endian)
2327 if(src.
id()==ID_byte_update_little_endian ||
2328 src.
id()==ID_byte_update_big_endian)
2330 else if(src.
id()==ID_byte_extract_little_endian ||
2331 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.
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)
bitvector_typet index_type()
unsignedbv_typet size_type()
Expression to define a mapping from an argument (index) to elements.
Array constructor from list of elements.
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
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
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
std::size_t size() const
Amount of nodes this expression tree contains.
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.
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.
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)
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
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.
Vector constructor from list of elements.
const constant_exprt & size() const
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
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
optionalt< 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)
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...
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 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 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 bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_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)