cprover
pointer_offset_size.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Pointer Logic
4 
5 Author: 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();
40  bit_field_bits += w;
41  result += bit_field_bits / 8;
42  bit_field_bits %= 8;
43  }
44  else if(comp.type().id() == ID_bool)
45  {
46  ++bit_field_bits;
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 
90 pointer_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 
101 pointer_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).subtype(), 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).subtype(), ns);
119  if(!sub.has_value())
120  return {};
121 
122  // get size
123  const mp_integer size =
124  numeric_cast_v<mp_integer>(to_vector_type(type).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  {
139  const struct_typet &struct_type=to_struct_type(type);
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  {
157  const union_typet &union_type=to_union_type(type);
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(to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
182  }
183  else if(type.id()==ID_c_enum_tag)
184  {
185  return pointer_offset_bits(ns.follow_tag(to_c_enum_tag_type(type)), ns);
186  }
187  else if(type.id()==ID_bool)
188  {
189  return mp_integer(1);
190  }
191  else if(type.id()==ID_pointer)
192  {
193  // the following is an MS extension
194  if(type.get_bool(ID_C_ptr32))
195  return mp_integer(32);
196 
197  return mp_integer(to_bitvector_type(type).get_width());
198  }
199  else if(type.id() == ID_union_tag)
200  {
201  return pointer_offset_bits(ns.follow_tag(to_union_tag_type(type)), ns);
202  }
203  else if(type.id() == ID_struct_tag)
204  {
205  return pointer_offset_bits(ns.follow_tag(to_struct_tag_type(type)), ns);
206  }
207  else if(type.id()==ID_code)
208  {
209  return mp_integer(0);
210  }
211  else if(type.id()==ID_string)
212  {
213  return mp_integer(32);
214  }
215  else
216  return {};
217 }
218 
220 member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
221 {
222  // need to distinguish structs and unions
223  const typet &type=ns.follow(member_expr.struct_op().type());
224  if(type.id()==ID_struct)
225  return member_offset_expr(
226  to_struct_type(type), member_expr.get_component_name(), ns);
227  else if(type.id()==ID_union)
228  return from_integer(0, size_type());
229  else
230  return {};
231 }
232 
234  const struct_typet &type,
235  const irep_idt &member,
236  const namespacet &ns)
237 {
238  PRECONDITION(size_type().get_width() != 0);
239  exprt result=from_integer(0, size_type());
240  std::size_t bit_field_bits=0;
241 
242  for(const auto &c : type.components())
243  {
244  if(c.get_name() == member)
245  break;
246 
247  if(c.type().id() == ID_c_bit_field)
248  {
249  std::size_t w = to_c_bit_field_type(c.type()).get_width();
250  bit_field_bits += w;
251  const std::size_t bytes = bit_field_bits / 8;
252  bit_field_bits %= 8;
253  if(bytes > 0)
254  result = plus_exprt(result, from_integer(bytes, result.type()));
255  }
256  else if(c.type().id() == ID_bool)
257  {
258  ++bit_field_bits;
259  const std::size_t bytes = bit_field_bits / 8;
260  bit_field_bits %= 8;
261  if(bytes > 0)
262  result = plus_exprt(result, from_integer(bytes, result.type()));
263  }
264  else
265  {
267  bit_field_bits == 0, "padding ensures offset at byte boundaries");
268  const typet &subtype = c.type();
269  auto sub_size = size_of_expr(subtype, ns);
270  if(!sub_size.has_value())
271  return {}; // give up
272  result = plus_exprt(result, sub_size.value());
273  }
274  }
275 
276  return simplify_expr(std::move(result), ns);
277 }
278 
280 {
281  if(type.id()==ID_array)
282  {
283  const auto &array_type = to_array_type(type);
284 
285  // special-case arrays of bits
286  if(array_type.subtype().id() == ID_bool)
287  {
288  auto bits = pointer_offset_bits(array_type, ns);
289 
290  if(bits.has_value())
291  return from_integer((*bits + 7) / 8, size_type());
292  }
293 
294  auto sub = size_of_expr(array_type.subtype(), ns);
295  if(!sub.has_value())
296  return {};
297 
298  const exprt &size = array_type.size();
299 
300  if(size.is_nil())
301  return {};
302 
303  const auto size_casted =
304  typecast_exprt::conditional_cast(size, sub.value().type());
305 
306  return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
307  }
308  else if(type.id()==ID_vector)
309  {
310  const auto &vector_type = to_vector_type(type);
311 
312  // special-case vectors of bits
313  if(vector_type.subtype().id() == ID_bool)
314  {
315  auto bits = pointer_offset_bits(vector_type, ns);
316 
317  if(bits.has_value())
318  return from_integer((*bits + 7) / 8, size_type());
319  }
320 
321  auto sub = size_of_expr(vector_type.subtype(), ns);
322  if(!sub.has_value())
323  return {};
324 
325  const exprt &size = to_vector_type(type).size();
326 
327  if(size.is_nil())
328  return {};
329 
330  const auto size_casted =
331  typecast_exprt::conditional_cast(size, sub.value().type());
332 
333  return simplify_expr(mult_exprt{size_casted, sub.value()}, ns);
334  }
335  else if(type.id()==ID_complex)
336  {
337  auto sub = size_of_expr(to_complex_type(type).subtype(), ns);
338  if(!sub.has_value())
339  return {};
340 
341  exprt size = from_integer(2, sub.value().type());
342  return simplify_expr(mult_exprt{std::move(size), sub.value()}, ns);
343  }
344  else if(type.id()==ID_struct)
345  {
346  const struct_typet &struct_type=to_struct_type(type);
347 
348  exprt result=from_integer(0, size_type());
349  std::size_t bit_field_bits=0;
350 
351  for(const auto &c : struct_type.components())
352  {
353  if(c.type().id() == ID_c_bit_field)
354  {
355  std::size_t w = to_c_bit_field_type(c.type()).get_width();
356  bit_field_bits += w;
357  const std::size_t bytes = bit_field_bits / 8;
358  bit_field_bits %= 8;
359  if(bytes > 0)
360  result = plus_exprt(result, from_integer(bytes, result.type()));
361  }
362  else if(c.type().id() == ID_bool)
363  {
364  ++bit_field_bits;
365  const std::size_t bytes = bit_field_bits / 8;
366  bit_field_bits %= 8;
367  if(bytes > 0)
368  result = plus_exprt(result, from_integer(bytes, result.type()));
369  }
370  else
371  {
373  bit_field_bits == 0, "padding ensures offset at byte boundaries");
374  const typet &subtype = c.type();
375  auto sub_size_opt = size_of_expr(subtype, ns);
376  if(!sub_size_opt.has_value())
377  return {};
378 
379  result = plus_exprt(result, sub_size_opt.value());
380  }
381  }
382 
383  return simplify_expr(std::move(result), ns);
384  }
385  else if(type.id()==ID_union)
386  {
387  const union_typet &union_type=to_union_type(type);
388 
389  mp_integer max_bytes=0;
390  exprt result=from_integer(0, size_type());
391 
392  // compute max
393 
394  for(const auto &c : union_type.components())
395  {
396  const typet &subtype = c.type();
397  exprt sub_size;
398 
399  auto sub_bits = pointer_offset_bits(subtype, ns);
400 
401  if(!sub_bits.has_value())
402  {
403  max_bytes=-1;
404 
405  auto sub_size_opt = size_of_expr(subtype, ns);
406  if(!sub_size_opt.has_value())
407  return {};
408  sub_size = sub_size_opt.value();
409  }
410  else
411  {
412  mp_integer sub_bytes = (*sub_bits + 7) / 8;
413 
414  if(max_bytes>=0)
415  {
416  if(max_bytes<sub_bytes)
417  {
418  max_bytes=sub_bytes;
419  result=from_integer(sub_bytes, size_type());
420  }
421 
422  continue;
423  }
424 
425  sub_size=from_integer(sub_bytes, size_type());
426  }
427 
428  result=if_exprt(
429  binary_relation_exprt(result, ID_lt, sub_size),
430  sub_size, result);
431 
432  simplify(result, ns);
433  }
434 
435  return result;
436  }
437  else if(type.id()==ID_signedbv ||
438  type.id()==ID_unsignedbv ||
439  type.id()==ID_fixedbv ||
440  type.id()==ID_floatbv ||
441  type.id()==ID_bv ||
442  type.id()==ID_c_bool ||
443  type.id()==ID_c_bit_field)
444  {
445  std::size_t width=to_bitvector_type(type).get_width();
446  std::size_t bytes=width/8;
447  if(bytes*8!=width)
448  bytes++;
449  return from_integer(bytes, size_type());
450  }
451  else if(type.id()==ID_c_enum)
452  {
453  std::size_t width =
454  to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
455  std::size_t bytes=width/8;
456  if(bytes*8!=width)
457  bytes++;
458  return from_integer(bytes, size_type());
459  }
460  else if(type.id()==ID_c_enum_tag)
461  {
462  return size_of_expr(ns.follow_tag(to_c_enum_tag_type(type)), ns);
463  }
464  else if(type.id()==ID_bool)
465  {
466  return from_integer(1, size_type());
467  }
468  else if(type.id()==ID_pointer)
469  {
470  // the following is an MS extension
471  if(type.get_bool(ID_C_ptr32))
472  return from_integer(4, size_type());
473 
474  std::size_t width=to_bitvector_type(type).get_width();
475  std::size_t bytes=width/8;
476  if(bytes*8!=width)
477  bytes++;
478  return from_integer(bytes, size_type());
479  }
480  else if(type.id() == ID_union_tag)
481  {
482  return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns);
483  }
484  else if(type.id() == ID_struct_tag)
485  {
486  return size_of_expr(ns.follow_tag(to_struct_tag_type(type)), ns);
487  }
488  else if(type.id()==ID_code)
489  {
490  return from_integer(0, size_type());
491  }
492  else if(type.id()==ID_string)
493  {
494  return from_integer(32/8, size_type());
495  }
496  else
497  return {};
498 }
499 
501 compute_pointer_offset(const exprt &expr, const namespacet &ns)
502 {
503  if(expr.id()==ID_symbol)
504  {
505  if(is_ssa_expr(expr))
506  return compute_pointer_offset(
507  to_ssa_expr(expr).get_original_expr(), ns);
508  else
509  return mp_integer(0);
510  }
511  else if(expr.id()==ID_index)
512  {
513  const index_exprt &index_expr=to_index_expr(expr);
515  index_expr.array().type().id() == ID_array,
516  "index into array expected, found " +
517  index_expr.array().type().id_string());
518 
519  auto o = compute_pointer_offset(index_expr.array(), ns);
520 
521  if(o.has_value())
522  {
523  const auto &array_type = to_array_type(index_expr.array().type());
524  auto sub_size = pointer_offset_size(array_type.subtype(), ns);
525 
526  if(sub_size.has_value() && *sub_size > 0)
527  {
528  const auto i = numeric_cast<mp_integer>(index_expr.index());
529  if(i.has_value())
530  return (*o) + (*i) * (*sub_size);
531  }
532  }
533 
534  // don't know
535  }
536  else if(expr.id()==ID_member)
537  {
538  const member_exprt &member_expr=to_member_expr(expr);
539  const exprt &op=member_expr.struct_op();
540  const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
541 
542  auto o = compute_pointer_offset(op, ns);
543 
544  if(o.has_value())
545  {
546  if(type.id()==ID_union)
547  return *o;
548 
550  to_struct_type(type), member_expr.get_component_name(), ns);
551 
552  if(member_offset.has_value())
553  return *o + *member_offset;
554  }
555  }
556  else if(expr.id()==ID_string_constant)
557  return mp_integer(0);
558 
559  return {}; // don't know
560 }
561 
564 {
565  const typet &type=
566  static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
567 
568  if(type.is_nil())
569  return {};
570 
571  const auto type_size = pointer_offset_size(type, ns);
572  auto val = numeric_cast<mp_integer>(expr);
573 
574  if(
575  !type_size.has_value() || *type_size < 0 || !val.has_value() ||
576  *val < *type_size || (*type_size == 0 && *val > 0))
577  {
578  return {};
579  }
580 
581  const typet t(size_type());
583  address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
584  "sizeof value does not fit size_type");
585 
586  mp_integer remainder=0;
587 
588  if(*type_size != 0)
589  {
590  remainder = *val % *type_size;
591  *val -= remainder;
592  *val /= *type_size;
593  }
594 
595  exprt result(ID_sizeof, t);
596  result.set(ID_type_arg, type);
597 
598  if(*val > 1)
599  result = mult_exprt(result, from_integer(*val, t));
600  if(remainder>0)
601  result=plus_exprt(result, from_integer(remainder, t));
602 
603  return typecast_exprt::conditional_cast(result, expr.type());
604 }
605 
607  const exprt &expr,
608  const mp_integer &offset_bytes,
609  const typet &target_type_raw,
610  const namespacet &ns)
611 {
612  if(offset_bytes == 0 && expr.type() == target_type_raw)
613  {
614  exprt result = expr;
615 
616  if(expr.type() != target_type_raw)
617  result.type() = target_type_raw;
618 
619  return result;
620  }
621 
622  if(
623  offset_bytes == 0 && expr.type().id() == ID_pointer &&
624  target_type_raw.id() == ID_pointer)
625  {
626  return typecast_exprt(expr, target_type_raw);
627  }
628 
629  const typet &source_type = ns.follow(expr.type());
630  const auto target_size_bits = pointer_offset_bits(target_type_raw, ns);
631  if(!target_size_bits.has_value())
632  return {};
633 
634  if(source_type.id()==ID_struct)
635  {
636  const struct_typet &struct_type = to_struct_type(source_type);
637 
638  mp_integer m_offset_bits = 0;
639  for(const auto &component : struct_type.components())
640  {
641  const auto m_size_bits = pointer_offset_bits(component.type(), ns);
642  if(!m_size_bits.has_value())
643  return {};
644 
645  // if this member completely contains the target, and this member is
646  // byte-aligned, recurse into it
647  if(
648  offset_bytes * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
649  offset_bytes * 8 + *target_size_bits <= m_offset_bits + *m_size_bits)
650  {
651  const member_exprt member(expr, component.get_name(), component.type());
653  member, offset_bytes - m_offset_bits / 8, target_type_raw, ns);
654  }
655 
656  m_offset_bits += *m_size_bits;
657  }
658  }
659  else if(source_type.id()==ID_array)
660  {
661  const array_typet &array_type = to_array_type(source_type);
662 
663  const auto elem_size_bits = pointer_offset_bits(array_type.subtype(), ns);
664 
665  // no arrays of non-byte-aligned, zero-, or unknown-sized objects
666  if(
667  elem_size_bits.has_value() && *elem_size_bits > 0 &&
668  *elem_size_bits % 8 == 0 && *target_size_bits <= *elem_size_bits)
669  {
670  const mp_integer elem_size_bytes = *elem_size_bits / 8;
671  const auto offset_inside_elem = offset_bytes % elem_size_bytes;
672  const auto target_size_bytes = *target_size_bits / 8;
673  // only recurse if the cell completely contains the target
674  if(offset_inside_elem + target_size_bytes <= elem_size_bytes)
675  {
677  index_exprt(
678  expr, from_integer(offset_bytes / elem_size_bytes, index_type())),
679  offset_inside_elem,
680  target_type_raw,
681  ns);
682  }
683  }
684  }
685  else if(
686  object_descriptor_exprt(expr).root_object().id() == ID_union &&
687  source_type.id() == ID_union)
688  {
689  const union_typet &union_type = to_union_type(source_type);
690 
691  for(const auto &component : union_type.components())
692  {
693  const auto m_size_bits = pointer_offset_bits(component.type(), ns);
694  if(!m_size_bits.has_value())
695  continue;
696 
697  // if this member completely contains the target, recurse into it
698  if(offset_bytes * 8 + *target_size_bits <= *m_size_bits)
699  {
700  const member_exprt member(expr, component.get_name(), component.type());
702  member, offset_bytes, target_type_raw, ns);
703  }
704  }
705  }
706 
707  return make_byte_extract(
708  expr, from_integer(offset_bytes, index_type()), target_type_raw);
709 }
710 
712  const exprt &expr,
713  const exprt &offset,
714  const typet &target_type,
715  const namespacet &ns)
716 {
717  const auto offset_bytes = numeric_cast<mp_integer>(offset);
718 
719  if(!offset_bytes.has_value())
720  return {};
721  else
722  return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
723 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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.
bitvector_typet index_type()
Definition: c_types.cpp:16
unsignedbv_typet size_type()
Definition: c_types.cpp:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
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:47
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
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:317
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:843
A constant literal expression.
Definition: std_expr.h:2753
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:2172
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
const std::string & id_string() const
Definition: irep.h:410
const irep_idt & id() const
Definition: irep.h:407
bool is_nil() const
Definition: irep.h:387
Extract member of struct or union.
Definition: std_expr.h:2613
const exprt & struct_op() const
Definition: std_expr.h:2643
irep_idt get_component_name() const
Definition: std_expr.h:2627
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.
Definition: pointer_expr.h:147
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:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
The union type.
Definition: c_types.h:112
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:308
const constant_exprt & size() const
Definition: std_types.cpp:239
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
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< 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(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
optionalt< 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: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
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
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 member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1040
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
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.