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