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
60bitvector_typet adjust_width(const typet &src, std::size_t new_width)
61{
62 if(src.id() == ID_unsignedbv)
63 return unsignedbv_typet(new_width);
64 else if(src.id() == ID_signedbv)
65 return signedbv_typet(new_width);
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,
81 const struct_typet &struct_type,
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())
95 component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
96 else
97 component_bits = to_bitvector_type(bitvector_expr.type()).get_width() -
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,
109 member_offset_bits + component_bits - 1);
110 bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
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())
118 member_offset_bits += component_bits;
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())
136 return union_exprt{irep_idt{}, nil_exprt{}, union_type};
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())
142 component_bits = numeric_cast_v<std::size_t>(widest_member->second);
143 else
144 component_bits = to_bitvector_type(bitvector_expr.type()).get_width();
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);
154 bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
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{
179 auto num_elements = numeric_cast<std::size_t>(array_type.size());
180 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
181
182 const std::size_t total_bits =
183 to_bitvector_type(bitvector_expr.type()).get_width();
184 if(!num_elements.has_value())
185 {
186 if(!subtype_bits.has_value() || *subtype_bits == 0)
187 num_elements = total_bits;
188 else
189 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
190 }
192 !num_elements.has_value() || !subtype_bits.has_value() ||
193 *subtype_bits * *num_elements == total_bits,
194 "subtype width times array size should be total bitvector width");
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 =
203 numeric_cast_v<std::size_t>(*subtype_bits);
204 const auto bounds = map_bounds(
205 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
206 bitvector_typet type =
207 adjust_width(bitvector_expr.type(), subtype_bits_int);
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,
229 const vector_typet &vector_type,
230 const endianness_mapt &endianness_map,
231 const namespacet &ns)
232{
233 const std::size_t num_elements =
234 numeric_cast_v<std::size_t>(vector_type.size());
235 auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
237 !subtype_bits.has_value() ||
238 *subtype_bits * num_elements ==
239 to_bitvector_type(bitvector_expr.type()).get_width(),
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 =
249 numeric_cast_v<std::size_t>(*subtype_bits);
250 const auto bounds = map_bounds(
251 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
252 bitvector_typet type =
253 adjust_width(bitvector_expr.type(), subtype_bits_int);
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,
275 const complex_typet &complex_type,
276 const endianness_mapt &endianness_map,
277 const namespacet &ns)
278{
279 const std::size_t total_bits =
280 to_bitvector_type(bitvector_expr.type()).get_width();
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 {
285 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
287 subtype_bits * 2 == total_bits,
288 "subtype width should be half of the total bitvector width");
289 }
290 else
291 subtype_bits = total_bits / 2;
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 =
298 adjust_width(bitvector_expr.type(), subtype_bits);
299
300 return complex_exprt{
302 extractbits_exprt{bitvector_expr, bounds_real.ub, bounds_real.lb, type},
303 complex_type.subtype(),
304 endianness_map,
305 ns),
307 extractbits_exprt{bitvector_expr, bounds_imag.ub, bounds_imag.lb, type},
308 complex_type.subtype(),
309 endianness_map,
310 ns),
311 complex_type};
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 =
342 typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width});
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 {
355 bitvector_expr,
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 {
370 bitvector_expr,
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,
402 const optionalt<mp_integer> &offset_bytes,
403 const optionalt<mp_integer> &max_bytes,
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;
461 ++array_comprehension_index_counter;
462 symbol_exprt array_comprehension_index{
463 "$array_comprehension_index_a_v" +
464 std::to_string(array_comprehension_index_counter),
465 c_index_type()};
466
467 index_exprt element{src,
468 div_exprt{array_comprehension_index,
469 from_integer(el_bytes, c_index_type())}};
470
471 exprt sub = unpack_rec(element, little_endian, {}, {}, ns, false);
472 exprt::operandst sub_operands = instantiate_byte_array(sub, 0, el_bytes, ns);
473
474 exprt body = sub_operands.front();
475 const mod_exprt offset{
476 array_comprehension_index,
477 from_integer(el_bytes, array_comprehension_index.type())};
478 for(std::size_t i = 1; i < el_bytes; ++i)
479 {
480 body = if_exprt{
481 equal_exprt{offset, from_integer(i, array_comprehension_index.type())},
482 sub_operands[i],
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),
494 mult_exprt{array_vector_size,
495 from_integer(el_bytes, array_vector_size.type())}}};
496}
497
512 const exprt &src,
513 const optionalt<mp_integer> &src_size,
514 const mp_integer &element_bits,
515 bool little_endian,
516 const optionalt<mp_integer> &offset_bytes,
517 const optionalt<mp_integer> &max_bytes,
518 const namespacet &ns)
519{
520 const std::size_t el_bytes =
521 numeric_cast_v<std::size_t>((element_bits + 7) / 8);
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
532 exprt::operandst byte_operands;
533 mp_integer first_element = 0;
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
537 optionalt<mp_integer> num_elements = src_size;
538 if(element_bits > 0 && element_bits % 8 == 0)
539 {
540 if(!num_elements.has_value())
541 {
542 // turn bytes into elements, rounding up
543 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
544 }
545
546 if(offset_bytes.has_value())
547 {
548 // compute offset as number of elements
549 first_element = *offset_bytes / el_bytes;
550 // insert offset_bytes-many nil bytes into the output array
551 byte_operands.resize(
552 numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
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)
561 num_elements = *max_bytes;
562
563 const exprt src_simp = simplify_expr(src, ns);
564
565 for(mp_integer i = first_element; i < *num_elements; ++i)
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 {
578 element = index_exprt(src_simp, from_integer(i, c_index_type()));
579 }
580
581 // recursively unpack each element so that we eventually just have an array
582 // of bytes left
583
584 const optionalt<mp_integer> element_max_bytes =
585 max_bytes
586 ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
588 const std::size_t element_max_bytes_int =
589 element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
590 : el_bytes;
591
592 exprt sub =
593 unpack_rec(element, little_endian, {}, element_max_bytes, ns, true);
594 exprt::operandst sub_operands =
595 instantiate_byte_array(sub, 0, element_max_bytes_int, ns);
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
620 exprt::operandst &&bit_fields,
621 std::size_t total_bits,
622 exprt::operandst &dest,
623 bool little_endian,
624 const optionalt<mp_integer> &offset_bytes,
625 const optionalt<mp_integer> &max_bytes,
626 const namespacet &ns)
627{
628 const concatenation_exprt concatenation{std::move(bit_fields),
629 bv_typet{total_bits}};
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,
652 const optionalt<mp_integer> &offset_bytes,
653 const optionalt<mp_integer> &max_bytes,
654 const namespacet &ns)
655{
656 const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
657 const struct_typet::componentst &components = struct_type.components();
658
659 optionalt<mp_integer> offset_in_member;
660 optionalt<mp_integer> max_bytes_left;
662
664 exprt::operandst byte_operands;
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,
692 byte_operands,
693 little_endian,
694 offset_in_member,
695 max_bytes_left,
696 ns);
697 bit_fields.reset();
698 }
699
700 if(offset_bytes.has_value())
701 {
702 offset_in_member = *offset_bytes - member_offset_bits / 8;
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 {
711 max_bytes_left = *max_bytes - member_offset_bits / 8;
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
724 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
725 bit_fields->first.insert(
726 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
727 typecast_exprt::conditional_cast(member, bv_typet{bits_int}));
728 bit_fields->second += bits_int;
729
730 member_offset_bits += *component_bits;
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())
748 member_offset_bits += *component_bits;
749 }
750
751 if(bit_fields.has_value())
753 std::move(bit_fields->first),
754 bit_fields->second,
755 byte_operands,
756 little_endian,
757 offset_in_member,
758 max_bytes_left,
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{
774 const complex_typet &complex_type = to_complex_type(src.type());
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
781 exprt sub_real = unpack_rec(
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
790 exprt sub_imag = unpack_rec(
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,
821 const optionalt<mp_integer> &offset_bytes,
822 const optionalt<mp_integer> &max_bytes,
823 const namespacet &ns,
824 bool unpack_byte_array)
825{
826 if(src.type().id()==ID_array)
827 {
828 const array_typet &array_type=to_array_type(src.type());
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
837 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.size());
838 return unpack_array_vector(
839 src,
840 constant_size_opt,
841 *element_bits,
842 little_endian,
843 offset_bytes,
844 max_bytes,
845 ns);
846 }
847 else if(src.type().id() == ID_vector)
848 {
849 const vector_typet &vector_type = to_vector_type(src.type());
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,
860 numeric_cast_v<mp_integer>(vector_type.size()),
861 *element_bits,
862 little_endian,
863 offset_bytes,
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,
894 offset_bytes,
895 max_bytes,
896 ns,
897 unpack_byte_array);
898 }
899 else if(src.id() == ID_string_constant)
900 {
901 return unpack_rec(
903 little_endian,
904 offset_bytes,
905 max_bytes,
906 ns,
907 unpack_byte_array);
908 }
909 else if(src.id() == ID_constant && src.type().id() == ID_string)
910 {
911 return unpack_rec(
913 little_endian,
914 offset_bytes,
915 max_bytes,
916 ns,
917 unpack_byte_array);
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
926 const mp_integer total_bits = *bits_opt;
927 mp_integer last_bit = total_bits;
928 mp_integer bit_offset = 0;
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
943 auto const src_as_bitvector = typecast_exprt::conditional_cast(
944 src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
945 auto const byte_type = bv_typet{8};
946 exprt::operandst byte_operands;
947 for(; bit_offset < last_bit; bit_offset += 8)
948 {
949 extractbits_exprt extractbits(
950 src_as_bitvector,
951 from_integer(bit_offset + 7, c_index_type()),
952 from_integer(bit_offset, c_index_type()),
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,
986 const byte_extract_exprt &unpacked,
987 const typet &subtype,
988 const mp_integer &element_bits,
989 const namespacet &ns)
990{
991 optionalt<std::size_t> num_elements;
992 if(src.type().id() == ID_array)
993 num_elements = numeric_cast<std::size_t>(to_array_type(src.type()).size());
994 else
995 num_elements = numeric_cast<std::size_t>(to_vector_type(src.type()).size());
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 {
1003 plus_exprt new_offset(
1004 unpacked.offset(),
1005 from_integer(i * element_bits / 8, unpacked.offset().type()));
1006
1007 byte_extract_exprt tmp(unpacked);
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;
1029 ++array_comprehension_index_counter;
1030 symbol_exprt array_comprehension_index{
1031 "$array_comprehension_index_a" +
1032 std::to_string(array_comprehension_index_counter),
1033 c_index_type()};
1034
1035 plus_exprt new_offset{
1036 unpacked.offset(),
1038 mult_exprt{
1039 array_comprehension_index,
1040 from_integer(element_bits / 8, array_comprehension_index.type())},
1041 unpacked.offset().type())};
1042
1043 byte_extract_exprt body(unpacked);
1044 body.type() = subtype;
1045 body.offset() = std::move(new_offset);
1046
1047 return array_comprehension_exprt{std::move(array_comprehension_index),
1048 lower_byte_extract(body, ns),
1049 array_type};
1050}
1051
1061 const byte_extract_exprt &src,
1062 const byte_extract_exprt &unpacked,
1063 const namespacet &ns)
1064{
1065 const complex_typet &complex_type = to_complex_type(src.type());
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
1073 byte_extract_exprt real{unpacked};
1074 real.type() = subtype;
1075
1076 const plus_exprt new_offset{
1077 unpacked.offset(),
1078 from_integer(*subtype_bits / 8, unpacked.offset().type())};
1079 byte_extract_exprt imag{unpacked};
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
1139 src.id() == ID_byte_extract_little_endian ||
1140 src.id() == ID_byte_extract_big_endian);
1141 const bool little_endian = src.id() == ID_byte_extract_little_endian;
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 {
1147 upper_bound_opt = simplify_expr(
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)
1155 upper_bound_opt = from_integer(0, size_type());
1156
1157 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.offset());
1158 const auto upper_bound_int_opt =
1159 numeric_cast<mp_integer>(upper_bound_opt.value_or(nil_exprt()));
1160
1161 byte_extract_exprt unpacked(src);
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 {
1192 const struct_typet &struct_type=to_struct_type(ns.follow(src.type()));
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
1220 plus_exprt new_offset(
1221 unpacked.offset(),
1223 member_offset_opt.value(), unpacked.offset().type()));
1224
1225 byte_extract_exprt tmp(unpacked);
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 {
1243 byte_extract_exprt tmp(unpacked);
1244 tmp.type() = widest_member->first.type();
1245
1246 return union_exprt(
1247 widest_member->first.get_name(),
1248 lower_byte_extract(tmp, ns),
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");
1276 size_bits = op0_bits;
1277 }
1278
1279 mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1280
1281 // get 'width'-many bytes, and concatenate
1282 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
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) &&
1299 !to_integer(to_constant_expr(offset_i), index) &&
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 {
1318 concatenation_exprt concatenation(
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,
1328 const exprt &value_as_byte_array,
1329 const optionalt<exprt> &non_const_update_bound,
1330 const namespacet &ns);
1331
1342 const byte_update_exprt &src,
1343 const typet &subtype,
1344 const exprt &value_as_byte_array,
1345 const exprt &non_const_update_bound,
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;
1351 ++array_comprehension_index_counter;
1352 symbol_exprt array_comprehension_index{
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{
1359 array_comprehension_index, src.offset().type()),
1360 ID_lt,
1361 src.offset()};
1362 binary_predicate_exprt upper_bound{
1364 array_comprehension_index, non_const_update_bound.type()),
1365 ID_ge,
1367 src.offset(), non_const_update_bound.type()),
1368 non_const_update_bound}};
1369
1370 if_exprt array_comprehension_body{
1371 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1372 index_exprt{src.op(), array_comprehension_index},
1375 value_as_byte_array,
1376 minus_exprt{array_comprehension_index,
1378 src.offset(), array_comprehension_index.type())}},
1379 subtype)};
1380
1381 return simplify_expr(
1382 array_comprehension_exprt{array_comprehension_index,
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,
1400 const array_exprt &value_as_byte_array,
1401 const optionalt<exprt> &non_const_update_bound,
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 {
1419 const index_exprt &index_expr = to_index_expr(e);
1420 if(index_expr.array() == src.op() && index_expr.index() == where)
1421 continue;
1422 }
1423
1424 exprt update_value;
1425 if(non_const_update_bound.has_value())
1426 {
1427 update_value = typecast_exprt::conditional_cast(
1429 from_integer(i, non_const_update_bound->type()),
1430 ID_lt,
1431 *non_const_update_bound},
1432 element,
1433 index_exprt{src.op(), where}},
1434 subtype);
1435 }
1436 else
1437 update_value = typecast_exprt::conditional_cast(element, subtype);
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,
1467 const exprt &value_as_byte_array,
1468 const exprt &non_const_update_bound,
1469 const exprt &initial_bytes,
1470 const exprt &first_index,
1471 const exprt &first_update_value,
1472 const namespacet &ns)
1473{
1474 const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1475 ? ID_byte_extract_little_endian
1476 : ID_byte_extract_big_endian;
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;
1481 ++array_comprehension_index_counter;
1482 symbol_exprt array_comprehension_index{
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{
1495 array_comprehension_index, first_index.type()),
1496 ID_lt,
1497 first_index};
1498
1499 // The actual value of updates other than at the start or end
1500 plus_exprt offset_expr{
1501 initial_bytes,
1502 mult_exprt{subtype_size,
1504 array_comprehension_index, first_index.type()),
1505 plus_exprt{first_index,
1506 from_integer(1, first_index.type())}}}};
1507 exprt update_value = lower_byte_extract(
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.
1516 div_exprt updated_elements{
1518 non_const_update_bound, subtype_size.type()),
1519 minus_exprt{subtype_size, from_integer(1, subtype_size.type())}},
1520 subtype_size};
1521
1522 // The last element to be updated: first_index + updated_elements - 1
1523 plus_exprt last_index{first_index,
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.
1528 mod_exprt tail_size{
1530 non_const_update_bound, initial_bytes.type()),
1531 initial_bytes},
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{
1538 array_comprehension_index, last_index.type()),
1539 ID_ge,
1540 if_exprt{equal_exprt{tail_size, from_integer(0, tail_size.type())},
1541 last_index,
1542 plus_exprt{last_index, from_integer(1, last_index.type())}}};
1543
1544 // The actual value of a partial update at the end.
1545 exprt last_update_value = lower_byte_operators(
1547 src.id(),
1548 index_exprt{src.op(), last_index},
1549 from_integer(0, src.offset().type()),
1550 byte_extract_exprt{extract_opcode,
1551 value_as_byte_array,
1553 last_index, subtype_size.type()),
1554 subtype_size},
1555 array_typet{bv_typet{8}, tail_size}}},
1556 ns);
1557
1558 if_exprt array_comprehension_body{
1559 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1560 index_exprt{src.op(), array_comprehension_index},
1561 if_exprt{
1563 array_comprehension_index, first_index.type()),
1564 first_index},
1565 first_update_value,
1567 array_comprehension_index, last_index.type()),
1568 last_index},
1569 std::move(last_update_value),
1570 std::move(update_value)}}};
1571
1572 return simplify_expr(
1573 array_comprehension_exprt{array_comprehension_index,
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,
1592 const exprt &value_as_byte_array,
1593 const optionalt<exprt> &non_const_update_bound,
1594 const namespacet &ns)
1595{
1596 const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1597 ? ID_byte_extract_little_endian
1598 : ID_byte_extract_big_endian;
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
1605 const exprt subtype_size = simplify_expr(
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
1612 exprt first_index = div_exprt{src.offset(), subtype_size};
1613 simplify(first_index, ns);
1614
1615 // compute the offset within that first element
1616 const exprt update_offset = mod_exprt{src.offset(), subtype_size};
1617
1618 // compute the number of bytes (from the update value) that are going to be
1619 // consumed for updating the first element
1620 exprt initial_bytes = minus_exprt{subtype_size, update_offset};
1621 exprt update_bound;
1622 if(non_const_update_bound.has_value())
1623 {
1624 update_bound = typecast_exprt::conditional_cast(
1625 *non_const_update_bound, subtype_size.type());
1626 }
1627 else
1628 {
1630 value_as_byte_array.id() == ID_array,
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 }
1635 initial_bytes =
1636 if_exprt{binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
1637 initial_bytes,
1638 update_bound};
1639 simplify(initial_bytes, ns);
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
1643 exprt first_update_value = lower_byte_operators(
1645 src.id(),
1646 index_exprt{src.op(), first_index},
1647 update_offset,
1648 byte_extract_exprt{extract_opcode,
1649 value_as_byte_array,
1650 from_integer(0, src.offset().type()),
1651 array_typet{bv_typet{8}, initial_bytes}}},
1652 ns);
1653
1654 if(value_as_byte_array.id() != ID_array)
1655 {
1657 src,
1658 subtype,
1659 subtype_size,
1660 value_as_byte_array,
1661 *non_const_update_bound,
1662 initial_bytes,
1663 first_index,
1664 first_update_value,
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())
1675 step_size = numeric_cast_v<std::size_t>(to_constant_expr(subtype_size));
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())
1682 offset = numeric_cast_v<std::size_t>(to_constant_expr(initial_bytes));
1683
1684 with_exprt result{src.op(), first_index, first_update_value};
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(
1691 plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1692
1693 exprt offset_expr = simplify_expr(
1694 plus_exprt{
1695 initial_bytes,
1696 mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}},
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()),
1704 byte_extract_exprt{extract_opcode,
1705 value_as_byte_array,
1706 std::move(offset_expr),
1707 array_typet{bv_typet{8}, subtype_size}}},
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(
1720 plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1721
1722 exprt element = lower_byte_operators(
1724 src.id(),
1725 index_exprt{src.op(), where},
1726 from_integer(0, src.offset().type()),
1728 extract_opcode,
1729 value_as_byte_array,
1730 from_integer(offset, src.offset().type()),
1731 array_typet{bv_typet{8}, from_integer(tail_size, size_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,
1752 const exprt &value_as_byte_array,
1753 const optionalt<exprt> &non_const_update_bound,
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 ||
1769 non_const_update_bound.has_value() || value_as_byte_array.id() != ID_array)
1770 {
1772 src, subtype, value_as_byte_array, non_const_update_bound, ns);
1773 }
1774
1775 std::size_t num_elements =
1776 numeric_cast_v<std::size_t>(to_constant_expr(size));
1777 mp_integer offset_bytes =
1778 numeric_cast_v<mp_integer>(to_constant_expr(src.offset()));
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 {
1794 mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
1795 mp_integer update_elements = *subtype_bits / 8;
1796 exprt::operandst::const_iterator first =
1797 value_as_byte_array.operands().begin();
1798 exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
1799 if(update_offset < 0)
1800 {
1801 INVARIANT(
1802 value_as_byte_array.operands().size() > -update_offset,
1803 "indices past the update should be handled above");
1804 first += numeric_cast_v<std::ptrdiff_t>(-update_offset);
1805 }
1806 else
1807 {
1808 update_elements -= update_offset;
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)
1815 end = first + numeric_cast_v<std::ptrdiff_t>(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),
1825 array_typet{bv_typet{8}, from_integer(update_size, size_type())}}};
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,
1852 const struct_typet &struct_type,
1853 const exprt &value_as_byte_array,
1854 const optionalt<exprt> &non_const_update_bound,
1855 const namespacet &ns)
1856{
1857 const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1858 ? ID_byte_extract_little_endian
1859 : ID_byte_extract_big_endian;
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);
1877 auto offset_bytes = numeric_cast<mp_integer>(offset);
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));
1890 member_offset_bits += *element_width;
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
1902 const byte_extract_exprt byte_extract_expr{
1903 extract_opcode,
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;
1909 bu.set_op(lower_byte_extract(byte_extract_expr, ns));
1910 bu.type() = bu.op().type();
1911
1912 return lower_byte_extract(
1914 extract_opcode,
1916 bu, value_as_byte_array, non_const_update_bound, ns),
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.
1926 mp_integer update_elements = (*element_width + 7) / 8;
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");
1935 first = numeric_cast_v<std::size_t>(-*offset_bytes);
1936 }
1937 else
1938 {
1939 update_elements -= *offset_bytes;
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());
1951 exprt::operandst update_values =
1952 instantiate_byte_array(value_as_byte_array, first, end, ns);
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.
1958 exprt update_size_expr = from_integer(update_size, size_type());
1959 array_exprt update_expr{std::move(update_values),
1960 array_typet{bv_typet{8}, update_size_expr}};
1961 optionalt<exprt> member_update_bound;
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
1967 const exprt remaining_update_bytes = typecast_exprt::conditional_cast(
1968 if_exprt{
1970 *non_const_update_bound,
1971 ID_gt,
1972 from_integer(first, non_const_update_bound->type())},
1973 minus_exprt{*non_const_update_bound,
1974 from_integer(first, non_const_update_bound->type())},
1975 from_integer(0, 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:
1979 update_size_expr = if_exprt{
1980 binary_predicate_exprt{update_size_expr, ID_lt, remaining_update_bytes},
1981 update_size_expr,
1982 remaining_update_bytes};
1983 simplify(update_size_expr, ns);
1984 member_update_bound = std::move(update_size_expr);
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 =
1990 numeric_cast_v<std::size_t>(member_offset_bits % 8);
1991 const std::size_t element_bits_int =
1992 numeric_cast_v<std::size_t>(*element_width);
1993
1994 const bool little_endian = src.id() == ID_byte_update_little_endian;
1995 if(shift != 0)
1996 {
1997 member = concatenation_exprt{
1998 typecast_exprt::conditional_cast(member, bv_typet{element_bits_int}),
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};
2009 exprt updated_element =
2010 lower_byte_update(bu, update_expr, member_update_bound, ns);
2011
2012 if(shift == 0)
2013 elements.push_back(updated_element);
2014 else
2015 {
2016 elements.push_back(typecast_exprt::conditional_cast(
2017 extractbits_exprt{updated_element,
2018 element_bits_int - 1 + (little_endian ? shift : 0),
2019 (little_endian ? shift : 0),
2020 bv_typet{element_bits_int}},
2021 comp.type()));
2022 }
2023
2024 member_offset_bits += *element_width;
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,
2042 const exprt &value_as_byte_array,
2043 const optionalt<exprt> &non_const_update_bound,
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;
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(),
2059 lower_byte_update(bu, value_as_byte_array, non_const_update_bound, ns),
2060 src.type()};
2061}
2062
2072 const byte_update_exprt &src,
2073 const exprt &value_as_byte_array,
2074 const optionalt<exprt> &non_const_update_bound,
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());
2087 CHECK_RETURN(*element_width > 0);
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,
2104 to_array_expr(value_as_byte_array),
2105 non_const_update_bound,
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())),
2117 value_as_byte_array,
2118 non_const_update_bound,
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())),
2128 value_as_byte_array,
2129 non_const_update_bound,
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
2144 exprt::operandst update_bytes;
2145 if(value_as_byte_array.id() == ID_array)
2146 update_bytes = value_as_byte_array.operands();
2147 else
2148 {
2149 update_bytes =
2150 instantiate_byte_array(value_as_byte_array, 0, (type_bits + 7) / 8, ns);
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
2158 exprt val_before =
2159 typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
2160 if(bit_width > type_bits)
2161 {
2162 val_before =
2163 concatenation_exprt{from_integer(0, bv_typet{bit_width - type_bits}),
2164 val_before,
2165 bv_typet{bit_width}};
2166
2167 if(!is_little_endian)
2168 to_concatenation_expr(val_before)
2169 .op0()
2170 .swap(to_concatenation_expr(val_before).op1());
2171 }
2172
2173 if(non_const_update_bound.has_value())
2174 {
2175 const exprt src_as_bytes = unpack_rec(
2176 val_before,
2177 src.id() == ID_byte_update_little_endian,
2178 mp_integer{0},
2179 mp_integer{update_bytes.size()},
2180 ns);
2181 CHECK_RETURN(src_as_bytes.id() == ID_array);
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] =
2187 from_integer(i, non_const_update_bound->type()),
2188 ID_lt,
2189 *non_const_update_bound},
2190 update_bytes[i],
2191 src_as_bytes.operands()[i]};
2192 }
2193 }
2194
2195 // build mask
2196 exprt mask;
2197 if(is_little_endian)
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();
2207 mult_exprt offset_times_eight{src.offset(), from_integer(8, offset_type)};
2208
2209 const binary_predicate_exprt offset_ge_zero{
2210 offset_times_eight, ID_ge, from_integer(0, offset_type)};
2211
2212 if_exprt mask_shifted{offset_ge_zero,
2213 shl_exprt{mask, offset_times_eight},
2214 lshr_exprt{mask, offset_times_eight}};
2215 if(!is_little_endian)
2216 mask_shifted.true_case().swap(mask_shifted.false_case());
2217
2218 // original_bits &= ~mask
2219 bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}};
2220
2221 // concatenate and zero-extend the value
2222 concatenation_exprt value{update_bytes, bv_typet{update_size_bits}};
2223 if(is_little_endian)
2224 std::reverse(value.operands().begin(), value.operands().end());
2225
2226 exprt zero_extended;
2227 if(bit_width > update_size_bits)
2228 {
2229 zero_extended = concatenation_exprt{
2230 from_integer(0, bv_typet{bit_width - update_size_bits}),
2231 value,
2232 bv_typet{bit_width}};
2233
2234 if(!is_little_endian)
2235 to_concatenation_expr(zero_extended)
2236 .op0()
2237 .swap(to_concatenation_expr(zero_extended).op1());
2238 }
2239 else
2240 zero_extended = value;
2241
2242 // shift the value
2243 if_exprt value_shifted{offset_ge_zero,
2244 shl_exprt{zero_extended, offset_times_eight},
2245 lshr_exprt{zero_extended, offset_times_eight}};
2246 if(!is_little_endian)
2247 value_shifted.true_case().swap(value_shifted.false_case());
2248
2249 // original_bits |= newvalue
2250 bitor_exprt bitor_expr{bitand_expr, value_shifted};
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(
2261 bitor_expr, bounds.ub, bounds.lb, bv_typet{type_bits}},
2262 src.type()),
2263 ns);
2264 }
2265
2266 return simplify_expr(
2267 typecast_exprt::conditional_cast(bitor_expr, src.type()), ns);
2268 }
2269 else
2270 {
2272 false, "lower_byte_update does not yet support ", src.type().id_string());
2273 }
2274}
2275
2277{
2279 src.id() == ID_byte_update_little_endian ||
2280 src.id() == ID_byte_update_big_endian,
2281 "byte update expression should either be little or big endian");
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.
2297 optionalt<exprt> non_const_update_bound;
2298 // update value, may require extension to full bytes
2299 exprt update_value = src.value();
2300 auto update_size_expr_opt = size_of_expr(update_value.type(), ns);
2301 CHECK_RETURN(update_size_expr_opt.has_value());
2302 simplify(update_size_expr_opt.value(), ns);
2303
2304 if(!update_size_expr_opt.value().is_constant())
2305 non_const_update_bound = *update_size_expr_opt;
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");
2314 const size_t update_bits_int = numeric_cast_v<size_t>(*update_bits);
2315
2316 if(update_bits_int % 8 != 0)
2317 {
2319 can_cast_type<bitvector_typet>(update_value.type()),
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);
2327 extractbits_exprt extra_bits{
2328 src.op(), bounds.ub, bounds.lb, bv_typet{n_extra_bits}};
2329
2330 update_value = concatenation_exprt{
2332 update_value, bv_typet{update_bits_int}),
2333 extra_bits,
2334 adjust_width(update_value.type(), update_bits_int + n_extra_bits)};
2335 }
2336 else
2337 {
2338 update_size_expr_opt =
2339 from_integer(update_bits_int / 8, update_size_expr_opt->type());
2340 }
2341 }
2342
2343 const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2344 ? ID_byte_extract_little_endian
2345 : ID_byte_extract_big_endian;
2346
2347 const byte_extract_exprt byte_extract_expr{
2348 extract_opcode,
2349 update_value,
2350 from_integer(0, src.offset().type()),
2351 array_typet{bv_typet{8}, *update_size_expr_opt}};
2352
2353 const exprt value_as_byte_array = lower_byte_extract(byte_extract_expr, ns);
2354
2355 exprt result =
2356 lower_byte_update(src, value_as_byte_array, non_const_update_bound, ns);
2357 return result;
2358}
2359
2360bool has_byte_operator(const exprt &src)
2361{
2362 if(src.id()==ID_byte_update_little_endian ||
2363 src.id()==ID_byte_update_big_endian ||
2364 src.id()==ID_byte_extract_little_endian ||
2365 src.id()==ID_byte_extract_big_endian)
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 ||
2386 src.id()==ID_byte_update_big_endian)
2387 return lower_byte_update(to_byte_update_expr(tmp), ns);
2388 else if(src.id()==ID_byte_extract_little_endian ||
2389 src.id()==ID_byte_extract_big_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
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
void set_op(exprt e)
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
exprt & index()
Definition std_expr.h:1363
exprt & array()
Definition std_expr.h:1353
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
const componentst & components() const
Definition std_types.h:147
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
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition c_types.cpp:318
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.
nonstd::optional< T > optionalt
Definition optional.h:35
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)
BigInt mp_integer
Definition smt_terms.h:12
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
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition std_types.h:887
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