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,
120 if(components.empty())
125 std::size_t component_bits;
126 if(widest_member.has_value())
127 component_bits = numeric_cast_v<std::size_t>(widest_member->second);
131 if(component_bits == 0)
138 const auto bounds =
map_bounds(endianness_map, 0, component_bits - 1);
140 const irep_idt &component_name = widest_member.has_value()
141 ? widest_member->first.get_name()
142 : components.front().get_name();
143 const typet &component_type = widest_member.has_value()
144 ? widest_member->first.type()
145 : components.front().type();
159 const exprt &bitvector_expr,
164 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
167 const std::size_t total_bits =
169 if(!num_elements.has_value())
171 if(!subtype_bits.has_value() || *subtype_bits == 0)
172 num_elements = total_bits;
174 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
177 !num_elements.has_value() || !subtype_bits.has_value() ||
178 *subtype_bits * *num_elements == total_bits,
179 "subtype width times array size should be total bitvector width");
182 operands.reserve(*num_elements);
183 for(std::size_t i = 0; i < *num_elements; ++i)
185 if(subtype_bits.has_value())
187 const std::size_t subtype_bits_int =
188 numeric_cast_v<std::size_t>(*subtype_bits);
190 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
194 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
206 return array_exprt{std::move(operands), array_type};
212 const exprt &bitvector_expr,
217 const std::size_t num_elements =
218 numeric_cast_v<std::size_t>(vector_type.
size());
221 !subtype_bits.has_value() ||
222 *subtype_bits * num_elements ==
224 "subtype width times vector size should be total bitvector width");
227 operands.reserve(num_elements);
228 for(std::size_t i = 0; i < num_elements; ++i)
230 if(subtype_bits.has_value())
232 const std::size_t subtype_bits_int =
233 numeric_cast_v<std::size_t>(*subtype_bits);
235 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
239 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
257 const exprt &bitvector_expr,
262 const std::size_t total_bits =
265 std::size_t subtype_bits;
266 if(subtype_bits_opt.has_value())
268 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
270 subtype_bits * 2 == total_bits,
271 "subtype width should be half of the total bitvector width");
274 subtype_bits = total_bits / 2;
276 const auto bounds_real =
map_bounds(endianness_map, 0, subtype_bits - 1);
277 const auto bounds_imag =
278 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
310 const exprt &bitvector_expr,
311 const typet &target_type,
319 target_type.
id() == ID_c_enum || target_type.
id() == ID_c_enum_tag ||
320 target_type.
id() == ID_string)
329 if(target_type.
id() == ID_struct)
334 else if(target_type.
id() == ID_struct_tag)
341 result.
type() = target_type;
342 return std::move(result);
344 else if(target_type.
id() == ID_union)
347 bitvector_expr,
to_union_type(target_type), endianness_map, ns);
349 else if(target_type.
id() == ID_union_tag)
356 result.
type() = target_type;
357 return std::move(result);
359 else if(target_type.
id() == ID_array)
362 bitvector_expr,
to_array_type(target_type), endianness_map, ns);
364 else if(target_type.
id() == ID_vector)
369 else if(target_type.
id() == ID_complex)
377 false,
"bv_to_expr does not yet support ", target_type.
id_string());
387 bool unpack_byte_array =
false);
397 std::size_t lower_bound,
398 std::size_t upper_bound,
403 if(src.
id() == ID_array)
407 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
408 src.
operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
412 bytes.reserve(upper_bound - lower_bound);
413 for(std::size_t i = lower_bound; i < upper_bound; ++i)
443 const std::size_t el_bytes =
444 numeric_cast_v<std::size_t>((element_bits + 7) / 8);
446 if(!src_size.has_value() && !max_bytes.has_value())
450 static std::size_t array_comprehension_index_counter = 0;
451 ++array_comprehension_index_counter;
453 "$array_comprehension_index_a_v" +
466 exprt body = sub_operands.front();
468 array_comprehension_index,
469 from_integer(el_bytes, array_comprehension_index.type())};
470 for(std::size_t i = 1; i < el_bytes; ++i)
478 const exprt array_vector_size = src.
type().
id() == ID_vector
483 std::move(array_comprehension_index),
497 if(element_bits > 0 && element_bits % 8 == 0)
499 if(!num_elements.has_value())
502 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
505 if(offset_bytes.has_value())
508 first_element = *offset_bytes / el_bytes;
510 byte_operands.resize(
511 numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
520 num_elements = *max_bytes;
524 for(
mp_integer i = first_element; i < *num_elements; ++i)
529 (src_simp.
id() == ID_array || src_simp.
id() == ID_vector) &&
532 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
533 element = src_simp.
operands()[index_int];
545 ? std::min(
mp_integer{el_bytes}, *max_bytes - byte_operands.size())
547 const std::size_t element_max_bytes_int =
548 element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
552 unpack_rec(element, little_endian, {}, element_max_bytes, ns,
true);
555 byte_operands.insert(
556 byte_operands.end(), sub_operands.begin(), sub_operands.end());
558 if(max_bytes && byte_operands.size() >= *max_bytes)
562 const std::size_t size = byte_operands.size();
564 std::move(byte_operands),
580 std::size_t total_bits,
591 unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns,
true);
595 std::make_move_iterator(sub.
operands().begin()),
596 std::make_move_iterator(sub.
operands().end()));
624 for(
auto it = components.begin(); it != components.end(); ++it)
626 const auto &comp = *it;
635 component_bits.has_value() ||
636 (std::next(it) == components.end() && !bit_fields.has_value()),
637 "members of non-constant width should come last in a struct");
640 if(src.
id() == ID_struct)
646 if(bit_fields.has_value())
649 std::move(bit_fields->first),
659 if(offset_bytes.has_value())
664 if(*offset_in_member < 0)
665 offset_in_member.reset();
668 if(max_bytes.has_value())
671 if(*max_bytes_left < 0)
678 (component_bits.has_value() && *component_bits % 8 != 0))
680 if(!bit_fields.has_value())
683 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
684 bit_fields->first.insert(
685 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
687 bit_fields->second += bits_int;
695 !bit_fields.has_value(),
696 "all preceding members should have been processed");
699 member, little_endian, offset_in_member, max_bytes_left, ns,
true);
701 byte_operands.insert(
703 std::make_move_iterator(sub.
operands().begin()),
704 std::make_move_iterator(sub.
operands().end()));
706 if(component_bits.has_value())
710 if(bit_fields.has_value())
712 std::move(bit_fields->first),
720 const std::size_t size = byte_operands.size();
756 byte_operands.insert(
758 std::make_move_iterator(sub_imag.
operands().begin()),
759 std::make_move_iterator(sub_imag.
operands().end()));
761 const std::size_t size = byte_operands.size();
783 bool unpack_byte_array)
785 if(src.
type().
id()==ID_array)
793 if(!unpack_byte_array && *element_bits == 8)
796 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.
size());
806 else if(src.
type().
id() == ID_vector)
814 if(!unpack_byte_array && *element_bits == 8)
819 numeric_cast_v<mp_integer>(vector_type.
size()),
826 else if(src.
type().
id() == ID_complex)
830 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
832 return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
834 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
843 for(
const auto &comp : components)
847 if(!element_width.has_value() || *element_width <= max_width)
850 max_width = *element_width;
851 max_comp_type = comp.type();
852 max_comp_name = comp.get_name();
859 member, little_endian, offset_bytes, max_bytes, ns,
true);
862 else if(src.
type().
id() == ID_pointer)
872 else if(src.
id() == ID_string_constant)
882 else if(src.
id() == ID_constant && src.
type().
id() == ID_string)
892 else if(src.
type().
id()!=ID_empty)
897 DATA_INVARIANT(bits_opt.has_value(),
"basic type should have a fixed size");
903 if(max_bytes.has_value())
905 const auto max_bits = *max_bytes * 8;
908 last_bit = std::min(last_bit, max_bits);
912 bit_offset = std::max(
mp_integer{0}, last_bit - max_bits);
917 src,
bv_typet{numeric_cast_v<std::size_t>(total_bits)});
920 for(; bit_offset < last_bit; bit_offset += 8)
932 byte_operands.push_back(extractbits);
934 byte_operands.insert(byte_operands.begin(), extractbits);
937 const std::size_t size = byte_operands.size();
939 std::move(byte_operands),
964 if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
969 real.
type() = subtype;
975 imag.
type() = subtype;
1034 src.
id() == ID_byte_extract_little_endian ||
1035 src.
id() == ID_byte_extract_big_endian);
1036 const bool little_endian = src.
id() == ID_byte_extract_little_endian;
1040 if(upper_bound_opt.has_value())
1044 upper_bound_opt.value(),
1046 src.
offset(), upper_bound_opt.value().
type())),
1049 else if(src.
type().
id() == ID_empty)
1052 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.
offset());
1053 const auto upper_bound_int_opt =
1054 numeric_cast<mp_integer>(upper_bound_opt.value_or(
nil_exprt()));
1058 src.
op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
1063 if(src.
type().
id()==ID_array)
1072 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1074 auto num_elements = numeric_cast<std::size_t>(array_type.
size());
1076 if(num_elements.has_value())
1079 operands.reserve(*num_elements);
1080 for(std::size_t i = 0; i < *num_elements; ++i)
1087 tmp.
type() = subtype;
1088 tmp.
offset() = new_offset;
1099 static std::size_t array_comprehension_index_counter = 0;
1100 ++array_comprehension_index_counter;
1102 "$array_comprehension_index_a" +
1111 *element_bits / 8, array_comprehension_index.type())},
1115 body.
type() = subtype;
1116 body.
offset() = std::move(new_offset);
1124 else if(src.
type().
id() == ID_vector)
1133 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1135 const std::size_t num_elements =
1136 numeric_cast_v<std::size_t>(vector_type.
size());
1139 operands.reserve(num_elements);
1140 for(std::size_t i = 0; i < num_elements; ++i)
1147 tmp.
type() = subtype;
1156 else if(src.
type().
id() == ID_complex)
1159 if(result.has_value())
1160 return std::move(*result);
1164 else if(src.
type().
id() == ID_struct || src.
type().
id() == ID_struct_tag)
1172 for(
const auto &comp : components)
1178 !component_bits.has_value() || *component_bits == 0 ||
1179 *component_bits % 8 != 0)
1185 auto member_offset_opt =
1188 if(!member_offset_opt.has_value())
1197 member_offset_opt.value(), unpacked.
offset().
type()));
1200 tmp.
type()=comp.type();
1209 else if(src.
type().
id() == ID_union || src.
type().
id() == ID_union_tag)
1215 if(widest_member.has_value())
1218 tmp.
type() = widest_member->first.type();
1221 widest_member->first.get_name(),
1227 const exprt &root=unpacked.
op();
1231 if(root.
type().
id() == ID_vector)
1239 subtype_bits.has_value() && *subtype_bits == 8,
1240 "offset bits are byte aligned");
1243 if(!size_bits.has_value())
1248 op0_bits.has_value(),
1249 "the extracted width or the source width must be known");
1250 size_bits = op0_bits;
1253 mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1256 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1258 op.reserve(width_bytes);
1260 for(std::size_t i=0; i<width_bytes; i++)
1263 std::size_t offset_int=
1264 little_endian?(width_bytes-i-1):i;
1271 offset_i.is_constant() &&
1272 (root.
id() == ID_array || root.
id() == ID_vector) &&
1274 index < root.
operands().size() && index >= 0)
1277 op.push_back(root.
operands()[numeric_cast_v<std::size_t>(index)]);
1302 const exprt &value_as_byte_array,
1317 const typet &subtype,
1318 const exprt &value_as_byte_array,
1319 const exprt &non_const_update_bound,
1324 static std::size_t array_comprehension_index_counter = 0;
1325 ++array_comprehension_index_counter;
1327 "$array_comprehension_index_u_a_v" +
1333 array_comprehension_index, src.
offset().
type()),
1338 array_comprehension_index, non_const_update_bound.
type()),
1341 src.
offset(), non_const_update_bound.
type()),
1342 non_const_update_bound}};
1345 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1349 value_as_byte_array,
1352 src.
offset(), array_comprehension_index.
type())}},
1357 std::move(array_comprehension_body),
1373 const typet &subtype,
1381 for(std::size_t i = 0; i < value_as_byte_array.
operands().size(); ++i)
1391 if(e.id() == ID_index)
1394 if(index_expr.
array() == src.
op() && index_expr.
index() == where)
1399 if(non_const_update_bound.has_value())
1405 *non_const_update_bound},
1413 if(result.
id() != ID_with)
1414 result =
with_exprt{result, where, update_value};
1439 const typet &subtype,
1440 const exprt &subtype_size,
1441 const exprt &value_as_byte_array,
1442 const exprt &non_const_update_bound,
1443 const exprt &initial_bytes,
1444 const exprt &first_index,
1445 const exprt &first_update_value,
1448 const irep_idt extract_opcode = src.
id() == ID_byte_update_little_endian
1449 ? ID_byte_extract_little_endian
1450 : ID_byte_extract_big_endian;
1454 static std::size_t array_comprehension_index_counter = 0;
1455 ++array_comprehension_index_counter;
1457 "$array_comprehension_index_u_a_v_u" +
1469 array_comprehension_index, first_index.
type()),
1478 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.
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)
bitvector_typet index_type()
unsignedbv_typet size_type()
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Expression to define a mapping from an argument (index) to elements.
Array constructor from list of elements.
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.
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.
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
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)