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).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 =
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(
182  to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width());
183  }
184  else if(type.id()==ID_c_enum_tag)
185  {
186  return pointer_offset_bits(ns.follow_tag(to_c_enum_tag_type(type)), ns);
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  {
202  return pointer_offset_bits(ns.follow_tag(to_union_tag_type(type)), ns);
203  }
204  else if(type.id() == ID_struct_tag)
205  {
206  return pointer_offset_bits(ns.follow_tag(to_struct_tag_type(type)), ns);
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 
221 member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
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  {
259  ++bit_field_bits;
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  {
347  const struct_typet &struct_type=to_struct_type(type);
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  {
365  ++bit_field_bits;
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  {
388  const union_typet &union_type=to_union_type(type);
389 
390  mp_integer max_bytes=0;
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();
398  exprt sub_size;
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  {
417  if(max_bytes<sub_bytes)
418  {
419  max_bytes=sub_bytes;
420  result=from_integer(sub_bytes, size_type());
421  }
422 
423  continue;
424  }
425 
426  sub_size=from_integer(sub_bytes, size_type());
427  }
428 
429  result=if_exprt(
430  binary_relation_exprt(result, ID_lt, sub_size),
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 
502 compute_pointer_offset(const exprt &expr, const namespacet &ns)
503 {
504  if(expr.id()==ID_symbol)
505  {
506  if(is_ssa_expr(expr))
507  return compute_pointer_offset(
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  {
514  const index_exprt &index_expr=to_index_expr(expr);
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  {
539  const member_exprt &member_expr=to_member_expr(expr);
540  const exprt &op=member_expr.struct_op();
541  const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
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,
609  const mp_integer &offset_bytes,
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 &&
625  target_type_raw.id() == ID_pointer)
626  {
627  return typecast_exprt(expr, target_type_raw);
628  }
629 
630  const typet &source_type = ns.follow(expr.type());
631  const auto target_size_bits = pointer_offset_bits(target_type_raw, ns);
632  if(!target_size_bits.has_value())
633  return {};
634 
635  if(source_type.id()==ID_struct)
636  {
637  const struct_typet &struct_type = to_struct_type(source_type);
638 
639  mp_integer m_offset_bits = 0;
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 &&
650  offset_bytes * 8 + *target_size_bits <= m_offset_bits + *m_size_bits)
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 
657  m_offset_bits += *m_size_bits;
658  }
659  }
660  else if(source_type.id()==ID_array)
661  {
662  const array_typet &array_type = to_array_type(source_type);
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 &&
670  *elem_size_bits % 8 == 0 && *target_size_bits <= *elem_size_bits)
671  {
672  const mp_integer elem_size_bytes = *elem_size_bits / 8;
673  const auto offset_inside_elem = offset_bytes % elem_size_bytes;
674  const auto target_size_bytes = *target_size_bits / 8;
675  // only recurse if the cell completely contains the target
676  if(offset_inside_elem + target_size_bytes <= elem_size_bytes)
677  {
679  index_exprt(
680  expr,
681  from_integer(
682  offset_bytes / elem_size_bytes, array_type.index_type())),
683  offset_inside_elem,
684  target_type_raw,
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  {
693  const union_typet &union_type = to_union_type(source_type);
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
702  if(offset_bytes * 8 + *target_size_bits <= *m_size_bits)
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(
712  expr, from_integer(offset_bytes, c_index_type()), target_type_raw);
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)
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.
unsignedbv_typet size_type()
Definition: c_types.cpp:68
bitvector_typet c_index_type()
Definition: c_types.cpp:16
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 union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
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 union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
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
Arrays with given size.
Definition: std_types.h:763
typet index_type() const
The type of the index expressions into any instance of this type.
Definition: std_types.cpp:33
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
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
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const std::string & id_string() const
Definition: irep.h:399
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
const exprt & struct_op() const
Definition: std_expr.h:2697
irep_idt get_component_name() const
Definition: std_expr.h:2681
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:167
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
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:318
const constant_exprt & size() const
Definition: std_types.cpp:253
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:2751
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
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.