cprover
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 "invariant.h"
18#include "namespace.h"
19#include "pointer_expr.h"
20#include "simplify_expr.h"
21#include "ssa_expr.h"
22#include "std_expr.h"
23
25 const struct_typet &type,
26 const irep_idt &member,
27 const namespacet &ns)
28{
29 mp_integer result = 0;
30 std::size_t bit_field_bits = 0;
31
32 for(const auto &comp : type.components())
33 {
34 if(comp.get_name() == member)
35 return result;
36
37 if(comp.type().id() == ID_c_bit_field)
38 {
39 const std::size_t w = to_c_bit_field_type(comp.type()).get_width();
41 result += bit_field_bits / 8;
42 bit_field_bits %= 8;
43 }
44 else if(comp.type().id() == ID_bool)
45 {
47 result += bit_field_bits / 8;
48 bit_field_bits %= 8;
49 }
50 else
51 {
53 bit_field_bits == 0, "padding ensures offset at byte boundaries");
54 const auto sub_size = pointer_offset_size(comp.type(), ns);
55 if(!sub_size.has_value())
56 return {};
57 else
58 result += *sub_size;
59 }
60 }
61
62 return result;
63}
64
66 const struct_typet &type,
67 const irep_idt &member,
68 const namespacet &ns)
69{
70 mp_integer offset=0;
71 const struct_typet::componentst &components=type.components();
72
73 for(const auto &comp : components)
74 {
75 if(comp.get_name()==member)
76 return offset;
77
78 auto member_bits = pointer_offset_bits(comp.type(), ns);
79 if(!member_bits.has_value())
80 return {};
81
82 offset += *member_bits;
83 }
84
85 return {};
86}
87
90pointer_offset_size(const typet &type, const namespacet &ns)
91{
92 auto bits = pointer_offset_bits(type, ns);
93
94 if(bits.has_value())
95 return (*bits + 7) / 8;
96 else
97 return {};
98}
99
101pointer_offset_bits(const typet &type, const namespacet &ns)
102{
103 if(type.id()==ID_array)
104 {
105 auto sub = pointer_offset_bits(to_array_type(type).element_type(), ns);
106 if(!sub.has_value())
107 return {};
108
109 // get size - we can only distinguish the elements if the size is constant
110 const auto size = numeric_cast<mp_integer>(to_array_type(type).size());
111 if(!size.has_value())
112 return {};
113
114 return (*sub) * (*size);
115 }
116 else if(type.id()==ID_vector)
117 {
118 auto sub = pointer_offset_bits(to_vector_type(type).element_type(), ns);
119 if(!sub.has_value())
120 return {};
121
122 // get size
123 const mp_integer size =
125
126 return (*sub) * size;
127 }
128 else if(type.id()==ID_complex)
129 {
130 auto sub = pointer_offset_bits(to_complex_type(type).subtype(), ns);
131
132 if(sub.has_value())
133 return (*sub) * 2;
134 else
135 return {};
136 }
137 else if(type.id()==ID_struct)
138 {
140 mp_integer result=0;
141
142 for(const auto &c : struct_type.components())
143 {
144 const typet &subtype = c.type();
145 auto sub_size = pointer_offset_bits(subtype, ns);
146
147 if(!sub_size.has_value())
148 return {};
149
150 result += *sub_size;
151 }
152
153 return result;
154 }
155 else if(type.id()==ID_union)
156 {
158
159 if(union_type.components().empty())
160 return mp_integer{0};
161
162 const auto widest_member = union_type.find_widest_union_component(ns);
163
164 if(widest_member.has_value())
165 return widest_member->second;
166 else
167 return {};
168 }
169 else if(type.id()==ID_signedbv ||
170 type.id()==ID_unsignedbv ||
171 type.id()==ID_fixedbv ||
172 type.id()==ID_floatbv ||
173 type.id()==ID_bv ||
174 type.id()==ID_c_bool ||
175 type.id()==ID_c_bit_field)
176 {
177 return mp_integer(to_bitvector_type(type).get_width());
178 }
179 else if(type.id()==ID_c_enum)
180 {
181 return mp_integer(
182 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width());
183 }
184 else if(type.id()==ID_c_enum_tag)
185 {
187 }
188 else if(type.id()==ID_bool)
189 {
190 return mp_integer(1);
191 }
192 else if(type.id()==ID_pointer)
193 {
194 // the following is an MS extension
195 if(type.get_bool(ID_C_ptr32))
196 return mp_integer(32);
197
198 return mp_integer(to_bitvector_type(type).get_width());
199 }
200 else if(type.id() == ID_union_tag)
201 {
203 }
204 else if(type.id() == ID_struct_tag)
205 {
207 }
208 else if(type.id()==ID_code)
209 {
210 return mp_integer(0);
211 }
212 else if(type.id()==ID_string)
213 {
214 return mp_integer(32);
215 }
216 else
217 return {};
218}
219
222{
223 // need to distinguish structs and unions
224 const typet &type=ns.follow(member_expr.struct_op().type());
225 if(type.id()==ID_struct)
226 return member_offset_expr(
227 to_struct_type(type), member_expr.get_component_name(), ns);
228 else if(type.id()==ID_union)
229 return from_integer(0, size_type());
230 else
231 return {};
232}
233
235 const struct_typet &type,
236 const irep_idt &member,
237 const namespacet &ns)
238{
239 PRECONDITION(size_type().get_width() != 0);
240 exprt result=from_integer(0, size_type());
241 std::size_t bit_field_bits=0;
242
243 for(const auto &c : type.components())
244 {
245 if(c.get_name() == member)
246 break;
247
248 if(c.type().id() == ID_c_bit_field)
249 {
250 std::size_t w = to_c_bit_field_type(c.type()).get_width();
251 bit_field_bits += w;
252 const std::size_t bytes = bit_field_bits / 8;
253 bit_field_bits %= 8;
254 if(bytes > 0)
255 result = plus_exprt(result, from_integer(bytes, result.type()));
256 }
257 else if(c.type().id() == ID_bool)
258 {
260 const std::size_t bytes = bit_field_bits / 8;
261 bit_field_bits %= 8;
262 if(bytes > 0)
263 result = plus_exprt(result, from_integer(bytes, result.type()));
264 }
265 else
266 {
268 bit_field_bits == 0, "padding ensures offset at byte boundaries");
269 const typet &subtype = c.type();
270 auto sub_size = size_of_expr(subtype, ns);
271 if(!sub_size.has_value())
272 return {}; // give up
273 result = plus_exprt(result, sub_size.value());
274 }
275 }
276
277 return simplify_expr(std::move(result), ns);
278}
279
281{
282 if(type.id()==ID_array)
283 {
284 const auto &array_type = to_array_type(type);
285
286 // special-case arrays of bits
287 if(array_type.element_type().id() == ID_bool)
288 {
289 auto bits = pointer_offset_bits(array_type, ns);
290
291 if(bits.has_value())
292 return from_integer((*bits + 7) / 8, size_type());
293 }
294
295 auto sub = size_of_expr(array_type.element_type(), ns);
296 if(!sub.has_value())
297 return {};
298
299 const exprt &size = array_type.size();
300
301 if(size.is_nil())
302 return {};
303
304 const auto size_casted =
305 typecast_exprt::conditional_cast(size, sub.value().type());
306
307 return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
308 }
309 else if(type.id()==ID_vector)
310 {
311 const auto &vector_type = to_vector_type(type);
312
313 // special-case vectors of bits
314 if(vector_type.element_type().id() == ID_bool)
315 {
316 auto bits = pointer_offset_bits(vector_type, ns);
317
318 if(bits.has_value())
319 return from_integer((*bits + 7) / 8, 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 / 8;
359 bit_field_bits %= 8;
360 if(bytes > 0)
361 result = plus_exprt(result, from_integer(bytes, result.type()));
362 }
363 else if(c.type().id() == ID_bool)
364 {
366 const std::size_t bytes = bit_field_bits / 8;
367 bit_field_bits %= 8;
368 if(bytes > 0)
369 result = plus_exprt(result, from_integer(bytes, result.type()));
370 }
371 else
372 {
374 bit_field_bits == 0, "padding ensures offset at byte boundaries");
375 const typet &subtype = c.type();
376 auto sub_size_opt = size_of_expr(subtype, ns);
377 if(!sub_size_opt.has_value())
378 return {};
379
380 result = plus_exprt(result, sub_size_opt.value());
381 }
382 }
383
384 return simplify_expr(std::move(result), ns);
385 }
386 else if(type.id()==ID_union)
387 {
389
391 exprt result=from_integer(0, size_type());
392
393 // compute max
394
395 for(const auto &c : union_type.components())
396 {
397 const typet &subtype = c.type();
399
400 auto sub_bits = pointer_offset_bits(subtype, ns);
401
402 if(!sub_bits.has_value())
403 {
404 max_bytes=-1;
405
406 auto sub_size_opt = size_of_expr(subtype, ns);
407 if(!sub_size_opt.has_value())
408 return {};
409 sub_size = sub_size_opt.value();
410 }
411 else
412 {
413 mp_integer sub_bytes = (*sub_bits + 7) / 8;
414
415 if(max_bytes>=0)
416 {
418 {
421 }
422
423 continue;
424 }
425
427 }
428
429 result=if_exprt(
431 sub_size, result);
432
433 simplify(result, ns);
434 }
435
436 return result;
437 }
438 else if(type.id()==ID_signedbv ||
439 type.id()==ID_unsignedbv ||
440 type.id()==ID_fixedbv ||
441 type.id()==ID_floatbv ||
442 type.id()==ID_bv ||
443 type.id()==ID_c_bool ||
444 type.id()==ID_c_bit_field)
445 {
446 std::size_t width=to_bitvector_type(type).get_width();
447 std::size_t bytes=width/8;
448 if(bytes*8!=width)
449 bytes++;
450 return from_integer(bytes, size_type());
451 }
452 else if(type.id()==ID_c_enum)
453 {
454 std::size_t width =
455 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
456 std::size_t bytes=width/8;
457 if(bytes*8!=width)
458 bytes++;
459 return from_integer(bytes, size_type());
460 }
461 else if(type.id()==ID_c_enum_tag)
462 {
463 return size_of_expr(ns.follow_tag(to_c_enum_tag_type(type)), ns);
464 }
465 else if(type.id()==ID_bool)
466 {
467 return from_integer(1, size_type());
468 }
469 else if(type.id()==ID_pointer)
470 {
471 // the following is an MS extension
472 if(type.get_bool(ID_C_ptr32))
473 return from_integer(4, size_type());
474
475 std::size_t width=to_bitvector_type(type).get_width();
476 std::size_t bytes=width/8;
477 if(bytes*8!=width)
478 bytes++;
479 return from_integer(bytes, size_type());
480 }
481 else if(type.id() == ID_union_tag)
482 {
483 return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns);
484 }
485 else if(type.id() == ID_struct_tag)
486 {
487 return size_of_expr(ns.follow_tag(to_struct_tag_type(type)), ns);
488 }
489 else if(type.id()==ID_code)
490 {
491 return from_integer(0, size_type());
492 }
493 else if(type.id()==ID_string)
494 {
495 return from_integer(32/8, size_type());
496 }
497 else
498 return {};
499}
500
503{
504 if(expr.id()==ID_symbol)
505 {
506 if(is_ssa_expr(expr))
508 to_ssa_expr(expr).get_original_expr(), ns);
509 else
510 return mp_integer(0);
511 }
512 else if(expr.id()==ID_index)
513 {
516 index_expr.array().type().id() == ID_array,
517 "index into array expected, found " +
518 index_expr.array().type().id_string());
519
520 auto o = compute_pointer_offset(index_expr.array(), ns);
521
522 if(o.has_value())
523 {
524 const auto &array_type = to_array_type(index_expr.array().type());
525 auto sub_size = pointer_offset_size(array_type.element_type(), ns);
526
527 if(sub_size.has_value() && *sub_size > 0)
528 {
529 const auto i = numeric_cast<mp_integer>(index_expr.index());
530 if(i.has_value())
531 return (*o) + (*i) * (*sub_size);
532 }
533 }
534
535 // don't know
536 }
537 else if(expr.id()==ID_member)
538 {
540 const exprt &op=member_expr.struct_op();
542
543 auto o = compute_pointer_offset(op, ns);
544
545 if(o.has_value())
546 {
547 if(type.id()==ID_union)
548 return *o;
549
551 to_struct_type(type), member_expr.get_component_name(), ns);
552
553 if(member_offset.has_value())
554 return *o + *member_offset;
555 }
556 }
557 else if(expr.id()==ID_string_constant)
558 return mp_integer(0);
559
560 return {}; // don't know
561}
562
565{
566 const typet &type=
567 static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
568
569 if(type.is_nil())
570 return {};
571
572 const auto type_size = pointer_offset_size(type, ns);
573 auto val = numeric_cast<mp_integer>(expr);
574
575 if(
576 !type_size.has_value() || *type_size < 0 || !val.has_value() ||
577 *val < *type_size || (*type_size == 0 && *val > 0))
578 {
579 return {};
580 }
581
582 const typet t(size_type());
584 address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
585 "sizeof value does not fit size_type");
586
587 mp_integer remainder=0;
588
589 if(*type_size != 0)
590 {
591 remainder = *val % *type_size;
592 *val -= remainder;
593 *val /= *type_size;
594 }
595
596 exprt result(ID_sizeof, t);
597 result.set(ID_type_arg, type);
598
599 if(*val > 1)
600 result = mult_exprt(result, from_integer(*val, t));
601 if(remainder>0)
602 result=plus_exprt(result, from_integer(remainder, t));
603
604 return typecast_exprt::conditional_cast(result, expr.type());
605}
606
608 const exprt &expr,
610 const typet &target_type_raw,
611 const namespacet &ns)
612{
613 if(offset_bytes == 0 && expr.type() == target_type_raw)
614 {
615 exprt result = expr;
616
617 if(expr.type() != target_type_raw)
618 result.type() = target_type_raw;
619
620 return result;
621 }
622
623 if(
624 offset_bytes == 0 && expr.type().id() == ID_pointer &&
626 {
627 return typecast_exprt(expr, target_type_raw);
628 }
629
630 const typet &source_type = ns.follow(expr.type());
632 if(!target_size_bits.has_value())
633 return {};
634
635 if(source_type.id()==ID_struct)
636 {
638
640 for(const auto &component : struct_type.components())
641 {
642 const auto m_size_bits = pointer_offset_bits(component.type(), ns);
643 if(!m_size_bits.has_value())
644 return {};
645
646 // if this member completely contains the target, and this member is
647 // byte-aligned, recurse into it
648 if(
649 offset_bytes * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
651 {
652 const member_exprt member(expr, component.get_name(), component.type());
654 member, offset_bytes - m_offset_bits / 8, target_type_raw, ns);
655 }
656
658 }
659 }
660 else if(source_type.id()==ID_array)
661 {
663
664 const auto elem_size_bits =
665 pointer_offset_bits(array_type.element_type(), ns);
666
667 // no arrays of non-byte-aligned, zero-, or unknown-sized objects
668 if(
669 elem_size_bits.has_value() && *elem_size_bits > 0 &&
671 {
674 const auto target_size_bytes = *target_size_bits / 8;
675 // only recurse if the cell completely contains the target
677 {
680 expr,
682 offset_bytes / elem_size_bytes, array_type.index_type())),
685 ns);
686 }
687 }
688 }
689 else if(
690 object_descriptor_exprt(expr).root_object().id() == ID_union &&
691 source_type.id() == ID_union)
692 {
694
695 for(const auto &component : union_type.components())
696 {
697 const auto m_size_bits = pointer_offset_bits(component.type(), ns);
698 if(!m_size_bits.has_value())
699 continue;
700
701 // if this member completely contains the target, recurse into it
703 {
704 const member_exprt member(expr, component.get_name(), component.type());
706 member, offset_bytes, target_type_raw, ns);
707 }
708 }
709 }
710
711 return make_byte_extract(
713}
714
716 const exprt &expr,
717 const exprt &offset,
718 const typet &target_type,
719 const namespacet &ns)
720{
721 const auto offset_bytes = numeric_cast<mp_integer>(offset);
722
723 if(!offset_bytes.has_value())
724 return {};
725 else
726 return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
727}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
unsignedbv_typet size_type()
Definition c_types.cpp:68
bitvector_typet c_index_type()
Definition c_types.cpp:16
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition c_types.h:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:302
const 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:344
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:202
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Arrays with given size.
Definition std_types.h:763
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
std::size_t get_width() const
Definition std_types.h:864
A constant literal expression.
Definition std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
The trinary if-then-else operator.
Definition std_expr.h:2226
Array index operator.
Definition std_expr.h:1328
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
Extract member of struct or union.
Definition std_expr.h:2667
Binary multiplication Associativity is not specified.
Definition std_expr.h:1019
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
Split an expression into a base object and a (byte) offset.
The plus expression Associativity is not specified.
Definition std_expr.h:914
Structure type, corresponds to C style structs.
Definition std_types.h:231
Base type for structs and unions.
Definition std_types.h:62
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:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
The type of an expression, extends irept.
Definition type.h:29
The union type.
Definition c_types.h:125
const constant_exprt & size() const
API to expression classes for Pointers.
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
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:48
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1040
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1082
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
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.