cprover
Loading...
Searching...
No Matches
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 "expr_lowering.h"
10
11#include <algorithm>
12
13#include <util/arith_tools.h>
14#include <util/bitvector_expr.h>
15#include <util/byte_operators.h>
16#include <util/c_types.h>
17#include <util/endianness_map.h>
18#include <util/expr_util.h>
19#include <util/namespace.h>
21#include <util/simplify_expr.h>
23
24static exprt bv_to_expr(
25 const exprt &bitvector_expr,
26 const typet &target_type,
27 const endianness_mapt &endianness_map,
28 const namespacet &ns);
29
30struct boundst
31{
32 std::size_t lb;
33 std::size_t ub;
34};
35
38 const endianness_mapt &endianness_map,
39 std::size_t lower_bound,
40 std::size_t upper_bound)
41{
42 boundst result;
43 result.lb = lower_bound;
44 result.ub = upper_bound;
45
46 if(result.ub < endianness_map.number_of_bits())
47 {
48 result.lb = endianness_map.map_bit(result.lb);
49 result.ub = endianness_map.map_bit(result.ub);
50
51 // big-endian bounds need swapping
52 if(result.ub < result.lb)
53 std::swap(result.lb, result.ub);
54 }
55
56 return result;
57}
58
61{
62 if(src.id() == ID_unsignedbv)
64 else if(src.id() == ID_signedbv)
66 else if(src.id() == ID_bv)
67 return bv_typet(new_width);
68 else if(src.id() == ID_c_enum) // we use the underlying type
69 return adjust_width(to_c_enum_type(src).underlying_type(), new_width);
70 else if(src.id() == ID_c_bit_field)
71 return c_bit_field_typet(
72 to_c_bit_field_type(src).underlying_type(), new_width);
73 else
74 PRECONDITION(false);
75}
76
80 const exprt &bitvector_expr,
82 const endianness_mapt &endianness_map,
83 const namespacet &ns)
84{
85 const struct_typet::componentst &components = struct_type.components();
86
87 exprt::operandst operands;
88 operands.reserve(components.size());
89 std::size_t member_offset_bits = 0;
90 for(const auto &comp : components)
91 {
92 const auto component_bits_opt = pointer_offset_bits(comp.type(), ns);
93 std::size_t component_bits;
94 if(component_bits_opt.has_value())
96 else
99
100 if(component_bits == 0)
101 {
102 operands.push_back(constant_exprt{irep_idt{}, comp.type()});
103 continue;
104 }
105
106 const auto bounds = map_bounds(
107 endianness_map,
111 operands.push_back(bv_to_expr(
112 extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
113 comp.type(),
114 endianness_map,
115 ns));
116
117 if(component_bits_opt.has_value())
119 }
120
121 return struct_exprt{std::move(operands), struct_type};
122}
123
127 const exprt &bitvector_expr,
128 const union_typet &union_type,
129 const endianness_mapt &endianness_map,
130 const namespacet &ns)
131{
132 const union_typet::componentst &components = union_type.components();
133
134 // empty union, handled the same way as done in expr_initializert
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
145
146 if(component_bits == 0)
147 {
148 return union_exprt{components.front().get_name(),
149 constant_exprt{irep_idt{}, components.front().type()},
150 union_type};
151 }
152
153 const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
155 const irep_idt &component_name = widest_member.has_value()
156 ? widest_member->first.get_name()
157 : components.front().get_name();
158 const typet &component_type = widest_member.has_value()
159 ? widest_member->first.type()
160 : components.front().type();
161 return union_exprt{
162 component_name,
164 extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
165 component_type,
166 endianness_map,
167 ns),
168 union_type};
169}
170
174 const exprt &bitvector_expr,
175 const array_typet &array_type,
176 const endianness_mapt &endianness_map,
177 const namespacet &ns)
178{
180 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
181
182 const std::size_t total_bits =
184 if(!num_elements.has_value())
185 {
186 if(!subtype_bits.has_value() || *subtype_bits == 0)
188 else
190 }
192 !num_elements.has_value() || !subtype_bits.has_value() ||
194 "subtype width times array size should be total bitvector width");
195
196 exprt::operandst operands;
197 operands.reserve(*num_elements);
198 for(std::size_t i = 0; i < *num_elements; ++i)
199 {
200 if(subtype_bits.has_value())
201 {
202 const std::size_t subtype_bits_int =
204 const auto bounds = map_bounds(
205 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
206 bitvector_typet type =
208 operands.push_back(bv_to_expr(
210 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
211 array_type.element_type(),
212 endianness_map,
213 ns));
214 }
215 else
216 {
217 operands.push_back(bv_to_expr(
218 bitvector_expr, array_type.element_type(), endianness_map, ns));
219 }
220 }
221
222 return array_exprt{std::move(operands), array_type};
223}
224
228 const exprt &bitvector_expr,
230 const endianness_mapt &endianness_map,
231 const namespacet &ns)
232{
233 const std::size_t num_elements =
235 auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
237 !subtype_bits.has_value() ||
240 "subtype width times vector size should be total bitvector width");
241
242 exprt::operandst operands;
243 operands.reserve(num_elements);
244 for(std::size_t i = 0; i < num_elements; ++i)
245 {
246 if(subtype_bits.has_value())
247 {
248 const std::size_t subtype_bits_int =
250 const auto bounds = map_bounds(
251 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
252 bitvector_typet type =
254 operands.push_back(bv_to_expr(
256 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
257 vector_type.element_type(),
258 endianness_map,
259 ns));
260 }
261 else
262 {
263 operands.push_back(bv_to_expr(
264 bitvector_expr, vector_type.element_type(), endianness_map, ns));
265 }
266 }
267
268 return vector_exprt{std::move(operands), vector_type};
269}
270
274 const exprt &bitvector_expr,
276 const endianness_mapt &endianness_map,
277 const namespacet &ns)
278{
279 const std::size_t total_bits =
281 const auto subtype_bits_opt = pointer_offset_bits(complex_type.subtype(), ns);
282 std::size_t subtype_bits;
283 if(subtype_bits_opt.has_value())
284 {
288 "subtype width should be half of the total bitvector width");
289 }
290 else
292
293 const auto bounds_real = map_bounds(endianness_map, 0, subtype_bits - 1);
294 const auto bounds_imag =
295 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
296
297 const bitvector_typet type =
299
300 return complex_exprt{
303 complex_type.subtype(),
304 endianness_map,
305 ns),
308 complex_type.subtype(),
309 endianness_map,
310 ns),
312}
313
328 const exprt &bitvector_expr,
329 const typet &target_type,
330 const endianness_mapt &endianness_map,
331 const namespacet &ns)
332{
334
335 if(
336 can_cast_type<bitvector_typet>(target_type) ||
337 target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
338 target_type.id() == ID_string)
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
347 if(target_type.id() == ID_struct)
348 {
349 return bv_to_struct_expr(
350 bitvector_expr, to_struct_type(target_type), endianness_map, ns);
351 }
352 else if(target_type.id() == ID_struct_tag)
353 {
356 ns.follow_tag(to_struct_tag_type(target_type)),
357 endianness_map,
358 ns);
359 result.type() = target_type;
360 return std::move(result);
361 }
362 else if(target_type.id() == ID_union)
363 {
364 return bv_to_union_expr(
365 bitvector_expr, to_union_type(target_type), endianness_map, ns);
366 }
367 else if(target_type.id() == ID_union_tag)
368 {
371 ns.follow_tag(to_union_tag_type(target_type)),
372 endianness_map,
373 ns);
374 result.type() = target_type;
375 return std::move(result);
376 }
377 else if(target_type.id() == ID_array)
378 {
379 return bv_to_array_expr(
380 bitvector_expr, to_array_type(target_type), endianness_map, ns);
381 }
382 else if(target_type.id() == ID_vector)
383 {
384 return bv_to_vector_expr(
385 bitvector_expr, to_vector_type(target_type), endianness_map, ns);
386 }
387 else if(target_type.id() == ID_complex)
388 {
389 return bv_to_complex_expr(
390 bitvector_expr, to_complex_type(target_type), endianness_map, ns);
391 }
392 else
393 {
395 false, "bv_to_expr does not yet support ", target_type.id_string());
396 }
397}
398
399static exprt unpack_rec(
400 const exprt &src,
401 bool little_endian,
404 const namespacet &ns,
405 bool unpack_byte_array = false);
406
414 const exprt &src,
415 std::size_t lower_bound,
416 std::size_t upper_bound,
417 const namespacet &ns)
418{
419 PRECONDITION(lower_bound <= upper_bound);
420
421 if(src.id() == ID_array)
422 {
423 PRECONDITION(upper_bound <= src.operands().size());
424 return exprt::operandst{
425 src.operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
426 src.operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
427 }
428
429 PRECONDITION(src.type().id() == ID_array || src.type().id() == ID_vector);
434 8);
435 exprt::operandst bytes;
436 bytes.reserve(upper_bound - lower_bound);
437 for(std::size_t i = lower_bound; i < upper_bound; ++i)
438 {
439 const index_exprt idx{src, from_integer(i, c_index_type())};
440 bytes.push_back(simplify_expr(idx, ns));
441 }
442 return bytes;
443}
444
453 const exprt &src,
454 std::size_t el_bytes,
455 bool little_endian,
456 const namespacet &ns)
457{
458 // TODO we either need a symbol table here or make array comprehensions
459 // introduce a scope
460 static std::size_t array_comprehension_index_counter = 0;
463 "$array_comprehension_index_a_v" +
464 std::to_string(array_comprehension_index_counter),
465 c_index_type()};
466
467 index_exprt element{src,
470
471 exprt sub = unpack_rec(element, little_endian, {}, {}, ns, false);
473
474 exprt body = sub_operands.front();
475 const mod_exprt offset{
478 for(std::size_t i = 1; i < el_bytes; ++i)
479 {
480 body = if_exprt{
483 body};
484 }
485
486 const exprt array_vector_size = src.type().id() == ID_vector
487 ? to_vector_type(src.type()).size()
488 : to_array_type(src.type()).size();
489
491 std::move(array_comprehension_index),
492 std::move(body),
496}
497
512 const exprt &src,
515 bool little_endian,
518 const namespacet &ns)
519{
520 const std::size_t el_bytes =
522
523 if(!src_size.has_value() && !max_bytes.has_value())
524 {
526 el_bytes > 0 && element_bits % 8 == 0,
527 "unpacking of arrays with non-byte-aligned elements is not supported");
529 src, el_bytes, little_endian, ns);
530 }
531
534
535 // refine the number of elements to extract in case the element width is known
536 // and a multiple of bytes; otherwise we will expand the entire array/vector
538 if(element_bits > 0 && element_bits % 8 == 0)
539 {
540 if(!num_elements.has_value())
541 {
542 // turn bytes into elements, rounding up
544 }
545
546 if(offset_bytes.has_value())
547 {
548 // compute offset as number of elements
550 // insert offset_bytes-many nil bytes into the output array
551 byte_operands.resize(
553 from_integer(0, bv_typet{8}));
554 }
555 }
556
557 // the maximum number of bytes is an upper bound in case the size of the
558 // array/vector is unknown; if element_bits was usable above this will
559 // have been turned into a number of elements already
560 if(!num_elements)
562
563 const exprt src_simp = simplify_expr(src, ns);
564
566 {
567 exprt element;
568
569 if(
570 (src_simp.id() == ID_array || src_simp.id() == ID_vector) &&
571 i < src_simp.operands().size())
572 {
573 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
574 element = src_simp.operands()[index_int];
575 }
576 else
577 {
579 }
580
581 // recursively unpack each element so that we eventually just have an array
582 // of bytes left
583
586 ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
588 const std::size_t element_max_bytes_int =
590 : el_bytes;
591
592 exprt sub =
593 unpack_rec(element, little_endian, {}, element_max_bytes, ns, true);
596 byte_operands.insert(
597 byte_operands.end(), sub_operands.begin(), sub_operands.end());
598
599 if(max_bytes && byte_operands.size() >= *max_bytes)
600 break;
601 }
602
603 const std::size_t size = byte_operands.size();
604 return array_exprt(
605 std::move(byte_operands),
607}
608
621 std::size_t total_bits,
623 bool little_endian,
626 const namespacet &ns)
627{
630
631 exprt sub =
632 unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns, true);
633
634 dest.insert(
635 dest.end(),
636 std::make_move_iterator(sub.operands().begin()),
637 std::make_move_iterator(sub.operands().end()));
638}
639
650 const exprt &src,
651 bool little_endian,
654 const namespacet &ns)
655{
657 const struct_typet::componentst &components = struct_type.components();
658
662
665 for(auto it = components.begin(); it != components.end(); ++it)
666 {
667 const auto &comp = *it;
668 auto component_bits = pointer_offset_bits(comp.type(), ns);
669
670 // We can only handle a member of unknown width when it is the last member
671 // and is byte-aligned. Members of unknown width in the middle would leave
672 // us with unknown alignment of subsequent members, and queuing them up as
673 // bit fields is not possible either as the total width of the concatenation
674 // could not be determined.
676 component_bits.has_value() ||
677 (std::next(it) == components.end() && !bit_fields.has_value()),
678 "members of non-constant width should come last in a struct");
679
680 member_exprt member(src, comp.get_name(), comp.type());
681 if(src.id() == ID_struct)
682 simplify(member, ns);
683
684 // Is it a byte-aligned member?
685 if(member_offset_bits % 8 == 0)
686 {
687 if(bit_fields.has_value())
688 {
690 std::move(bit_fields->first),
691 bit_fields->second,
693 little_endian,
696 ns);
697 bit_fields.reset();
698 }
699
700 if(offset_bytes.has_value())
701 {
703 // if the offset is negative, offset_in_member remains unset, which has
704 // the same effect as setting it to zero
705 if(*offset_in_member < 0)
706 offset_in_member.reset();
707 }
708
709 if(max_bytes.has_value())
710 {
712 if(*max_bytes_left < 0)
713 break;
714 }
715 }
716
717 if(
718 member_offset_bits % 8 != 0 ||
719 (component_bits.has_value() && *component_bits % 8 != 0))
720 {
721 if(!bit_fields.has_value())
722 bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
723
725 bit_fields->first.insert(
726 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
728 bit_fields->second += bits_int;
729
731
732 continue;
733 }
734
735 INVARIANT(
736 !bit_fields.has_value(),
737 "all preceding members should have been processed");
738
739 exprt sub = unpack_rec(
740 member, little_endian, offset_in_member, max_bytes_left, ns, true);
741
742 byte_operands.insert(
743 byte_operands.end(),
744 std::make_move_iterator(sub.operands().begin()),
745 std::make_move_iterator(sub.operands().end()));
746
747 if(component_bits.has_value())
749 }
750
751 if(bit_fields.has_value())
753 std::move(bit_fields->first),
754 bit_fields->second,
756 little_endian,
759 ns);
760
761 const std::size_t size = byte_operands.size();
762 return array_exprt{std::move(byte_operands),
764}
765
771static array_exprt
772unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
773{
775 const typet &subtype = complex_type.subtype();
776
777 auto subtype_bits = pointer_offset_bits(subtype, ns);
778 CHECK_RETURN(subtype_bits.has_value());
779 CHECK_RETURN(*subtype_bits % 8 == 0);
780
783 little_endian,
784 mp_integer{0},
785 *subtype_bits / 8,
786 ns,
787 true);
788 exprt::operandst byte_operands = std::move(sub_real.operands());
789
792 little_endian,
793 mp_integer{0},
794 *subtype_bits / 8,
795 ns,
796 true);
797 byte_operands.insert(
798 byte_operands.end(),
799 std::make_move_iterator(sub_imag.operands().begin()),
800 std::make_move_iterator(sub_imag.operands().end()));
801
802 const std::size_t size = byte_operands.size();
803 return array_exprt{std::move(byte_operands),
805}
806
816// array of bytes
819 const exprt &src,
820 bool little_endian,
823 const namespacet &ns,
825{
826 if(src.type().id()==ID_array)
827 {
829 const typet &subtype = array_type.element_type();
830
831 auto element_bits = pointer_offset_bits(subtype, ns);
832 CHECK_RETURN(element_bits.has_value());
833
834 if(!unpack_byte_array && *element_bits == 8)
835 return src;
836
838 return unpack_array_vector(
839 src,
842 little_endian,
844 max_bytes,
845 ns);
846 }
847 else if(src.type().id() == ID_vector)
848 {
850 const typet &subtype = vector_type.element_type();
851
852 auto element_bits = pointer_offset_bits(subtype, ns);
853 CHECK_RETURN(element_bits.has_value());
854
855 if(!unpack_byte_array && *element_bits == 8)
856 return src;
857
858 return unpack_array_vector(
859 src,
862 little_endian,
864 max_bytes,
865 ns);
866 }
867 else if(src.type().id() == ID_complex)
868 {
869 return unpack_complex(src, little_endian, ns);
870 }
871 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
872 {
873 return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
874 }
875 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
876 {
877 const union_typet &union_type = to_union_type(ns.follow(src.type()));
878
879 const auto widest_member = union_type.find_widest_union_component(ns);
880
881 if(widest_member.has_value())
882 {
883 member_exprt member{
884 src, widest_member->first.get_name(), widest_member->first.type()};
885 return unpack_rec(
886 member, little_endian, offset_bytes, widest_member->second, ns, true);
887 }
888 }
889 else if(src.type().id() == ID_pointer)
890 {
891 return unpack_rec(
893 little_endian,
895 max_bytes,
896 ns,
898 }
899 else if(src.id() == ID_string_constant)
900 {
901 return unpack_rec(
903 little_endian,
905 max_bytes,
906 ns,
908 }
909 else if(src.id() == ID_constant && src.type().id() == ID_string)
910 {
911 return unpack_rec(
913 little_endian,
915 max_bytes,
916 ns,
918 }
919 else if(src.type().id()!=ID_empty)
920 {
921 // a basic type; we turn that into extractbits while considering
922 // endianness
923 auto bits_opt = pointer_offset_bits(src.type(), ns);
924 DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
925
929
930 if(max_bytes.has_value())
931 {
932 const auto max_bits = *max_bytes * 8;
933 if(little_endian)
934 {
935 last_bit = std::min(last_bit, max_bits);
936 }
937 else
938 {
939 bit_offset = std::max(mp_integer{0}, last_bit - max_bits);
940 }
941 }
942
945 auto const byte_type = bv_typet{8};
947 for(; bit_offset < last_bit; bit_offset += 8)
948 {
953 byte_type);
954
955 // endianness_mapt should be the point of reference for mapping out
956 // endianness, but we need to work on elements here instead of
957 // individual bits
958 if(little_endian)
959 byte_operands.push_back(extractbits);
960 else
961 byte_operands.insert(byte_operands.begin(), extractbits);
962 }
963
964 const std::size_t size = byte_operands.size();
965 return array_exprt(
966 std::move(byte_operands),
968 }
969
970 return array_exprt(
972}
973
985 const byte_extract_exprt &src,
987 const typet &subtype,
989 const namespacet &ns)
990{
992 if(src.type().id() == ID_array)
994 else
996
997 if(num_elements.has_value())
998 {
999 exprt::operandst operands;
1000 operands.reserve(*num_elements);
1001 for(std::size_t i = 0; i < *num_elements; ++i)
1002 {
1004 unpacked.offset(),
1005 from_integer(i * element_bits / 8, unpacked.offset().type()));
1006
1008 tmp.type() = subtype;
1009 tmp.offset() = new_offset;
1010
1011 operands.push_back(lower_byte_extract(tmp, ns));
1012 }
1013
1014 exprt result;
1015 if(src.type().id() == ID_array)
1016 result = array_exprt{std::move(operands), to_array_type(src.type())};
1017 else
1018 result = vector_exprt{std::move(operands), to_vector_type(src.type())};
1019
1020 return simplify_expr(result, ns);
1021 }
1022
1023 DATA_INVARIANT(src.type().id() == ID_array, "vectors have constant size");
1024 const array_typet &array_type = to_array_type(src.type());
1025
1026 // TODO we either need a symbol table here or make array comprehensions
1027 // introduce a scope
1028 static std::size_t array_comprehension_index_counter = 0;
1031 "$array_comprehension_index_a" +
1032 std::to_string(array_comprehension_index_counter),
1033 c_index_type()};
1034
1036 unpacked.offset(),
1038 mult_exprt{
1041 unpacked.offset().type())};
1042
1044 body.type() = subtype;
1045 body.offset() = std::move(new_offset);
1046
1048 lower_byte_extract(body, ns),
1049 array_type};
1050}
1051
1061 const byte_extract_exprt &src,
1063 const namespacet &ns)
1064{
1066 const typet &subtype = complex_type.subtype();
1067
1068 auto subtype_bits = pointer_offset_bits(subtype, ns);
1069 if(!subtype_bits.has_value() || *subtype_bits % 8 != 0)
1070 return {};
1071
1072 // offset remains unchanged
1074 real.type() = subtype;
1075
1076 const plus_exprt new_offset{
1077 unpacked.offset(),
1078 from_integer(*subtype_bits / 8, unpacked.offset().type())};
1080 imag.type() = subtype;
1081 imag.offset() = simplify_expr(new_offset, ns);
1082
1083 return simplify_expr(
1085 lower_byte_extract(real, ns), lower_byte_extract(imag, ns), complex_type},
1086 ns);
1087}
1088
1092{
1093 // General notes about endianness and the bit-vector conversion:
1094 // A single byte with value 0b10001000 is stored (in irept) as
1095 // exactly this string literal, and its bit-vector encoding will be
1096 // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
1097 //
1098 // A multi-byte value like x=256 would be:
1099 // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
1100 // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
1101 // - irept representation: 0000000100000000
1102 // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
1103 // <... 8bits ...> <... 8bits ...>
1104 //
1105 // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
1106 // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
1107 //
1108 // The semantics of byte_extract(endianness, op, offset, T) is:
1109 // interpret ((char*)&op)+offset as the endianness-ordered storage
1110 // of an object of type T at address ((char*)&op)+offset
1111 // For some T x, byte_extract(endianness, x, 0, T) must yield x.
1112 //
1113 // byte_extract for a composite type T or an array will interpret
1114 // the individual subtypes with suitable endianness; the overall
1115 // order of components is not affected by endianness.
1116 //
1117 // Examples:
1118 // unsigned char A[4];
1119 // byte_extract_little_endian(A, 0, unsigned short) requests that
1120 // A[0],A[1] be interpreted as the storage of an unsigned short with
1121 // A[1] being the most-significant byte; byte_extract_big_endian for
1122 // the same operands will select A[0] as the most-significant byte.
1123 //
1124 // int A[2] = {0x01020304,0xDEADBEEF}
1125 // byte_extract_big_endian(A, 0, short) should yield 0x0102
1126 // byte_extract_little_endian(A, 0, short) should yield 0x0304
1127 // To obtain this we first compute byte arrays while taking into
1128 // account endianness:
1129 // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
1130 // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
1131 // We extract the relevant bytes starting from ((char*)A)+0:
1132 // big-endian: {01,02}; little-endian: {04,03}
1133 // Finally we place them in the appropriate byte order as indicated
1134 // by endianness:
1135 // big-endian: (short)concatenation(01,02)=0x0102
1136 // little-endian: (short)concatenation(03,04)=0x0304
1137
1141 const bool little_endian = src.id() == ID_byte_extract_little_endian;
1142
1143 // determine an upper bound of the last byte we might need
1144 auto upper_bound_opt = size_of_expr(src.type(), ns);
1145 if(upper_bound_opt.has_value())
1146 {
1148 plus_exprt(
1149 upper_bound_opt.value(),
1151 src.offset(), upper_bound_opt.value().type())),
1152 ns);
1153 }
1154 else if(src.type().id() == ID_empty)
1156
1158 const auto upper_bound_int_opt =
1160
1162 unpacked.op() = unpack_rec(
1163 src.op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
1166 .get_width() == 8);
1167
1168 if(src.type().id() == ID_array || src.type().id() == ID_vector)
1169 {
1170 const typet &subtype = to_type_with_subtype(src.type()).subtype();
1171
1172 // consider ways of dealing with arrays of unknown subtype size or with a
1173 // subtype size that does not fit byte boundaries; currently we fall back to
1174 // stitching together consecutive elements down below
1175 auto element_bits = pointer_offset_bits(subtype, ns);
1176 if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
1177 {
1179 src, unpacked, subtype, *element_bits, ns);
1180 }
1181 }
1182 else if(src.type().id() == ID_complex)
1183 {
1184 auto result = lower_byte_extract_complex(src, unpacked, ns);
1185 if(result.has_value())
1186 return std::move(*result);
1187
1188 // else fall back to generic lowering that uses bit masks, below
1189 }
1190 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
1191 {
1193 const struct_typet::componentst &components=struct_type.components();
1194
1195 bool failed=false;
1196 struct_exprt s({}, src.type());
1197
1198 for(const auto &comp : components)
1199 {
1200 auto component_bits = pointer_offset_bits(comp.type(), ns);
1201
1202 // the next member would be misaligned, abort
1203 if(
1204 !component_bits.has_value() || *component_bits == 0 ||
1205 *component_bits % 8 != 0)
1206 {
1207 failed=true;
1208 break;
1209 }
1210
1211 auto member_offset_opt =
1212 member_offset_expr(struct_type, comp.get_name(), ns);
1213
1214 if(!member_offset_opt.has_value())
1215 {
1216 failed = true;
1217 break;
1218 }
1219
1221 unpacked.offset(),
1223 member_offset_opt.value(), unpacked.offset().type()));
1224
1226 tmp.type()=comp.type();
1227 tmp.offset()=new_offset;
1228
1230 }
1231
1232 if(!failed)
1233 return simplify_expr(std::move(s), ns);
1234 }
1235 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
1236 {
1237 const union_typet &union_type = to_union_type(ns.follow(src.type()));
1238
1239 const auto widest_member = union_type.find_widest_union_component(ns);
1240
1241 if(widest_member.has_value())
1242 {
1244 tmp.type() = widest_member->first.type();
1245
1246 return union_exprt(
1247 widest_member->first.get_name(),
1249 src.type());
1250 }
1251 }
1252
1253 const exprt &root=unpacked.op();
1254 const exprt &offset=unpacked.offset();
1255
1256 optionalt<typet> subtype;
1257 if(root.type().id() == ID_vector)
1258 subtype = to_vector_type(root.type()).element_type();
1259 else
1260 subtype = to_array_type(root.type()).element_type();
1261
1262 auto subtype_bits = pointer_offset_bits(*subtype, ns);
1263
1265 subtype_bits.has_value() && *subtype_bits == 8,
1266 "offset bits are byte aligned");
1267
1268 auto size_bits = pointer_offset_bits(unpacked.type(), ns);
1269 if(!size_bits.has_value())
1270 {
1271 auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
1272 // all cases with non-constant width should have been handled above
1274 op0_bits.has_value(),
1275 "the extracted width or the source width must be known");
1277 }
1278
1279 mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1280
1281 // get 'width'-many bytes, and concatenate
1284 op.reserve(width_bytes);
1285
1286 for(std::size_t i=0; i<width_bytes; i++)
1287 {
1288 // the most significant byte comes first in the concatenation!
1289 std::size_t offset_int=
1290 little_endian?(width_bytes-i-1):i;
1291
1292 plus_exprt offset_i(from_integer(offset_int, offset.type()), offset);
1293 simplify(offset_i, ns);
1294
1295 mp_integer index = 0;
1296 if(
1297 offset_i.is_constant() &&
1298 (root.id() == ID_array || root.id() == ID_vector) &&
1300 index < root.operands().size() && index >= 0)
1301 {
1302 // offset is constant and in range
1303 op.push_back(root.operands()[numeric_cast_v<std::size_t>(index)]);
1304 }
1305 else
1306 {
1307 op.push_back(index_exprt(root, offset_i));
1308 }
1309 }
1310
1311 if(width_bytes==1)
1312 {
1313 return simplify_expr(
1314 typecast_exprt::conditional_cast(op.front(), src.type()), ns);
1315 }
1316 else // width_bytes>=2
1317 {
1319 std::move(op), adjust_width(*subtype, width_bytes * 8));
1320
1321 endianness_mapt map(concatenation.type(), little_endian, ns);
1322 return bv_to_expr(concatenation, src.type(), map, ns);
1323 }
1324}
1325
1327 const byte_update_exprt &src,
1330 const namespacet &ns);
1331
1342 const byte_update_exprt &src,
1343 const typet &subtype,
1346 const namespacet &ns)
1347{
1348 // TODO we either need a symbol table here or make array comprehensions
1349 // introduce a scope
1350 static std::size_t array_comprehension_index_counter = 0;
1353 "$array_comprehension_index_u_a_v" +
1354 std::to_string(array_comprehension_index_counter),
1355 c_index_type()};
1356
1357 binary_predicate_exprt lower_bound{
1360 ID_lt,
1361 src.offset()};
1362 binary_predicate_exprt upper_bound{
1365 ID_ge,
1367 src.offset(), non_const_update_bound.type()),
1369
1371 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1378 src.offset(), array_comprehension_index.type())}},
1379 subtype)};
1380
1381 return simplify_expr(
1383 std::move(array_comprehension_body),
1384 to_array_type(src.type())},
1385 ns);
1386}
1387
1398 const byte_update_exprt &src,
1399 const typet &subtype,
1402 const namespacet &ns)
1403{
1404 // apply 'array-update-with' num_elements times
1405 exprt result = src.op();
1406
1407 for(std::size_t i = 0; i < value_as_byte_array.operands().size(); ++i)
1408 {
1409 const exprt &element = value_as_byte_array.operands()[i];
1410
1411 const exprt where = simplify_expr(
1412 plus_exprt{src.offset(), from_integer(i, src.offset().type())}, ns);
1413
1414 // skip elements that wouldn't change (skip over typecasts as we might have
1415 // some signed/unsigned char conversions)
1416 const exprt &e = skip_typecast(element);
1417 if(e.id() == ID_index)
1418 {
1420 if(index_expr.array() == src.op() && index_expr.index() == where)
1421 continue;
1422 }
1423
1425 if(non_const_update_bound.has_value())
1426 {
1430 ID_lt,
1432 element,
1433 index_exprt{src.op(), where}},
1434 subtype);
1435 }
1436 else
1438
1439 if(result.id() != ID_with)
1440 result = with_exprt{result, where, update_value};
1441 else
1442 result.add_to_operands(where, update_value);
1443 }
1444
1445 return simplify_expr(std::move(result), ns);
1446}
1447
1464 const byte_update_exprt &src,
1465 const typet &subtype,
1466 const exprt &subtype_size,
1469 const exprt &initial_bytes,
1470 const exprt &first_index,
1472 const namespacet &ns)
1473{
1477
1478 // TODO we either need a symbol table here or make array comprehensions
1479 // introduce a scope
1480 static std::size_t array_comprehension_index_counter = 0;
1483 "$array_comprehension_index_u_a_v_u" +
1484 std::to_string(array_comprehension_index_counter),
1485 c_index_type()};
1486
1487 // all arithmetic uses offset/index types
1488 PRECONDITION(subtype_size.type() == src.offset().type());
1489 PRECONDITION(initial_bytes.type() == src.offset().type());
1490 PRECONDITION(first_index.type() == src.offset().type());
1491
1492 // the bound from where updates start
1493 binary_predicate_exprt lower_bound{
1496 ID_lt,
1497 first_index};
1498
1499 // The actual value of updates other than at the start or end
1506 from_integer(1, first_index.type())}}}};
1509 extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
1510 ns);
1511
1512 // The number of target array/vector elements being replaced, not including
1513 // a possible partial update at the end of the updated range, which is handled
1514 // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
1515 // round up to the nearest multiple of subtype_size.
1520 subtype_size};
1521
1522 // The last element to be updated: first_index + updated_elements - 1
1524 minus_exprt{std::move(updated_elements),
1525 from_integer(1, first_index.type())}};
1526
1527 // The size of a partial update at the end of the updated range, may be zero.
1532 subtype_size};
1533
1534 // The bound where updates end, which is conditional on the partial update
1535 // being empty.
1536 binary_predicate_exprt upper_bound{
1539 ID_ge,
1541 last_index,
1543
1544 // The actual value of a partial update at the end.
1547 src.id(),
1548 index_exprt{src.op(), last_index},
1549 from_integer(0, src.offset().type()),
1553 last_index, subtype_size.type()),
1554 subtype_size},
1556 ns);
1557
1559 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1561 if_exprt{
1564 first_index},
1568 last_index},
1569 std::move(last_update_value),
1570 std::move(update_value)}}};
1571
1572 return simplify_expr(
1574 std::move(array_comprehension_body),
1575 to_array_type(src.type())},
1576 ns);
1577}
1578
1590 const byte_update_exprt &src,
1591 const typet &subtype,
1594 const namespacet &ns)
1595{
1599
1600 // do all arithmetic below using index/offset types - the array theory
1601 // back-end is really picky about indices having the same type
1602 auto subtype_size_opt = size_of_expr(subtype, ns);
1603 CHECK_RETURN(subtype_size_opt.has_value());
1604
1607 subtype_size_opt.value(), src.offset().type()),
1608 ns);
1609
1610 // compute the index of the first element of the array/vector that may be
1611 // updated
1613 simplify(first_index, ns);
1614
1615 // compute the offset within that first element
1617
1618 // compute the number of bytes (from the update value) that are going to be
1619 // consumed for updating the first element
1622 if(non_const_update_bound.has_value())
1623 {
1626 }
1627 else
1628 {
1631 "value should be an array expression if the update bound is constant");
1632 update_bound =
1633 from_integer(value_as_byte_array.operands().size(), initial_bytes.type());
1634 }
1638 update_bound};
1640
1641 // encode the first update: update the original element at first_index with
1642 // initial_bytes-many bytes extracted from value_as_byte_array
1645 src.id(),
1646 index_exprt{src.op(), first_index},
1650 from_integer(0, src.offset().type()),
1652 ns);
1653
1654 if(value_as_byte_array.id() != ID_array)
1655 {
1657 src,
1658 subtype,
1665 ns);
1666 }
1667
1668 // We will update one array/vector element at a time - compute the number of
1669 // update values that will be consumed in each step. If we cannot determine a
1670 // constant value at this time we assume it's at least one byte. The
1671 // byte_extract_exprt within the loop uses the symbolic value (subtype_size),
1672 // we just need to make sure we make progress for the loop to terminate.
1673 std::size_t step_size = 1;
1674 if(subtype_size.is_constant())
1676 // Given the first update already encoded, keep track of the offset into the
1677 // update value. Again, the expressions within the loop use the symbolic
1678 // value, this is just an optimization in case we can determine a constant
1679 // offset.
1680 std::size_t offset = 0;
1681 if(initial_bytes.is_constant())
1683
1685
1686 std::size_t i = 1;
1687 for(; offset + step_size <= value_as_byte_array.operands().size();
1688 offset += step_size, ++i)
1689 {
1690 exprt where = simplify_expr(
1692
1694 plus_exprt{
1697 ns);
1698
1699 exprt element = lower_byte_operators(
1701 src.id(),
1702 index_exprt{src.op(), where},
1703 from_integer(0, src.offset().type()),
1706 std::move(offset_expr),
1708 ns);
1709
1710 result.add_to_operands(std::move(where), std::move(element));
1711 }
1712
1713 // do the tail
1714 if(offset < value_as_byte_array.operands().size())
1715 {
1716 const std::size_t tail_size =
1717 value_as_byte_array.operands().size() - offset;
1718
1719 exprt where = simplify_expr(
1721
1722 exprt element = lower_byte_operators(
1724 src.id(),
1725 index_exprt{src.op(), where},
1726 from_integer(0, src.offset().type()),
1730 from_integer(offset, src.offset().type()),
1732 ns);
1733
1734 result.add_to_operands(std::move(where), std::move(element));
1735 }
1736
1737 return simplify_expr(std::move(result), ns);
1738}
1739
1750 const byte_update_exprt &src,
1751 const typet &subtype,
1754 const namespacet &ns)
1755{
1756 const bool is_array = src.type().id() == ID_array;
1757 exprt size;
1758 if(is_array)
1759 size = to_array_type(src.type()).size();
1760 else
1761 size = to_vector_type(src.type()).size();
1762
1763 auto subtype_bits = pointer_offset_bits(subtype, ns);
1764
1765 // fall back to bytewise updates in all non-constant or dubious cases
1766 if(
1767 !size.is_constant() || !src.offset().is_constant() ||
1768 !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
1770 {
1772 src, subtype, value_as_byte_array, non_const_update_bound, ns);
1773 }
1774
1775 std::size_t num_elements =
1779
1780 exprt::operandst elements;
1781 elements.reserve(num_elements);
1782
1783 std::size_t i = 0;
1784 // copy the prefix not affected by the update
1785 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
1786 elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())});
1787
1788 // the modified elements
1789 for(; i < num_elements &&
1790 i * *subtype_bits <
1791 (offset_bytes + value_as_byte_array.operands().size()) * 8;
1792 ++i)
1793 {
1796 exprt::operandst::const_iterator first =
1797 value_as_byte_array.operands().begin();
1798 exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1799 if(update_offset < 0)
1800 {
1801 INVARIANT(
1802 value_as_byte_array.operands().size() > -update_offset,
1803 "indices past the update should be handled above");
1805 }
1806 else
1807 {
1809 INVARIANT(
1810 update_elements > 0,
1811 "indices before the update should be handled above");
1812 }
1813
1814 if(std::distance(first, end) > update_elements)
1816 exprt::operandst update_values{first, end};
1817 const std::size_t update_size = update_values.size();
1818
1819 const byte_update_exprt bu{
1820 src.id(),
1821 index_exprt{src.op(), from_integer(i, c_index_type())},
1822 from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
1824 std::move(update_values),
1826 elements.push_back(lower_byte_operators(bu, ns));
1827 }
1828
1829 // copy the tail not affected by the update
1830 for(; i < num_elements; ++i)
1831 elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())});
1832
1833 if(is_array)
1834 return simplify_expr(
1835 array_exprt{std::move(elements), to_array_type(src.type())}, ns);
1836 else
1837 return simplify_expr(
1838 vector_exprt{std::move(elements), to_vector_type(src.type())}, ns);
1839}
1840
1851 const byte_update_exprt &src,
1855 const namespacet &ns)
1856{
1860
1861 exprt::operandst elements;
1862 elements.reserve(struct_type.components().size());
1863
1865 for(const auto &comp : struct_type.components())
1866 {
1867 auto element_width = pointer_offset_bits(comp.type(), ns);
1868
1869 exprt member = member_exprt{src.op(), comp.get_name(), comp.type()};
1870
1871 // compute the update offset relative to this struct member - will be
1872 // negative if we are already in the middle of the update or beyond it
1873 exprt offset = simplify_expr(
1874 minus_exprt{src.offset(),
1876 ns);
1878 // we don't need to update anything when
1879 // 1) the update offset is greater than the end of this member (thus the
1880 // relative offset is greater than this element) or
1881 // 2) the update offset plus the size of the update is less than the member
1882 // offset
1883 if(
1884 offset_bytes.has_value() &&
1885 (*offset_bytes * 8 >= *element_width ||
1886 (value_as_byte_array.id() == ID_array && *offset_bytes < 0 &&
1887 -*offset_bytes >= value_as_byte_array.operands().size())))
1888 {
1889 elements.push_back(std::move(member));
1891 continue;
1892 }
1893 else if(!offset_bytes.has_value())
1894 {
1895 // The offset to update is not constant; abort the attempt to update
1896 // indiviual struct members and instead turn the operand-to-be-updated
1897 // into a byte array, which we know how to update even if the offset is
1898 // non-constant.
1899 auto src_size_opt = size_of_expr(src.type(), ns);
1900 CHECK_RETURN(src_size_opt.has_value());
1901
1904 src.op(),
1905 from_integer(0, src.offset().type()),
1906 array_typet{bv_typet{8}, src_size_opt.value()}};
1907
1908 byte_update_exprt bu = src;
1910 bu.type() = bu.op().type();
1911
1912 return lower_byte_extract(
1917 from_integer(0, src.offset().type()),
1918 src.type()},
1919 ns);
1920 }
1921
1922 // We now need to figure out how many bytes to consume from the update
1923 // value. If the size of the update is unknown, then we need to leave some
1924 // of this work to a back-end solver via the non_const_update_bound branch
1925 // below.
1927 std::size_t first = 0;
1928 if(*offset_bytes < 0)
1929 {
1930 offset = from_integer(0, src.offset().type());
1931 INVARIANT(
1932 value_as_byte_array.id() != ID_array ||
1933 value_as_byte_array.operands().size() > -*offset_bytes,
1934 "members past the update should be handled above");
1936 }
1937 else
1938 {
1940 INVARIANT(
1941 update_elements > 0,
1942 "members before the update should be handled above");
1943 }
1944
1945 // Now that we have an idea on how many bytes we need from the update value,
1946 // determine the exact range [first, end) in the update value, and create
1947 // that sequence of bytes (via instantiate_byte_array).
1948 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1949 if(value_as_byte_array.id() == ID_array)
1950 end = std::min(end, value_as_byte_array.operands().size());
1953 const std::size_t update_size = update_values.size();
1954
1955 // With an upper bound on the size of the update established, construct the
1956 // actual update expression. If the exact size of the update is unknown,
1957 // make the size expression conditional.
1962 if(non_const_update_bound.has_value())
1963 {
1964 // The size of the update is not constant, and thus is to be symbolically
1965 // bound; first see how many bytes we have left in the update:
1966 // non_const_update_bound > first ? non_const_update_bound - first: 0
1968 if_exprt{
1971 ID_gt,
1972 from_integer(first, non_const_update_bound->type())},
1974 from_integer(first, non_const_update_bound->type())},
1976 size_type());
1977 // Now take the minimum of update-bytes-left and the previously computed
1978 // size of the member to be updated:
1985 }
1986
1987 // We have established the bytes to use for the update, but now need to
1988 // account for sub-byte members.
1989 const std::size_t shift =
1991 const std::size_t element_bits_int =
1993
1994 const bool little_endian = src.id() == ID_byte_update_little_endian;
1995 if(shift != 0)
1996 {
1997 member = concatenation_exprt{
1999 from_integer(0, bv_typet{shift}),
2000 bv_typet{shift + element_bits_int}};
2001
2002 if(!little_endian)
2003 to_concatenation_expr(member).op0().swap(
2004 to_concatenation_expr(member).op1());
2005 }
2006
2007 // Finally construct the updated member.
2008 byte_update_exprt bu{src.id(), std::move(member), offset, update_expr};
2011
2012 if(shift == 0)
2013 elements.push_back(updated_element);
2014 else
2015 {
2016 elements.push_back(typecast_exprt::conditional_cast(
2018 element_bits_int - 1 + (little_endian ? shift : 0),
2019 (little_endian ? shift : 0),
2021 comp.type()));
2022 }
2023
2025 }
2026
2027 return simplify_expr(struct_exprt{std::move(elements), struct_type}, ns);
2028}
2029
2040 const byte_update_exprt &src,
2041 const union_typet &union_type,
2044 const namespacet &ns)
2045{
2046 const auto widest_member = union_type.find_widest_union_component(ns);
2047
2049 widest_member.has_value(),
2050 "lower_byte_update of union of unknown size is not supported");
2051
2052 byte_update_exprt bu = src;
2053 bu.set_op(member_exprt{
2054 src.op(), widest_member->first.get_name(), widest_member->first.type()});
2055 bu.type() = widest_member->first.type();
2056
2057 return union_exprt{
2058 widest_member->first.get_name(),
2060 src.type()};
2061}
2062
2072 const byte_update_exprt &src,
2075 const namespacet &ns)
2076{
2077 if(src.type().id() == ID_array || src.type().id() == ID_vector)
2078 {
2079 optionalt<typet> subtype;
2080 if(src.type().id() == ID_vector)
2081 subtype = to_vector_type(src.type()).element_type();
2082 else
2083 subtype = to_array_type(src.type()).element_type();
2084
2085 auto element_width = pointer_offset_bits(*subtype, ns);
2086 CHECK_RETURN(element_width.has_value());
2088 CHECK_RETURN(*element_width % 8 == 0);
2089
2090 if(*element_width == 8)
2091 {
2092 if(value_as_byte_array.id() != ID_array)
2093 {
2095 non_const_update_bound.has_value(),
2096 "constant update bound should yield an array expression");
2098 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2099 }
2100
2102 src,
2103 *subtype,
2106 ns);
2107 }
2108 else
2110 src, *subtype, value_as_byte_array, non_const_update_bound, ns);
2111 }
2112 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
2113 {
2115 src,
2116 to_struct_type(ns.follow(src.type())),
2119 ns);
2120 result.type() = src.type();
2121 return result;
2122 }
2123 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
2124 {
2126 src,
2127 to_union_type(ns.follow(src.type())),
2130 ns);
2131 result.type() = src.type();
2132 return result;
2133 }
2134 else if(
2136 src.type().id() == ID_c_enum || src.type().id() == ID_c_enum_tag)
2137 {
2138 // mask out the bits to be updated, shift the value according to the
2139 // offset and bit-or
2140 const auto type_width = pointer_offset_bits(src.type(), ns);
2141 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2142 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2143
2145 if(value_as_byte_array.id() == ID_array)
2146 update_bytes = value_as_byte_array.operands();
2147 else
2148 {
2149 update_bytes =
2151 }
2152
2153 const std::size_t update_size_bits = update_bytes.size() * 8;
2154 const std::size_t bit_width = std::max(type_bits, update_size_bits);
2155
2156 const bool is_little_endian = src.id() == ID_byte_update_little_endian;
2157
2159 typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
2160 if(bit_width > type_bits)
2161 {
2162 val_before =
2164 val_before,
2165 bv_typet{bit_width}};
2166
2167 if(!is_little_endian)
2169 .op0()
2171 }
2172
2173 if(non_const_update_bound.has_value())
2174 {
2176 val_before,
2178 mp_integer{0},
2179 mp_integer{update_bytes.size()},
2180 ns);
2182 CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
2183 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2184 {
2185 update_bytes[i] =
2188 ID_lt,
2190 update_bytes[i],
2191 src_as_bytes.operands()[i]};
2192 }
2193 }
2194
2195 // build mask
2196 exprt mask;
2198 mask = from_integer(power(2, update_size_bits) - 1, bv_typet{bit_width});
2199 else
2200 {
2201 mask = from_integer(
2202 power(2, bit_width) - power(2, bit_width - update_size_bits),
2203 bv_typet{bit_width});
2204 }
2205
2206 const typet &offset_type = src.offset().type();
2208
2211
2215 if(!is_little_endian)
2216 mask_shifted.true_case().swap(mask_shifted.false_case());
2217
2218 // original_bits &= ~mask
2220
2221 // concatenate and zero-extend the value
2224 std::reverse(value.operands().begin(), value.operands().end());
2225
2227 if(bit_width > update_size_bits)
2228 {
2230 from_integer(0, bv_typet{bit_width - update_size_bits}),
2231 value,
2232 bv_typet{bit_width}};
2233
2234 if(!is_little_endian)
2236 .op0()
2238 }
2239 else
2240 zero_extended = value;
2241
2242 // shift the value
2246 if(!is_little_endian)
2247 value_shifted.true_case().swap(value_shifted.false_case());
2248
2249 // original_bits |= newvalue
2251
2252 if(bit_width > type_bits)
2253 {
2254 endianness_mapt endianness_map(
2255 bitor_expr.type(), src.id() == ID_byte_update_little_endian, ns);
2256 const auto bounds = map_bounds(endianness_map, 0, type_bits - 1);
2257
2258 return simplify_expr(
2262 src.type()),
2263 ns);
2264 }
2265
2266 return simplify_expr(
2268 }
2269 else
2270 {
2272 false, "lower_byte_update does not yet support ", src.type().id_string());
2273 }
2274}
2275
2277{
2281 "byte update expression should either be little or big endian");
2282
2283 // An update of a void-typed object or update by a void-typed value is the
2284 // source operand (this is questionable, but may arise when dereferencing
2285 // invalid pointers).
2286 if(src.type().id() == ID_empty || src.value().type().id() == ID_empty)
2287 return src.op();
2288
2289 // byte_update lowering proceeds as follows:
2290 // 1) Determine the size of the update, with the size of the object to be
2291 // updated as an upper bound. We fail if neither can be determined.
2292 // 2) Turn the update value into a byte array of the size determined above.
2293 // 3) If the offset is not constant, turn the object into a byte array, and
2294 // use a "with" expression to encode the update; else update the values in
2295 // place.
2296 // 4) Construct a new object.
2298 // update value, may require extension to full bytes
2299 exprt update_value = src.value();
2302 simplify(update_size_expr_opt.value(), ns);
2303
2304 if(!update_size_expr_opt.value().is_constant())
2306 else
2307 {
2308 auto update_bits = pointer_offset_bits(update_value.type(), ns);
2309 // If the following invariant fails, then the type was only found to be
2310 // constant via simplification. Such instances should be fixed at the place
2311 // introducing these constant-but-not-constant_exprt type sizes.
2313 update_bits.has_value(), "constant size-of should imply fixed bit width");
2315
2316 if(update_bits_int % 8 != 0)
2317 {
2320 "non-byte aligned type expected to be a bitvector type");
2321 size_t n_extra_bits = 8 - update_bits_int % 8;
2322
2323 endianness_mapt endianness_map(
2324 src.op().type(), src.id() == ID_byte_update_little_endian, ns);
2325 const auto bounds = map_bounds(
2326 endianness_map, update_bits_int, update_bits_int + n_extra_bits - 1);
2328 src.op(), bounds.ub, bounds.lb, bv_typet{n_extra_bits}};
2329
2333 extra_bits,
2335 }
2336 else
2337 {
2340 }
2341 }
2342
2346
2350 from_integer(0, src.offset().type()),
2352
2354
2355 exprt result =
2357 return result;
2358}
2359
2360bool has_byte_operator(const exprt &src)
2361{
2362 if(src.id()==ID_byte_update_little_endian ||
2366 return true;
2367
2368 forall_operands(it, src)
2369 if(has_byte_operator(*it))
2370 return true;
2371
2372 return false;
2373}
2374
2376{
2377 exprt tmp=src;
2378
2379 // destroys any sharing, should use hash table
2380 Forall_operands(it, tmp)
2381 {
2382 *it = lower_byte_operators(*it, ns);
2383 }
2384
2385 if(src.id()==ID_byte_update_little_endian ||
2388 else if(src.id()==ID_byte_extract_little_endian ||
2391 else
2392 return tmp;
2393}
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 concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet size_type()
Definition c_types.cpp:68
bitvector_typet c_index_type()
Definition c_types.cpp:16
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:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:302
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:202
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3182
Array constructor from list of elements.
Definition std_expr.h:1476
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:643
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition std_types.h:853
std::size_t get_width() const
Definition std_types.h:864
Fixed-width bit-vector without numerical interpretation.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
const exprt & op() 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:1761
Imaginary part of the expression describing a complex number.
Definition std_expr.h:1874
Real part of the expression describing a complex number.
Definition std_expr.h:1829
Complex numbers made of pair of given subtype.
Definition std_types.h:1057
Concatenation of bit-vector operands.
A constant literal expression.
Definition std_expr.h:2807
Division.
Definition std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
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:1225
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition expr.cpp:26
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:136
Extracts a sub-range of a bit-vector operand.
The trinary if-then-else operator.
Definition std_expr.h:2226
Array index operator.
Definition std_expr.h:1328
const std::string & id_string() const
Definition irep.h:399
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
Logical right shift.
Extract member of struct or union.
Definition std_expr.h:2667
Binary minus.
Definition std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition std_expr.h:1019
exprt & op0()
Definition std_expr.h:844
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
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:2874
Boolean OR.
Definition std_expr.h:2082
The plus expression Associativity is not specified.
Definition std_expr.h:914
Left shift.
Fixed-width bit-vector with two's complement interpretation.
Struct constructor from list of elements.
Definition std_expr.h:1722
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:80
const typet & subtype() const
Definition type.h:156
Semantic type conversion.
Definition std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1611
The union type.
Definition c_types.h:125
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Definition std_expr.h:1575
The vector type.
Definition std_types.h:996
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1006
Operator to update elements in structs and arrays.
Definition std_expr.h:2312
#define forall_operands(it, expr)
Definition expr.h:18
#define Forall_operands(it, expr)
Definition expr.h:25
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
STL namespace.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, const namespacet &ns)
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
static exprt lower_byte_update_byte_array_vector(const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte array value_as_byte_array as updat...
static array_exprt unpack_struct(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
static exprt bv_to_expr(const exprt &bitvector_expr, const typet &target_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an expression of type target_type.
static complex_exprt bv_to_complex_expr(const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.
static exprt lower_byte_update_struct(const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a struct typed operand using the byte array value_as_byte_array as update ...
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
static optionalt< exprt > lower_byte_extract_complex(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components t...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
static array_exprt unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
static vector_exprt bv_to_vector_expr(const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.
static exprt lower_byte_update_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
static struct_exprt bv_to_struct_expr(const exprt &bitvector_expr, const struct_typet &struct_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a struct-typed expression.
static union_exprt bv_to_union_expr(const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a union-typed expression.
bool has_byte_operator(const exprt &src)
static array_exprt bv_to_array_expr(const exprt &bitvector_expr, const array_typet &array_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to an array-typed expression.
static boundst map_bounds(const endianness_mapt &endianness_map, std::size_t lower_bound, std::size_t upper_bound)
Map bit boundaries according to endianness.
static exprt lower_byte_update_union(const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to a union typed operand using the byte array value_as_byte_array as update v...
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
static exprt lower_byte_extract_array_vector(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const typet &subtype, const mp_integer &element_bits, const namespacet &ns)
Rewrite a byte extraction of an array/vector-typed result to byte extraction of the individual compon...
static exprt unpack_array_vector(const exprt &src, const optionalt< mp_integer > &src_size, const mp_integer &element_bits, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Rewrite an array or vector into its individual bytes.
static exprt unpack_rec(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const namespacet &ns)
Build the individual bytes to be used in an update.
static exprt lower_byte_update_byte_array_vector_non_const(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector of bytes using the byte-array typed expression value_as_by...
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src to an array/vector typed operand using the byte array value_as_byte_array as ...
static exprt lower_byte_update_array_vector_unbounded(const byte_update_exprt &src, const typet &subtype, const exprt &subtype_size, const exprt &value_as_byte_array, const exprt &non_const_update_bound, const exprt &initial_bytes, const exprt &first_index, const exprt &first_update_value, const namespacet &ns)
Apply a byte update src to an array/vector typed operand, using the byte array value_as_byte_array as...
static void process_bit_fields(exprt::operandst &&bit_fields, std::size_t total_bits, exprt::operandst &dest, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
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:510
#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:1391
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1506
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1040
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:474
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1082
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
const string_constantt & to_string_constant(const exprt &expr)
std::size_t lb
std::size_t ub
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177