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 "c_types.h"
16 #include "invariant.h"
17 #include "namespace.h"
18 #include "simplify_expr.h"
19 #include "ssa_expr.h"
20 #include "std_expr.h"
21 
23  const struct_typet &_type,
24  const namespacet &_ns):
25  current({0, 0}),
26  type(_type),
27  ns(_ns),
28  bit_field_bits(0)
29 {
30 }
31 
33 {
34  if(current.second!=-1) // Already failed?
35  {
36  const auto &comp=type.components()[current.first];
37  if(comp.type().id()==ID_c_bit_field)
38  {
39  // take the extra bytes needed
40  std::size_t w=to_c_bit_field_type(comp.type()).get_width();
41  bit_field_bits += w;
42  current.second += bit_field_bits / 8;
43  bit_field_bits %= 8;
44  }
45  else
46  {
48  bit_field_bits == 0, "padding ensures offset at byte boundaries");
49  const typet &subtype=comp.type();
50  mp_integer sub_size=pointer_offset_size(subtype, ns);
51  if(sub_size==-1)
52  current.second=-1; // give up
53  else current.second+=sub_size;
54  }
55  }
56  ++current.first;
57  return *this;
58 }
59 
61  const struct_typet &type,
62  const irep_idt &member,
63  const namespacet &ns)
64 {
65  const struct_typet::componentst &components=type.components();
66  member_offset_iterator offsets(type, ns);
67 
68  for(struct_typet::componentst::const_iterator
69  it=components.begin();
70  it!=components.end() && offsets->second!=-1;
71  ++it, ++offsets)
72  {
73  if(it->get_name()==member)
74  break;
75  }
76 
77  return offsets->second;
78 }
79 
81  const struct_typet &type,
82  const irep_idt &member,
83  const namespacet &ns)
84 {
85  mp_integer offset=0;
86  const struct_typet::componentst &components=type.components();
87 
88  for(const auto &comp : components)
89  {
90  if(comp.get_name()==member)
91  break;
92 
93  mp_integer member_bits=pointer_offset_bits(comp.type(), ns);
94  if(member_bits==-1)
95  return member_bits;
96 
97  offset+=member_bits;
98  }
99 
100  return offset;
101 }
102 
105  const typet &type,
106  const namespacet &ns)
107 {
108  mp_integer bits=pointer_offset_bits(type, ns);
109  if(bits==-1)
110  return -1;
111  return (bits+7)/8;
112 }
113 
115  const typet &type,
116  const namespacet &ns)
117 {
118  if(type.id()==ID_array)
119  {
120  mp_integer sub=pointer_offset_bits(type.subtype(), ns);
121  if(sub<0)
122  return -1;
123 
124  // get size
125  const exprt &size=to_array_type(type).size();
126 
127  // constant?
128  mp_integer i;
129 
130  if(to_integer(size, i))
131  return -1; // we cannot distinguish the elements
132 
133  return sub*i;
134  }
135  else if(type.id()==ID_vector)
136  {
137  mp_integer sub=pointer_offset_bits(type.subtype(), ns);
138  if(sub<0)
139  return -1;
140 
141  // get size
142  const exprt &size=to_vector_type(type).size();
143 
144  // constant?
145  mp_integer i;
146 
147  if(to_integer(size, i))
148  return -1; // we cannot distinguish the elements
149 
150  return sub*i;
151  }
152  else if(type.id()==ID_complex)
153  {
154  mp_integer sub=pointer_offset_bits(type.subtype(), ns);
155  if(sub<0)
156  return -1;
157 
158  return sub*2;
159  }
160  else if(type.id()==ID_struct)
161  {
162  const struct_typet &struct_type=to_struct_type(type);
163  const struct_typet::componentst &components=
164  struct_type.components();
165 
166  mp_integer result=0;
167 
168  for(struct_typet::componentst::const_iterator
169  it=components.begin();
170  it!=components.end();
171  it++)
172  {
173  const typet &subtype=it->type();
174  mp_integer sub_size=pointer_offset_bits(subtype, ns);
175  if(sub_size==-1)
176  return -1;
177  result+=sub_size;
178  }
179 
180  return result;
181  }
182  else if(type.id()==ID_union)
183  {
184  const union_typet &union_type=to_union_type(type);
185  const union_typet::componentst &components=
186  union_type.components();
187 
188  mp_integer result=0;
189 
190  // compute max
191 
192  for(union_typet::componentst::const_iterator
193  it=components.begin();
194  it!=components.end();
195  it++)
196  {
197  const typet &subtype=it->type();
198  mp_integer sub_size=pointer_offset_bits(subtype, ns);
199  if(sub_size==-1)
200  return -1;
201  if(sub_size>result)
202  result=sub_size;
203  }
204 
205  return result;
206  }
207  else if(type.id()==ID_signedbv ||
208  type.id()==ID_unsignedbv ||
209  type.id()==ID_fixedbv ||
210  type.id()==ID_floatbv ||
211  type.id()==ID_bv ||
212  type.id()==ID_c_bool ||
213  type.id()==ID_c_bit_field)
214  {
215  return to_bitvector_type(type).get_width();
216  }
217  else if(type.id()==ID_c_enum)
218  {
219  return to_bitvector_type(type.subtype()).get_width();
220  }
221  else if(type.id()==ID_c_enum_tag)
222  {
223  return pointer_offset_bits(ns.follow_tag(to_c_enum_tag_type(type)), ns);
224  }
225  else if(type.id()==ID_bool)
226  {
227  return 1;
228  }
229  else if(type.id()==ID_pointer)
230  {
231  // the following is an MS extension
232  if(type.get_bool(ID_C_ptr32))
233  return 32;
234 
235  return to_bitvector_type(type).get_width();
236  }
237  else if(type.id()==ID_symbol)
238  {
239  return pointer_offset_bits(ns.follow(type), ns);
240  }
241  else if(type.id()==ID_code)
242  {
243  return 0;
244  }
245  else if(type.id()==ID_string)
246  {
247  return 32;
248  }
249  else
250  return -1;
251 }
252 
254  const member_exprt &member_expr,
255  const namespacet &ns)
256 {
257  // need to distinguish structs and unions
258  const typet &type=ns.follow(member_expr.struct_op().type());
259  if(type.id()==ID_struct)
260  return member_offset_expr(
261  to_struct_type(type), member_expr.get_component_name(), ns);
262  else if(type.id()==ID_union)
263  return from_integer(0, size_type());
264  else
265  return nil_exprt();
266 }
267 
269  const struct_typet &type,
270  const irep_idt &member,
271  const namespacet &ns)
272 {
273  const struct_typet::componentst &components=type.components();
274 
275  exprt result=from_integer(0, size_type());
276  std::size_t bit_field_bits=0;
277 
278  for(struct_typet::componentst::const_iterator
279  it=components.begin();
280  it!=components.end();
281  it++)
282  {
283  if(it->get_name()==member)
284  break;
285 
286  if(it->type().id()==ID_c_bit_field)
287  {
288  std::size_t w=to_c_bit_field_type(it->type()).get_width();
289  bit_field_bits += w;
290  const std::size_t bytes = bit_field_bits / 8;
291  bit_field_bits %= 8;
292  result=plus_exprt(result, from_integer(bytes, result.type()));
293  }
294  else
295  {
297  bit_field_bits == 0, "padding ensures offset at byte boundaries");
298  const typet &subtype=it->type();
299  exprt sub_size=size_of_expr(subtype, ns);
300  if(sub_size.is_nil())
301  return nil_exprt(); // give up
302  result=plus_exprt(result, sub_size);
303  }
304  }
305 
306  simplify(result, ns);
307 
308  return result;
309 }
310 
312  const typet &type,
313  const namespacet &ns)
314 {
315  if(type.id()==ID_array)
316  {
317  exprt sub=size_of_expr(type.subtype(), ns);
318  if(sub.is_nil())
319  return nil_exprt();
320 
321  // get size
322  exprt size=to_array_type(type).size();
323 
324  if(size.is_nil())
325  return nil_exprt();
326 
327  if(size.type()!=sub.type())
328  size.make_typecast(sub.type());
329 
330  mult_exprt result(size, sub);
331  simplify(result, ns);
332 
333  return result;
334  }
335  else if(type.id()==ID_vector)
336  {
337  exprt sub=size_of_expr(type.subtype(), ns);
338  if(sub.is_nil())
339  return nil_exprt();
340 
341  // get size
342  exprt size=to_vector_type(type).size();
343 
344  if(size.is_nil())
345  return nil_exprt();
346 
347  if(size.type()!=sub.type())
348  size.make_typecast(sub.type());
349 
350  mult_exprt result(size, sub);
351  simplify(result, ns);
352 
353  return result;
354  }
355  else if(type.id()==ID_complex)
356  {
357  exprt sub=size_of_expr(type.subtype(), ns);
358  if(sub.is_nil())
359  return nil_exprt();
360 
361  const exprt size=from_integer(2, sub.type());
362 
363  mult_exprt result(size, sub);
364  simplify(result, ns);
365 
366  return result;
367  }
368  else if(type.id()==ID_struct)
369  {
370  const struct_typet &struct_type=to_struct_type(type);
371  const struct_typet::componentst &components=
372  struct_type.components();
373 
374  exprt result=from_integer(0, size_type());
375  std::size_t bit_field_bits=0;
376 
377  for(struct_typet::componentst::const_iterator
378  it=components.begin();
379  it!=components.end();
380  it++)
381  {
382  if(it->type().id()==ID_c_bit_field)
383  {
384  std::size_t w=to_c_bit_field_type(it->type()).get_width();
385  bit_field_bits += w;
386  const std::size_t bytes = bit_field_bits / 8;
387  bit_field_bits %= 8;
388  result=plus_exprt(result, from_integer(bytes, result.type()));
389  }
390  else
391  {
393  bit_field_bits == 0, "padding ensures offset at byte boundaries");
394  const typet &subtype=it->type();
395  exprt sub_size=size_of_expr(subtype, ns);
396  if(sub_size.is_nil())
397  return nil_exprt();
398 
399  result=plus_exprt(result, sub_size);
400  }
401  }
402 
403  simplify(result, ns);
404 
405  return result;
406  }
407  else if(type.id()==ID_union)
408  {
409  const union_typet &union_type=to_union_type(type);
410  const union_typet::componentst &components=
411  union_type.components();
412 
413  mp_integer max_bytes=0;
414  exprt result=from_integer(0, size_type());
415 
416  // compute max
417 
418  for(union_typet::componentst::const_iterator
419  it=components.begin();
420  it!=components.end();
421  it++)
422  {
423  const typet &subtype=it->type();
424  exprt sub_size;
425 
426  mp_integer sub_bits=pointer_offset_bits(subtype, ns);
427 
428  if(sub_bits==-1)
429  {
430  max_bytes=-1;
431 
432  sub_size=size_of_expr(subtype, ns);
433  if(sub_size.is_nil())
434  return nil_exprt();
435  }
436  else
437  {
438  mp_integer sub_bytes=(sub_bits+7)/8;
439 
440  if(max_bytes>=0)
441  {
442  if(max_bytes<sub_bytes)
443  {
444  max_bytes=sub_bytes;
445  result=from_integer(sub_bytes, size_type());
446  }
447 
448  continue;
449  }
450 
451  sub_size=from_integer(sub_bytes, size_type());
452  }
453 
454  result=if_exprt(
455  binary_relation_exprt(result, ID_lt, sub_size),
456  sub_size, result);
457 
458  simplify(result, ns);
459  }
460 
461  return result;
462  }
463  else if(type.id()==ID_signedbv ||
464  type.id()==ID_unsignedbv ||
465  type.id()==ID_fixedbv ||
466  type.id()==ID_floatbv ||
467  type.id()==ID_bv ||
468  type.id()==ID_c_bool ||
469  type.id()==ID_c_bit_field)
470  {
471  std::size_t width=to_bitvector_type(type).get_width();
472  std::size_t bytes=width/8;
473  if(bytes*8!=width)
474  bytes++;
475  return from_integer(bytes, size_type());
476  }
477  else if(type.id()==ID_c_enum)
478  {
479  std::size_t width=to_bitvector_type(type.subtype()).get_width();
480  std::size_t bytes=width/8;
481  if(bytes*8!=width)
482  bytes++;
483  return from_integer(bytes, size_type());
484  }
485  else if(type.id()==ID_c_enum_tag)
486  {
487  return size_of_expr(ns.follow_tag(to_c_enum_tag_type(type)), ns);
488  }
489  else if(type.id()==ID_bool)
490  {
491  return from_integer(1, size_type());
492  }
493  else if(type.id()==ID_pointer)
494  {
495  // the following is an MS extension
496  if(type.get_bool(ID_C_ptr32))
497  return from_integer(4, size_type());
498 
499  std::size_t width=to_bitvector_type(type).get_width();
500  std::size_t bytes=width/8;
501  if(bytes*8!=width)
502  bytes++;
503  return from_integer(bytes, size_type());
504  }
505  else if(type.id()==ID_symbol)
506  {
507  return size_of_expr(ns.follow(type), ns);
508  }
509  else if(type.id()==ID_code)
510  {
511  return from_integer(0, size_type());
512  }
513  else if(type.id()==ID_string)
514  {
515  return from_integer(32/8, size_type());
516  }
517  else
518  return nil_exprt();
519 }
520 
522  const exprt &expr,
523  const namespacet &ns)
524 {
525  if(expr.id()==ID_symbol)
526  {
527  if(is_ssa_expr(expr))
528  return compute_pointer_offset(
529  to_ssa_expr(expr).get_original_expr(), ns);
530  else
531  return 0;
532  }
533  else if(expr.id()==ID_index)
534  {
535  const index_exprt &index_expr=to_index_expr(expr);
536  const typet &array_type=ns.follow(index_expr.array().type());
538  array_type.id()==ID_array,
539  "index into array expected, found "+array_type.id_string());
540 
541  mp_integer o=compute_pointer_offset(index_expr.array(), ns);
542 
543  if(o!=-1)
544  {
545  mp_integer sub_size=
546  pointer_offset_size(array_type.subtype(), ns);
547 
548  mp_integer i;
549 
550  if(sub_size>0 && !to_integer(index_expr.index(), i))
551  return o+i*sub_size;
552  }
553 
554  // don't know
555  }
556  else if(expr.id()==ID_member)
557  {
558  const member_exprt &member_expr=to_member_expr(expr);
559  const exprt &op=member_expr.struct_op();
560  const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
561 
563 
564  if(o!=-1)
565  {
566  if(type.id()==ID_union)
567  return o;
568 
569  return o+member_offset(
570  to_struct_type(type), member_expr.get_component_name(), ns);
571  }
572  }
573  else if(expr.id()==ID_string_constant)
574  return 0;
575 
576  return -1; // don't know
577 }
578 
580  const constant_exprt &expr,
581  const namespacet &ns)
582 {
583  const typet &type=
584  static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
585 
586  mp_integer type_size=-1, val=-1;
587 
588  if(type.is_not_nil())
589  type_size=pointer_offset_size(type, ns);
590 
591  if(type_size<0 ||
592  to_integer(expr, val) ||
593  val<type_size ||
594  (type_size==0 && val>0))
595  return nil_exprt();
596 
597  const typet t(size_type());
599  address_bits(val+1)<=pointer_offset_bits(t, ns),
600  "sizeof value does not fit size_type");
601 
602  mp_integer remainder=0;
603  if(type_size!=0)
604  {
605  remainder=val%type_size;
606  val-=remainder;
607  val/=type_size;
608  }
609 
610  exprt result(ID_sizeof, t);
611  result.set(ID_type_arg, type);
612 
613  if(val>1)
614  result=mult_exprt(result, from_integer(val, t));
615  if(remainder>0)
616  result=plus_exprt(result, from_integer(remainder, t));
617 
618  if(result.type()!=expr.type())
619  result.make_typecast(expr.type());
620 
621  return result;
622 }
623 
625  exprt &result,
626  mp_integer offset,
627  const typet &target_type_raw,
628  const namespacet &ns)
629 {
630  const typet &source_type=ns.follow(result.type());
631  const typet &target_type=ns.follow(target_type_raw);
632 
633  if(offset==0 && source_type==target_type)
634  return true;
635 
636  if(source_type.id()==ID_struct)
637  {
638  const auto &st=to_struct_type(source_type);
639  const struct_typet::componentst &components=st.components();
640  member_offset_iterator offsets(st, ns);
641  while(offsets->first<components.size() &&
642  offsets->second!=-1 &&
643  offsets->second<=offset)
644  {
645  auto nextit=offsets;
646  ++nextit;
647  if((offsets->first+1)==components.size() || offset<nextit->second)
648  {
649  // This field might be, or might contain, the answer.
650  result=
651  member_exprt(
652  result,
653  components[offsets->first].get_name(),
654  components[offsets->first].type());
655  return
657  result, offset-offsets->second, target_type, ns);
658  }
659  ++offsets;
660  }
661  return false;
662  }
663  else if(source_type.id()==ID_array)
664  {
665  // A cell of the array might be, or contain, the subexpression
666  // we're looking for.
667  const auto &at=to_array_type(source_type);
668  mp_integer elem_size=pointer_offset_size(at.subtype(), ns);
669  if(elem_size==-1)
670  return false;
671  mp_integer cellidx=offset/elem_size;
672  if(cellidx < 0 || !cellidx.is_long())
673  return false;
674  offset=offset%elem_size;
675  result=index_exprt(result, from_integer(cellidx, unsignedbv_typet(64)));
676  return get_subexpression_at_offset(result, offset, target_type, ns);
677  }
678  else
679  return false;
680 }
681 
683  exprt &result,
684  const exprt &offset,
685  const typet &target_type,
686  const namespacet &ns)
687 {
688  mp_integer offset_const;
689  if(to_integer(offset, offset_const))
690  return false;
691  return get_subexpression_at_offset(result, offset_const, target_type, ns);
692 }
The type of an expression.
Definition: type.h:22
exprt size_of_expr(const typet &type, const namespacet &ns)
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
BigInt mp_integer
Definition: mp_arith.h:22
const struct_typet & type
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
bool is_not_nil() const
Definition: irep.h:103
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1150
member_offset_iterator(const struct_typet &_type, const namespacet &_ns)
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::vector< componentt > componentst
Definition: std_types.h:243
exprt build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
const componentst & components() const
Definition: std_types.h:245
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
The trinary if-then-else operator.
Definition: std_expr.h:3361
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
unsignedbv_typet size_type()
Definition: c_types.cpp:58
A constant literal expression.
Definition: std_expr.h:4424
Structure type.
Definition: std_types.h:297
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:74
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Extract member of struct or union.
Definition: std_expr.h:3871
const irep_idt & id() const
Definition: irep.h:189
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
The NIL expression.
Definition: std_expr.h:4510
bool get_subexpression_at_offset(exprt &result, mp_integer offset, const typet &target_type_raw, const namespacet &ns)
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const exprt & size() const
Definition: std_types.h:1639
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1660
const exprt & size() const
Definition: std_types.h:1014
The plus expression.
Definition: std_expr.h:893
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
std::size_t get_width() const
Definition: std_types.h:1129
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:747
binary multiplication
Definition: std_expr.h:1017
Pointer Logic.
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
exprt & index()
Definition: std_expr.h:1496
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3911
The union type.
Definition: std_types.h:458
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
irep_idt get_component_name() const
Definition: std_expr.h:3895
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:173
member_offset_iterator & operator++()
const std::string & id_string() const
Definition: irep.h:192
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1402
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
mp_integer member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool simplify(exprt &expr, const namespacet &ns)
array index operator
Definition: std_expr.h:1462