CBMC: /home/runner/work/cbmc/cbmc/src/util/pointer_offset_size.cpp Source File

CBMC
Loading...
Searching...
No Matches
pointer_offset_size.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Pointer Logic
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "pointer_offset_size.h"
13
14#include "arith_tools.h"
15#include "byte_operators.h"
16#include "c_types.h"
17#include "config.h"
18#include "invariant.h"
19#include "namespace.h"
20#include "pointer_expr.h"
21#include "simplify_expr.h"
22#include "ssa_expr.h"
23#include "std_expr.h"
24
25 std::optional<mp_integer> member_offset(
26 const struct_typet &type,
27 const irep_idt &member,
28 const namespacet &ns)
29{
30 mp_integer result = 0;
31 std::size_t bit_field_bits = 0;
32
33 for(const auto &comp : type.components())
34 {
35 if(comp.get_name() == member)
36 return result;
37
38 if(comp.type().id() == ID_c_bit_field)
39 {
40 const std::size_t w = to_c_bit_field_type(comp.type()).get_width();
42 result += bit_field_bits / config.ansi_c.char_width;
43 bit_field_bits %= config.ansi_c.char_width;
44 }
45 else if(comp.is_boolean())
46 {
48 result += bit_field_bits / config.ansi_c.char_width;
49 bit_field_bits %= config.ansi_c.char_width;
50 }
51 else
52 {
54 bit_field_bits == 0, "padding ensures offset at byte boundaries");
55 const auto sub_size = pointer_offset_size(comp.type(), ns);
56 if(!sub_size.has_value())
57 return {};
58 else
59 result += *sub_size;
60 }
61 }
62
63 return result;
64}
65
66 std::optional<mp_integer> member_offset_bits(
67 const struct_typet &type,
68 const irep_idt &member,
69 const namespacet &ns)
70{
71 mp_integer offset=0;
72 const struct_typet::componentst &components=type.components();
73
74 for(const auto &comp : components)
75 {
76 if(comp.get_name()==member)
77 return offset;
78
79 auto member_bits = pointer_offset_bits(comp.type(), ns);
80 if(!member_bits.has_value())
81 return {};
82
83 offset += *member_bits;
84 }
85
86 return {};
87}
88
90std::optional<mp_integer>
91 pointer_offset_size(const typet &type, const namespacet &ns)
92{
93 auto bits = pointer_offset_bits(type, ns);
94
95 if(bits.has_value())
96 return (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
97 else
98 return {};
99}
100
101std::optional<mp_integer>
102 pointer_offset_bits(const typet &type, const namespacet &ns)
103{
104 if(type.id()==ID_array)
105 {
106 auto sub = pointer_offset_bits(to_array_type(type).element_type(), ns);
107 if(!sub.has_value())
108 return {};
109
110 // get size - we can only distinguish the elements if the size is constant
111 const auto size = numeric_cast<mp_integer>(to_array_type(type).size());
112 if(!size.has_value())
113 return {};
114
115 return (*sub) * (*size);
116 }
117 else if(type.id()==ID_vector)
118 {
119 auto sub = pointer_offset_bits(to_vector_type(type).element_type(), ns);
120 if(!sub.has_value())
121 return {};
122
123 // get size
124 const mp_integer size =
126
127 return (*sub) * size;
128 }
129 else if(type.id()==ID_complex)
130 {
131 auto sub = pointer_offset_bits(to_complex_type(type).subtype(), ns);
132
133 if(sub.has_value())
134 return (*sub) * 2;
135 else
136 return {};
137 }
138 else if(type.id()==ID_struct)
139 {
141 mp_integer result=0;
142
143 for(const auto &c : struct_type.components())
144 {
145 const typet &subtype = c.type();
146 auto sub_size = pointer_offset_bits(subtype, ns);
147
148 if(!sub_size.has_value())
149 return {};
150
151 result += *sub_size;
152 }
153
154 return result;
155 }
156 else if(type.id()==ID_union)
157 {
159
160 if(union_type.components().empty())
161 return mp_integer{0};
162
163 const auto widest_member = union_type.find_widest_union_component(ns);
164
165 if(widest_member.has_value())
166 return widest_member->second;
167 else
168 return {};
169 }
170 else if(type.id()==ID_signedbv ||
171 type.id()==ID_unsignedbv ||
172 type.id()==ID_fixedbv ||
173 type.id()==ID_floatbv ||
174 type.id()==ID_bv ||
175 type.id()==ID_c_bool ||
176 type.id()==ID_c_bit_field)
177 {
178 return mp_integer(to_bitvector_type(type).get_width());
179 }
180 else if(type.id()==ID_c_enum)
181 {
182 return mp_integer(
183 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width());
184 }
185 else if(type.id()==ID_c_enum_tag)
186 {
188 }
189 else if(type.id()==ID_bool)
190 {
191 return mp_integer(1);
192 }
193 else if(type.id()==ID_pointer)
194 {
195 // the following is an MS extension
196 if(type.get_bool(ID_C_ptr32))
197 return mp_integer(32);
198
199 return mp_integer(to_bitvector_type(type).get_width());
200 }
201 else if(type.id() == ID_union_tag)
202 {
204 }
205 else if(type.id() == ID_struct_tag)
206 {
208 }
209 else if(type.id()==ID_code)
210 {
211 return mp_integer(0);
212 }
213 else if(type.id()==ID_string)
214 {
215 return mp_integer(32);
216 }
217 else
218 return {};
219}
220
221std::optional<exprt>
223{
224 // need to distinguish structs and unions
225 const typet &compound_type = member_expr.struct_op().type();
226 if(compound_type.id() == ID_struct || compound_type.id() == ID_struct_tag)
227 {
229 compound_type.id() == ID_struct_tag
230 ? ns.follow_tag(to_struct_tag_type(compound_type))
231 : to_struct_type(compound_type);
232 return member_offset_expr(
233 struct_type, member_expr.get_component_name(), ns);
234 }
235 else if(compound_type.id() == ID_union || compound_type.id() == ID_union_tag)
236 return from_integer(0, size_type());
237 else
238 return {};
239}
240
241 std::optional<exprt> member_offset_expr(
242 const struct_typet &type,
243 const irep_idt &member,
244 const namespacet &ns)
245{
246 PRECONDITION(size_type().get_width() != 0);
247 exprt result=from_integer(0, size_type());
248 std::size_t bit_field_bits=0;
249
250 for(const auto &c : type.components())
251 {
252 if(c.get_name() == member)
253 break;
254
255 if(c.type().id() == ID_c_bit_field)
256 {
257 std::size_t w = to_c_bit_field_type(c.type()).get_width();
258 bit_field_bits += w;
259 const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
260 bit_field_bits %= config.ansi_c.char_width;
261 if(bytes > 0)
262 result = plus_exprt(result, from_integer(bytes, result.type()));
263 }
264 else if(c.is_boolean())
265 {
267 const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
268 bit_field_bits %= config.ansi_c.char_width;
269 if(bytes > 0)
270 result = plus_exprt(result, from_integer(bytes, result.type()));
271 }
272 else
273 {
275 bit_field_bits == 0, "padding ensures offset at byte boundaries");
276 const typet &subtype = c.type();
277 auto sub_size = size_of_expr(subtype, ns);
278 if(!sub_size.has_value())
279 return {}; // give up
280 result = plus_exprt(result, sub_size.value());
281 }
282 }
283
284 return simplify_expr(std::move(result), ns);
285}
286
287 std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
288{
289 if(type.id()==ID_array)
290 {
291 const auto &array_type = to_array_type(type);
292
293 auto sub = size_of_expr(array_type.element_type(), ns);
294 if(!sub.has_value())
295 return {};
296
297 const exprt &size = array_type.size();
298
299 if(size.is_nil())
300 return {};
301
302 const auto size_casted =
303 typecast_exprt::conditional_cast(size, sub.value().type());
304
305 return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
306 }
307 else if(type.id()==ID_vector)
308 {
309 const auto &vector_type = to_vector_type(type);
310
311 // special-case vectors of bits
312 if(vector_type.element_type().id() == ID_bool)
313 {
314 auto bits = pointer_offset_bits(vector_type, ns);
315
316 if(bits.has_value())
317 return from_integer(
318 (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,
319 size_type());
320 }
321
322 auto sub = size_of_expr(vector_type.element_type(), ns);
323 if(!sub.has_value())
324 return {};
325
326 const exprt &size = to_vector_type(type).size();
327
328 if(size.is_nil())
329 return {};
330
331 const auto size_casted =
332 typecast_exprt::conditional_cast(size, sub.value().type());
333
334 return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
335 }
336 else if(type.id()==ID_complex)
337 {
338 auto sub = size_of_expr(to_complex_type(type).subtype(), ns);
339 if(!sub.has_value())
340 return {};
341
342 exprt size = from_integer(2, sub.value().type());
343 return simplify_expr(mult_exprt{std::move(size), sub.value()}, ns);
344 }
345 else if(type.id()==ID_struct)
346 {
348
349 exprt result=from_integer(0, size_type());
350 std::size_t bit_field_bits=0;
351
352 for(const auto &c : struct_type.components())
353 {
354 if(c.type().id() == ID_c_bit_field)
355 {
356 std::size_t w = to_c_bit_field_type(c.type()).get_width();
357 bit_field_bits += w;
358 const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
359 bit_field_bits %= config.ansi_c.char_width;
360 if(bytes > 0)
361 result = plus_exprt(result, from_integer(bytes, result.type()));
362 }
363 else if(c.type().get_bool(ID_C_flexible_array_member))
364 {
365 // flexible array members do not change the sizeof result
366 continue;
367 }
368 else
369 {
371 bit_field_bits == 0, "padding ensures offset at byte boundaries");
372 const typet &subtype = c.type();
373 auto sub_size_opt = size_of_expr(subtype, ns);
374 if(!sub_size_opt.has_value())
375 return {};
376
377 result = plus_exprt(result, sub_size_opt.value());
378 }
379 }
380
381 return simplify_expr(std::move(result), ns);
382 }
383 else if(type.id()==ID_union)
384 {
386
388 exprt result=from_integer(0, size_type());
389
390 // compute max
391
392 for(const auto &c : union_type.components())
393 {
394 const typet &subtype = c.type();
396
397 auto sub_bits = pointer_offset_bits(subtype, ns);
398
399 if(!sub_bits.has_value())
400 {
401 max_bytes=-1;
402
403 auto sub_size_opt = size_of_expr(subtype, ns);
404 if(!sub_size_opt.has_value())
405 return {};
406 sub_size = sub_size_opt.value();
407 }
408 else
409 {
411 (*sub_bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
412
413 if(max_bytes>=0)
414 {
416 {
419 }
420
421 continue;
422 }
423
425 }
426
427 result=if_exprt(
429 sub_size, result);
430
431 simplify(result, ns);
432 }
433
434 return result;
435 }
436 else if(type.id()==ID_signedbv ||
437 type.id()==ID_unsignedbv ||
438 type.id()==ID_fixedbv ||
439 type.id()==ID_floatbv ||
440 type.id()==ID_bv ||
441 type.id()==ID_c_bool ||
442 type.id()==ID_c_bit_field)
443 {
444 std::size_t width=to_bitvector_type(type).get_width();
445 std::size_t bytes = width / config.ansi_c.char_width;
446 if(bytes * config.ansi_c.char_width != width)
447 bytes++;
448 return from_integer(bytes, size_type());
449 }
450 else if(type.id()==ID_c_enum)
451 {
452 return size_of_expr(to_c_enum_type(type).underlying_type(), ns);
453 }
454 else if(type.id()==ID_c_enum_tag)
455 {
456 return size_of_expr(ns.follow_tag(to_c_enum_tag_type(type)), ns);
457 }
458 else if(type.id()==ID_bool)
459 {
460 // bool is a mathematical type, and has no memory layout
461 return {};
462 }
463 else if(type.id()==ID_pointer)
464 {
465 // the following is an MS extension
466 if(type.get_bool(ID_C_ptr32))
467 return from_integer(32 / config.ansi_c.char_width, size_type());
468
469 std::size_t width=to_bitvector_type(type).get_width();
470 std::size_t bytes = width / config.ansi_c.char_width;
471 if(bytes * config.ansi_c.char_width != width)
472 bytes++;
473 return from_integer(bytes, size_type());
474 }
475 else if(type.id() == ID_union_tag)
476 {
477 return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns);
478 }
479 else if(type.id() == ID_struct_tag)
480 {
481 return size_of_expr(ns.follow_tag(to_struct_tag_type(type)), ns);
482 }
483 else if(type.id()==ID_code)
484 {
485 return from_integer(0, size_type());
486 }
487 else if(type.id()==ID_string)
488 {
489 return from_integer(32 / config.ansi_c.char_width, size_type());
490 }
491 else if(type.id() == ID_rational)
492 {
493 // these shouldn't really have sizes but this will do
494 return from_integer(1, size_type());
495 }
496 else
497 return {};
498}
499
500 bool is_zero_width(const typet &type, const namespacet &ns)
501{
502 if(type.id() == ID_empty)
503 return true;
504 else if(type.id() == ID_struct_tag)
505 return is_zero_width(ns.follow_tag(to_struct_tag_type(type)), ns);
506 else if(type.id() == ID_union_tag)
507 return is_zero_width(ns.follow_tag(to_union_tag_type(type)), ns);
508 else if(type.id() == ID_c_enum_tag)
509 return is_zero_width(ns.follow_tag(to_c_enum_tag_type(type)), ns);
510 else if(type.id() == ID_c_enum)
511 return is_zero_width(to_c_enum_type(type).subtype(), ns);
512 else if(type.id() == ID_struct || type.id() == ID_union)
513 {
514 for(const auto &comp : to_struct_union_type(type).components())
515 {
516 if(!is_zero_width(comp.type(), ns))
517 return false;
518 }
519 return true;
520 }
522 {
523 // we ignore array_type->size().is_zero() for now as there may be
524 // out-of-bounds accesses that we need to model
525 return is_zero_width(array_type->element_type(), ns);
526 }
528 {
529 return bv_type->width() == 0;
530 }
531 else
532 return false;
533}
534
535std::optional<mp_integer>
537{
538 if(expr.id()==ID_symbol)
539 {
540 if(is_ssa_expr(expr))
542 to_ssa_expr(expr).get_original_expr(), ns);
543 else
544 return mp_integer(0);
545 }
546 else if(expr.id()==ID_index)
547 {
550 index_expr.array().type().id() == ID_array,
551 "index into array expected, found " +
552 index_expr.array().type().id_string());
553
554 auto o = compute_pointer_offset(index_expr.array(), ns);
555
556 if(o.has_value())
557 {
558 const auto &array_type = to_array_type(index_expr.array().type());
559 auto sub_size = pointer_offset_size(array_type.element_type(), ns);
560
561 if(sub_size.has_value() && *sub_size > 0)
562 {
563 const auto i = numeric_cast<mp_integer>(index_expr.index());
564 if(i.has_value())
565 return (*o) + (*i) * (*sub_size);
566 }
567 }
568
569 // don't know
570 }
571 else if(expr.id()==ID_member)
572 {
574 const exprt &op=member_expr.struct_op();
575
576 auto o = compute_pointer_offset(op, ns);
577
578 if(o.has_value())
579 {
580 if(op.type().id() == ID_union || op.type().id() == ID_union_tag)
581 return *o;
582
584 op.type().id() == ID_struct_tag
586 : to_struct_type(op.type());
587 auto member_offset =
588 ::member_offset(struct_type, member_expr.get_component_name(), ns);
589
590 if(member_offset.has_value())
591 return *o + *member_offset;
592 }
593 }
594 else if(expr.id()==ID_string_constant)
595 return mp_integer(0);
596
597 return {}; // don't know
598}
599
600 std::optional<exprt> get_subexpression_at_offset(
601 const exprt &expr,
603 const typet &target_type_raw,
604 const namespacet &ns)
605{
606 if(offset_bytes == 0 && expr.type() == target_type_raw)
607 return expr;
608
609 if(
610 offset_bytes == 0 && expr.type().id() == ID_pointer &&
612 {
613 return typecast_exprt(expr, target_type_raw);
614 }
615
617 if(!target_size_bits.has_value())
618 return {};
619
620 if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
621 {
623 expr.type().id() == ID_struct_tag
625 : to_struct_type(expr.type());
626
628 for(const auto &component : struct_type.components())
629 {
630 const auto m_size_bits = pointer_offset_bits(component.type(), ns);
631 if(!m_size_bits.has_value())
632 return {};
633
634 // if this member completely contains the target, and this member is
635 // byte-aligned, recurse into it
636 if(
637 offset_bytes * config.ansi_c.char_width >= m_offset_bits &&
638 m_offset_bits % config.ansi_c.char_width == 0 &&
639 offset_bytes * config.ansi_c.char_width + *target_size_bits <=
641 {
642 const member_exprt member(expr, component.get_name(), component.type());
644 member,
647 ns);
648 }
649
651 }
652 }
653 else if(expr.type().id() == ID_array)
654 {
655 const array_typet &array_type = to_array_type(expr.type());
656
657 const auto elem_size_bits =
658 pointer_offset_bits(array_type.element_type(), ns);
659
660 // no arrays of non-byte-aligned, zero-, or unknown-sized objects
661 if(
662 array_type.size().is_constant() && elem_size_bits.has_value() &&
663 *elem_size_bits > 0 && *elem_size_bits % config.ansi_c.char_width == 0 &&
665 {
666 const mp_integer array_size =
669 *elem_size_bits / config.ansi_c.char_width;
672 const auto target_size_bytes =
673 *target_size_bits / config.ansi_c.char_width;
674 // only recurse if the cell completely contains the target
675 if(
676 index < array_size &&
678 {
681 expr,
683 offset_bytes / elem_size_bytes, array_type.index_type())),
686 ns);
687 }
688 }
689 }
690 else if(
691 object_descriptor_exprt(expr).root_object().id() == ID_union &&
692 (expr.type().id() == ID_union || expr.type().id() == ID_union_tag))
693 {
694 const union_typet &union_type =
695 expr.type().id() == ID_union_tag
696 ? ns.follow_tag(to_union_tag_type(expr.type()))
697 : to_union_type(expr.type());
698
699 for(const auto &component : union_type.components())
700 {
701 const auto m_size_bits = pointer_offset_bits(component.type(), ns);
702 if(!m_size_bits.has_value())
703 continue;
704
705 // if this member completely contains the target, recurse into it
706 if(
707 offset_bytes * config.ansi_c.char_width + *target_size_bits <=
709 {
710 const member_exprt member(expr, component.get_name(), component.type());
712 member, offset_bytes, target_type_raw, ns);
713 }
714 }
715 }
716
717 return make_byte_extract(
719}
720
721 static bool is_multiplication_by_constant(const exprt &expr)
722{
723 if(expr.id() != ID_mult)
724 return false;
725 if(expr.operands().size() != 2)
726 return false;
727 return to_multi_ary_expr(expr).op0().is_constant() ||
728 to_multi_ary_expr(expr).op1().is_constant();
729}
730
731 std::optional<exprt> get_subexpression_at_offset(
732 const exprt &expr,
733 const exprt &offset,
734 const typet &target_type,
735 const namespacet &ns)
736{
737 const auto offset_bytes = numeric_cast<mp_integer>(offset);
738
739 if(!offset_bytes.has_value())
740 {
741 // offset is not a constant; try to see whether it is a multiple of a
742 // constant, or a sum that involves a multiple of a constant
744 {
745 const auto target_size_bits = pointer_offset_bits(target_type, ns);
746 const auto elem_size_bits =
747 pointer_offset_bits(array_type->element_type(), ns);
748
749 // no arrays of zero-, or unknown-sized elements, or ones where elements
750 // have a bit-width that isn't a multiple of bytes
751 if(
752 !target_size_bits.has_value() || !elem_size_bits.has_value() ||
753 *elem_size_bits <= 0 ||
754 *elem_size_bits % config.ansi_c.char_width != 0 ||
756 {
757 return {};
758 }
759
761 *elem_size_bits / config.ansi_c.char_width;
762
763 // If we have an offset C + x (where C is a constant) we can try to
764 // recurse by first looking at the member at offset C.
765 if(
766 offset.id() == ID_plus && offset.operands().size() == 2 &&
767 (to_multi_ary_expr(offset).op0().is_constant() ||
768 to_multi_ary_expr(offset).op1().is_constant()))
769 {
770 const plus_exprt &offset_plus = to_plus_expr(offset);
772 offset_plus.op0().is_constant() ? offset_plus.op0()
773 : offset_plus.op1()));
774 const exprt &other_factor = offset_plus.op0().is_constant()
775 ? offset_plus.op1()
776 : offset_plus.op0();
777
778 auto expr_at_offset_C =
779 get_subexpression_at_offset(expr, const_factor, target_type, ns);
780
781 if(
782 expr_at_offset_C.has_value() && expr_at_offset_C->id() == ID_index &&
783 to_index_expr(*expr_at_offset_C).index() == 0)
784 {
786 to_index_expr(*expr_at_offset_C).array(),
788 target_type,
789 ns);
790 }
791 }
792 // If we have an offset that is a sum of multiplications of the form K * i
793 // or i * K (where K is a constant) then try to recurse while removing one
794 // element from this sum.
795 else if(
796 offset.id() == ID_plus && offset.operands().size() == 2 &&
798 {
799 const plus_exprt &offset_plus = to_plus_expr(offset);
800 const mult_exprt &mul = to_mult_expr(offset_plus.op0());
801 const exprt &remaining_offset = offset_plus.op1();
803 to_constant_expr(mul.op0().is_constant() ? mul.op0() : mul.op1()));
804 const exprt &other_factor =
805 mul.op0().is_constant() ? mul.op1() : mul.op0();
806
808 return {};
809
810 exprt index = mult_exprt{
813
816 expr,
817 typecast_exprt::conditional_cast(index, array_type->index_type())},
819 target_type,
820 ns);
821 }
822
823 // give up if the offset expression isn't of the form K * i or i * K
824 // (where K is a constant)
826 {
827 return {};
828 }
829
830 const mult_exprt &offset_mult = to_mult_expr(offset);
832 offset_mult.op0().is_constant() ? offset_mult.op0()
833 : offset_mult.op1()));
834 const exprt &other_factor =
835 offset_mult.op0().is_constant() ? offset_mult.op1() : offset_mult.op0();
836
837 if(
840 {
841 // Decompose the flat index into outer and inner indices using
842 // integer division and remainder. This is correct because
843 // multi-dimensional arrays are laid out contiguously, so
844 // flat_offset = k * const_factor maps to array[k / divider] at
845 // remaining offset (k % divider) * const_factor within that
846 // element. An inner index exceeding the inner dimension simply
847 // wraps to the next element, which is the correct flat-layout
848 // semantics.
850 exprt index = div_exprt{
853 mod_exprt{
856
859 expr,
860 typecast_exprt::conditional_cast(index, array_type->index_type())},
862 target_type,
863 ns);
864 }
865 else if(const_factor % elem_size_bytes != 0)
866 return {};
867
868 exprt index = mult_exprt{
871
874 expr,
875 typecast_exprt::conditional_cast(index, array_type->index_type())},
876 0,
877 target_type,
878 ns);
879 }
880 else if(
881 auto struct_tag_type =
883 {
884 // If the struct only has a single member then we recurse into that
885 // member.
886 const auto &components = ns.follow_tag(*struct_tag_type).components();
887 if(components.size() == 1)
888 {
890 member_exprt{expr, components.front()}, offset, target_type, ns);
891 }
892 // If we have an offset C + x (where C is a constant) we can try to
893 // recurse by first looking at the member at offset C.
894 else if(
895 offset.id() == ID_plus && offset.operands().size() == 2 &&
896 (to_multi_ary_expr(offset).op0().is_constant() ||
897 to_multi_ary_expr(offset).op1().is_constant()))
898 {
899 const plus_exprt &offset_plus = to_plus_expr(offset);
901 offset_plus.op0().is_constant() ? offset_plus.op0()
902 : offset_plus.op1()));
903 const exprt &other_factor = offset_plus.op0().is_constant()
904 ? offset_plus.op1()
905 : offset_plus.op0();
906
907 auto expr_at_offset_C =
908 get_subexpression_at_offset(expr, const_factor, target_type, ns);
909
910 if(
911 expr_at_offset_C.has_value() && expr_at_offset_C->id() == ID_index &&
912 to_index_expr(*expr_at_offset_C).index() == 0)
913 {
915 to_index_expr(*expr_at_offset_C).array(),
917 target_type,
918 ns);
919 }
920 }
921
922 return {};
923 }
924 else if(expr.type().id() == ID_union || expr.type().id() == ID_union_tag)
925 {
926 // For union-typed expressions with non-constant offset, access
927 // through the widest member to avoid expensive byte_extract lowering.
928 // This is safe when the widest member covers the full union (no
929 // trailing padding beyond it), since all members start at offset 0.
930 if(expr.id() == ID_symbol || expr.id() == ID_member)
931 {
932 const union_typet &union_type =
933 expr.type().id() == ID_union_tag
934 ? ns.follow_tag(to_union_tag_type(expr.type()))
935 : to_union_type(expr.type());
936
937 const auto union_size = pointer_offset_bits(union_type, ns);
938 const auto widest_member = union_type.find_widest_union_component(ns);
939 if(
940 widest_member.has_value() && union_size.has_value() &&
941 widest_member->second == *union_size)
942 {
943 const member_exprt member(
944 expr, widest_member->first.get_name(), widest_member->first.type());
945 return get_subexpression_at_offset(member, offset, target_type, ns);
946 }
947 }
948 return {};
949 }
950 else
951 return {};
952 }
953 else
954 return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
955}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
bitvector_typet c_index_type()
Definition c_types.cpp:16
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition c_types.h: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 c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Arrays with given size.
Definition std_types.h:806
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:784
struct configt::ansi_ct ansi_c
Division.
Definition std_expr.h:1152
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:57
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:213
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
The trinary if-then-else operator.
Definition std_expr.h:2426
Array index operator.
Definition std_expr.h:1431
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
Extract member of struct or union.
Definition std_expr.h:2866
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1216
Binary multiplication Associativity is not specified.
Definition std_expr.h:1104
exprt & op1()
Definition std_expr.h:942
exprt & op0()
Definition std_expr.h:936
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Split an expression into a base object and a (byte) offset.
Definition pointer_expr.h:181
The plus expression Associativity is not specified.
Definition std_expr.h:1006
Structure type, corresponds to C style structs.
Definition std_types.h:230
const componentst & components() const
Definition std_types.h:146
std::vector< componentt > componentst
Definition std_types.h:139
Semantic type conversion.
Definition std_expr.h:1995
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
The type of an expression, extends irept.
Definition type.h:29
The union type.
Definition c_types.h:147
API to expression classes for Pointers.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
bool is_zero_width(const typet &type, const namespacet &ns)
Returns true iff type has effective width of zero bits.
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
static bool is_multiplication_by_constant(const exprt &expr)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#define 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
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:291
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1494
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1134
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition std_expr.h:1045
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:991
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2953
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3078
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1006
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:28
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:307
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:517
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1048
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:213
#define size_type
Definition unistd.c:186

AltStyle によって変換されたページ (->オリジナル) /