CBMC
Loading...
Searching...
No Matches
lower_byte_operators.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "arith_tools.h"
10#include "bitvector_expr.h"
11#include "byte_operators.h"
12#include "c_types.h"
13#include "endianness_map.h"
14#include "expr_util.h"
15#include "namespace.h"
16#include "narrow.h"
17#include "pointer_offset_size.h"
18#include "simplify_expr.h"
19#include "string_constant.h"
20
21#include <algorithm>
22
23static exprt bv_to_expr(
24 const exprt &bitvector_expr,
25 const typet &target_type,
26 const endianness_mapt &endianness_map,
27 const namespacet &ns);
28
29struct boundst
30{
31 std::size_t lb;
32 std::size_t ub;
33};
34
37 const endianness_mapt &endianness_map,
38 std::size_t lower_bound,
39 std::size_t upper_bound)
40{
41 boundst result;
42 result.lb = lower_bound;
43 result.ub = upper_bound;
44
45 if(result.ub < endianness_map.number_of_bits())
46 {
47 result.lb = endianness_map.map_bit(result.lb);
48 result.ub = endianness_map.map_bit(result.ub);
49
50 // big-endian bounds need swapping
51 if(result.ub < result.lb)
52 std::swap(result.lb, result.ub);
53 }
54
55 return result;
56}
57
60{
61 if(src.id() == ID_unsignedbv)
63 else if(src.id() == ID_signedbv)
65 else if(src.id() == ID_bv)
66 return bv_typet(new_width);
67 else if(src.id() == ID_c_enum) // we use the underlying type
68 return adjust_width(to_c_enum_type(src).underlying_type(), new_width);
69 else if(src.id() == ID_c_bit_field)
70 return c_bit_field_typet(
71 to_c_bit_field_type(src).underlying_type(), new_width);
72 else
73 PRECONDITION(false);
74}
75
79 const exprt &bitvector_expr,
81 const endianness_mapt &endianness_map,
82 const namespacet &ns)
83{
84 const struct_typet::componentst &components = struct_type.components();
85
86 exprt::operandst operands;
87 operands.reserve(components.size());
88 std::size_t member_offset_bits = 0;
89 for(const auto &comp : components)
90 {
91 const auto component_bits_opt = pointer_offset_bits(comp.type(), ns);
92 std::size_t component_bits;
93 if(component_bits_opt.has_value())
95 else
96 component_bits = to_bitvector_type(bitvector_expr.type()).get_width() -
98
99 if(component_bits == 0)
100 {
101 operands.push_back(
102 bv_to_expr(bitvector_expr, comp.type(), endianness_map, ns));
103 continue;
104 }
105
106 const auto bounds = map_bounds(
107 endianness_map,
111 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
112 operands.push_back(bv_to_expr(
113 extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)},
114 comp.type(),
115 endianness_map,
116 ns));
117
118 if(component_bits_opt.has_value())
120 }
121
122 return struct_exprt{std::move(operands), struct_type};
123}
124
128 const exprt &bitvector_expr,
129 const union_typet &union_type,
130 const endianness_mapt &endianness_map,
131 const namespacet &ns)
132{
133 const union_typet::componentst &components = union_type.components();
134
135 if(components.empty())
137
138 const auto widest_member = union_type.find_widest_union_component(ns);
139
140 std::size_t component_bits;
141 if(widest_member.has_value())
143 else
144 component_bits = to_bitvector_type(bitvector_expr.type()).get_width();
145
146 if(component_bits == 0)
147 {
148 return union_exprt{
149 components.front().get_name(),
150 bv_to_expr(bitvector_expr, components.front().type(), endianness_map, ns),
151 union_type};
152 }
153
154 const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
156 const irep_idt &component_name = widest_member.has_value()
157 ? widest_member->first.get_name()
158 : components.front().get_name();
159 const typet &component_type = widest_member.has_value()
160 ? widest_member->first.type()
161 : components.front().type();
162 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
163 return union_exprt{
164 component_name,
166 extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)},
167 component_type,
168 endianness_map,
169 ns),
170 union_type};
171}
172
176 const exprt &bitvector_expr,
177 const array_typet &array_type,
178 const endianness_mapt &endianness_map,
179 const namespacet &ns)
180{
182 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
183
184 const std::size_t total_bits =
185 to_bitvector_type(bitvector_expr.type()).get_width();
186 if(!num_elements.has_value())
187 {
188 if(!subtype_bits.has_value() || *subtype_bits == 0)
190 else
192 }
194 !num_elements.has_value() || !subtype_bits.has_value() ||
196 "subtype width times array size should be total bitvector width");
197
198 exprt::operandst operands;
199 operands.reserve(*num_elements);
200 for(std::size_t i = 0; i < *num_elements; ++i)
201 {
202 if(subtype_bits.has_value())
203 {
204 const std::size_t subtype_bits_int =
206 const auto bounds = map_bounds(
207 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
208 bitvector_typet type =
210 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
211 operands.push_back(bv_to_expr(
212 extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)},
213 array_type.element_type(),
214 endianness_map,
215 ns));
216 }
217 else
218 {
219 operands.push_back(bv_to_expr(
220 bitvector_expr, array_type.element_type(), endianness_map, ns));
221 }
222 }
223
224 return array_exprt{std::move(operands), array_type};
225}
226
230 const exprt &bitvector_expr,
232 const endianness_mapt &endianness_map,
233 const namespacet &ns)
234{
235 const std::size_t num_elements =
237 auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
239 !subtype_bits.has_value() ||
241 to_bitvector_type(bitvector_expr.type()).get_width(),
242 "subtype width times vector size should be total bitvector width");
243
244 exprt::operandst operands;
245 operands.reserve(num_elements);
246 for(std::size_t i = 0; i < num_elements; ++i)
247 {
248 if(subtype_bits.has_value())
249 {
250 const std::size_t subtype_bits_int =
252 const auto bounds = map_bounds(
253 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
254 bitvector_typet type =
256 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
257 operands.push_back(bv_to_expr(
258 extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)},
259 vector_type.element_type(),
260 endianness_map,
261 ns));
262 }
263 else
264 {
265 operands.push_back(bv_to_expr(
266 bitvector_expr, vector_type.element_type(), endianness_map, ns));
267 }
268 }
269
270 return vector_exprt{std::move(operands), vector_type};
271}
272
276 const exprt &bitvector_expr,
278 const endianness_mapt &endianness_map,
279 const namespacet &ns)
280{
281 const std::size_t total_bits =
282 to_bitvector_type(bitvector_expr.type()).get_width();
283 const auto subtype_bits_opt = pointer_offset_bits(complex_type.subtype(), ns);
284 std::size_t subtype_bits;
285 if(subtype_bits_opt.has_value())
286 {
290 "subtype width should be half of the total bitvector width");
291 }
292 else
294
295 const auto bounds_real = map_bounds(endianness_map, 0, subtype_bits - 1);
296 const auto bounds_imag =
297 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
298
299 const bitvector_typet type =
301
302 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
303 return complex_exprt{
306 complex_type.subtype(),
307 endianness_map,
308 ns),
311 complex_type.subtype(),
312 endianness_map,
313 ns),
315}
316
331 const exprt &bitvector_expr,
332 const typet &target_type,
333 const endianness_mapt &endianness_map,
334 const namespacet &ns)
335{
337
338 if(target_type.id() == ID_floatbv)
339 {
340 std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width();
341 exprt bv_expr =
343 return simplify_expr(
344 typecast_exprt::conditional_cast(bv_expr, target_type), ns);
345 }
346 else if(
347 can_cast_type<bitvector_typet>(target_type) ||
348 target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
349 target_type.id() == ID_string ||
350 (target_type.id() == ID_bool &&
351 to_bitvector_type(bitvector_expr.type()).get_width() == 1))
352 {
353 return simplify_expr(
355 }
356 else if(target_type.id() == ID_struct)
357 {
358 return bv_to_struct_expr(
359 bitvector_expr, to_struct_type(target_type), endianness_map, ns);
360 }
361 else if(target_type.id() == ID_struct_tag)
362 {
365 ns.follow_tag(to_struct_tag_type(target_type)),
366 endianness_map,
367 ns);
368 result.type() = target_type;
369 return std::move(result);
370 }
371 else if(target_type.id() == ID_union)
372 {
373 return bv_to_union_expr(
374 bitvector_expr, to_union_type(target_type), endianness_map, ns);
375 }
376 else if(target_type.id() == ID_union_tag)
377 {
378 exprt result = bv_to_union_expr(
380 ns.follow_tag(to_union_tag_type(target_type)),
381 endianness_map,
382 ns);
383 result.type() = target_type;
384 return result;
385 }
386 else if(target_type.id() == ID_array)
387 {
388 return bv_to_array_expr(
389 bitvector_expr, to_array_type(target_type), endianness_map, ns);
390 }
391 else if(target_type.id() == ID_vector)
392 {
393 return bv_to_vector_expr(
394 bitvector_expr, to_vector_type(target_type), endianness_map, ns);
395 }
396 else if(target_type.id() == ID_complex)
397 {
398 return bv_to_complex_expr(
399 bitvector_expr, to_complex_type(target_type), endianness_map, ns);
400 }
401 else
402 {
404 false, "bv_to_expr does not yet support ", target_type.id_string());
405 }
406}
407
408static exprt unpack_rec(
409 const exprt &src,
410 bool little_endian,
411 const std::optional<mp_integer> &offset_bytes,
412 const std::optional<mp_integer> &max_bytes,
413 const std::size_t bits_per_byte,
414 const namespacet &ns,
415 bool unpack_byte_array = false);
416
425 const exprt &src,
426 std::size_t lower_bound,
427 std::size_t upper_bound,
428 const std::size_t bits_per_byte,
429 const namespacet &ns)
430{
431 PRECONDITION(lower_bound <= upper_bound);
432
433 if(src.id() == ID_array)
434 {
435 PRECONDITION(upper_bound <= src.operands().size());
436 return exprt::operandst{
437 src.operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
438 src.operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
439 }
440
441 const typet &element_type = src.type().id() == ID_array
442 ? to_array_type(src.type()).element_type()
443 : to_vector_type(src.type()).element_type();
444 const typet index_type = src.type().id() == ID_array
445 ? to_array_type(src.type()).index_type()
446 : to_vector_type(src.type()).index_type();
448 can_cast_type<bitvector_typet>(element_type) &&
449 to_bitvector_type(element_type).get_width() == bits_per_byte);
450 exprt::operandst bytes;
451 bytes.reserve(upper_bound - lower_bound);
452 for(std::size_t i = lower_bound; i < upper_bound; ++i)
453 {
454 const index_exprt idx{src, from_integer(i, index_type)};
455 bytes.push_back(simplify_expr(idx, ns));
456 }
457 return bytes;
458}
459
469 const exprt &src,
470 std::size_t el_bytes,
471 bool little_endian,
472 const std::size_t bits_per_byte,
473 const namespacet &ns)
474{
475 const typet index_type = src.type().id() == ID_array
476 ? to_array_type(src.type()).index_type()
477 : to_vector_type(src.type()).index_type();
478
479 // TODO we either need a symbol table here or make array comprehensions
480 // introduce a scope
481 static std::size_t array_comprehension_index_counter = 0;
484 "$array_comprehension_index_a_v" +
485 std::to_string(array_comprehension_index_counter),
486 index_type};
487
488 index_exprt element{
489 src,
491
492 exprt sub =
493 unpack_rec(element, little_endian, {}, {}, bits_per_byte, ns, false);
496
497 exprt body = sub_operands.front();
498 const mod_exprt offset{
501 for(std::size_t i = 1; i < el_bytes; ++i)
502 {
503 body = if_exprt{
505 sub_operands[i],
506 body};
507 }
508
509 const exprt array_vector_size = src.type().id() == ID_vector
510 ? to_vector_type(src.type()).size()
511 : to_array_type(src.type()).size();
512
514 std::move(array_comprehension_index),
515 std::move(body),
520}
521
538 const exprt &src,
539 const std::optional<mp_integer> &src_size,
541 bool little_endian,
542 const std::optional<mp_integer> &offset_bytes,
543 const std::optional<mp_integer> &max_bytes,
544 const std::size_t bits_per_byte,
545 const namespacet &ns)
546{
547 const std::size_t el_bytes = numeric_cast_v<std::size_t>(
549
550 if(!src_size.has_value() && !max_bytes.has_value())
551 {
553 el_bytes > 0 && element_bits % bits_per_byte == 0,
554 "unpacking of arrays with non-byte-aligned elements is not supported");
556 src, el_bytes, little_endian, bits_per_byte, ns);
557 }
558
561
562 // refine the number of elements to extract in case the element width is known
563 // and a multiple of bytes; otherwise we will expand the entire array/vector
564 std::optional<mp_integer> num_elements = src_size;
565 if(element_bits > 0 && element_bits % bits_per_byte == 0)
566 {
567 if(!num_elements.has_value())
568 {
569 // turn bytes into elements, rounding up
571 }
572
573 if(offset_bytes.has_value())
574 {
575 // compute offset as number of elements
577 // insert offset_bytes-many nil bytes into the output array
578 byte_operands.resize(
582 bv_typet{bits_per_byte}.all_zeros_expr());
583 }
584 }
585
586 // the maximum number of bytes is an upper bound in case the size of the
587 // array/vector is unknown; if element_bits was usable above this will
588 // have been turned into a number of elements already
589 if(!num_elements)
591
592 const exprt src_simp = simplify_expr(src, ns);
593 const typet index_type = src_simp.type().id() == ID_array
594 ? to_array_type(src_simp.type()).index_type()
595 : to_vector_type(src_simp.type()).index_type();
596
597 for(mp_integer i = first_element; i < *num_elements; ++i)
598 {
599 exprt element;
600
601 if(
602 (src_simp.id() == ID_array || src_simp.id() == ID_vector) &&
603 i < src_simp.operands().size())
604 {
605 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
606 element = src_simp.operands()[index_int];
607 }
608 else
609 {
610 element = index_exprt(src_simp, from_integer(i, index_type));
611 }
612
613 // recursively unpack each element so that we eventually just have an array
614 // of bytes left
615
616 const std::optional<mp_integer> element_max_bytes =
618 ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
619 : std::optional<mp_integer>{};
620 const std::size_t element_max_bytes_int =
622 : el_bytes;
623
624 exprt sub = unpack_rec(
625 element, little_endian, {}, element_max_bytes, bits_per_byte, ns, true);
628 byte_operands.insert(
629 byte_operands.end(), sub_operands.begin(), sub_operands.end());
630
631 if(max_bytes && byte_operands.size() >= *max_bytes)
632 break;
633 }
634
635 const std::size_t size = byte_operands.size();
636 return array_exprt(
637 std::move(byte_operands),
639}
640
654 std::size_t total_bits,
655 exprt::operandst &dest,
656 bool little_endian,
657 const std::optional<mp_integer> &offset_bytes,
658 const std::optional<mp_integer> &max_bytes,
659 const std::size_t bits_per_byte,
660 const namespacet &ns)
661{
663 std::move(bit_fields), bv_typet{total_bits}};
664
665 exprt sub = unpack_rec(
667 little_endian,
669 max_bytes,
671 ns,
672 true);
673
674 dest.insert(
675 dest.end(),
676 std::make_move_iterator(sub.operands().begin()),
677 std::make_move_iterator(sub.operands().end()));
678}
679
691 const exprt &src,
692 bool little_endian,
693 const std::optional<mp_integer> &offset_bytes,
694 const std::optional<mp_integer> &max_bytes,
695 const std::size_t bits_per_byte,
696 const namespacet &ns)
697{
699 src.type().id() == ID_struct_tag
701 : to_struct_type(src.type());
702 const struct_typet::componentst &components = struct_type.components();
703
704 std::optional<mp_integer> offset_in_member;
705 std::optional<mp_integer> max_bytes_left;
706 std::optional<std::pair<exprt::operandst, std::size_t>> bit_fields;
707
710 for(auto it = components.begin(); it != components.end(); ++it)
711 {
712 const auto &comp = *it;
713 auto component_bits = pointer_offset_bits(comp.type(), ns);
714
715 // We can only handle a member of unknown width when it is the last member
716 // and is byte-aligned. Members of unknown width in the middle would leave
717 // us with unknown alignment of subsequent members, and queuing them up as
718 // bit fields is not possible either as the total width of the concatenation
719 // could not be determined.
721 component_bits.has_value() ||
722 (std::next(it) == components.end() && !bit_fields.has_value()),
723 "members of non-constant width should come last in a struct");
724
725 member_exprt member(src, comp.get_name(), comp.type());
726 if(src.id() == ID_struct)
727 simplify(member, ns);
728
729 // Is it a byte-aligned member?
731 {
732 if(bit_fields.has_value())
733 {
735 std::move(bit_fields->first),
736 bit_fields->second,
738 little_endian,
742 ns);
743 bit_fields.reset();
744 }
745
746 if(offset_bytes.has_value())
747 {
749 // if the offset is negative, offset_in_member remains unset, which has
750 // the same effect as setting it to zero
751 if(*offset_in_member < 0)
752 offset_in_member.reset();
753 }
754
755 if(max_bytes.has_value())
756 {
758 if(*max_bytes_left < 0)
759 break;
760 }
761 }
762
763 if(
765 (component_bits.has_value() && *component_bits % bits_per_byte != 0))
766 {
767 if(!bit_fields.has_value())
768 bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
769
771 bit_fields->first.insert(
772 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
774 bit_fields->second += bits_int;
775
777
778 continue;
779 }
780
781 INVARIANT(
782 !bit_fields.has_value(),
783 "all preceding members should have been processed");
784
785 if(
786 component_bits.has_value() && offset_in_member.has_value() &&
788 {
789 // we won't actually need this component, fill in zeros instead of
790 // computing an unpacking
791 byte_operands.resize(
792 byte_operands.size() +
794 bv_typet{bits_per_byte}.all_zeros_expr());
795 }
796 else
797 {
798 exprt sub = unpack_rec(
799 member,
800 little_endian,
804 ns,
805 true);
806
807 byte_operands.insert(
808 byte_operands.end(),
809 std::make_move_iterator(sub.operands().begin()),
810 std::make_move_iterator(sub.operands().end()));
811 }
812
813 if(component_bits.has_value())
815 }
816
817 // any remaining bit fields?
818 if(bit_fields.has_value())
819 {
821 std::move(bit_fields->first),
822 bit_fields->second,
824 little_endian,
828 ns);
829 }
830
831 const std::size_t size = byte_operands.size();
832 return array_exprt{
833 std::move(byte_operands),
835}
836
844 const exprt &src,
845 bool little_endian,
846 const std::size_t bits_per_byte,
847 const namespacet &ns)
848{
850 const typet &subtype = complex_type.subtype();
851
852 auto subtype_bits = pointer_offset_bits(subtype, ns);
853 CHECK_RETURN(subtype_bits.has_value());
855
858 little_endian,
859 mp_integer{0},
862 ns,
863 true);
864 exprt::operandst byte_operands = std::move(sub_real.operands());
865
868 little_endian,
869 mp_integer{0},
872 ns,
873 true);
874 byte_operands.insert(
875 byte_operands.end(),
876 std::make_move_iterator(sub_imag.operands().begin()),
877 std::make_move_iterator(sub_imag.operands().end()));
878
879 const std::size_t size = byte_operands.size();
880 return array_exprt{
881 std::move(byte_operands),
883}
884
895// array of bytes
898 const exprt &src,
899 bool little_endian,
900 const std::optional<mp_integer> &offset_bytes,
901 const std::optional<mp_integer> &max_bytes,
902 const std::size_t bits_per_byte,
903 const namespacet &ns,
905{
906 if(src.type().id() == ID_array)
907 {
909 const typet &subtype = array_type.element_type();
910
911 auto element_bits = pointer_offset_bits(subtype, ns);
912 CHECK_RETURN(element_bits.has_value());
913
914 if(
917 {
918 return src;
919 }
920
922 return unpack_array_vector(
923 src,
926 little_endian,
928 max_bytes,
930 ns);
931 }
932 else if(src.type().id() == ID_vector)
933 {
935 const typet &subtype = vector_type.element_type();
936
937 auto element_bits = pointer_offset_bits(subtype, ns);
938 CHECK_RETURN(element_bits.has_value());
939
940 if(
943 {
944 return src;
945 }
946
947 return unpack_array_vector(
948 src,
951 little_endian,
953 max_bytes,
955 ns);
956 }
957 else if(src.type().id() == ID_complex)
958 {
959 return unpack_complex(src, little_endian, bits_per_byte, ns);
960 }
961 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
962 {
963 return unpack_struct(
964 src, little_endian, offset_bytes, max_bytes, bits_per_byte, ns);
965 }
966 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
967 {
968 const union_typet &union_type =
969 src.type().id() == ID_union_tag
971 : to_union_type(src.type());
972
973 const auto widest_member = union_type.find_widest_union_component(ns);
974
975 if(widest_member.has_value())
976 {
977 member_exprt member{
978 src, widest_member->first.get_name(), widest_member->first.type()};
979 return unpack_rec(
980 member,
981 little_endian,
983 widest_member->second,
985 ns,
986 true);
987 }
988 else if(!union_type.components().empty())
989 {
990 member_exprt member{src, union_type.components().front()};
991 return unpack_rec(
992 member,
993 little_endian,
995 max_bytes,
997 ns,
998 true);
999 }
1000 }
1001 else if(src.type().id() == ID_pointer)
1002 {
1003 return unpack_rec(
1004 typecast_exprt{src, bv_typet{to_pointer_type(src.type()).get_width()}},
1005 little_endian,
1007 max_bytes,
1009 ns,
1011 }
1012 else if(src.id() == ID_string_constant)
1013 {
1014 return unpack_rec(
1016 little_endian,
1018 max_bytes,
1020 ns,
1022 }
1023 else if(src.is_constant() && src.type().id() == ID_string)
1024 {
1025 return unpack_rec(
1027 little_endian,
1029 max_bytes,
1031 ns,
1033 }
1034 else if(src.type().id() != ID_empty)
1035 {
1036 // a basic type; we turn that into extractbits while considering
1037 // endianness
1038 auto bits_opt = pointer_offset_bits(src.type(), ns);
1039 DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
1040
1044
1045 if(max_bytes.has_value())
1046 {
1047 const auto max_bits = *max_bytes * bits_per_byte;
1048 if(little_endian)
1049 {
1050 last_bit = std::min(last_bit, max_bits);
1051 }
1052 else
1053 {
1054 bit_offset = std::max(mp_integer{0}, last_bit - max_bits);
1055 }
1056 }
1057
1060 auto const byte_type = bv_typet{bits_per_byte};
1064
1066 {
1068 pointer_offset_bits(src_as_bitvector.type(), ns).has_value());
1071 from_integer(bit_offset, array_type.index_type()),
1072 byte_type);
1073
1074 // endianness_mapt should be the point of reference for mapping out
1075 // endianness, but we need to work on elements here instead of
1076 // individual bits
1077 if(little_endian)
1078 byte_operands.push_back(extractbits);
1079 else
1080 byte_operands.insert(byte_operands.begin(), extractbits);
1081 }
1082
1083 const std::size_t size = byte_operands.size();
1084 array_type.size() = from_integer(size, size_type());
1085 return array_exprt{std::move(byte_operands), std::move(array_type)};
1086 }
1087
1088 return array_exprt(
1090}
1091
1103 const byte_extract_exprt &src,
1105 const typet &subtype,
1106 const mp_integer &element_bits,
1107 const namespacet &ns)
1108{
1109 std::optional<std::size_t> num_elements;
1110 if(src.type().id() == ID_array)
1112 else
1114
1115 if(num_elements.has_value())
1116 {
1117 exprt::operandst operands;
1118 operands.reserve(*num_elements);
1119 for(std::size_t i = 0; i < *num_elements; ++i)
1120 {
1122 unpacked.offset(),
1124 i * element_bits / src.get_bits_per_byte(),
1125 unpacked.offset().type()));
1126
1128 tmp.type() = subtype;
1129 tmp.offset() = new_offset;
1130
1131 operands.push_back(lower_byte_extract(tmp, ns));
1132 }
1133
1134 exprt result;
1135 if(src.type().id() == ID_array)
1136 result = array_exprt{std::move(operands), to_array_type(src.type())};
1137 else
1138 result = vector_exprt{std::move(operands), to_vector_type(src.type())};
1139
1140 return simplify_expr(result, ns);
1141 }
1142
1143 DATA_INVARIANT(src.type().id() == ID_array, "vectors have constant size");
1144 const array_typet &array_type = to_array_type(src.type());
1145
1146 // TODO we either need a symbol table here or make array comprehensions
1147 // introduce a scope
1148 static std::size_t array_comprehension_index_counter = 0;
1151 "$array_comprehension_index_a" +
1152 std::to_string(array_comprehension_index_counter),
1153 array_type.index_type()};
1154
1156 unpacked.offset(),
1158 mult_exprt{
1163 unpacked.offset().type())};
1164
1166 body.type() = subtype;
1167 body.offset() = std::move(new_offset);
1168
1170 std::move(array_comprehension_index),
1171 lower_byte_extract(body, ns),
1172 array_type};
1173}
1174
1183static std::optional<exprt> lower_byte_extract_complex(
1184 const byte_extract_exprt &src,
1186 const namespacet &ns)
1187{
1189 const typet &subtype = complex_type.subtype();
1190
1191 auto subtype_bits = pointer_offset_bits(subtype, ns);
1192 if(!subtype_bits.has_value() || *subtype_bits % src.get_bits_per_byte() != 0)
1193 return {};
1194
1195 // offset remains unchanged
1197 real.type() = subtype;
1198
1199 const plus_exprt new_offset{
1200 unpacked.offset(),
1202 *subtype_bits / src.get_bits_per_byte(), unpacked.offset().type())};
1204 imag.type() = subtype;
1205 imag.offset() = simplify_expr(new_offset, ns);
1206
1207 return simplify_expr(
1209 lower_byte_extract(real, ns), lower_byte_extract(imag, ns), complex_type},
1210 ns);
1211}
1212
1216{
1217 // General notes about endianness and the bit-vector conversion:
1218 // A single byte with value 0b10001000 is stored (in irept) as
1219 // exactly this string literal, and its bit-vector encoding will be
1220 // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
1221 //
1222 // A multi-byte value like x=256 would be:
1223 // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
1224 // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
1225 // - irept representation: 0000000100000000
1226 // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
1227 // <... 8bits ...> <... 8bits ...>
1228 //
1229 // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
1230 // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
1231 //
1232 // The semantics of byte_extract(endianness, op, offset, T) is:
1233 // interpret ((char*)&op)+offset as the endianness-ordered storage
1234 // of an object of type T at address ((char*)&op)+offset
1235 // For some T x, byte_extract(endianness, x, 0, T) must yield x.
1236 //
1237 // byte_extract for a composite type T or an array will interpret
1238 // the individual subtypes with suitable endianness; the overall
1239 // order of components is not affected by endianness.
1240 //
1241 // Examples:
1242 // unsigned char A[4];
1243 // byte_extract_little_endian(A, 0, unsigned short) requests that
1244 // A[0],A[1] be interpreted as the storage of an unsigned short with
1245 // A[1] being the most-significant byte; byte_extract_big_endian for
1246 // the same operands will select A[0] as the most-significant byte.
1247 //
1248 // int A[2] = {0x01020304,0xDEADBEEF}
1249 // byte_extract_big_endian(A, 0, short) should yield 0x0102
1250 // byte_extract_little_endian(A, 0, short) should yield 0x0304
1251 // To obtain this we first compute byte arrays while taking into
1252 // account endianness:
1253 // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
1254 // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
1255 // We extract the relevant bytes starting from ((char*)A)+0:
1256 // big-endian: {01,02}; little-endian: {04,03}
1257 // Finally we place them in the appropriate byte order as indicated
1258 // by endianness:
1259 // big-endian: (short)concatenation(01,02)=0x0102
1260 // little-endian: (short)concatenation(03,04)=0x0304
1261
1265 const bool little_endian = src.id() == ID_byte_extract_little_endian;
1266
1267 // determine an upper bound of the last byte we might need
1268 auto upper_bound_opt = size_of_expr(src.type(), ns);
1269 if(upper_bound_opt.has_value())
1270 {
1272 plus_exprt(
1273 upper_bound_opt.value(),
1275 src.offset(), upper_bound_opt.value().type())),
1276 ns);
1277 }
1278 else if(src.type().id() == ID_empty)
1280
1282 const auto upper_bound_int_opt =
1284
1286 unpacked.op() = unpack_rec(
1287 src.op(),
1288 little_endian,
1291 src.get_bits_per_byte(),
1292 ns);
1294 to_bitvector_type(to_type_with_subtype(unpacked.op().type()).subtype())
1295 .get_width() == src.get_bits_per_byte());
1296
1297 if(src.type().id() == ID_array || src.type().id() == ID_vector)
1298 {
1299 const typet &subtype = to_type_with_subtype(src.type()).subtype();
1300
1301 // consider ways of dealing with arrays of unknown subtype size or with a
1302 // subtype size that does not fit byte boundaries; currently we fall back to
1303 // stitching together consecutive elements down below
1304 auto element_bits = pointer_offset_bits(subtype, ns);
1305 if(
1306 element_bits.has_value() && *element_bits >= 1 &&
1307 *element_bits % src.get_bits_per_byte() == 0)
1308 {
1310 src, unpacked, subtype, *element_bits, ns);
1311 }
1312 }
1313 else if(src.type().id() == ID_complex)
1314 {
1315 auto result = lower_byte_extract_complex(src, unpacked, ns);
1316 if(result.has_value())
1317 return std::move(*result);
1318
1319 // else fall back to generic lowering that uses bit masks, below
1320 }
1321 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
1322 {
1323 const struct_typet &struct_type =
1324 src.type().id() == ID_struct_tag
1326 : to_struct_type(src.type());
1327 const struct_typet::componentst &components = struct_type.components();
1328
1329 bool failed = false;
1330 struct_exprt s({}, src.type());
1331
1332 for(const auto &comp : components)
1333 {
1334 auto component_bits = pointer_offset_bits(comp.type(), ns);
1335
1336 // the next member would be misaligned, abort
1337 if(
1338 !component_bits.has_value() ||
1339 *component_bits % src.get_bits_per_byte() != 0)
1340 {
1341 failed = true;
1342 break;
1343 }
1344
1345 auto member_offset_opt =
1346 member_offset_expr(struct_type, comp.get_name(), ns);
1347
1348 if(!member_offset_opt.has_value())
1349 {
1350 failed = true;
1351 break;
1352 }
1353
1355 unpacked.offset(),
1357 member_offset_opt.value(), unpacked.offset().type()));
1358
1360 tmp.type() = comp.type();
1361 tmp.offset() = new_offset;
1362
1364 }
1365
1366 if(!failed)
1367 return simplify_expr(std::move(s), ns);
1368 }
1369 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
1370 {
1371 const union_typet &union_type =
1372 src.type().id() == ID_union_tag
1373 ? ns.follow_tag(to_union_tag_type(src.type()))
1374 : to_union_type(src.type());
1375
1376 const auto widest_member = union_type.find_widest_union_component(ns);
1377
1378 if(widest_member.has_value())
1379 {
1381 tmp.type() = widest_member->first.type();
1382
1383 return union_exprt(
1384 widest_member->first.get_name(),
1386 src.type());
1387 }
1388 }
1389
1390 const exprt &root = unpacked.op();
1391 const exprt &offset = unpacked.offset();
1392
1393 std::optional<typet> subtype;
1394 std::optional<typet> index_type;
1395 if(root.type().id() == ID_vector)
1396 {
1397 subtype = to_vector_type(root.type()).element_type();
1398 index_type = to_vector_type(root.type()).index_type();
1399 }
1400 else
1401 {
1402 subtype = to_array_type(root.type()).element_type();
1403 index_type = to_array_type(root.type()).index_type();
1404 }
1405
1406 auto subtype_bits = pointer_offset_bits(*subtype, ns);
1407
1409 subtype_bits.has_value() && *subtype_bits == src.get_bits_per_byte(),
1410 "offset bits are byte aligned");
1411
1412 auto size_bits = pointer_offset_bits(unpacked.type(), ns);
1413 if(!size_bits.has_value())
1414 {
1415 auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
1416 // all cases with non-constant width should have been handled above
1418 op0_bits.has_value(),
1419 "the extracted width or the source width must be known");
1421 }
1422
1424 (*size_bits) / src.get_bits_per_byte() +
1425 (((*size_bits) % src.get_bits_per_byte() == 0) ? 0 : 1);
1426
1427 // get 'width'-many bytes, and concatenate
1430 op.reserve(width_bytes);
1431
1432 for(std::size_t i = 0; i < width_bytes; i++)
1433 {
1434 // the most significant byte comes first in the concatenation!
1435 std::size_t offset_int = little_endian ? (width_bytes - i - 1) : i;
1436
1438 from_integer(offset_int, *index_type),
1439 typecast_exprt::conditional_cast(offset, *index_type)};
1440 simplify(offset_i, ns);
1441
1442 mp_integer index = 0;
1443 if(
1444 offset_i.is_constant() &&
1445 (root.id() == ID_array || root.id() == ID_vector) &&
1447 index < root.operands().size() && index >= 0)
1448 {
1449 // offset is constant and in range
1450 op.push_back(root.operands()[numeric_cast_v<std::size_t>(index)]);
1451 }
1452 else
1453 {
1454 op.push_back(index_exprt(root, offset_i));
1455 }
1456 }
1457
1458 if(width_bytes == 1)
1459 {
1460 return simplify_expr(
1461 typecast_exprt::conditional_cast(op.front(), src.type()), ns);
1462 }
1463 else // width_bytes>=2
1464 {
1466 std::move(op),
1467 adjust_width(*subtype, width_bytes * src.get_bits_per_byte()));
1468
1469 endianness_mapt map(concatenation.type(), little_endian, ns);
1470 return bv_to_expr(concatenation, src.type(), map, ns);
1471 }
1472}
1473
1475 const byte_update_exprt &src,
1477 const std::optional<exprt> &non_const_update_bound,
1478 const namespacet &ns);
1479
1490 const byte_update_exprt &src,
1491 const typet &subtype,
1494 const namespacet &ns)
1495{
1496 // TODO we either need a symbol table here or make array comprehensions
1497 // introduce a scope
1498 static std::size_t array_comprehension_index_counter = 0;
1501 "$array_comprehension_index_u_a_v" +
1502 std::to_string(array_comprehension_index_counter),
1503 to_array_type(src.type()).index_type()};
1504
1505 binary_predicate_exprt lower_bound{
1507 array_comprehension_index, src.offset().type()),
1508 ID_lt,
1509 src.offset()};
1510 binary_predicate_exprt upper_bound{
1513 ID_ge,
1514 plus_exprt{
1516 src.offset(), non_const_update_bound.type()),
1518
1521 src.id() == ID_byte_update_big_endian);
1522 const bool little_endian = src.id() == ID_byte_update_little_endian;
1523 endianness_mapt map(
1524 to_array_type(value_as_byte_array.type()).element_type(),
1525 little_endian,
1526 ns);
1528 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1530 bv_to_expr(
1536 src.offset(), array_comprehension_index.type())}},
1537 subtype,
1538 map,
1539 ns)};
1540
1541 return simplify_expr(
1544 std::move(array_comprehension_body),
1545 to_array_type(src.type())},
1546 ns);
1547}
1548
1559 const byte_update_exprt &src,
1560 const typet &subtype,
1562 const std::optional<exprt> &non_const_update_bound,
1563 const namespacet &ns)
1564{
1567 src.id() == ID_byte_update_big_endian);
1568 const bool little_endian = src.id() == ID_byte_update_little_endian;
1569
1570 const typet index_type = src.type().id() == ID_array
1571 ? to_array_type(src.type()).index_type()
1572 : to_vector_type(src.type()).index_type();
1573
1574 // apply 'array-update-with' num_elements times
1575 exprt result = src.op();
1576
1577 for(std::size_t i = 0; i < value_as_byte_array.operands().size(); ++i)
1578 {
1579 const exprt &element = value_as_byte_array.operands()[i];
1580
1581 exprt where = simplify_expr(
1582 plus_exprt{
1583 typecast_exprt::conditional_cast(src.offset(), index_type),
1584 from_integer(i, index_type)},
1585 ns);
1586
1587 // skip elements that wouldn't change (skip over typecasts as we might have
1588 // some signed/unsigned char conversions)
1589 const exprt &e = skip_typecast(element);
1590 if(e.id() == ID_index)
1591 {
1593 if(index_expr.array() == src.op() && index_expr.index() == where)
1594 continue;
1595 }
1596
1597 endianness_mapt map(element.type(), little_endian, ns);
1598 exprt update_value = bv_to_expr(element, subtype, map, ns);
1599 if(non_const_update_bound.has_value())
1600 {
1604 ID_lt,
1607 index_exprt{src.op(), where}};
1608 }
1609
1610 result = with_exprt{result, std::move(where), std::move(update_value)};
1611 }
1612
1613 return simplify_expr(std::move(result), ns);
1614}
1615
1632 const byte_update_exprt &src,
1633 const typet &subtype,
1634 const exprt &subtype_size,
1637 const exprt &initial_bytes,
1638 const exprt &first_index,
1640 const namespacet &ns)
1641{
1645
1646 // TODO we either need a symbol table here or make array comprehensions
1647 // introduce a scope
1648 static std::size_t array_comprehension_index_counter = 0;
1651 "$array_comprehension_index_u_a_v_u" +
1652 std::to_string(array_comprehension_index_counter),
1653 to_array_type(src.type()).index_type()};
1654
1655 // all arithmetic uses offset/index types
1656 PRECONDITION(array_comprehension_index.type() == src.offset().type());
1657 PRECONDITION(subtype_size.type() == src.offset().type());
1658 PRECONDITION(initial_bytes.type() == src.offset().type());
1659 PRECONDITION(first_index.type() == src.offset().type());
1660
1661 // the bound from where updates start
1662 binary_predicate_exprt lower_bound{
1665 ID_lt,
1666 first_index};
1667
1668 // The actual value of updates other than at the start or end
1671 mult_exprt{
1681 std::move(offset_expr),
1682 src.get_bits_per_byte(),
1683 subtype},
1684 ns);
1685
1686 // The number of target array/vector elements being replaced, not including
1687 // a possible partial update at the end of the updated range, which is handled
1688 // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
1689 // round up to the nearest multiple of subtype_size.
1691 plus_exprt{
1695 subtype_size};
1696
1697 // The last element to be updated: first_index + updated_elements - 1
1701 std::move(updated_elements), from_integer(1, first_index.type())}};
1702
1703 // The size of a partial update at the end of the updated range, may be zero.
1710 subtype_size.type()),
1711 subtype_size};
1712
1713 // The bound where updates end, which is conditional on the partial update
1714 // being empty.
1715 binary_predicate_exprt upper_bound{
1718 ID_ge,
1719 if_exprt{
1721 last_index,
1723
1724 // The actual value of a partial update at the end.
1727 src.id(),
1728 index_exprt{src.op(), last_index},
1731 subtype_size}},
1733 src.get_bits_per_byte()},
1734 ns);
1735
1737 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1739 if_exprt{
1743 first_index},
1745 if_exprt{
1749 last_index},
1750 std::move(last_update_value),
1751 std::move(update_value)}}};
1752
1753 return simplify_expr(
1756 std::move(array_comprehension_body),
1757 to_array_type(src.type())},
1758 ns);
1759}
1760
1772 const byte_update_exprt &src,
1773 const typet &subtype,
1775 const std::optional<exprt> &non_const_update_bound,
1776 const namespacet &ns)
1777{
1778 // do all arithmetic below using index/offset types - the array theory
1779 // back-end is really picky about indices having the same type
1780 auto subtype_size_opt = size_of_expr(subtype, ns);
1781 CHECK_RETURN(subtype_size_opt.has_value());
1782
1785 subtype_size_opt.value(), src.offset().type()),
1786 ns);
1787
1788 // compute the index of the first element of the array/vector that may be
1789 // updated
1791 src.offset().type() == to_array_type(src.op().type()).index_type());
1793 simplify(first_index, ns);
1794
1795 // compute the offset within that first element
1797
1798 // compute the number of bytes (from the update value) that are going to be
1799 // consumed for updating the first element
1800 const exprt update_size =
1801 from_integer(value_as_byte_array.operands().size(), subtype_size.type());
1804 if(non_const_update_bound.has_value())
1805 {
1808 }
1809 else
1810 {
1813 "value should be an array expression if the update bound is constant");
1815 }
1819 update_bound};
1821
1822 // encode the first update: update the original element at first_index (the
1823 // actual update will only be initial_bytes-many bytes from
1824 // value_as_byte_array)
1827 src.id(),
1828 index_exprt{src.op(), first_index},
1831 src.get_bits_per_byte()},
1832 ns);
1833
1834 if(value_as_byte_array.id() != ID_array)
1835 {
1837 src,
1838 subtype,
1845 ns);
1846 }
1847
1848 // We will update one array/vector element at a time - compute the number of
1849 // update values that will be consumed in each step. If we cannot determine a
1850 // constant value at this time we assume it's at least one byte. The
1851 // byte_extract_exprt within the loop uses the symbolic value (subtype_size),
1852 // we just need to make sure we make progress for the loop to terminate.
1853 std::size_t step_size = 1;
1854 if(subtype_size.is_constant())
1856 // Given the first update already encoded, keep track of the offset into the
1857 // update value. Again, the expressions within the loop use the symbolic
1858 // value, this is just an optimization in case we can determine a constant
1859 // offset.
1860 std::size_t offset = 0;
1861 if(initial_bytes.is_constant())
1863
1865
1867 [&src,
1868 &first_index,
1870 &subtype_size,
1872 &ns,
1873 &result](std::size_t i) -> void {
1874 exprt where = simplify_expr(
1876
1881 ns);
1882
1883 exprt element = lower_byte_update(
1885 src.id(),
1886 index_exprt{src.op(), where},
1889 src.get_bits_per_byte()},
1890 ns);
1891
1892 result = with_exprt{result, std::move(where), std::move(element)};
1893 };
1894
1895 std::size_t i = 1;
1896 for(; offset + step_size <= value_as_byte_array.operands().size();
1897 offset += step_size, ++i)
1898 {
1900 }
1901
1902 // do the tail
1903 if(offset < value_as_byte_array.operands().size())
1905
1906 return simplify_expr(std::move(result), ns);
1907}
1908
1922 const byte_update_exprt &src,
1923 const mp_integer &offset_bits,
1924 const exprt &element_to_update,
1925 const mp_integer &subtype_bits,
1928 const std::optional<exprt> &non_const_update_bound,
1929 const namespacet &ns)
1930{
1931 // We need to take one or more bytes from value_as_byte_array to modify the
1932 // target element. We need to compute:
1933 // - The position in value_as_byte_array to take bytes from: If subtype_bits
1934 // is less than the size of a byte, then multiple struct/array/vector elements
1935 // will need to be updated using the same byte.
1936 std::size_t first = 0;
1937 // - An upper bound on the number of bytes required from value_as_byte_array.
1939 (subtype_bits + src.get_bits_per_byte() - 1) / src.get_bits_per_byte();
1940 // - The offset into the target element: If subtype_bits is greater or equal
1941 // to the size of a byte, then there may be an offset into the target element
1942 // that needs to be taken into account, and multiple bytes will be required.
1944
1946 {
1947 INVARIANT(
1948 value_as_byte_array.id() != ID_array ||
1949 value_as_byte_array.operands().size() * src.get_bits_per_byte() >
1951 "indices past the update should be handled below");
1956 src.get_bits_per_byte();
1959 }
1960 else
1961 {
1963 INVARIANT(
1964 update_elements > 0, "indices before the update should be handled above");
1965 }
1966
1967 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1968 if(value_as_byte_array.id() == ID_array)
1969 end = std::min(end, value_as_byte_array.operands().size());
1971 value_as_byte_array, first, end, src.get_bits_per_byte(), ns);
1972 const std::size_t update_size = update_values.size();
1974 const array_typet update_type{
1976
1977 // each case below will set "new_value" as appropriate
1978 exprt new_value;
1979
1980 if(
1983 {
1984 new_value = array_exprt{update_values, update_type};
1985 }
1986 else
1987 {
1988 if(src.id() == ID_byte_update_little_endian)
1989 std::reverse(update_values.begin(), update_values.end());
1991 {
1992 if(src.id() == ID_byte_update_little_endian)
1993 {
1994 new_value = lshr_exprt{
1998 }
1999 else
2000 {
2001 new_value = shl_exprt{
2005 }
2006 }
2007 else
2008 {
2009 const std::size_t offset_bits_int =
2011 const std::size_t subtype_bits_int =
2013
2018 new_value = concatenation_exprt{
2026 }
2027
2031
2034 new_value,
2035 from_integer(0, src.offset().type()),
2036 src.get_bits_per_byte(),
2037 update_type};
2038
2039 new_value = lower_byte_extract(byte_extract_expr, ns);
2040
2042 }
2043
2044 // With an upper bound on the size of the update established, construct the
2045 // actual update expression. If the exact size of the update is unknown,
2046 // make the size expression conditional.
2047 const byte_update_exprt bu{
2048 src.id(),
2052 src.offset().type()),
2053 new_value,
2054 src.get_bits_per_byte()};
2055
2056 std::optional<exprt> update_bound;
2057 if(non_const_update_bound.has_value())
2058 {
2059 // The size of the update is not constant, and thus is to be symbolically
2060 // bound; first see how many bytes we have left in the update:
2061 // non_const_update_bound > first ? non_const_update_bound - first: 0
2063 if_exprt{
2066 ID_gt,
2067 from_integer(first, non_const_update_bound->type())},
2070 from_integer(first, non_const_update_bound->type())},
2072 size_type());
2073 // Now take the minimum of update-bytes-left and the previously computed
2074 // size of the element to be updated:
2076 if_exprt{
2080 ns);
2081 }
2082
2083 return lower_byte_update(bu, new_value, update_bound, ns);
2084}
2085
2097 const byte_update_exprt &src,
2098 const typet &subtype,
2099 const std::optional<mp_integer> &subtype_bits,
2101 const std::optional<exprt> &non_const_update_bound,
2102 const namespacet &ns)
2103{
2104 const bool is_array = src.type().id() == ID_array;
2105 exprt size;
2106 typet index_type;
2107 if(is_array)
2108 {
2109 size = to_array_type(src.type()).size();
2110 index_type = to_array_type(src.type()).index_type();
2111 }
2112 else
2113 {
2114 size = to_vector_type(src.type()).size();
2115 index_type = to_vector_type(src.type()).index_type();
2116 }
2117
2118 // fall back to bytewise updates in all non-constant or dubious cases
2119 if(
2120 !size.is_constant() || !src.offset().is_constant() ||
2121 !subtype_bits.has_value() || value_as_byte_array.id() != ID_array)
2122 {
2124 src, subtype, value_as_byte_array, non_const_update_bound, ns);
2125 }
2126
2127 std::size_t num_elements =
2131 src.get_bits_per_byte();
2132
2133 exprt::operandst elements;
2134 elements.reserve(num_elements);
2135
2136 std::size_t i = 0;
2137 // copy the prefix not affected by the update
2138 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bits; ++i)
2139 elements.push_back(index_exprt{src.op(), from_integer(i, index_type)});
2140
2141 // the modified elements
2142 for(;
2143 i < num_elements &&
2144 i * *subtype_bits < offset_bits + value_as_byte_array.operands().size() *
2145 src.get_bits_per_byte();
2146 ++i)
2147 {
2148 elements.push_back(lower_byte_update_single_element(
2149 src,
2151 index_exprt{src.op(), from_integer(i, index_type)},
2152 *subtype_bits,
2153 i * *subtype_bits,
2156 ns));
2157 }
2158
2159 // copy the tail not affected by the update
2160 for(; i < num_elements; ++i)
2161 elements.push_back(index_exprt{src.op(), from_integer(i, index_type)});
2162
2163 if(is_array)
2164 return simplify_expr(
2165 array_exprt{std::move(elements), to_array_type(src.type())}, ns);
2166 else
2167 return simplify_expr(
2168 vector_exprt{std::move(elements), to_vector_type(src.type())}, ns);
2169}
2170
2181 const byte_update_exprt &src,
2184 const std::optional<exprt> &non_const_update_bound,
2185 const namespacet &ns)
2186{
2187 exprt::operandst elements;
2188 elements.reserve(struct_type.components().size());
2189
2191 for(const auto &comp : struct_type.components())
2192 {
2193 auto element_width = pointer_offset_bits(comp.type(), ns);
2194
2195 // compute the update offset relative to this struct member - will be
2196 // negative if we are already in the middle of the update or beyond it
2197 exprt offset = simplify_expr(
2199 mult_exprt{
2200 src.offset(),
2201 from_integer(src.get_bits_per_byte(), src.offset().type())},
2202 from_integer(member_offset_bits, src.offset().type())},
2203 ns);
2205 if(!offset_bits.has_value() || !element_width.has_value())
2206 {
2207 // The offset to update is not constant, either because the original
2208 // offset in src never was, or because a struct member has an unknown
2209 // offset. Abort the attempt to update individual struct members and
2210 // instead turn the operand-to-be-updated into a byte array, which we know
2211 // how to update even if the offset is non-constant.
2215
2216 auto src_size_opt = size_of_expr(src.type(), ns);
2217 CHECK_RETURN(src_size_opt.has_value());
2218
2221 src.op(),
2222 from_integer(0, src.offset().type()),
2223 src.get_bits_per_byte(),
2225
2226 byte_update_exprt bu = src;
2228 bu.type() = bu.op().type();
2229
2230 return lower_byte_extract(
2235 from_integer(0, src.offset().type()),
2236 src.get_bits_per_byte(),
2237 src.type()},
2238 ns);
2239 }
2240
2241 exprt member = member_exprt{src.op(), comp.get_name(), comp.type()};
2242
2243 // we don't need to update anything when
2244 // 1) the update offset is greater than the end of this member (thus the
2245 // relative offset is greater than this element) or
2246 // 2) the update offset plus the size of the update is less than the member
2247 // offset
2248 if(
2250 (value_as_byte_array.id() == ID_array && *offset_bits < 0 &&
2251 -*offset_bits >=
2252 value_as_byte_array.operands().size() * src.get_bits_per_byte()))
2253 {
2254 elements.push_back(member);
2256 continue;
2257 }
2258
2259 elements.push_back(lower_byte_update_single_element(
2260 src,
2262 member,
2267 ns));
2268
2270 }
2271
2272 return simplify_expr(struct_exprt{std::move(elements), struct_type}, ns);
2273}
2274
2285 const byte_update_exprt &src,
2286 const union_typet &union_type,
2288 const std::optional<exprt> &non_const_update_bound,
2289 const namespacet &ns)
2290{
2291 const auto widest_member = union_type.find_widest_union_component(ns);
2292
2294 widest_member.has_value(),
2295 "lower_byte_update of union of unknown size is not supported");
2296
2297 byte_update_exprt bu = src;
2298 bu.set_op(member_exprt{
2299 src.op(), widest_member->first.get_name(), widest_member->first.type()});
2300 bu.type() = widest_member->first.type();
2301
2302 return union_exprt{
2303 widest_member->first.get_name(),
2305 src.type()};
2306}
2307
2317 const byte_update_exprt &src,
2319 const std::optional<exprt> &non_const_update_bound,
2320 const namespacet &ns)
2321{
2322 if(src.type().id() == ID_array || src.type().id() == ID_vector)
2323 {
2324 std::optional<typet> subtype;
2325 if(src.type().id() == ID_vector)
2326 subtype = to_vector_type(src.type()).element_type();
2327 else
2328 subtype = to_array_type(src.type()).element_type();
2329
2330 auto element_width = pointer_offset_bits(*subtype, ns);
2331
2332 if(element_width.has_value() && *element_width == src.get_bits_per_byte())
2333 {
2334 if(value_as_byte_array.id() != ID_array)
2335 {
2337 non_const_update_bound.has_value(),
2338 "constant update bound should yield an array expression");
2340 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2341 }
2342
2344 src,
2345 *subtype,
2348 ns);
2349 }
2350 else
2351 {
2353 src,
2354 *subtype,
2358 ns);
2359 }
2360 }
2361 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
2362 {
2363 const struct_typet &struct_type =
2364 src.type().id() == ID_struct_tag
2366 : to_struct_type(src.type());
2369 result.type() = src.type();
2370 return result;
2371 }
2372 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
2373 {
2374 const union_typet &union_type =
2375 src.type().id() == ID_union_tag
2376 ? ns.follow_tag(to_union_tag_type(src.type()))
2377 : to_union_type(src.type());
2380 result.type() = src.type();
2381 return result;
2382 }
2383 else if(
2385 src.type().id() == ID_c_enum || src.type().id() == ID_c_enum_tag)
2386 {
2387 // mask out the bits to be updated, shift the value according to the
2388 // offset and bit-or
2389 const auto type_width = pointer_offset_bits(src.type(), ns);
2390 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2391 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2392
2394 if(value_as_byte_array.id() == ID_array)
2395 update_bytes = value_as_byte_array.operands();
2396 else
2397 {
2400 0,
2401 (type_bits + src.get_bits_per_byte() - 1) / src.get_bits_per_byte(),
2402 src.get_bits_per_byte(),
2403 ns);
2404 }
2405
2406 const std::size_t update_size_bits =
2407 update_bytes.size() * src.get_bits_per_byte();
2408 const std::size_t bit_width = std::max(type_bits, update_size_bits);
2409
2410 const bool is_little_endian = src.id() == ID_byte_update_little_endian;
2411
2413 typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
2414 if(bit_width > type_bits)
2415 {
2417 bv_typet{bit_width - type_bits}.all_zeros_expr(),
2418 val_before,
2419 bv_typet{bit_width}};
2420
2421 if(!is_little_endian)
2423 .op0()
2424 .swap(to_concatenation_expr(val_before).op1());
2425 }
2426
2427 if(non_const_update_bound.has_value())
2428 {
2430 val_before,
2432 mp_integer{0},
2433 mp_integer{update_bytes.size()},
2434 src.get_bits_per_byte(),
2435 ns);
2437 CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
2438 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2439 {
2443 ID_lt,
2445 update_bytes[i],
2446 src_as_bytes.operands()[i]};
2447 }
2448 }
2449
2450 // build mask
2451 exprt mask;
2453 mask = from_integer(power(2, update_size_bits) - 1, bv_typet{bit_width});
2454 else
2455 {
2456 mask = from_integer(
2457 power(2, bit_width) - power(2, bit_width - update_size_bits),
2458 bv_typet{bit_width});
2459 }
2460
2461 const typet &offset_type = src.offset().type();
2464
2467
2472 if(!is_little_endian)
2473 {
2474 mask_shifted.true_case().swap(mask_shifted.false_case());
2475 to_shift_expr(mask_shifted.true_case())
2476 .distance()
2477 .swap(to_shift_expr(mask_shifted.false_case()).distance());
2478 }
2479
2480 // original_bits &= ~mask
2482
2483 // concatenate and zero-extend the value
2486 std::reverse(value.operands().begin(), value.operands().end());
2487
2489 if(bit_width > update_size_bits)
2490 {
2492 zero_extended = zero_extend_exprt{value, bv_typet{bit_width}};
2493 else
2494 {
2495 // Big endian -- the zero is added as LSB.
2497 value,
2498 bv_typet{bit_width - update_size_bits}.all_zeros_expr(),
2499 bv_typet{bit_width}};
2500 }
2501 }
2502 else
2503 zero_extended = value;
2504
2505 // shift the value
2510 if(!is_little_endian)
2511 {
2512 value_shifted.true_case().swap(value_shifted.false_case());
2513 to_shift_expr(value_shifted.true_case())
2514 .distance()
2515 .swap(to_shift_expr(value_shifted.false_case()).distance());
2516 }
2517
2518 // original_bits |= newvalue
2520
2521 if(bit_width > type_bits)
2522 {
2523 endianness_mapt endianness_map(
2524 bitor_expr.type(), src.id() == ID_byte_update_little_endian, ns);
2525 const auto bounds = map_bounds(endianness_map, 0, type_bits - 1);
2526
2527 PRECONDITION(pointer_offset_bits(bitor_expr.type(), ns).has_value());
2528 return simplify_expr(
2531 src.type()),
2532 ns);
2533 }
2534
2535 return simplify_expr(
2537 }
2538 else
2539 {
2541 false, "lower_byte_update does not yet support ", src.type().id_string());
2542 }
2543}
2544
2546{
2550 "byte update expression should either be little or big endian");
2551
2552 // An update of a void-typed object or update by a void-typed value is the
2553 // source operand (this is questionable, but may arise when dereferencing
2554 // invalid pointers).
2555 if(src.type().id() == ID_empty || src.value().type().id() == ID_empty)
2556 return src.op();
2557
2558 // byte_update lowering proceeds as follows:
2559 // 1) Determine the size of the update, with the size of the object to be
2560 // updated as an upper bound. We fail if neither can be determined.
2561 // 2) Turn the update value into a byte array of the size determined above.
2562 // 3) If the offset is not constant, turn the object into a byte array, and
2563 // use a "with" expression to encode the update; else update the values in
2564 // place.
2565 // 4) Construct a new object.
2566 std::optional<exprt> non_const_update_bound;
2567 // update value, may require extension to full bytes
2568 exprt update_value = src.value();
2571 simplify(update_size_expr_opt.value(), ns);
2572
2576 const std::size_t bits_per_byte = src.get_bits_per_byte();
2577
2578 if(!update_size_expr_opt.value().is_constant())
2580 else
2581 {
2582 auto update_bits = pointer_offset_bits(update_value.type(), ns);
2583 // If the following invariant fails, then the type was only found to be
2584 // constant via simplification. Such instances should be fixed at the place
2585 // introducing these constant-but-not-constant_exprt type sizes.
2587 update_bits.has_value(), "constant size-of should imply fixed bit width");
2589
2591 {
2594 "non-byte aligned type expected to be a bitvector type");
2597 src.op(),
2599 plus_exprt{
2600 src.offset(),
2602 ns),
2603 src.get_bits_per_byte(),
2605 const exprt overlapping_byte =
2607
2610
2614 extra_bits,
2616 }
2617 else
2618 {
2621 }
2622 }
2623
2627 from_integer(0, src.offset().type()),
2628 src.get_bits_per_byte(),
2630
2632
2633 exprt result =
2635 return result;
2636}
2637
2639{
2640 exprt tmp = src;
2641
2642 // destroys any sharing, should use hash table
2643 Forall_operands(it, tmp)
2644 {
2645 *it = lower_byte_operators(*it, ns);
2646 }
2647
2648 if(
2651 {
2653 }
2654 else if(
2657 {
2659 }
2660 else
2661 return tmp;
2662}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition c_types.h:80
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3544
Array constructor from list of elements.
Definition std_expr.h:1621
Arrays with given size.
Definition std_types.h:807
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition std_types.h:909
Fixed-width bit-vector without numerical interpretation.
constant_exprt all_zeros_expr() const
Expression of type type extracted from some object op starting at position offset (given in number of...
std::size_t get_bits_per_byte() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
const exprt & op() const
std::size_t get_bits_per_byte() const
const exprt & value() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition c_types.h:20
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
Real part of the expression describing a complex number.
Definition std_expr.h:1984
Complex numbers made of pair of given subtype.
Definition std_types.h:1133
Concatenation of bit-vector operands.
Division.
Definition std_expr.h:1157
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1834
Maps a big-endian offset to a little-endian offset.
size_t number_of_bits() const
size_t map_bit(size_t bit) const
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
Extracts a sub-range of a bit-vector operand.
The trinary if-then-else operator.
Definition std_expr.h:2502
Array index operator.
Definition std_expr.h:1470
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
Logical right shift.
Extract member of struct or union.
Definition std_expr.h:2972
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3209
Boolean OR.
Definition std_expr.h:2275
The plus expression Associativity is not specified.
Definition std_expr.h:1002
Left shift.
Fixed-width bit-vector with two's complement interpretation.
Struct constructor from list of elements.
Definition std_expr.h:1877
Structure type, corresponds to C style structs.
Definition std_types.h:231
std::vector< componentt > componentst
Definition std_types.h:140
Expression to hold a symbol (variable)
Definition std_expr.h:131
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
The unary minus expression.
Definition std_expr.h:484
Union constructor from single element.
Definition std_expr.h:1770
The union type.
Definition c_types.h:147
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Definition std_expr.h:1734
The vector type.
Definition std_types.h:1064
Operator to update elements in structs and arrays.
Definition std_expr.h:2603
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
#define Forall_operands(it, expr)
Definition expr.h:27
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update v...
static exprt lower_byte_update_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as updat...
static exprt bv_to_expr(const exprt &bitvector_expr, const typet &target_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an expression of type target_type.
static exprt bv_to_union_expr(const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a union-typed expression.
static complex_exprt bv_to_complex_expr(const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.
static array_exprt unpack_struct(const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const std::size_t bits_per_byte, const namespacet &ns)
Build the individual bytes to be used in an update.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
static vector_exprt bv_to_vector_expr(const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.
static void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
static struct_exprt bv_to_struct_expr(const exprt &bitvector_expr, const struct_typet &struct_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a struct-typed expression.
static array_exprt unpack_complex(const exprt &src, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const std::optional< mp_integer > &subtype_bits, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as ...
static exprt lower_byte_update_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
static array_exprt bv_to_array_expr(const exprt &bitvector_expr, const array_typet &array_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an array-typed expression.
static boundst map_bounds(const endianness_mapt &endianness_map, std::size_t lower_bound, std::size_t upper_bound)
Map bit boundaries according to endianness.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
static exprt lower_byte_extract_array_vector(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const typet &subtype, const mp_integer &element_bits, const namespacet &ns)
Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual compon...
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
static exprt unpack_array_vector(const exprt &src, const std::optional< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
static exprt unpack_rec(const exprt &src, bool little_endian, const std::optional< mp_integer > &offset_bytes, const std::optional< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
static exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update ...
static std::optional< exprt > lower_byte_extract_complex(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components t...
static exprt lower_byte_update_byte_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_by...
static exprt lower_byte_update_single_element(const byte_update_exprt &src, const mp_integer &offset_bits, const exprt &element_to_update, const mp_integer &subtype_bits, const mp_integer &bits_already_set, const exprt &value_as_byte_array, const std::optional< exprt > &non_const_update_bound, const namespacet &ns)
Byte update a struct/array/vector element.
static exprt lower_byte_update_array_vector_unbounded(const byte_update_exprt &src, const typet &subtype, const exprt &subtype_size, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const exprt &initial_bytes, const exprt &first_index, const exprt &first_update_value, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
const string_constantt & to_string_constant(const exprt &expr)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
#define size_type
Definition unistd.c:186