cprover
Loading...
Searching...
No Matches
lower_byte_operators.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "arith_tools.h"
10#include "bitvector_expr.h"
11#include "byte_operators.h"
12#include "c_types.h"
13#include "endianness_map.h"
14#include "expr_util.h"
15#include "namespace.h"
16#include "narrow.h"
17#include "pointer_offset_size.h"
18#include "simplify_expr.h"
19#include "string_constant.h"
20
21#include <algorithm>
22
23static exprt bv_to_expr(
24 const exprt &bitvector_expr,
25 const typet &target_type,
26 const endianness_mapt &endianness_map,
27 const namespacet &ns);
28
29struct boundst
30{
31 std::size_t lb;
32 std::size_t ub;
33};
34
37 const endianness_mapt &endianness_map,
38 std::size_t lower_bound,
39 std::size_t upper_bound)
40{
41 boundst result;
42 result.lb = lower_bound;
43 result.ub = upper_bound;
44
45 if(result.ub < endianness_map.number_of_bits())
46 {
47 result.lb = endianness_map.map_bit(result.lb);
48 result.ub = endianness_map.map_bit(result.ub);
49
50 // big-endian bounds need swapping
51 if(result.ub < result.lb)
52 std::swap(result.lb, result.ub);
53 }
54
55 return result;
56}
57
59bitvector_typet adjust_width(const typet &src, std::size_t new_width)
60{
61 if(src.id() == ID_unsignedbv)
62 return unsignedbv_typet(new_width);
63 else if(src.id() == ID_signedbv)
64 return signedbv_typet(new_width);
65 else if(src.id() == ID_bv)
66 return bv_typet(new_width);
67 else if(src.id() == ID_c_enum) // we use the underlying type
68 return adjust_width(to_c_enum_type(src).underlying_type(), new_width);
69 else if(src.id() == ID_c_bit_field)
70 return c_bit_field_typet(
71 to_c_bit_field_type(src).underlying_type(), new_width);
72 else
73 PRECONDITION(false);
74}
75
79 const exprt &bitvector_expr,
80 const struct_typet &struct_type,
81 const endianness_mapt &endianness_map,
82 const namespacet &ns)
83{
84 const struct_typet::componentst &components = struct_type.components();
85
86 exprt::operandst operands;
87 operands.reserve(components.size());
88 std::size_t member_offset_bits = 0;
89 for(const auto &comp : components)
90 {
91 const auto component_bits_opt = pointer_offset_bits(comp.type(), ns);
92 std::size_t component_bits;
93 if(component_bits_opt.has_value())
94 component_bits = numeric_cast_v<std::size_t>(*component_bits_opt);
95 else
96 component_bits = to_bitvector_type(bitvector_expr.type()).get_width() -
98
99 if(component_bits == 0)
100 {
101 operands.push_back(
102 bv_to_expr(bitvector_expr, comp.type(), endianness_map, ns));
103 continue;
104 }
105
106 const auto bounds = map_bounds(
107 endianness_map,
109 member_offset_bits + component_bits - 1);
110 bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
111 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
112 operands.push_back(bv_to_expr(
113 extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
114 comp.type(),
115 endianness_map,
116 ns));
117
118 if(component_bits_opt.has_value())
119 member_offset_bits += component_bits;
120 }
121
122 return struct_exprt{std::move(operands), struct_type};
123}
124
128 const exprt &bitvector_expr,
129 const union_typet &union_type,
130 const endianness_mapt &endianness_map,
131 const namespacet &ns)
132{
133 const union_typet::componentst &components = union_type.components();
134
135 if(components.empty())
136 return empty_union_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{
149 components.front().get_name(),
150 bv_to_expr(bitvector_expr, components.front().type(), endianness_map, ns),
151 union_type};
152 }
153
154 const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
155 bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits);
156 const irep_idt &component_name = widest_member.has_value()
157 ? widest_member->first.get_name()
158 : components.front().get_name();
159 const typet &component_type = widest_member.has_value()
160 ? widest_member->first.type()
161 : components.front().type();
162 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
163 return union_exprt{
164 component_name,
166 extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
167 component_type,
168 endianness_map,
169 ns),
170 union_type};
171}
172
176 const exprt &bitvector_expr,
177 const array_typet &array_type,
178 const endianness_mapt &endianness_map,
179 const namespacet &ns)
180{
181 auto num_elements = numeric_cast<std::size_t>(array_type.size());
182 auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
183
184 const std::size_t total_bits =
185 to_bitvector_type(bitvector_expr.type()).get_width();
186 if(!num_elements.has_value())
187 {
188 if(!subtype_bits.has_value() || *subtype_bits == 0)
189 num_elements = total_bits;
190 else
191 num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
192 }
194 !num_elements.has_value() || !subtype_bits.has_value() ||
195 *subtype_bits * *num_elements == total_bits,
196 "subtype width times array size should be total bitvector width");
197
198 exprt::operandst operands;
199 operands.reserve(*num_elements);
200 for(std::size_t i = 0; i < *num_elements; ++i)
201 {
202 if(subtype_bits.has_value())
203 {
204 const std::size_t subtype_bits_int =
205 numeric_cast_v<std::size_t>(*subtype_bits);
206 const auto bounds = map_bounds(
207 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
208 bitvector_typet type =
209 adjust_width(bitvector_expr.type(), subtype_bits_int);
210 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
211 operands.push_back(bv_to_expr(
213 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
214 array_type.element_type(),
215 endianness_map,
216 ns));
217 }
218 else
219 {
220 operands.push_back(bv_to_expr(
221 bitvector_expr, array_type.element_type(), endianness_map, ns));
222 }
223 }
224
225 return array_exprt{std::move(operands), array_type};
226}
227
231 const exprt &bitvector_expr,
232 const vector_typet &vector_type,
233 const endianness_mapt &endianness_map,
234 const namespacet &ns)
235{
236 const std::size_t num_elements =
237 numeric_cast_v<std::size_t>(vector_type.size());
238 auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
240 !subtype_bits.has_value() ||
241 *subtype_bits * num_elements ==
242 to_bitvector_type(bitvector_expr.type()).get_width(),
243 "subtype width times vector size should be total bitvector width");
244
245 exprt::operandst operands;
246 operands.reserve(num_elements);
247 for(std::size_t i = 0; i < num_elements; ++i)
248 {
249 if(subtype_bits.has_value())
250 {
251 const std::size_t subtype_bits_int =
252 numeric_cast_v<std::size_t>(*subtype_bits);
253 const auto bounds = map_bounds(
254 endianness_map, i * subtype_bits_int, ((i + 1) * subtype_bits_int) - 1);
255 bitvector_typet type =
256 adjust_width(bitvector_expr.type(), subtype_bits_int);
257 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
258 operands.push_back(bv_to_expr(
260 bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
261 vector_type.element_type(),
262 endianness_map,
263 ns));
264 }
265 else
266 {
267 operands.push_back(bv_to_expr(
268 bitvector_expr, vector_type.element_type(), endianness_map, ns));
269 }
270 }
271
272 return vector_exprt{std::move(operands), vector_type};
273}
274
278 const exprt &bitvector_expr,
279 const complex_typet &complex_type,
280 const endianness_mapt &endianness_map,
281 const namespacet &ns)
282{
283 const std::size_t total_bits =
284 to_bitvector_type(bitvector_expr.type()).get_width();
285 const auto subtype_bits_opt = pointer_offset_bits(complex_type.subtype(), ns);
286 std::size_t subtype_bits;
287 if(subtype_bits_opt.has_value())
288 {
289 subtype_bits = numeric_cast_v<std::size_t>(*subtype_bits_opt);
291 subtype_bits * 2 == total_bits,
292 "subtype width should be half of the total bitvector width");
293 }
294 else
295 subtype_bits = total_bits / 2;
296
297 const auto bounds_real = map_bounds(endianness_map, 0, subtype_bits - 1);
298 const auto bounds_imag =
299 map_bounds(endianness_map, subtype_bits, subtype_bits * 2 - 1);
300
301 const bitvector_typet type =
302 adjust_width(bitvector_expr.type(), subtype_bits);
303
304 PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value());
305 return complex_exprt{
307 extractbits_exprt{bitvector_expr, bounds_real.ub, bounds_real.lb, type},
308 complex_type.subtype(),
309 endianness_map,
310 ns),
312 extractbits_exprt{bitvector_expr, bounds_imag.ub, bounds_imag.lb, type},
313 complex_type.subtype(),
314 endianness_map,
315 ns),
316 complex_type};
317}
318
333 const exprt &bitvector_expr,
334 const typet &target_type,
335 const endianness_mapt &endianness_map,
336 const namespacet &ns)
337{
339
340 if(target_type.id() == ID_floatbv)
341 {
342 std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width();
343 exprt bv_expr =
344 typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width});
345 return simplify_expr(
346 typecast_exprt::conditional_cast(bv_expr, target_type), ns);
347 }
348 else if(
349 can_cast_type<bitvector_typet>(target_type) ||
350 target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
351 target_type.id() == ID_string)
352 {
353 return simplify_expr(
354 typecast_exprt::conditional_cast(bitvector_expr, target_type), ns);
355 }
356
357 if(target_type.id() == ID_struct)
358 {
359 return bv_to_struct_expr(
360 bitvector_expr, to_struct_type(target_type), endianness_map, ns);
361 }
362 else if(target_type.id() == ID_struct_tag)
363 {
365 bitvector_expr,
366 ns.follow_tag(to_struct_tag_type(target_type)),
367 endianness_map,
368 ns);
369 result.type() = target_type;
370 return std::move(result);
371 }
372 else if(target_type.id() == ID_union)
373 {
374 return bv_to_union_expr(
375 bitvector_expr, to_union_type(target_type), endianness_map, ns);
376 }
377 else if(target_type.id() == ID_union_tag)
378 {
379 exprt result = bv_to_union_expr(
380 bitvector_expr,
381 ns.follow_tag(to_union_tag_type(target_type)),
382 endianness_map,
383 ns);
384 result.type() = target_type;
385 return result;
386 }
387 else if(target_type.id() == ID_array)
388 {
389 return bv_to_array_expr(
390 bitvector_expr, to_array_type(target_type), endianness_map, ns);
391 }
392 else if(target_type.id() == ID_vector)
393 {
394 return bv_to_vector_expr(
395 bitvector_expr, to_vector_type(target_type), endianness_map, ns);
396 }
397 else if(target_type.id() == ID_complex)
398 {
399 return bv_to_complex_expr(
400 bitvector_expr, to_complex_type(target_type), endianness_map, ns);
401 }
402 else
403 {
405 false, "bv_to_expr does not yet support ", target_type.id_string());
406 }
407}
408
409static exprt unpack_rec(
410 const exprt &src,
411 bool little_endian,
412 const optionalt<mp_integer> &offset_bytes,
413 const optionalt<mp_integer> &max_bytes,
414 const std::size_t bits_per_byte,
415 const namespacet &ns,
416 bool unpack_byte_array = false);
417
426 const exprt &src,
427 std::size_t lower_bound,
428 std::size_t upper_bound,
429 const std::size_t bits_per_byte,
430 const namespacet &ns)
431{
432 PRECONDITION(lower_bound <= upper_bound);
433
434 if(src.id() == ID_array)
435 {
436 PRECONDITION(upper_bound <= src.operands().size());
437 return exprt::operandst{
438 src.operands().begin() + narrow_cast<std::ptrdiff_t>(lower_bound),
439 src.operands().begin() + narrow_cast<std::ptrdiff_t>(upper_bound)};
440 }
441
442 const typet &element_type = src.type().id() == ID_array
445 const typet index_type = src.type().id() == ID_array
446 ? to_array_type(src.type()).index_type()
447 : to_vector_type(src.type()).index_type();
449 can_cast_type<bitvector_typet>(element_type) &&
450 to_bitvector_type(element_type).get_width() == bits_per_byte);
451 exprt::operandst bytes;
452 bytes.reserve(upper_bound - lower_bound);
453 for(std::size_t i = lower_bound; i < upper_bound; ++i)
454 {
455 const index_exprt idx{src, from_integer(i, index_type)};
456 bytes.push_back(simplify_expr(idx, ns));
457 }
458 return bytes;
459}
460
470 const exprt &src,
471 std::size_t el_bytes,
472 bool little_endian,
473 const std::size_t bits_per_byte,
474 const namespacet &ns)
475{
476 const typet index_type = src.type().id() == ID_array
477 ? to_array_type(src.type()).index_type()
478 : to_vector_type(src.type()).index_type();
479
480 // TODO we either need a symbol table here or make array comprehensions
481 // introduce a scope
482 static std::size_t array_comprehension_index_counter = 0;
483 ++array_comprehension_index_counter;
484 symbol_exprt array_comprehension_index{
485 "$array_comprehension_index_a_v" +
486 std::to_string(array_comprehension_index_counter),
487 index_type};
488
489 index_exprt element{
490 src,
491 div_exprt{array_comprehension_index, from_integer(el_bytes, index_type)}};
492
493 exprt sub =
494 unpack_rec(element, little_endian, {}, {}, bits_per_byte, ns, false);
495 exprt::operandst sub_operands =
496 instantiate_byte_array(sub, 0, el_bytes, bits_per_byte, ns);
497
498 exprt body = sub_operands.front();
499 const mod_exprt offset{
500 array_comprehension_index,
501 from_integer(el_bytes, array_comprehension_index.type())};
502 for(std::size_t i = 1; i < el_bytes; ++i)
503 {
504 body = if_exprt{
505 equal_exprt{offset, from_integer(i, array_comprehension_index.type())},
506 sub_operands[i],
507 body};
508 }
509
510 const exprt array_vector_size = src.type().id() == ID_vector
511 ? to_vector_type(src.type()).size()
512 : to_array_type(src.type()).size();
513
515 std::move(array_comprehension_index),
516 std::move(body),
518 bv_typet{bits_per_byte},
520 array_vector_size, from_integer(el_bytes, array_vector_size.type())}}};
521}
522
539 const exprt &src,
540 const optionalt<mp_integer> &src_size,
541 const mp_integer &element_bits,
542 bool little_endian,
543 const optionalt<mp_integer> &offset_bytes,
544 const optionalt<mp_integer> &max_bytes,
545 const std::size_t bits_per_byte,
546 const namespacet &ns)
547{
548 const std::size_t el_bytes = numeric_cast_v<std::size_t>(
549 (element_bits + bits_per_byte - 1) / bits_per_byte);
550
551 if(!src_size.has_value() && !max_bytes.has_value())
552 {
554 el_bytes > 0 && element_bits % bits_per_byte == 0,
555 "unpacking of arrays with non-byte-aligned elements is not supported");
557 src, el_bytes, little_endian, bits_per_byte, ns);
558 }
559
560 exprt::operandst byte_operands;
561 mp_integer first_element = 0;
562
563 // refine the number of elements to extract in case the element width is known
564 // and a multiple of bytes; otherwise we will expand the entire array/vector
565 optionalt<mp_integer> num_elements = src_size;
566 if(element_bits > 0 && element_bits % bits_per_byte == 0)
567 {
568 if(!num_elements.has_value())
569 {
570 // turn bytes into elements, rounding up
571 num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
572 }
573
574 if(offset_bytes.has_value())
575 {
576 // compute offset as number of elements
577 first_element = *offset_bytes / el_bytes;
578 // insert offset_bytes-many nil bytes into the output array
579 byte_operands.resize(
581 *offset_bytes - (*offset_bytes % el_bytes),
582 *num_elements * el_bytes)),
583 from_integer(0, bv_typet{bits_per_byte}));
584 }
585 }
586
587 // the maximum number of bytes is an upper bound in case the size of the
588 // array/vector is unknown; if element_bits was usable above this will
589 // have been turned into a number of elements already
590 if(!num_elements)
591 num_elements = *max_bytes;
592
593 const exprt src_simp = simplify_expr(src, ns);
594 const typet index_type = src_simp.type().id() == ID_array
595 ? to_array_type(src_simp.type()).index_type()
596 : to_vector_type(src_simp.type()).index_type();
597
598 for(mp_integer i = first_element; i < *num_elements; ++i)
599 {
600 exprt element;
601
602 if(
603 (src_simp.id() == ID_array || src_simp.id() == ID_vector) &&
604 i < src_simp.operands().size())
605 {
606 const std::size_t index_int = numeric_cast_v<std::size_t>(i);
607 element = src_simp.operands()[index_int];
608 }
609 else
610 {
611 element = index_exprt(src_simp, from_integer(i, index_type));
612 }
613
614 // recursively unpack each element so that we eventually just have an array
615 // of bytes left
616
617 const optionalt<mp_integer> element_max_bytes =
618 max_bytes
619 ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
621 const std::size_t element_max_bytes_int =
622 element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
623 : el_bytes;
624
625 exprt sub = unpack_rec(
626 element, little_endian, {}, element_max_bytes, bits_per_byte, ns, true);
627 exprt::operandst sub_operands =
628 instantiate_byte_array(sub, 0, element_max_bytes_int, bits_per_byte, ns);
629 byte_operands.insert(
630 byte_operands.end(), sub_operands.begin(), sub_operands.end());
631
632 if(max_bytes && byte_operands.size() >= *max_bytes)
633 break;
634 }
635
636 const std::size_t size = byte_operands.size();
637 return array_exprt(
638 std::move(byte_operands),
639 array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())});
640}
641
654 exprt::operandst &&bit_fields,
655 std::size_t total_bits,
656 exprt::operandst &dest,
657 bool little_endian,
658 const optionalt<mp_integer> &offset_bytes,
659 const optionalt<mp_integer> &max_bytes,
660 const std::size_t bits_per_byte,
661 const namespacet &ns)
662{
663 const concatenation_exprt concatenation{
664 std::move(bit_fields), bv_typet{total_bits}};
665
666 exprt sub = unpack_rec(
667 concatenation,
668 little_endian,
669 offset_bytes,
670 max_bytes,
671 bits_per_byte,
672 ns,
673 true);
674
675 dest.insert(
676 dest.end(),
677 std::make_move_iterator(sub.operands().begin()),
678 std::make_move_iterator(sub.operands().end()));
679}
680
692 const exprt &src,
693 bool little_endian,
694 const optionalt<mp_integer> &offset_bytes,
695 const optionalt<mp_integer> &max_bytes,
696 const std::size_t bits_per_byte,
697 const namespacet &ns)
698{
699 const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
700 const struct_typet::componentst &components = struct_type.components();
701
702 optionalt<mp_integer> offset_in_member;
703 optionalt<mp_integer> max_bytes_left;
705
707 exprt::operandst byte_operands;
708 for(auto it = components.begin(); it != components.end(); ++it)
709 {
710 const auto &comp = *it;
711 auto component_bits = pointer_offset_bits(comp.type(), ns);
712
713 // We can only handle a member of unknown width when it is the last member
714 // and is byte-aligned. Members of unknown width in the middle would leave
715 // us with unknown alignment of subsequent members, and queuing them up as
716 // bit fields is not possible either as the total width of the concatenation
717 // could not be determined.
719 component_bits.has_value() ||
720 (std::next(it) == components.end() && !bit_fields.has_value()),
721 "members of non-constant width should come last in a struct");
722
723 member_exprt member(src, comp.get_name(), comp.type());
724 if(src.id() == ID_struct)
725 simplify(member, ns);
726
727 // Is it a byte-aligned member?
728 if(member_offset_bits % bits_per_byte == 0)
729 {
730 if(bit_fields.has_value())
731 {
733 std::move(bit_fields->first),
734 bit_fields->second,
735 byte_operands,
736 little_endian,
737 offset_in_member,
738 max_bytes_left,
739 bits_per_byte,
740 ns);
741 bit_fields.reset();
742 }
743
744 if(offset_bytes.has_value())
745 {
746 offset_in_member = *offset_bytes - member_offset_bits / bits_per_byte;
747 // if the offset is negative, offset_in_member remains unset, which has
748 // the same effect as setting it to zero
749 if(*offset_in_member < 0)
750 offset_in_member.reset();
751 }
752
753 if(max_bytes.has_value())
754 {
755 max_bytes_left = *max_bytes - member_offset_bits / bits_per_byte;
756 if(*max_bytes_left < 0)
757 break;
758 }
759 }
760
761 if(
762 member_offset_bits % bits_per_byte != 0 ||
763 (component_bits.has_value() && *component_bits % bits_per_byte != 0))
764 {
765 if(!bit_fields.has_value())
766 bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
767
768 const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
769 bit_fields->first.insert(
770 little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
771 typecast_exprt::conditional_cast(member, bv_typet{bits_int}));
772 bit_fields->second += bits_int;
773
774 member_offset_bits += *component_bits;
775
776 continue;
777 }
778
779 INVARIANT(
780 !bit_fields.has_value(),
781 "all preceding members should have been processed");
782
783 if(
784 component_bits.has_value() && offset_in_member.has_value() &&
785 *offset_in_member * bits_per_byte >= *component_bits)
786 {
787 // we won't actually need this component, fill in zeros instead of
788 // computing an unpacking
789 byte_operands.resize(
790 byte_operands.size() +
791 numeric_cast_v<std::size_t>(*component_bits / bits_per_byte),
792 from_integer(0, bv_typet{bits_per_byte}));
793 }
794 else
795 {
796 exprt sub = unpack_rec(
797 member,
798 little_endian,
799 offset_in_member,
800 max_bytes_left,
801 bits_per_byte,
802 ns,
803 true);
804
805 byte_operands.insert(
806 byte_operands.end(),
807 std::make_move_iterator(sub.operands().begin()),
808 std::make_move_iterator(sub.operands().end()));
809 }
810
811 if(component_bits.has_value())
812 member_offset_bits += *component_bits;
813 }
814
815 // any remaining bit fields?
816 if(bit_fields.has_value())
817 {
819 std::move(bit_fields->first),
820 bit_fields->second,
821 byte_operands,
822 little_endian,
823 offset_in_member,
824 max_bytes_left,
825 bits_per_byte,
826 ns);
827 }
828
829 const std::size_t size = byte_operands.size();
830 return array_exprt{
831 std::move(byte_operands),
832 array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())}};
833}
834
842 const exprt &src,
843 bool little_endian,
844 const std::size_t bits_per_byte,
845 const namespacet &ns)
846{
847 const complex_typet &complex_type = to_complex_type(src.type());
848 const typet &subtype = complex_type.subtype();
849
850 auto subtype_bits = pointer_offset_bits(subtype, ns);
851 CHECK_RETURN(subtype_bits.has_value());
852 CHECK_RETURN(*subtype_bits % bits_per_byte == 0);
853
854 exprt sub_real = unpack_rec(
856 little_endian,
857 mp_integer{0},
858 *subtype_bits / bits_per_byte,
859 bits_per_byte,
860 ns,
861 true);
862 exprt::operandst byte_operands = std::move(sub_real.operands());
863
864 exprt sub_imag = unpack_rec(
866 little_endian,
867 mp_integer{0},
868 *subtype_bits / bits_per_byte,
869 bits_per_byte,
870 ns,
871 true);
872 byte_operands.insert(
873 byte_operands.end(),
874 std::make_move_iterator(sub_imag.operands().begin()),
875 std::make_move_iterator(sub_imag.operands().end()));
876
877 const std::size_t size = byte_operands.size();
878 return array_exprt{
879 std::move(byte_operands),
880 array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())}};
881}
882
893// array of bytes
896 const exprt &src,
897 bool little_endian,
898 const optionalt<mp_integer> &offset_bytes,
899 const optionalt<mp_integer> &max_bytes,
900 const std::size_t bits_per_byte,
901 const namespacet &ns,
902 bool unpack_byte_array)
903{
904 if(src.type().id() == ID_array)
905 {
906 const array_typet &array_type = to_array_type(src.type());
907 const typet &subtype = array_type.element_type();
908
909 auto element_bits = pointer_offset_bits(subtype, ns);
910 CHECK_RETURN(element_bits.has_value());
911
912 if(
913 !unpack_byte_array && *element_bits == bits_per_byte &&
915 {
916 return src;
917 }
918
919 const auto constant_size_opt = numeric_cast<mp_integer>(array_type.size());
920 return unpack_array_vector(
921 src,
922 constant_size_opt,
923 *element_bits,
924 little_endian,
925 offset_bytes,
926 max_bytes,
927 bits_per_byte,
928 ns);
929 }
930 else if(src.type().id() == ID_vector)
931 {
932 const vector_typet &vector_type = to_vector_type(src.type());
933 const typet &subtype = vector_type.element_type();
934
935 auto element_bits = pointer_offset_bits(subtype, ns);
936 CHECK_RETURN(element_bits.has_value());
937
938 if(
939 !unpack_byte_array && *element_bits == bits_per_byte &&
941 {
942 return src;
943 }
944
945 return unpack_array_vector(
946 src,
947 numeric_cast_v<mp_integer>(vector_type.size()),
948 *element_bits,
949 little_endian,
950 offset_bytes,
951 max_bytes,
952 bits_per_byte,
953 ns);
954 }
955 else if(src.type().id() == ID_complex)
956 {
957 return unpack_complex(src, little_endian, bits_per_byte, ns);
958 }
959 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
960 {
961 return unpack_struct(
962 src, little_endian, offset_bytes, max_bytes, bits_per_byte, ns);
963 }
964 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
965 {
966 const union_typet &union_type = to_union_type(ns.follow(src.type()));
967
968 const auto widest_member = union_type.find_widest_union_component(ns);
969
970 if(widest_member.has_value())
971 {
972 member_exprt member{
973 src, widest_member->first.get_name(), widest_member->first.type()};
974 return unpack_rec(
975 member,
976 little_endian,
977 offset_bytes,
978 widest_member->second,
979 bits_per_byte,
980 ns,
981 true);
982 }
983 else if(!union_type.components().empty())
984 {
985 member_exprt member{src, union_type.components().front()};
986 return unpack_rec(
987 member,
988 little_endian,
989 offset_bytes,
990 max_bytes,
991 bits_per_byte,
992 ns,
993 true);
994 }
995 }
996 else if(src.type().id() == ID_pointer)
997 {
998 return unpack_rec(
1000 little_endian,
1001 offset_bytes,
1002 max_bytes,
1003 bits_per_byte,
1004 ns,
1005 unpack_byte_array);
1006 }
1007 else if(src.id() == ID_string_constant)
1008 {
1009 return unpack_rec(
1011 little_endian,
1012 offset_bytes,
1013 max_bytes,
1014 bits_per_byte,
1015 ns,
1016 unpack_byte_array);
1017 }
1018 else if(src.is_constant() && src.type().id() == ID_string)
1019 {
1020 return unpack_rec(
1022 little_endian,
1023 offset_bytes,
1024 max_bytes,
1025 bits_per_byte,
1026 ns,
1027 unpack_byte_array);
1028 }
1029 else if(src.type().id() != ID_empty)
1030 {
1031 // a basic type; we turn that into extractbits while considering
1032 // endianness
1033 auto bits_opt = pointer_offset_bits(src.type(), ns);
1034 DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
1035
1036 const mp_integer total_bits = *bits_opt;
1037 mp_integer last_bit = total_bits;
1038 mp_integer bit_offset = 0;
1039
1040 if(max_bytes.has_value())
1041 {
1042 const auto max_bits = *max_bytes * bits_per_byte;
1043 if(little_endian)
1044 {
1045 last_bit = std::min(last_bit, max_bits);
1046 }
1047 else
1048 {
1049 bit_offset = std::max(mp_integer{0}, last_bit - max_bits);
1050 }
1051 }
1052
1053 auto const src_as_bitvector = typecast_exprt::conditional_cast(
1054 src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
1055 auto const byte_type = bv_typet{bits_per_byte};
1056 exprt::operandst byte_operands;
1057 array_typet array_type{
1058 bv_typet{bits_per_byte}, from_integer(0, size_type())};
1059
1060 for(; bit_offset < last_bit; bit_offset += bits_per_byte)
1061 {
1063 pointer_offset_bits(src_as_bitvector.type(), ns).has_value());
1064 extractbits_exprt extractbits(
1065 src_as_bitvector,
1066 from_integer(bit_offset + bits_per_byte - 1, array_type.index_type()),
1067 from_integer(bit_offset, array_type.index_type()),
1068 byte_type);
1069
1070 // endianness_mapt should be the point of reference for mapping out
1071 // endianness, but we need to work on elements here instead of
1072 // individual bits
1073 if(little_endian)
1074 byte_operands.push_back(extractbits);
1075 else
1076 byte_operands.insert(byte_operands.begin(), extractbits);
1077 }
1078
1079 const std::size_t size = byte_operands.size();
1080 array_type.size() = from_integer(size, size_type());
1081 return array_exprt{std::move(byte_operands), std::move(array_type)};
1082 }
1083
1084 return array_exprt(
1085 {}, array_typet{bv_typet{bits_per_byte}, from_integer(0, size_type())});
1086}
1087
1099 const byte_extract_exprt &src,
1100 const byte_extract_exprt &unpacked,
1101 const typet &subtype,
1102 const mp_integer &element_bits,
1103 const namespacet &ns)
1104{
1105 optionalt<std::size_t> num_elements;
1106 if(src.type().id() == ID_array)
1107 num_elements = numeric_cast<std::size_t>(to_array_type(src.type()).size());
1108 else
1109 num_elements = numeric_cast<std::size_t>(to_vector_type(src.type()).size());
1110
1111 if(num_elements.has_value())
1112 {
1113 exprt::operandst operands;
1114 // Work around spurious GCC warning about num_elements being uninitialised.
1115#pragma GCC diagnostic push
1116#ifndef __clang__
1117# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
1118#endif
1119 operands.reserve(*num_elements);
1120 for(std::size_t i = 0; i < *num_elements; ++i)
1121#pragma GCC diagnostic pop
1122 {
1123 plus_exprt new_offset(
1124 unpacked.offset(),
1126 i * element_bits / src.get_bits_per_byte(),
1127 unpacked.offset().type()));
1128
1129 byte_extract_exprt tmp(unpacked);
1130 tmp.type() = subtype;
1131 tmp.offset() = new_offset;
1132
1133 operands.push_back(lower_byte_extract(tmp, ns));
1134 }
1135
1136 exprt result;
1137 if(src.type().id() == ID_array)
1138 result = array_exprt{std::move(operands), to_array_type(src.type())};
1139 else
1140 result = vector_exprt{std::move(operands), to_vector_type(src.type())};
1141
1142 return simplify_expr(result, ns);
1143 }
1144
1145 DATA_INVARIANT(src.type().id() == ID_array, "vectors have constant size");
1146 const array_typet &array_type = to_array_type(src.type());
1147
1148 // TODO we either need a symbol table here or make array comprehensions
1149 // introduce a scope
1150 static std::size_t array_comprehension_index_counter = 0;
1151 ++array_comprehension_index_counter;
1152 symbol_exprt array_comprehension_index{
1153 "$array_comprehension_index_a" +
1154 std::to_string(array_comprehension_index_counter),
1155 array_type.index_type()};
1156
1157 plus_exprt new_offset{
1158 unpacked.offset(),
1160 mult_exprt{
1161 array_comprehension_index,
1163 element_bits / src.get_bits_per_byte(),
1164 array_comprehension_index.type())},
1165 unpacked.offset().type())};
1166
1167 byte_extract_exprt body(unpacked);
1168 body.type() = subtype;
1169 body.offset() = std::move(new_offset);
1170
1172 std::move(array_comprehension_index),
1173 lower_byte_extract(body, ns),
1174 array_type};
1175}
1176
1186 const byte_extract_exprt &src,
1187 const byte_extract_exprt &unpacked,
1188 const namespacet &ns)
1189{
1190 const complex_typet &complex_type = to_complex_type(src.type());
1191 const typet &subtype = complex_type.subtype();
1192
1193 auto subtype_bits = pointer_offset_bits(subtype, ns);
1194 if(!subtype_bits.has_value() || *subtype_bits % src.get_bits_per_byte() != 0)
1195 return {};
1196
1197 // offset remains unchanged
1198 byte_extract_exprt real{unpacked};
1199 real.type() = subtype;
1200
1201 const plus_exprt new_offset{
1202 unpacked.offset(),
1204 *subtype_bits / src.get_bits_per_byte(), unpacked.offset().type())};
1205 byte_extract_exprt imag{unpacked};
1206 imag.type() = subtype;
1207 imag.offset() = simplify_expr(new_offset, ns);
1208
1209 return simplify_expr(
1211 lower_byte_extract(real, ns), lower_byte_extract(imag, ns), complex_type},
1212 ns);
1213}
1214
1218{
1219 // General notes about endianness and the bit-vector conversion:
1220 // A single byte with value 0b10001000 is stored (in irept) as
1221 // exactly this string literal, and its bit-vector encoding will be
1222 // bvt bv={0,0,0,1,0,0,0,1}, i.e., bv[0]==0 and bv[7]==1
1223 //
1224 // A multi-byte value like x=256 would be:
1225 // - little-endian storage: ((char*)&x)[0]==0, ((char*)&x)[1]==1
1226 // - big-endian storage: ((char*)&x)[0]==1, ((char*)&x)[1]==0
1227 // - irept representation: 0000000100000000
1228 // - bvt: {0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0}
1229 // <... 8bits ...> <... 8bits ...>
1230 //
1231 // An array {0, 1} will be encoded as bvt bv={0,1}, i.e., bv[1]==1
1232 // concatenation(0, 1) will yield a bvt bv={1,0}, i.e., bv[1]==0
1233 //
1234 // The semantics of byte_extract(endianness, op, offset, T) is:
1235 // interpret ((char*)&op)+offset as the endianness-ordered storage
1236 // of an object of type T at address ((char*)&op)+offset
1237 // For some T x, byte_extract(endianness, x, 0, T) must yield x.
1238 //
1239 // byte_extract for a composite type T or an array will interpret
1240 // the individual subtypes with suitable endianness; the overall
1241 // order of components is not affected by endianness.
1242 //
1243 // Examples:
1244 // unsigned char A[4];
1245 // byte_extract_little_endian(A, 0, unsigned short) requests that
1246 // A[0],A[1] be interpreted as the storage of an unsigned short with
1247 // A[1] being the most-significant byte; byte_extract_big_endian for
1248 // the same operands will select A[0] as the most-significant byte.
1249 //
1250 // int A[2] = {0x01020304,0xDEADBEEF}
1251 // byte_extract_big_endian(A, 0, short) should yield 0x0102
1252 // byte_extract_little_endian(A, 0, short) should yield 0x0304
1253 // To obtain this we first compute byte arrays while taking into
1254 // account endianness:
1255 // big-endian byte representation: {01,02,03,04,DE,AB,BE,EF}
1256 // little-endian byte representation: {04,03,02,01,EF,BE,AB,DE}
1257 // We extract the relevant bytes starting from ((char*)A)+0:
1258 // big-endian: {01,02}; little-endian: {04,03}
1259 // Finally we place them in the appropriate byte order as indicated
1260 // by endianness:
1261 // big-endian: (short)concatenation(01,02)=0x0102
1262 // little-endian: (short)concatenation(03,04)=0x0304
1263
1265 src.id() == ID_byte_extract_little_endian ||
1266 src.id() == ID_byte_extract_big_endian);
1267 const bool little_endian = src.id() == ID_byte_extract_little_endian;
1268
1269 // determine an upper bound of the last byte we might need
1270 auto upper_bound_opt = size_of_expr(src.type(), ns);
1271 if(upper_bound_opt.has_value())
1272 {
1273 upper_bound_opt = simplify_expr(
1274 plus_exprt(
1275 upper_bound_opt.value(),
1277 src.offset(), upper_bound_opt.value().type())),
1278 ns);
1279 }
1280 else if(src.type().id() == ID_empty)
1281 upper_bound_opt = from_integer(0, size_type());
1282
1283 const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.offset());
1284 const auto upper_bound_int_opt =
1285 numeric_cast<mp_integer>(upper_bound_opt.value_or(nil_exprt()));
1286
1287 byte_extract_exprt unpacked(src);
1288 unpacked.op() = unpack_rec(
1289 src.op(),
1290 little_endian,
1291 lower_bound_int_opt,
1292 upper_bound_int_opt,
1293 src.get_bits_per_byte(),
1294 ns);
1297 .get_width() == src.get_bits_per_byte());
1298
1299 if(src.type().id() == ID_array || src.type().id() == ID_vector)
1300 {
1301 const typet &subtype = to_type_with_subtype(src.type()).subtype();
1302
1303 // consider ways of dealing with arrays of unknown subtype size or with a
1304 // subtype size that does not fit byte boundaries; currently we fall back to
1305 // stitching together consecutive elements down below
1306 auto element_bits = pointer_offset_bits(subtype, ns);
1307 if(
1308 element_bits.has_value() && *element_bits >= 1 &&
1309 *element_bits % src.get_bits_per_byte() == 0)
1310 {
1312 src, unpacked, subtype, *element_bits, ns);
1313 }
1314 }
1315 else if(src.type().id() == ID_complex)
1316 {
1317 auto result = lower_byte_extract_complex(src, unpacked, ns);
1318 if(result.has_value())
1319 return std::move(*result);
1320
1321 // else fall back to generic lowering that uses bit masks, below
1322 }
1323 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
1324 {
1325 const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
1326 const struct_typet::componentst &components = struct_type.components();
1327
1328 bool failed = false;
1329 struct_exprt s({}, src.type());
1330
1331 for(const auto &comp : components)
1332 {
1333 auto component_bits = pointer_offset_bits(comp.type(), ns);
1334
1335 // the next member would be misaligned, abort
1336 if(
1337 !component_bits.has_value() ||
1338 *component_bits % src.get_bits_per_byte() != 0)
1339 {
1340 failed = true;
1341 break;
1342 }
1343
1344 auto member_offset_opt =
1345 member_offset_expr(struct_type, comp.get_name(), ns);
1346
1347 if(!member_offset_opt.has_value())
1348 {
1349 failed = true;
1350 break;
1351 }
1352
1353 plus_exprt new_offset(
1354 unpacked.offset(),
1356 member_offset_opt.value(), unpacked.offset().type()));
1357
1358 byte_extract_exprt tmp(unpacked);
1359 tmp.type() = comp.type();
1360 tmp.offset() = new_offset;
1361
1363 }
1364
1365 if(!failed)
1366 return simplify_expr(std::move(s), ns);
1367 }
1368 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
1369 {
1370 const union_typet &union_type = to_union_type(ns.follow(src.type()));
1371
1372 const auto widest_member = union_type.find_widest_union_component(ns);
1373
1374 if(widest_member.has_value())
1375 {
1376 byte_extract_exprt tmp(unpacked);
1377 tmp.type() = widest_member->first.type();
1378
1379 return union_exprt(
1380 widest_member->first.get_name(),
1381 lower_byte_extract(tmp, ns),
1382 src.type());
1383 }
1384 }
1385
1386 const exprt &root = unpacked.op();
1387 const exprt &offset = unpacked.offset();
1388
1389 optionalt<typet> subtype;
1391 if(root.type().id() == ID_vector)
1392 {
1393 subtype = to_vector_type(root.type()).element_type();
1395 }
1396 else
1397 {
1398 subtype = to_array_type(root.type()).element_type();
1400 }
1401
1402 auto subtype_bits = pointer_offset_bits(*subtype, ns);
1403
1405 subtype_bits.has_value() && *subtype_bits == src.get_bits_per_byte(),
1406 "offset bits are byte aligned");
1407
1408 auto size_bits = pointer_offset_bits(unpacked.type(), ns);
1409 if(!size_bits.has_value())
1410 {
1411 auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
1412 // all cases with non-constant width should have been handled above
1414 op0_bits.has_value(),
1415 "the extracted width or the source width must be known");
1416 size_bits = op0_bits;
1417 }
1418
1419 mp_integer num_bytes =
1420 (*size_bits) / src.get_bits_per_byte() +
1421 (((*size_bits) % src.get_bits_per_byte() == 0) ? 0 : 1);
1422
1423 // get 'width'-many bytes, and concatenate
1424 const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
1426 op.reserve(width_bytes);
1427
1428 for(std::size_t i = 0; i < width_bytes; i++)
1429 {
1430 // the most significant byte comes first in the concatenation!
1431 std::size_t offset_int = little_endian ? (width_bytes - i - 1) : i;
1432
1433 plus_exprt offset_i{
1434 from_integer(offset_int, *index_type),
1436 simplify(offset_i, ns);
1437
1438 mp_integer index = 0;
1439 if(
1440 offset_i.is_constant() &&
1441 (root.id() == ID_array || root.id() == ID_vector) &&
1442 !to_integer(to_constant_expr(offset_i), index) &&
1443 index < root.operands().size() && index >= 0)
1444 {
1445 // offset is constant and in range
1446 op.push_back(root.operands()[numeric_cast_v<std::size_t>(index)]);
1447 }
1448 else
1449 {
1450 op.push_back(index_exprt(root, offset_i));
1451 }
1452 }
1453
1454 if(width_bytes == 1)
1455 {
1456 return simplify_expr(
1457 typecast_exprt::conditional_cast(op.front(), src.type()), ns);
1458 }
1459 else // width_bytes>=2
1460 {
1461 concatenation_exprt concatenation(
1462 std::move(op),
1463 adjust_width(*subtype, width_bytes * src.get_bits_per_byte()));
1464
1465 endianness_mapt map(concatenation.type(), little_endian, ns);
1466 return bv_to_expr(concatenation, src.type(), map, ns);
1467 }
1468}
1469
1471 const byte_update_exprt &src,
1472 const exprt &value_as_byte_array,
1473 const optionalt<exprt> &non_const_update_bound,
1474 const namespacet &ns);
1475
1486 const byte_update_exprt &src,
1487 const typet &subtype,
1488 const exprt &value_as_byte_array,
1489 const exprt &non_const_update_bound,
1490 const namespacet &ns)
1491{
1492 // TODO we either need a symbol table here or make array comprehensions
1493 // introduce a scope
1494 static std::size_t array_comprehension_index_counter = 0;
1495 ++array_comprehension_index_counter;
1496 symbol_exprt array_comprehension_index{
1497 "$array_comprehension_index_u_a_v" +
1498 std::to_string(array_comprehension_index_counter),
1499 to_array_type(src.type()).index_type()};
1500
1501 binary_predicate_exprt lower_bound{
1503 array_comprehension_index, src.offset().type()),
1504 ID_lt,
1505 src.offset()};
1506 binary_predicate_exprt upper_bound{
1508 array_comprehension_index, non_const_update_bound.type()),
1509 ID_ge,
1510 plus_exprt{
1512 src.offset(), non_const_update_bound.type()),
1513 non_const_update_bound}};
1514
1516 src.id() == ID_byte_update_little_endian ||
1517 src.id() == ID_byte_update_big_endian);
1518 const bool little_endian = src.id() == ID_byte_update_little_endian;
1519 endianness_mapt map(
1520 to_array_type(value_as_byte_array.type()).element_type(),
1521 little_endian,
1522 ns);
1523 if_exprt array_comprehension_body{
1524 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1525 index_exprt{src.op(), array_comprehension_index},
1526 bv_to_expr(
1528 value_as_byte_array,
1530 array_comprehension_index,
1532 src.offset(), array_comprehension_index.type())}},
1533 subtype,
1534 map,
1535 ns)};
1536
1537 return simplify_expr(
1539 array_comprehension_index,
1540 std::move(array_comprehension_body),
1541 to_array_type(src.type())},
1542 ns);
1543}
1544
1555 const byte_update_exprt &src,
1556 const typet &subtype,
1557 const array_exprt &value_as_byte_array,
1558 const optionalt<exprt> &non_const_update_bound,
1559 const namespacet &ns)
1560{
1562 src.id() == ID_byte_update_little_endian ||
1563 src.id() == ID_byte_update_big_endian);
1564 const bool little_endian = src.id() == ID_byte_update_little_endian;
1565
1566 const typet index_type = src.type().id() == ID_array
1567 ? to_array_type(src.type()).index_type()
1568 : to_vector_type(src.type()).index_type();
1569
1570 // apply 'array-update-with' num_elements times
1571 exprt result = src.op();
1572
1573 for(std::size_t i = 0; i < value_as_byte_array.operands().size(); ++i)
1574 {
1575 const exprt &element = value_as_byte_array.operands()[i];
1576
1577 exprt where = simplify_expr(
1578 plus_exprt{
1581 ns);
1582
1583 // skip elements that wouldn't change (skip over typecasts as we might have
1584 // some signed/unsigned char conversions)
1585 const exprt &e = skip_typecast(element);
1586 if(e.id() == ID_index)
1587 {
1588 const index_exprt &index_expr = to_index_expr(e);
1589 if(index_expr.array() == src.op() && index_expr.index() == where)
1590 continue;
1591 }
1592
1593 endianness_mapt map(element.type(), little_endian, ns);
1594 exprt update_value = bv_to_expr(element, subtype, map, ns);
1595 if(non_const_update_bound.has_value())
1596 {
1597 update_value = if_exprt{
1599 from_integer(i, non_const_update_bound->type()),
1600 ID_lt,
1601 *non_const_update_bound},
1602 update_value,
1603 index_exprt{src.op(), where}};
1604 }
1605
1606 if(result.id() != ID_with)
1607 result = with_exprt{result, std::move(where), std::move(update_value)};
1608 else
1609 result.add_to_operands(std::move(where), std::move(update_value));
1610 }
1611
1612 return simplify_expr(std::move(result), ns);
1613}
1614
1631 const byte_update_exprt &src,
1632 const typet &subtype,
1633 const exprt &subtype_size,
1634 const exprt &value_as_byte_array,
1635 const exprt &non_const_update_bound,
1636 const exprt &initial_bytes,
1637 const exprt &first_index,
1638 const exprt &first_update_value,
1639 const namespacet &ns)
1640{
1641 const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
1642 ? ID_byte_extract_little_endian
1643 : ID_byte_extract_big_endian;
1644
1645 // TODO we either need a symbol table here or make array comprehensions
1646 // introduce a scope
1647 static std::size_t array_comprehension_index_counter = 0;
1648 ++array_comprehension_index_counter;
1649 symbol_exprt array_comprehension_index{
1650 "$array_comprehension_index_u_a_v_u" +
1651 std::to_string(array_comprehension_index_counter),
1652 to_array_type(src.type()).index_type()};
1653
1654 // all arithmetic uses offset/index types
1655 PRECONDITION(array_comprehension_index.type() == src.offset().type());
1656 PRECONDITION(subtype_size.type() == src.offset().type());
1657 PRECONDITION(initial_bytes.type() == src.offset().type());
1658 PRECONDITION(first_index.type() == src.offset().type());
1659
1660 // the bound from where updates start
1661 binary_predicate_exprt lower_bound{
1663 array_comprehension_index, first_index.type()),
1664 ID_lt,
1665 first_index};
1666
1667 // The actual value of updates other than at the start or end
1668 plus_exprt offset_expr{
1669 initial_bytes,
1670 mult_exprt{
1671 subtype_size,
1674 array_comprehension_index, first_index.type()),
1675 plus_exprt{first_index, from_integer(1, first_index.type())}}}};
1676 exprt update_value = lower_byte_extract(
1678 extract_opcode,
1679 value_as_byte_array,
1680 std::move(offset_expr),
1681 src.get_bits_per_byte(),
1682 subtype},
1683 ns);
1684
1685 // The number of target array/vector elements being replaced, not including
1686 // a possible partial update at the end of the updated range, which is handled
1687 // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
1688 // round up to the nearest multiple of subtype_size.
1689 div_exprt updated_elements{
1690 plus_exprt{
1692 non_const_update_bound, subtype_size.type()),
1693 minus_exprt{subtype_size, from_integer(1, subtype_size.type())}},
1694 subtype_size};
1695
1696 // The last element to be updated: first_index + updated_elements - 1
1697 plus_exprt last_index{
1698 first_index,
1700 std::move(updated_elements), from_integer(1, first_index.type())}};
1701
1702 // The size of a partial update at the end of the updated range, may be zero.
1703 mod_exprt tail_size{
1707 non_const_update_bound, initial_bytes.type()),
1708 initial_bytes},
1709 subtype_size.type()),
1710 subtype_size};
1711
1712 // The bound where updates end, which is conditional on the partial update
1713 // being empty.
1714 binary_predicate_exprt upper_bound{
1716 array_comprehension_index, last_index.type()),
1717 ID_ge,
1718 if_exprt{
1719 equal_exprt{tail_size, from_integer(0, tail_size.type())},
1720 last_index,
1721 plus_exprt{last_index, from_integer(1, last_index.type())}}};
1722
1723 // The actual value of a partial update at the end.
1724 exprt last_update_value = lower_byte_update(
1726 src.id(),
1727 index_exprt{src.op(), last_index},
1729 typecast_exprt::conditional_cast(last_index, subtype_size.type()),
1730 subtype_size}},
1731 value_as_byte_array,
1732 src.get_bits_per_byte()},
1733 ns);
1734
1735 if_exprt array_comprehension_body{
1736 or_exprt{std::move(lower_bound), std::move(upper_bound)},
1737 index_exprt{src.op(), array_comprehension_index},
1738 if_exprt{
1741 array_comprehension_index, first_index.type()),
1742 first_index},
1743 first_update_value,
1744 if_exprt{
1747 array_comprehension_index, last_index.type()),
1748 last_index},
1749 std::move(last_update_value),
1750 std::move(update_value)}}};
1751
1752 return simplify_expr(
1754 array_comprehension_index,
1755 std::move(array_comprehension_body),
1756 to_array_type(src.type())},
1757 ns);
1758}
1759
1771 const byte_update_exprt &src,
1772 const typet &subtype,
1773 const exprt &value_as_byte_array,
1774 const optionalt<exprt> &non_const_update_bound,
1775 const namespacet &ns)
1776{
1777 // do all arithmetic below using index/offset types - the array theory
1778 // back-end is really picky about indices having the same type
1779 auto subtype_size_opt = size_of_expr(subtype, ns);
1780 CHECK_RETURN(subtype_size_opt.has_value());
1781
1782 const exprt subtype_size = simplify_expr(
1784 subtype_size_opt.value(), src.offset().type()),
1785 ns);
1786
1787 // compute the index of the first element of the array/vector that may be
1788 // updated
1790 src.offset().type() == to_array_type(src.op().type()).index_type());
1791 exprt first_index = div_exprt{src.offset(), subtype_size};
1792 simplify(first_index, ns);
1793
1794 // compute the offset within that first element
1795 const exprt update_offset = mod_exprt{src.offset(), subtype_size};
1796
1797 // compute the number of bytes (from the update value) that are going to be
1798 // consumed for updating the first element
1799 const exprt update_size =
1800 from_integer(value_as_byte_array.operands().size(), subtype_size.type());
1801 exprt initial_bytes = minus_exprt{subtype_size, update_offset};
1802 exprt update_bound;
1803 if(non_const_update_bound.has_value())
1804 {
1805 update_bound = typecast_exprt::conditional_cast(
1806 *non_const_update_bound, subtype_size.type());
1807 }
1808 else
1809 {
1811 value_as_byte_array.id() == ID_array,
1812 "value should be an array expression if the update bound is constant");
1813 update_bound = update_size;
1814 }
1815 initial_bytes = if_exprt{
1816 binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
1817 initial_bytes,
1818 update_bound};
1819 simplify(initial_bytes, ns);
1820
1821 // encode the first update: update the original element at first_index (the
1822 // actual update will only be initial_bytes-many bytes from
1823 // value_as_byte_array)
1824 exprt first_update_value = lower_byte_update(
1826 src.id(),
1827 index_exprt{src.op(), first_index},
1828 update_offset,
1829 value_as_byte_array,
1830 src.get_bits_per_byte()},
1831 ns);
1832
1833 if(value_as_byte_array.id() != ID_array)
1834 {
1836 src,
1837 subtype,
1838 subtype_size,
1839 value_as_byte_array,
1840 *non_const_update_bound,
1841 initial_bytes,
1842 first_index,
1843 first_update_value,
1844 ns);
1845 }
1846
1847 // We will update one array/vector element at a time - compute the number of
1848 // update values that will be consumed in each step. If we cannot determine a
1849 // constant value at this time we assume it's at least one byte. The
1850 // byte_extract_exprt within the loop uses the symbolic value (subtype_size),
1851 // we just need to make sure we make progress for the loop to terminate.
1852 std::size_t step_size = 1;
1853 if(subtype_size.is_constant())
1854 step_size = numeric_cast_v<std::size_t>(to_constant_expr(subtype_size));
1855 // Given the first update already encoded, keep track of the offset into the
1856 // update value. Again, the expressions within the loop use the symbolic
1857 // value, this is just an optimization in case we can determine a constant
1858 // offset.
1859 std::size_t offset = 0;
1860 if(initial_bytes.is_constant())
1861 offset = numeric_cast_v<std::size_t>(to_constant_expr(initial_bytes));
1862
1863 with_exprt result{src.op(), first_index, first_update_value};
1864
1865 auto lower_byte_update_array_vector_non_const_one_element =
1866 [&src,
1867 &first_index,
1868 &initial_bytes,
1869 &subtype_size,
1870 &value_as_byte_array,
1871 &ns,
1872 &result](std::size_t i) -> void {
1873 exprt where = simplify_expr(
1874 plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
1875
1876 exprt neg_offset_expr = simplify_expr(
1878 initial_bytes,
1879 mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}}},
1880 ns);
1881
1882 exprt element = lower_byte_update(
1884 src.id(),
1885 index_exprt{src.op(), where},
1886 neg_offset_expr,
1887 value_as_byte_array,
1888 src.get_bits_per_byte()},
1889 ns);
1890
1891 result.add_to_operands(std::move(where), std::move(element));
1892 };
1893
1894 std::size_t i = 1;
1895 for(; offset + step_size <= value_as_byte_array.operands().size();
1896 offset += step_size, ++i)
1897 {
1898 lower_byte_update_array_vector_non_const_one_element(i);
1899 }
1900
1901 // do the tail
1902 if(offset < value_as_byte_array.operands().size())
1903 lower_byte_update_array_vector_non_const_one_element(i);
1904
1905 return simplify_expr(std::move(result), ns);
1906}
1907
1921 const byte_update_exprt &src,
1922 const mp_integer &offset_bits,
1923 const exprt &element_to_update,
1924 const mp_integer &subtype_bits,
1925 const mp_integer &bits_already_set,
1926 const exprt &value_as_byte_array,
1927 const optionalt<exprt> &non_const_update_bound,
1928 const namespacet &ns)
1929{
1930 // We need to take one or more bytes from value_as_byte_array to modify the
1931 // target element. We need to compute:
1932 // - The position in value_as_byte_array to take bytes from: If subtype_bits
1933 // is less than the size of a byte, then multiple struct/array/vector elements
1934 // will need to be updated using the same byte.
1935 std::size_t first = 0;
1936 // - An upper bound on the number of bytes required from value_as_byte_array.
1937 mp_integer update_elements =
1938 (subtype_bits + src.get_bits_per_byte() - 1) / src.get_bits_per_byte();
1939 // - The offset into the target element: If subtype_bits is greater or equal
1940 // to the size of a byte, then there may be an offset into the target element
1941 // that needs to be taken into account, and multiple bytes will be required.
1942 mp_integer offset_bits_in_target_element = offset_bits - bits_already_set;
1943
1944 if(offset_bits_in_target_element < 0)
1945 {
1946 INVARIANT(
1947 value_as_byte_array.id() != ID_array ||
1948 value_as_byte_array.operands().size() * src.get_bits_per_byte() >
1949 -offset_bits_in_target_element,
1950 "indices past the update should be handled below");
1952 -offset_bits_in_target_element / src.get_bits_per_byte());
1953 offset_bits_in_target_element +=
1954 (-offset_bits_in_target_element / src.get_bits_per_byte()) *
1955 src.get_bits_per_byte();
1956 if(offset_bits_in_target_element < 0)
1957 ++update_elements;
1958 }
1959 else
1960 {
1961 update_elements -= offset_bits_in_target_element / src.get_bits_per_byte();
1962 INVARIANT(
1963 update_elements > 0, "indices before the update should be handled above");
1964 }
1965
1966 std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
1967 if(value_as_byte_array.id() == ID_array)
1968 end = std::min(end, value_as_byte_array.operands().size());
1970 value_as_byte_array, first, end, src.get_bits_per_byte(), ns);
1971 const std::size_t update_size = update_values.size();
1972 const exprt update_size_expr = from_integer(update_size, size_type());
1973 const array_typet update_type{
1974 bv_typet{src.get_bits_per_byte()}, update_size_expr};
1975
1976 // each case below will set "new_value" as appropriate
1977 exprt new_value;
1978
1979 if(
1980 offset_bits_in_target_element >= 0 &&
1981 offset_bits_in_target_element % src.get_bits_per_byte() == 0)
1982 {
1983 new_value = array_exprt{update_values, update_type};
1984 }
1985 else
1986 {
1987 if(src.id() == ID_byte_update_little_endian)
1988 std::reverse(update_values.begin(), update_values.end());
1989 if(offset_bits_in_target_element < 0)
1990 {
1991 if(src.id() == ID_byte_update_little_endian)
1992 {
1993 new_value = lshr_exprt{
1995 update_values, bv_typet{update_size * src.get_bits_per_byte()}},
1996 numeric_cast_v<std::size_t>(-offset_bits_in_target_element)};
1997 }
1998 else
1999 {
2000 new_value = shl_exprt{
2002 update_values, bv_typet{update_size * src.get_bits_per_byte()}},
2003 numeric_cast_v<std::size_t>(-offset_bits_in_target_element)};
2004 }
2005 }
2006 else
2007 {
2008 const std::size_t offset_bits_int =
2009 numeric_cast_v<std::size_t>(offset_bits_in_target_element);
2010 const std::size_t subtype_bits_int =
2011 numeric_cast_v<std::size_t>(subtype_bits);
2012
2013 extractbits_exprt bits_to_keep{
2014 element_to_update,
2015 subtype_bits_int - 1,
2016 subtype_bits_int - offset_bits_int,
2017 bv_typet{offset_bits_int}};
2018 new_value = concatenation_exprt{
2019 bits_to_keep,
2022 update_values, bv_typet{update_size * src.get_bits_per_byte()}},
2023 update_size * src.get_bits_per_byte() - 1,
2024 offset_bits_int,
2025 bv_typet{update_size * src.get_bits_per_byte() - offset_bits_int}},
2026 bv_typet{update_size * src.get_bits_per_byte()}};
2027 }
2028
2029 const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2030 ? ID_byte_extract_little_endian
2031 : ID_byte_extract_big_endian;
2032
2033 const byte_extract_exprt byte_extract_expr{
2034 extract_opcode,
2035 new_value,
2036 from_integer(0, src.offset().type()),
2037 src.get_bits_per_byte(),
2038 update_type};
2039
2040 new_value = lower_byte_extract(byte_extract_expr, ns);
2041
2042 offset_bits_in_target_element = 0;
2043 }
2044
2045 // With an upper bound on the size of the update established, construct the
2046 // actual update expression. If the exact size of the update is unknown,
2047 // make the size expression conditional.
2048 const byte_update_exprt bu{
2049 src.id(),
2050 element_to_update,
2052 offset_bits_in_target_element / src.get_bits_per_byte(),
2053 src.offset().type()),
2054 new_value,
2055 src.get_bits_per_byte()};
2056
2057 optionalt<exprt> update_bound;
2058 if(non_const_update_bound.has_value())
2059 {
2060 // The size of the update is not constant, and thus is to be symbolically
2061 // bound; first see how many bytes we have left in the update:
2062 // non_const_update_bound > first ? non_const_update_bound - first: 0
2063 const exprt remaining_update_bytes = typecast_exprt::conditional_cast(
2064 if_exprt{
2066 *non_const_update_bound,
2067 ID_gt,
2068 from_integer(first, non_const_update_bound->type())},
2070 *non_const_update_bound,
2071 from_integer(first, non_const_update_bound->type())},
2072 from_integer(0, non_const_update_bound->type())},
2073 size_type());
2074 // Now take the minimum of update-bytes-left and the previously computed
2075 // size of the element to be updated:
2076 update_bound = simplify_expr(
2077 if_exprt{
2078 binary_predicate_exprt{update_size_expr, ID_lt, remaining_update_bytes},
2079 update_size_expr,
2080 remaining_update_bytes},
2081 ns);
2082 }
2083
2084 return lower_byte_update(bu, new_value, update_bound, ns);
2085}
2086
2098 const byte_update_exprt &src,
2099 const typet &subtype,
2100 const optionalt<mp_integer> &subtype_bits,
2101 const exprt &value_as_byte_array,
2102 const optionalt<exprt> &non_const_update_bound,
2103 const namespacet &ns)
2104{
2105 const bool is_array = src.type().id() == ID_array;
2106 exprt size;
2108 if(is_array)
2109 {
2110 size = to_array_type(src.type()).size();
2112 }
2113 else
2114 {
2115 size = to_vector_type(src.type()).size();
2117 }
2118
2119 // fall back to bytewise updates in all non-constant or dubious cases
2120 if(
2121 !size.is_constant() || !src.offset().is_constant() ||
2122 !subtype_bits.has_value() || value_as_byte_array.id() != ID_array)
2123 {
2125 src, subtype, value_as_byte_array, non_const_update_bound, ns);
2126 }
2127
2128 std::size_t num_elements =
2130 mp_integer offset_bits =
2132 src.get_bits_per_byte();
2133
2134 exprt::operandst elements;
2135 elements.reserve(num_elements);
2136
2137 std::size_t i = 0;
2138 // copy the prefix not affected by the update
2139 for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bits; ++i)
2140 elements.push_back(index_exprt{src.op(), from_integer(i, index_type)});
2141
2142 // the modified elements
2143 for(;
2144 i < num_elements &&
2145 i * *subtype_bits < offset_bits + value_as_byte_array.operands().size() *
2146 src.get_bits_per_byte();
2147 ++i)
2148 {
2149 elements.push_back(lower_byte_update_single_element(
2150 src,
2151 offset_bits,
2152 index_exprt{src.op(), from_integer(i, index_type)},
2153 *subtype_bits,
2154 i * *subtype_bits,
2155 value_as_byte_array,
2156 non_const_update_bound,
2157 ns));
2158 }
2159
2160 // copy the tail not affected by the update
2161 for(; i < num_elements; ++i)
2162 elements.push_back(index_exprt{src.op(), from_integer(i, index_type)});
2163
2164 if(is_array)
2165 return simplify_expr(
2166 array_exprt{std::move(elements), to_array_type(src.type())}, ns);
2167 else
2168 return simplify_expr(
2169 vector_exprt{std::move(elements), to_vector_type(src.type())}, ns);
2170}
2171
2182 const byte_update_exprt &src,
2183 const struct_typet &struct_type,
2184 const exprt &value_as_byte_array,
2185 const optionalt<exprt> &non_const_update_bound,
2186 const namespacet &ns)
2187{
2188 exprt::operandst elements;
2189 elements.reserve(struct_type.components().size());
2190
2192 for(const auto &comp : struct_type.components())
2193 {
2194 auto element_width = pointer_offset_bits(comp.type(), ns);
2195
2196 // compute the update offset relative to this struct member - will be
2197 // negative if we are already in the middle of the update or beyond it
2198 exprt offset = simplify_expr(
2200 mult_exprt{
2201 src.offset(),
2202 from_integer(src.get_bits_per_byte(), src.offset().type())},
2204 ns);
2205 auto offset_bits = numeric_cast<mp_integer>(offset);
2206 if(!offset_bits.has_value() || !element_width.has_value())
2207 {
2208 // The offset to update is not constant, either because the original
2209 // offset in src never was, or because a struct member has an unknown
2210 // offset. Abort the attempt to update individual struct members and
2211 // instead turn the operand-to-be-updated into a byte array, which we know
2212 // how to update even if the offset is non-constant.
2213 const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2214 ? ID_byte_extract_little_endian
2215 : ID_byte_extract_big_endian;
2216
2217 auto src_size_opt = size_of_expr(src.type(), ns);
2218 CHECK_RETURN(src_size_opt.has_value());
2219
2220 const byte_extract_exprt byte_extract_expr{
2221 extract_opcode,
2222 src.op(),
2223 from_integer(0, src.offset().type()),
2224 src.get_bits_per_byte(),
2225 array_typet{bv_typet{src.get_bits_per_byte()}, src_size_opt.value()}};
2226
2227 byte_update_exprt bu = src;
2228 bu.set_op(lower_byte_extract(byte_extract_expr, ns));
2229 bu.type() = bu.op().type();
2230
2231 return lower_byte_extract(
2233 extract_opcode,
2235 bu, value_as_byte_array, non_const_update_bound, ns),
2236 from_integer(0, src.offset().type()),
2237 src.get_bits_per_byte(),
2238 src.type()},
2239 ns);
2240 }
2241
2242 exprt member = member_exprt{src.op(), comp.get_name(), comp.type()};
2243
2244 // we don't need to update anything when
2245 // 1) the update offset is greater than the end of this member (thus the
2246 // relative offset is greater than this element) or
2247 // 2) the update offset plus the size of the update is less than the member
2248 // offset
2249 if(
2250 *offset_bits >= *element_width ||
2251 (value_as_byte_array.id() == ID_array && *offset_bits < 0 &&
2252 -*offset_bits >=
2253 value_as_byte_array.operands().size() * src.get_bits_per_byte()))
2254 {
2255 elements.push_back(member);
2256 member_offset_bits += *element_width;
2257 continue;
2258 }
2259
2260 elements.push_back(lower_byte_update_single_element(
2261 src,
2262 *offset_bits + member_offset_bits,
2263 member,
2264 *element_width,
2266 value_as_byte_array,
2267 non_const_update_bound,
2268 ns));
2269
2270 member_offset_bits += *element_width;
2271 }
2272
2273 return simplify_expr(struct_exprt{std::move(elements), struct_type}, ns);
2274}
2275
2286 const byte_update_exprt &src,
2287 const union_typet &union_type,
2288 const exprt &value_as_byte_array,
2289 const optionalt<exprt> &non_const_update_bound,
2290 const namespacet &ns)
2291{
2292 const auto widest_member = union_type.find_widest_union_component(ns);
2293
2295 widest_member.has_value(),
2296 "lower_byte_update of union of unknown size is not supported");
2297
2298 byte_update_exprt bu = src;
2300 src.op(), widest_member->first.get_name(), widest_member->first.type()});
2301 bu.type() = widest_member->first.type();
2302
2303 return union_exprt{
2304 widest_member->first.get_name(),
2305 lower_byte_update(bu, value_as_byte_array, non_const_update_bound, ns),
2306 src.type()};
2307}
2308
2318 const byte_update_exprt &src,
2319 const exprt &value_as_byte_array,
2320 const optionalt<exprt> &non_const_update_bound,
2321 const namespacet &ns)
2322{
2323 if(src.type().id() == ID_array || src.type().id() == ID_vector)
2324 {
2325 optionalt<typet> subtype;
2326 if(src.type().id() == ID_vector)
2327 subtype = to_vector_type(src.type()).element_type();
2328 else
2329 subtype = to_array_type(src.type()).element_type();
2330
2331 auto element_width = pointer_offset_bits(*subtype, ns);
2332
2333 if(element_width.has_value() && *element_width == src.get_bits_per_byte())
2334 {
2335 if(value_as_byte_array.id() != ID_array)
2336 {
2338 non_const_update_bound.has_value(),
2339 "constant update bound should yield an array expression");
2341 src, *subtype, value_as_byte_array, *non_const_update_bound, ns);
2342 }
2343
2345 src,
2346 *subtype,
2347 to_array_expr(value_as_byte_array),
2348 non_const_update_bound,
2349 ns);
2350 }
2351 else
2352 {
2354 src,
2355 *subtype,
2356 element_width,
2357 value_as_byte_array,
2358 non_const_update_bound,
2359 ns);
2360 }
2361 }
2362 else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
2363 {
2365 src,
2366 to_struct_type(ns.follow(src.type())),
2367 value_as_byte_array,
2368 non_const_update_bound,
2369 ns);
2370 result.type() = src.type();
2371 return result;
2372 }
2373 else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
2374 {
2376 src,
2377 to_union_type(ns.follow(src.type())),
2378 value_as_byte_array,
2379 non_const_update_bound,
2380 ns);
2381 result.type() = src.type();
2382 return result;
2383 }
2384 else if(
2386 src.type().id() == ID_c_enum || src.type().id() == ID_c_enum_tag)
2387 {
2388 // mask out the bits to be updated, shift the value according to the
2389 // offset and bit-or
2390 const auto type_width = pointer_offset_bits(src.type(), ns);
2391 CHECK_RETURN(type_width.has_value() && *type_width > 0);
2392 const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
2393
2394 exprt::operandst update_bytes;
2395 if(value_as_byte_array.id() == ID_array)
2396 update_bytes = value_as_byte_array.operands();
2397 else
2398 {
2399 update_bytes = instantiate_byte_array(
2400 value_as_byte_array,
2401 0,
2402 (type_bits + src.get_bits_per_byte() - 1) / src.get_bits_per_byte(),
2403 src.get_bits_per_byte(),
2404 ns);
2405 }
2406
2407 const std::size_t update_size_bits =
2408 update_bytes.size() * src.get_bits_per_byte();
2409 const std::size_t bit_width = std::max(type_bits, update_size_bits);
2410
2411 const bool is_little_endian = src.id() == ID_byte_update_little_endian;
2412
2413 exprt val_before =
2414 typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
2415 if(bit_width > type_bits)
2416 {
2417 val_before = concatenation_exprt{
2418 from_integer(0, bv_typet{bit_width - type_bits}),
2419 val_before,
2420 bv_typet{bit_width}};
2421
2422 if(!is_little_endian)
2423 to_concatenation_expr(val_before)
2424 .op0()
2425 .swap(to_concatenation_expr(val_before).op1());
2426 }
2427
2428 if(non_const_update_bound.has_value())
2429 {
2430 const exprt src_as_bytes = unpack_rec(
2431 val_before,
2432 src.id() == ID_byte_update_little_endian,
2433 mp_integer{0},
2434 mp_integer{update_bytes.size()},
2435 src.get_bits_per_byte(),
2436 ns);
2437 CHECK_RETURN(src_as_bytes.id() == ID_array);
2438 CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
2439 for(std::size_t i = 0; i < update_bytes.size(); ++i)
2440 {
2441 update_bytes[i] = if_exprt{
2443 from_integer(i, non_const_update_bound->type()),
2444 ID_lt,
2445 *non_const_update_bound},
2446 update_bytes[i],
2447 src_as_bytes.operands()[i]};
2448 }
2449 }
2450
2451 // build mask
2452 exprt mask;
2453 if(is_little_endian)
2454 mask = from_integer(power(2, update_size_bits) - 1, bv_typet{bit_width});
2455 else
2456 {
2457 mask = from_integer(
2458 power(2, bit_width) - power(2, bit_width - update_size_bits),
2459 bv_typet{bit_width});
2460 }
2461
2462 const typet &offset_type = src.offset().type();
2463 mult_exprt offset_in_bits{
2464 src.offset(), from_integer(src.get_bits_per_byte(), offset_type)};
2465
2466 const binary_predicate_exprt offset_ge_zero{
2467 offset_in_bits, ID_ge, from_integer(0, offset_type)};
2468
2469 if_exprt mask_shifted{
2470 offset_ge_zero,
2471 shl_exprt{mask, offset_in_bits},
2472 lshr_exprt{mask, unary_minus_exprt{offset_in_bits}}};
2473 if(!is_little_endian)
2474 {
2475 mask_shifted.true_case().swap(mask_shifted.false_case());
2476 to_shift_expr(mask_shifted.true_case())
2477 .distance()
2478 .swap(to_shift_expr(mask_shifted.false_case()).distance());
2479 }
2480
2481 // original_bits &= ~mask
2482 bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}};
2483
2484 // concatenate and zero-extend the value
2485 concatenation_exprt value{update_bytes, bv_typet{update_size_bits}};
2486 if(is_little_endian)
2487 std::reverse(value.operands().begin(), value.operands().end());
2488
2489 exprt zero_extended;
2490 if(bit_width > update_size_bits)
2491 {
2492 zero_extended = concatenation_exprt{
2493 from_integer(0, bv_typet{bit_width - update_size_bits}),
2494 value,
2495 bv_typet{bit_width}};
2496
2497 if(!is_little_endian)
2498 to_concatenation_expr(zero_extended)
2499 .op0()
2500 .swap(to_concatenation_expr(zero_extended).op1());
2501 }
2502 else
2503 zero_extended = value;
2504
2505 // shift the value
2506 if_exprt value_shifted{
2507 offset_ge_zero,
2508 shl_exprt{zero_extended, offset_in_bits},
2509 lshr_exprt{zero_extended, unary_minus_exprt{offset_in_bits}}};
2510 if(!is_little_endian)
2511 {
2512 value_shifted.true_case().swap(value_shifted.false_case());
2513 to_shift_expr(value_shifted.true_case())
2514 .distance()
2515 .swap(to_shift_expr(value_shifted.false_case()).distance());
2516 }
2517
2518 // original_bits |= newvalue
2519 bitor_exprt bitor_expr{bitand_expr, value_shifted};
2520
2521 if(bit_width > type_bits)
2522 {
2523 endianness_mapt endianness_map(
2524 bitor_expr.type(), src.id() == ID_byte_update_little_endian, ns);
2525 const auto bounds = map_bounds(endianness_map, 0, type_bits - 1);
2526
2527 PRECONDITION(pointer_offset_bits(bitor_expr.type(), ns).has_value());
2528 return simplify_expr(
2531 bitor_expr, bounds.ub, bounds.lb, bv_typet{type_bits}},
2532 src.type()),
2533 ns);
2534 }
2535
2536 return simplify_expr(
2537 typecast_exprt::conditional_cast(bitor_expr, src.type()), ns);
2538 }
2539 else
2540 {
2542 false, "lower_byte_update does not yet support ", src.type().id_string());
2543 }
2544}
2545
2547{
2549 src.id() == ID_byte_update_little_endian ||
2550 src.id() == ID_byte_update_big_endian,
2551 "byte update expression should either be little or big endian");
2552
2553 // An update of a void-typed object or update by a void-typed value is the
2554 // source operand (this is questionable, but may arise when dereferencing
2555 // invalid pointers).
2556 if(src.type().id() == ID_empty || src.value().type().id() == ID_empty)
2557 return src.op();
2558
2559 // byte_update lowering proceeds as follows:
2560 // 1) Determine the size of the update, with the size of the object to be
2561 // updated as an upper bound. We fail if neither can be determined.
2562 // 2) Turn the update value into a byte array of the size determined above.
2563 // 3) If the offset is not constant, turn the object into a byte array, and
2564 // use a "with" expression to encode the update; else update the values in
2565 // place.
2566 // 4) Construct a new object.
2567 optionalt<exprt> non_const_update_bound;
2568 // update value, may require extension to full bytes
2569 exprt update_value = src.value();
2570 auto update_size_expr_opt = size_of_expr(update_value.type(), ns);
2571 CHECK_RETURN(update_size_expr_opt.has_value());
2572 simplify(update_size_expr_opt.value(), ns);
2573
2574 const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
2575 ? ID_byte_extract_little_endian
2576 : ID_byte_extract_big_endian;
2577 const std::size_t bits_per_byte = src.get_bits_per_byte();
2578
2579 if(!update_size_expr_opt.value().is_constant())
2580 non_const_update_bound = *update_size_expr_opt;
2581 else
2582 {
2583 auto update_bits = pointer_offset_bits(update_value.type(), ns);
2584 // If the following invariant fails, then the type was only found to be
2585 // constant via simplification. Such instances should be fixed at the place
2586 // introducing these constant-but-not-constant_exprt type sizes.
2588 update_bits.has_value(), "constant size-of should imply fixed bit width");
2589 const size_t update_bits_int = numeric_cast_v<size_t>(*update_bits);
2590
2591 if(update_bits_int % bits_per_byte != 0)
2592 {
2594 can_cast_type<bitvector_typet>(update_value.type()),
2595 "non-byte aligned type expected to be a bitvector type");
2596 const byte_extract_exprt overlapping_byte_extract{
2597 extract_opcode,
2598 src.op(),
2600 plus_exprt{
2601 src.offset(),
2602 from_integer(update_bits_int / bits_per_byte, src.offset().type())},
2603 ns),
2604 src.get_bits_per_byte(),
2605 bv_typet{bits_per_byte}};
2606 const exprt overlapping_byte =
2607 lower_byte_extract(overlapping_byte_extract, ns);
2608
2609 size_t n_extra_bits = bits_per_byte - update_bits_int % bits_per_byte;
2610 extractbits_exprt extra_bits{
2611 overlapping_byte, n_extra_bits - 1, 0, bv_typet{n_extra_bits}};
2612
2613 update_value = concatenation_exprt{
2615 update_value, bv_typet{update_bits_int}),
2616 extra_bits,
2617 adjust_width(update_value.type(), update_bits_int + n_extra_bits)};
2618 }
2619 else
2620 {
2621 update_size_expr_opt = from_integer(
2622 update_bits_int / bits_per_byte, update_size_expr_opt->type());
2623 }
2624 }
2625
2626 const byte_extract_exprt byte_extract_expr{
2627 extract_opcode,
2628 update_value,
2629 from_integer(0, src.offset().type()),
2630 src.get_bits_per_byte(),
2631 array_typet{bv_typet{bits_per_byte}, *update_size_expr_opt}};
2632
2633 const exprt value_as_byte_array = lower_byte_extract(byte_extract_expr, ns);
2634
2635 exprt result =
2636 lower_byte_update(src, value_as_byte_array, non_const_update_bound, ns);
2637 return result;
2638}
2639
2641{
2642 exprt tmp = src;
2643
2644 // destroys any sharing, should use hash table
2645 Forall_operands(it, tmp)
2646 {
2647 *it = lower_byte_operators(*it, ns);
2648 }
2649
2650 if(
2651 src.id() == ID_byte_update_little_endian ||
2652 src.id() == ID_byte_update_big_endian)
2653 {
2654 return lower_byte_update(to_byte_update_expr(tmp), ns);
2655 }
2656 else if(
2657 src.id() == ID_byte_extract_little_endian ||
2658 src.id() == ID_byte_extract_big_endian)
2659 {
2661 }
2662 else
2663 return tmp;
2664}
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.
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet index_type()
Definition c_types.cpp:22
unsignedbv_typet size_type()
Definition c_types.cpp:55
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition c_types.h:80
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3358
Array constructor from list of elements.
Definition std_expr.h:1563
Arrays with given size.
Definition std_types.h:763
typet index_type() const
The type of the index expressions into any instance of this type.
Definition std_types.cpp:33
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:676
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition std_types.h:865
std::size_t get_width() const
Definition std_types.h:876
Fixed-width bit-vector without numerical interpretation.
Expression of type type extracted from some object op starting at position offset (given in number of...
std::size_t get_bits_per_byte() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & offset() const
const exprt & op() const
void set_op(exprt e)
std::size_t get_bits_per_byte() const
const exprt & value() const
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition c_types.h:20
Complex constructor from a pair of numbers.
Definition std_expr.h:1858
Imaginary part of the expression describing a complex number.
Definition std_expr.h:1971
Real part of the expression describing a complex number.
Definition std_expr.h:1926
Complex numbers made of pair of given subtype.
Definition std_types.h:1077
Concatenation of bit-vector operands.
Division.
Definition std_expr.h:1097
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1774
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:1306
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
Extracts a sub-range of a bit-vector operand.
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
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:2794
Binary minus.
Definition std_expr.h:1006
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1168
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
exprt & op0()
Definition std_expr.h:877
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:3026
Boolean OR.
Definition std_expr.h:2179
The plus expression Associativity is not specified.
Definition std_expr.h:947
exprt & distance()
Left shift.
Fixed-width bit-vector with two's complement interpretation.
Struct constructor from list of elements.
Definition std_expr.h:1819
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:113
const typet & subtype() const
Definition type.h:154
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
The unary minus expression.
Definition std_expr.h:423
Union constructor from single element.
Definition std_expr.h:1708
The union type.
Definition c_types.h:147
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:305
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Definition std_expr.h:1672
The vector type.
Definition std_types.h:1008
const constant_exprt & size() const
typet index_type() const
The type of any index expression into an instance of this type.
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1024
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
#define Forall_operands(it, expr)
Definition expr.h:27
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
static exprt lower_byte_update_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 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 std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector 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 exprt bv_to_union_expr(const exprt &bitvector_expr, const union_typet &union_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a union-typed expression.
static complex_exprt bv_to_complex_expr(const exprt &bitvector_expr, const complex_typet &complex_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a complex-typed expression.
static 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 ...
static exprt unpack_rec(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array=false)
Rewrite an object into its individual bytes.
static exprt::operandst instantiate_byte_array(const exprt &src, std::size_t lower_bound, std::size_t upper_bound, const std::size_t bits_per_byte, const namespacet &ns)
Build the individual bytes to be used in an update.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
static optionalt< exprt > lower_byte_extract_complex(const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns)
Rewrite a byte extraction of a complex-typed result to byte extraction of the individual components t...
static exprt lower_byte_update_array_vector(const byte_update_exprt &src, const typet &subtype, const optionalt< mp_integer > &subtype_bits, 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 ...
bitvector_typet adjust_width(const typet &src, std::size_t new_width)
changes the width of the given bitvector type
static vector_exprt bv_to_vector_expr(const exprt &bitvector_expr, const vector_typet &vector_type, const endianness_mapt &endianness_map, const namespacet &ns)
Convert a bitvector-typed expression bitvector_expr to a vector-typed expression.
static 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 array_exprt unpack_complex(const exprt &src, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a complex_exprt into its individual bytes.
static exprt unpack_array_vector_no_known_bounds(const exprt &src, std::size_t el_bytes, bool little_endian, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite an array or vector into its individual bytes when no maximum number of bytes is known.
static exprt lower_byte_update_single_element(const byte_update_exprt &src, const mp_integer &offset_bits, const exprt &element_to_update, const mp_integer &subtype_bits, const mp_integer &bits_already_set, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Byte update a struct/array/vector element.
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 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 std::size_t bits_per_byte, const namespacet &ns)
Extract bytes from a sequence of bitvector-typed elements.
static array_exprt unpack_struct(const exprt &src, bool little_endian, const optionalt< mp_integer > &offset_bytes, const optionalt< mp_integer > &max_bytes, const std::size_t bits_per_byte, const namespacet &ns)
Rewrite a struct-typed expression into its individual bytes.
static exprt 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_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...
output_type narrow_cast(input_type value)
Alias for static_cast intended to be used for numeric casting Rationale: Easier to grep than static_c...
Definition narrow.h:19
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:18
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1603
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
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:1102
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition std_types.h:899
const string_constantt & to_string_constant(const exprt &expr)
static bool failed(bool error_indicator)
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175