cprover
c_sizeof.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Conversion of sizeof Expressions
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_sizeof.h"
13 
14 #include <util/config.h>
15 #include <util/arith_tools.h>
16 #include <util/simplify_expr.h>
17 #include <util/std_expr.h>
18 #include <util/c_types.h>
19 
20 #include "c_typecast.h"
21 
23 {
24  // this implementation will eventually be replaced
25  // by size_of_expr in util/pointer_offset_size.h
26  exprt dest;
27 
28  if(type.id()==ID_signedbv ||
29  type.id()==ID_unsignedbv ||
30  type.id()==ID_floatbv ||
31  type.id()==ID_fixedbv ||
32  type.id()==ID_c_bool)
33  {
34  // We round up to bytes.
35  // See special treatment for bit-fields below.
36  std::size_t bits=to_bitvector_type(type).get_width();
37  std::size_t bytes=bits/8;
38  if((bits%8)!=0)
39  bytes++;
40  dest=from_integer(bytes, size_type());
41  }
42  else if(type.id()==ID_incomplete_c_enum)
43  {
44  // refuse to give a size
45  return nil_exprt();
46  }
47  else if(type.id()==ID_c_enum)
48  {
49  // check the subtype
50  dest=sizeof_rec(type.subtype());
51  }
52  else if(type.id()==ID_c_enum_tag)
53  {
54  // follow the tag
56  }
57  else if(type.id()==ID_pointer)
58  {
59  // the following is an MS extension
60  if(type.get_bool(ID_C_ptr32))
61  return from_integer(4, size_type());
62 
63  std::size_t bits=config.ansi_c.pointer_width;
64  std::size_t bytes=bits/8;
65  if((bits%8)!=0)
66  bytes++;
67  dest=from_integer(bytes, size_type());
68  }
69  else if(type.id()==ID_bool)
70  {
71  // We fit booleans into a byte.
72  // Don't confuse with c_bool, which is a bit-vector type.
73  dest=from_integer(1, size_type());
74  }
75  else if(type.id()==ID_array)
76  {
77  const exprt &size_expr=
78  to_array_type(type).size();
79 
80  if(size_expr.is_nil())
81  {
82  // treated like an empty array
83  dest=from_integer(0, size_type());
84  }
85  else
86  {
87  exprt tmp_dest=sizeof_rec(type.subtype());
88 
89  if(tmp_dest.is_nil())
90  return tmp_dest;
91 
92  mp_integer a, b;
93 
94  if(!to_integer(tmp_dest, a) &&
95  !to_integer(size_expr, b))
96  {
97  dest=from_integer(a*b, size_type());
98  }
99  else
100  {
101  dest.id(ID_mult);
102  dest.type()=size_type();
103  dest.copy_to_operands(size_expr);
104  dest.move_to_operands(tmp_dest);
105  c_implicit_typecast(dest.op0(), dest.type(), ns);
106  c_implicit_typecast(dest.op1(), dest.type(), ns);
107  }
108  }
109  }
110  else if(type.id()==ID_struct)
111  {
112  const struct_typet::componentst &components=
113  to_struct_type(type).components();
114 
115  dest=from_integer(0, size_type());
116 
117  mp_integer bit_field_width=0;
118 
119  for(const auto &comp : components)
120  {
121  const typet &sub_type=ns.follow(comp.type());
122 
123  if(comp.get_bool(ID_is_type))
124  {
125  }
126  else if(sub_type.id()==ID_code)
127  {
128  }
129  else if(sub_type.id()==ID_c_bit_field)
130  {
131  // We just sum them up.
132  // This assumes they are properly padded.
133  bit_field_width+=to_c_bit_field_type(sub_type).get_width();
134  }
135  else
136  {
137  exprt tmp=sizeof_rec(sub_type);
138 
139  if(tmp.is_nil())
140  return tmp;
141 
142  dest=plus_exprt(dest, tmp);
143  }
144  }
145 
146  if(bit_field_width!=0)
147  dest=plus_exprt(dest, from_integer(bit_field_width/8, size_type()));
148  }
149  else if(type.id()==ID_union)
150  {
151  // the empty union will have size 0
152  exprt max_size=from_integer(0, size_type());
153 
154  const union_typet::componentst &components=
155  to_union_type(type).components();
156 
157  for(const auto &comp : components)
158  {
159  if(comp.get_bool(ID_is_type) || comp.type().id()==ID_code)
160  continue;
161 
162  const typet &sub_type=comp.type();
163 
164  exprt tmp;
165 
166  if(sub_type.id()==ID_c_bit_field)
167  {
168  std::size_t width=to_c_bit_field_type(sub_type).get_width();
169  tmp=
170  from_integer(width/8, size_type());
171  }
172  else
173  {
174  tmp=sizeof_rec(sub_type);
175 
176  if(tmp.is_nil())
177  return nil_exprt();
178  }
179 
180  max_size=if_exprt(
181  binary_relation_exprt(max_size, ID_lt, tmp),
182  tmp, max_size);
183 
184  simplify(max_size, ns);
185  }
186 
187  dest=max_size;
188  }
189  else if(type.id()==ID_symbol)
190  {
191  return sizeof_rec(ns.follow(type));
192  }
193  else if(type.id()==ID_empty)
194  {
195  // gcc says that sizeof(void)==1, ISO C doesn't
196  dest=from_integer(1, size_type());
197  }
198  else if(type.id()==ID_vector)
199  {
200  // simply multiply
201  const exprt &size_expr=
202  to_vector_type(type).size();
203 
204  exprt tmp_dest=sizeof_rec(type.subtype());
205 
206  if(tmp_dest.is_nil())
207  return tmp_dest;
208 
209  mp_integer a, b;
210 
211  if(!to_integer(tmp_dest, a) &&
212  !to_integer(size_expr, b))
213  {
214  dest=from_integer(a*b, size_type());
215  }
216  else
217  {
218  dest.id(ID_mult);
219  dest.type()=size_type();
220  dest.copy_to_operands(size_expr);
221  dest.move_to_operands(tmp_dest);
222  c_implicit_typecast(dest.op0(), dest.type(), ns);
223  c_implicit_typecast(dest.op1(), dest.type(), ns);
224  }
225  }
226  else if(type.id()==ID_complex)
227  {
228  // this is a pair
229 
230  exprt tmp_dest=sizeof_rec(type.subtype());
231 
232  if(tmp_dest.is_nil())
233  return tmp_dest;
234 
235  mp_integer a;
236 
237  if(!to_integer(tmp_dest, a))
238  dest=from_integer(a*2, size_type());
239  else
240  return nil_exprt();
241  }
242  else
243  {
244  // We give up; this shouldn't really happen on 'proper' C types,
245  // but we do have some artificial ones that simply have no
246  // meaningful size.
247  dest.make_nil();
248  }
249 
250  return dest;
251 }
252 
254  const struct_typet &type,
255  const irep_idt &component_name)
256 {
257  const struct_typet::componentst &components=
258  type.components();
259 
260  exprt dest=from_integer(0, size_type());
261 
262  mp_integer bit_field_width=0;
263 
264  for(const auto &comp : components)
265  {
266  if(comp.get_name()==component_name)
267  {
268  // done
269  if(bit_field_width!=0)
270  dest=plus_exprt(dest, from_integer(bit_field_width/8, size_type()));
271  return dest;
272  }
273 
274  if(comp.get_bool(ID_is_type))
275  continue;
276 
277  const typet &sub_type=ns.follow(comp.type());
278 
279  if(sub_type.id()==ID_code)
280  {
281  }
282  else if(sub_type.id()==ID_c_bit_field)
283  {
284  // We just sum them up.
285  // This assumes they are properly padded.
286  bit_field_width+=to_c_bit_field_type(sub_type).get_width();
287  }
288  else
289  {
290  exprt tmp=sizeof_rec(sub_type);
291 
292  if(tmp.is_nil())
293  return tmp;
294 
295  exprt sum=plus_exprt(dest, tmp);
296  dest=sum;
297  }
298  }
299 
300  return nil_exprt();
301 }
302 
303 exprt c_sizeof(const typet &src, const namespacet &ns)
304 {
305  c_sizeoft c_sizeof_inst(ns);
306  exprt tmp=c_sizeof_inst(src);
307  simplify(tmp, ns);
308  return tmp;
309 }
310 
312  const struct_typet &src,
313  const irep_idt &component_name,
314  const namespacet &ns)
315 {
316  c_sizeoft c_sizeof_inst(ns);
317  exprt tmp=c_sizeof_inst.c_offsetof(src, component_name);
318  simplify(tmp, ns);
319  return tmp;
320 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:19
bool is_nil() const
Definition: irep.h:103
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
exprt & op0()
Definition: expr.h:84
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::vector< componentt > componentst
Definition: std_types.h:240
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
const componentst & components() const
Definition: std_types.h:242
The trinary if-then-else operator.
Definition: std_expr.h:2771
typet & type()
Definition: expr.h:60
unsignedbv_typet size_type()
Definition: c_types.cpp:57
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
configt config
Definition: config.cpp:21
virtual exprt sizeof_rec(const typet &type)
Definition: c_sizeof.cpp:22
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
const irep_idt & id() const
Definition: irep.h:189
exprt c_sizeof(const typet &src, const namespacet &ns)
Definition: c_sizeof.cpp:303
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
The NIL expression.
Definition: std_expr.h:3764
API to expression classes.
exprt & op1()
Definition: expr.h:87
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
bool c_implicit_typecast(exprt &expr, const typet &dest_type, const namespacet &ns)
Definition: c_typecast.cpp:26
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
const namespacet & ns
Definition: c_sizeof.h:37
Base class for all expressions.
Definition: expr.h:46
void make_nil()
Definition: irep.h:243
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
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
exprt c_offsetof(const struct_typet &type, const irep_idt &component_name)
Definition: c_sizeof.cpp:253
bool simplify(exprt &expr, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051