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
25std::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
66std::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>
91pointer_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>
102pointer_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
241std::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
287std::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
492 return {};
493}
494
495std::optional<mp_integer>
497{
498 if(expr.id()==ID_symbol)
499 {
500 if(is_ssa_expr(expr))
502 to_ssa_expr(expr).get_original_expr(), ns);
503 else
504 return mp_integer(0);
505 }
506 else if(expr.id()==ID_index)
507 {
510 index_expr.array().type().id() == ID_array,
511 "index into array expected, found " +
512 index_expr.array().type().id_string());
513
514 auto o = compute_pointer_offset(index_expr.array(), ns);
515
516 if(o.has_value())
517 {
518 const auto &array_type = to_array_type(index_expr.array().type());
519 auto sub_size = pointer_offset_size(array_type.element_type(), ns);
520
521 if(sub_size.has_value() && *sub_size > 0)
522 {
523 const auto i = numeric_cast<mp_integer>(index_expr.index());
524 if(i.has_value())
525 return (*o) + (*i) * (*sub_size);
526 }
527 }
528
529 // don't know
530 }
531 else if(expr.id()==ID_member)
532 {
534 const exprt &op=member_expr.struct_op();
535
536 auto o = compute_pointer_offset(op, ns);
537
538 if(o.has_value())
539 {
540 if(op.type().id() == ID_union || op.type().id() == ID_union_tag)
541 return *o;
542
544 op.type().id() == ID_struct_tag
546 : to_struct_type(op.type());
547 auto member_offset =
548 ::member_offset(struct_type, member_expr.get_component_name(), ns);
549
550 if(member_offset.has_value())
551 return *o + *member_offset;
552 }
553 }
554 else if(expr.id()==ID_string_constant)
555 return mp_integer(0);
556
557 return {}; // don't know
558}
559
560std::optional<exprt> get_subexpression_at_offset(
561 const exprt &expr,
563 const typet &target_type_raw,
564 const namespacet &ns)
565{
566 if(offset_bytes == 0 && expr.type() == target_type_raw)
567 return expr;
568
569 if(
570 offset_bytes == 0 && expr.type().id() == ID_pointer &&
572 {
573 return typecast_exprt(expr, target_type_raw);
574 }
575
577 if(!target_size_bits.has_value())
578 return {};
579
580 if(expr.type().id() == ID_struct || expr.type().id() == ID_struct_tag)
581 {
583 expr.type().id() == ID_struct_tag
585 : to_struct_type(expr.type());
586
588 for(const auto &component : struct_type.components())
589 {
590 const auto m_size_bits = pointer_offset_bits(component.type(), ns);
591 if(!m_size_bits.has_value())
592 return {};
593
594 // if this member completely contains the target, and this member is
595 // byte-aligned, recurse into it
596 if(
597 offset_bytes * config.ansi_c.char_width >= m_offset_bits &&
598 m_offset_bits % config.ansi_c.char_width == 0 &&
599 offset_bytes * config.ansi_c.char_width + *target_size_bits <=
601 {
602 const member_exprt member(expr, component.get_name(), component.type());
604 member,
607 ns);
608 }
609
611 }
612 }
613 else if(expr.type().id() == ID_array)
614 {
615 const array_typet &array_type = to_array_type(expr.type());
616
617 const auto elem_size_bits =
618 pointer_offset_bits(array_type.element_type(), ns);
619
620 // no arrays of non-byte-aligned, zero-, or unknown-sized objects
621 if(
622 array_type.size().is_constant() && elem_size_bits.has_value() &&
623 *elem_size_bits > 0 && *elem_size_bits % config.ansi_c.char_width == 0 &&
625 {
626 const mp_integer array_size =
629 *elem_size_bits / config.ansi_c.char_width;
632 const auto target_size_bytes =
633 *target_size_bits / config.ansi_c.char_width;
634 // only recurse if the cell completely contains the target
635 if(
636 index < array_size &&
638 {
641 expr,
643 offset_bytes / elem_size_bytes, array_type.index_type())),
646 ns);
647 }
648 }
649 }
650 else if(
651 object_descriptor_exprt(expr).root_object().id() == ID_union &&
652 (expr.type().id() == ID_union || expr.type().id() == ID_union_tag))
653 {
654 const union_typet &union_type =
655 expr.type().id() == ID_union_tag
656 ? ns.follow_tag(to_union_tag_type(expr.type()))
657 : to_union_type(expr.type());
658
659 for(const auto &component : union_type.components())
660 {
661 const auto m_size_bits = pointer_offset_bits(component.type(), ns);
662 if(!m_size_bits.has_value())
663 continue;
664
665 // if this member completely contains the target, recurse into it
666 if(
667 offset_bytes * config.ansi_c.char_width + *target_size_bits <=
669 {
670 const member_exprt member(expr, component.get_name(), component.type());
672 member, offset_bytes, target_type_raw, ns);
673 }
674 }
675 }
676
677 return make_byte_extract(
679}
680
681std::optional<exprt> get_subexpression_at_offset(
682 const exprt &expr,
683 const exprt &offset,
684 const typet &target_type,
685 const namespacet &ns)
686{
687 const auto offset_bytes = numeric_cast<mp_integer>(offset);
688
689 if(!offset_bytes.has_value())
690 return {};
691 else
692 return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
693}
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:562
Arrays with given size.
Definition std_types.h:807
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
struct configt::ansi_ct ansi_c
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:56
typet & type()
Return the type of the expression.
Definition expr.h:84
The trinary if-then-else operator.
Definition std_expr.h:2497
Array index operator.
Definition std_expr.h:1470
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:2971
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
Definition std_expr.h:1002
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
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
The 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)
std::optional< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
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:97
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
#define size_type
Definition unistd.c:186