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_union_tag)
242  {
243  return pointer_offset_bits(ns.follow_tag(to_union_tag_type(type)), ns);
244  }
245  else if(type.id() == ID_struct_tag)
246  {
247  return pointer_offset_bits(ns.follow_tag(to_struct_tag_type(type)), ns);
248  }
249  else if(type.id()==ID_code)
250  {
251  return 0;
252  }
253  else if(type.id()==ID_string)
254  {
255  return 32;
256  }
257  else
258  return -1;
259 }
260 
262  const member_exprt &member_expr,
263  const namespacet &ns)
264 {
265  // need to distinguish structs and unions
266  const typet &type=ns.follow(member_expr.struct_op().type());
267  if(type.id()==ID_struct)
268  return member_offset_expr(
269  to_struct_type(type), member_expr.get_component_name(), ns);
270  else if(type.id()==ID_union)
271  return from_integer(0, size_type());
272  else
273  return nil_exprt();
274 }
275 
277  const struct_typet &type,
278  const irep_idt &member,
279  const namespacet &ns)
280 {
281  const struct_typet::componentst &components=type.components();
282 
283  exprt result=from_integer(0, size_type());
284  std::size_t bit_field_bits=0;
285 
286  for(struct_typet::componentst::const_iterator
287  it=components.begin();
288  it!=components.end();
289  it++)
290  {
291  if(it->get_name()==member)
292  break;
293 
294  if(it->type().id()==ID_c_bit_field)
295  {
296  std::size_t w=to_c_bit_field_type(it->type()).get_width();
297  bit_field_bits += w;
298  const std::size_t bytes = bit_field_bits / 8;
299  bit_field_bits %= 8;
300  result=plus_exprt(result, from_integer(bytes, result.type()));
301  }
302  else
303  {
305  bit_field_bits == 0, "padding ensures offset at byte boundaries");
306  const typet &subtype=it->type();
307  exprt sub_size=size_of_expr(subtype, ns);
308  if(sub_size.is_nil())
309  return nil_exprt(); // give up
310  result=plus_exprt(result, sub_size);
311  }
312  }
313 
314  simplify(result, ns);
315 
316  return result;
317 }
318 
320  const typet &type,
321  const namespacet &ns)
322 {
323  if(type.id()==ID_array)
324  {
325  exprt sub=size_of_expr(type.subtype(), ns);
326  if(sub.is_nil())
327  return nil_exprt();
328 
329  // get size
330  exprt size=to_array_type(type).size();
331 
332  if(size.is_nil())
333  return nil_exprt();
334 
335  if(size.type()!=sub.type())
336  size.make_typecast(sub.type());
337 
338  mult_exprt result(size, sub);
339  simplify(result, ns);
340 
341  return result;
342  }
343  else if(type.id()==ID_vector)
344  {
345  exprt sub=size_of_expr(type.subtype(), ns);
346  if(sub.is_nil())
347  return nil_exprt();
348 
349  // get size
350  exprt size=to_vector_type(type).size();
351 
352  if(size.is_nil())
353  return nil_exprt();
354 
355  if(size.type()!=sub.type())
356  size.make_typecast(sub.type());
357 
358  mult_exprt result(size, sub);
359  simplify(result, ns);
360 
361  return result;
362  }
363  else if(type.id()==ID_complex)
364  {
365  exprt sub=size_of_expr(type.subtype(), ns);
366  if(sub.is_nil())
367  return nil_exprt();
368 
369  const exprt size=from_integer(2, sub.type());
370 
371  mult_exprt result(size, sub);
372  simplify(result, ns);
373 
374  return result;
375  }
376  else if(type.id()==ID_struct)
377  {
378  const struct_typet &struct_type=to_struct_type(type);
379  const struct_typet::componentst &components=
380  struct_type.components();
381 
382  exprt result=from_integer(0, size_type());
383  std::size_t bit_field_bits=0;
384 
385  for(struct_typet::componentst::const_iterator
386  it=components.begin();
387  it!=components.end();
388  it++)
389  {
390  if(it->type().id()==ID_c_bit_field)
391  {
392  std::size_t w=to_c_bit_field_type(it->type()).get_width();
393  bit_field_bits += w;
394  const std::size_t bytes = bit_field_bits / 8;
395  bit_field_bits %= 8;
396  result=plus_exprt(result, from_integer(bytes, result.type()));
397  }
398  else
399  {
401  bit_field_bits == 0, "padding ensures offset at byte boundaries");
402  const typet &subtype=it->type();
403  exprt sub_size=size_of_expr(subtype, ns);
404  if(sub_size.is_nil())
405  return nil_exprt();
406 
407  result=plus_exprt(result, sub_size);
408  }
409  }
410 
411  simplify(result, ns);
412 
413  return result;
414  }
415  else if(type.id()==ID_union)
416  {
417  const union_typet &union_type=to_union_type(type);
418  const union_typet::componentst &components=
419  union_type.components();
420 
421  mp_integer max_bytes=0;
422  exprt result=from_integer(0, size_type());
423 
424  // compute max
425 
426  for(union_typet::componentst::const_iterator
427  it=components.begin();
428  it!=components.end();
429  it++)
430  {
431  const typet &subtype=it->type();
432  exprt sub_size;
433 
434  mp_integer sub_bits=pointer_offset_bits(subtype, ns);
435 
436  if(sub_bits==-1)
437  {
438  max_bytes=-1;
439 
440  sub_size=size_of_expr(subtype, ns);
441  if(sub_size.is_nil())
442  return nil_exprt();
443  }
444  else
445  {
446  mp_integer sub_bytes=(sub_bits+7)/8;
447 
448  if(max_bytes>=0)
449  {
450  if(max_bytes<sub_bytes)
451  {
452  max_bytes=sub_bytes;
453  result=from_integer(sub_bytes, size_type());
454  }
455 
456  continue;
457  }
458 
459  sub_size=from_integer(sub_bytes, size_type());
460  }
461 
462  result=if_exprt(
463  binary_relation_exprt(result, ID_lt, sub_size),
464  sub_size, result);
465 
466  simplify(result, ns);
467  }
468 
469  return result;
470  }
471  else if(type.id()==ID_signedbv ||
472  type.id()==ID_unsignedbv ||
473  type.id()==ID_fixedbv ||
474  type.id()==ID_floatbv ||
475  type.id()==ID_bv ||
476  type.id()==ID_c_bool ||
477  type.id()==ID_c_bit_field)
478  {
479  std::size_t width=to_bitvector_type(type).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)
486  {
487  std::size_t width=to_bitvector_type(type.subtype()).get_width();
488  std::size_t bytes=width/8;
489  if(bytes*8!=width)
490  bytes++;
491  return from_integer(bytes, size_type());
492  }
493  else if(type.id()==ID_c_enum_tag)
494  {
495  return size_of_expr(ns.follow_tag(to_c_enum_tag_type(type)), ns);
496  }
497  else if(type.id()==ID_bool)
498  {
499  return from_integer(1, size_type());
500  }
501  else if(type.id()==ID_pointer)
502  {
503  // the following is an MS extension
504  if(type.get_bool(ID_C_ptr32))
505  return from_integer(4, size_type());
506 
507  std::size_t width=to_bitvector_type(type).get_width();
508  std::size_t bytes=width/8;
509  if(bytes*8!=width)
510  bytes++;
511  return from_integer(bytes, size_type());
512  }
513  else if(type.id()==ID_symbol)
514  {
515  return size_of_expr(ns.follow(type), ns);
516  }
517  else if(type.id() == ID_union_tag)
518  {
519  return size_of_expr(ns.follow_tag(to_union_tag_type(type)), ns);
520  }
521  else if(type.id() == ID_struct_tag)
522  {
523  return size_of_expr(ns.follow_tag(to_struct_tag_type(type)), ns);
524  }
525  else if(type.id()==ID_code)
526  {
527  return from_integer(0, size_type());
528  }
529  else if(type.id()==ID_string)
530  {
531  return from_integer(32/8, size_type());
532  }
533  else
534  return nil_exprt();
535 }
536 
538  const exprt &expr,
539  const namespacet &ns)
540 {
541  if(expr.id()==ID_symbol)
542  {
543  if(is_ssa_expr(expr))
544  return compute_pointer_offset(
545  to_ssa_expr(expr).get_original_expr(), ns);
546  else
547  return 0;
548  }
549  else if(expr.id()==ID_index)
550  {
551  const index_exprt &index_expr=to_index_expr(expr);
552  const typet &array_type=ns.follow(index_expr.array().type());
554  array_type.id()==ID_array,
555  "index into array expected, found "+array_type.id_string());
556 
557  mp_integer o=compute_pointer_offset(index_expr.array(), ns);
558 
559  if(o!=-1)
560  {
561  mp_integer sub_size=
562  pointer_offset_size(array_type.subtype(), ns);
563 
564  mp_integer i;
565 
566  if(sub_size>0 && !to_integer(index_expr.index(), i))
567  return o+i*sub_size;
568  }
569 
570  // don't know
571  }
572  else if(expr.id()==ID_member)
573  {
574  const member_exprt &member_expr=to_member_expr(expr);
575  const exprt &op=member_expr.struct_op();
576  const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
577 
579 
580  if(o!=-1)
581  {
582  if(type.id()==ID_union)
583  return o;
584 
585  return o+member_offset(
586  to_struct_type(type), member_expr.get_component_name(), ns);
587  }
588  }
589  else if(expr.id()==ID_string_constant)
590  return 0;
591 
592  return -1; // don't know
593 }
594 
596  const constant_exprt &expr,
597  const namespacet &ns)
598 {
599  const typet &type=
600  static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
601 
602  mp_integer type_size=-1, val=-1;
603 
604  if(type.is_not_nil())
605  type_size=pointer_offset_size(type, ns);
606 
607  if(type_size<0 ||
608  to_integer(expr, val) ||
609  val<type_size ||
610  (type_size==0 && val>0))
611  return nil_exprt();
612 
613  const typet t(size_type());
615  address_bits(val+1)<=pointer_offset_bits(t, ns),
616  "sizeof value does not fit size_type");
617 
618  mp_integer remainder=0;
619  if(type_size!=0)
620  {
621  remainder=val%type_size;
622  val-=remainder;
623  val/=type_size;
624  }
625 
626  exprt result(ID_sizeof, t);
627  result.set(ID_type_arg, type);
628 
629  if(val>1)
630  result=mult_exprt(result, from_integer(val, t));
631  if(remainder>0)
632  result=plus_exprt(result, from_integer(remainder, t));
633 
634  if(result.type()!=expr.type())
635  result.make_typecast(expr.type());
636 
637  return result;
638 }
639 
641  exprt &result,
642  mp_integer offset,
643  const typet &target_type_raw,
644  const namespacet &ns)
645 {
646  const typet &source_type=ns.follow(result.type());
647  const typet &target_type=ns.follow(target_type_raw);
648 
649  if(offset==0 && source_type==target_type)
650  return true;
651 
652  if(source_type.id()==ID_struct)
653  {
654  const auto &st=to_struct_type(source_type);
655  const struct_typet::componentst &components=st.components();
656  member_offset_iterator offsets(st, ns);
657  while(offsets->first<components.size() &&
658  offsets->second!=-1 &&
659  offsets->second<=offset)
660  {
661  auto nextit=offsets;
662  ++nextit;
663  if((offsets->first+1)==components.size() || offset<nextit->second)
664  {
665  // This field might be, or might contain, the answer.
666  result=
667  member_exprt(
668  result,
669  components[offsets->first].get_name(),
670  components[offsets->first].type());
671  return
673  result, offset-offsets->second, target_type, ns);
674  }
675  ++offsets;
676  }
677  return false;
678  }
679  else if(source_type.id()==ID_array)
680  {
681  // A cell of the array might be, or contain, the subexpression
682  // we're looking for.
683  const auto &at=to_array_type(source_type);
684  mp_integer elem_size=pointer_offset_size(at.subtype(), ns);
685  if(elem_size==-1)
686  return false;
687  mp_integer cellidx=offset/elem_size;
688  if(cellidx < 0 || !cellidx.is_long())
689  return false;
690  offset=offset%elem_size;
691  result=index_exprt(result, from_integer(cellidx, unsignedbv_typet(64)));
692  return get_subexpression_at_offset(result, offset, target_type, ns);
693  }
694  else
695  return false;
696 }
697 
699  exprt &result,
700  const exprt &offset,
701  const typet &target_type,
702  const namespacet &ns)
703 {
704  mp_integer offset_const;
705  if(to_integer(offset, offset_const))
706  return false;
707  return get_subexpression_at_offset(result, offset_const, target_type, ns);
708 }
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:1229
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:172
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
bool is_not_nil() const
Definition: irep.h:173
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1159
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:3359
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:4422
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:80
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:3869
const irep_idt & id() const
Definition: irep.h:259
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:4508
bool get_subexpression_at_offset(exprt &result, mp_integer offset, const typet &target_type_raw, const namespacet &ns)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:603
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const exprt & size() const
Definition: std_types.h:1648
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a struct_tag_typet.
Definition: std_types.h:566
const exprt & size() const
Definition: std_types.h:1023
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::size_t get_width() const
Definition: std_types.h:1138
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:1054
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3909
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:3893
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:262
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:1411
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:278
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:286
bool simplify(exprt &expr, const namespacet &ns)
array index operator
Definition: std_expr.h:1462