cprover
padding.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "padding.h"
13 
14 #include <algorithm>
15 
16 #include <util/config.h>
18 #include <util/simplify_expr.h>
19 #include <util/arith_tools.h>
20 
21 mp_integer alignment(const typet &type, const namespacet &ns)
22 {
23  // we need to consider a number of different cases:
24  // - alignment specified in the source, which will be recorded in
25  // ID_C_alignment
26  // - alignment induced by packing ("The alignment of a member will
27  // be on a boundary that is either a multiple of n or a multiple of
28  // the size of the member, whichever is smaller."); both
29  // ID_C_alignment and ID_C_packed will be set
30  // - natural alignment, when neither ID_C_alignment nor ID_C_packed
31  // are set
32  // - dense packing with only ID_C_packed set.
33 
34  // is the alignment given?
35  const exprt &given_alignment=
36  static_cast<const exprt &>(type.find(ID_C_alignment));
37 
38  mp_integer a_int;
39 
40  // we trust it blindly, no matter how nonsensical
41  if(given_alignment.is_nil() ||
42  to_integer(given_alignment, a_int))
43  a_int=0;
44 
45  // alignment but no packing
46  if(a_int>0 && !type.get_bool(ID_C_packed))
47  return a_int;
48  // no alignment, packing
49  else if(a_int==0 && type.get_bool(ID_C_packed))
50  return 1;
51 
52  // compute default
53  mp_integer result;
54 
55  if(type.id()==ID_array)
56  result=alignment(type.subtype(), ns);
57  else if(type.id()==ID_struct || type.id()==ID_union)
58  {
59  const struct_union_typet::componentst &components=
61 
62  result=1;
63 
64  // get the max
65  // (should really be the smallest common denominator)
66  for(struct_union_typet::componentst::const_iterator
67  it=components.begin();
68  it!=components.end();
69  it++)
70  result=std::max(result, alignment(it->type(), ns));
71  }
72  else if(type.id()==ID_unsignedbv ||
73  type.id()==ID_signedbv ||
74  type.id()==ID_fixedbv ||
75  type.id()==ID_floatbv ||
76  type.id()==ID_c_bool ||
77  type.id()==ID_pointer)
78  {
79  result=pointer_offset_size(type, ns);
80  }
81  else if(type.id()==ID_c_enum)
82  result=alignment(type.subtype(), ns);
83  else if(type.id()==ID_c_enum_tag)
84  result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns);
85  else if(type.id()==ID_symbol)
86  result=alignment(ns.follow(type), ns);
87  else if(type.id()==ID_c_bit_field)
88  {
89  // we align these according to the 'underlying type'
90  result=alignment(type.subtype(), ns);
91  }
92  else
93  result=1;
94 
95  // if an alignment had been provided and packing was requested, take
96  // the smallest alignment
97  if(a_int>0 && a_int<result)
98  result=a_int;
99 
100  return result;
101 }
102 
105 {
106  const typet &subtype = type.subtype();
107 
108  if(subtype.id() == ID_bool)
109  {
110  // This is the 'proper' bool.
111  return 1;
112  }
113  else if(
114  subtype.id() == ID_signedbv || subtype.id() == ID_unsignedbv ||
115  subtype.id() == ID_c_bool)
116  {
117  return to_bitvector_type(subtype).get_width();
118  }
119  else if(subtype.id() == ID_c_enum_tag)
120  {
121  // These point to an enum, which has a sub-subtype,
122  // which may be smaller or larger than int, and we thus have
123  // to check.
124  const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
125 
126  if(c_enum_type.id() == ID_c_enum)
127  return c_enum_type.subtype().get_int(ID_width);
128  else
129  return {};
130  }
131  else
132  return {};
133 }
134 
135 static struct_typet::componentst::iterator pad_bit_field(
136  struct_typet::componentst &components,
137  struct_typet::componentst::iterator where,
138  std::size_t pad_bits)
139 {
140  const c_bit_field_typet padding_type(
141  unsignedbv_typet(pad_bits), pad_bits);
142 
143  struct_typet::componentt component(
144  "$bit_field_pad" + std::to_string(where - components.begin()),
145  padding_type);
146 
147  component.set_is_padding(true);
148 
149  return std::next(components.insert(where, component));
150 }
151 
152 static struct_typet::componentst::iterator pad(
153  struct_typet::componentst &components,
154  struct_typet::componentst::iterator where,
155  std::size_t pad_bits)
156 {
157  const unsignedbv_typet padding_type(pad_bits);
158 
159  struct_typet::componentt component(
160  "$pad" + std::to_string(where - components.begin()),
161  padding_type);
162 
163  component.set_is_padding(true);
164 
165  return std::next(components.insert(where, component));
166 }
167 
168 static void add_padding_msvc(struct_typet &type, const namespacet &ns)
169 {
170  struct_typet::componentst &components=type.components();
171 
172  std::size_t bit_field_bits = 0, underlying_bits = 0;
173  mp_integer offset = 0;
174 
175  bool is_packed = type.get_bool(ID_C_packed);
176 
177  for(struct_typet::componentst::iterator it = components.begin();
178  it != components.end();
179  it++)
180  {
181  // there is exactly one case in which padding is not added:
182  // if we continue a bit-field with size>0 and the same underlying width
183 
184  if(
185  it->type().id() == ID_c_bit_field &&
186  to_c_bit_field_type(it->type()).get_width() != 0 &&
187  underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0) ==
188  underlying_bits)
189  {
190  // do not add padding, but count the bits
191  const auto width = to_c_bit_field_type(it->type()).get_width();
192  bit_field_bits += width;
193  }
194  else
195  {
196  // pad up any remaining bit field
197  if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
198  {
199  const std::size_t pad_bits =
200  underlying_bits - (bit_field_bits % underlying_bits);
201  it = pad_bit_field(components, it, pad_bits);
202  offset += (bit_field_bits + pad_bits) / config.ansi_c.char_width;
203  underlying_bits = bit_field_bits = 0;
204  }
205 
206  // pad up to underlying type unless the struct is packed
207  if(!is_packed)
208  {
209  const mp_integer a = alignment(it->type(), ns);
210  if(a > 1)
211  {
212  const mp_integer displacement = offset % a;
213 
214  if(displacement != 0)
215  {
216  const mp_integer pad_bytes = a - displacement;
217  std::size_t pad_bits =
218  integer2size_t(pad_bytes * config.ansi_c.char_width);
219  it = pad(components, it, pad_bits);
220  offset += pad_bytes;
221  }
222  }
223  }
224 
225  // do we start a new bit field?
226  if(it->type().id() == ID_c_bit_field)
227  {
228  underlying_bits =
229  underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0);
230  const auto width = to_c_bit_field_type(it->type()).get_width();
231  bit_field_bits += width;
232  }
233  else
234  {
235  // keep track of offset
236  const mp_integer size = pointer_offset_size(it->type(), ns);
237  if(size >= 1)
238  offset += size;
239  }
240  }
241  }
242 
243  // Add padding at the end?
244  // Bit-field
245  if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
246  {
247  const std::size_t pad =
248  underlying_bits - (bit_field_bits % underlying_bits);
249  pad_bit_field(components, components.end(), pad);
250  offset += (bit_field_bits + pad) / config.ansi_c.char_width;
251  }
252 
253  // alignment of the struct
254  // Note that this is done even if the struct is packed.
255  const mp_integer a = alignment(type, ns);
256  const mp_integer displacement = offset % a;
257 
258  if(displacement != 0)
259  {
260  const mp_integer pad_bytes = a - displacement;
261  const std::size_t pad_bits =
262  integer2size_t(pad_bytes * config.ansi_c.char_width);
263  pad(components, components.end(), pad_bits);
264  offset += pad_bytes;
265  }
266 }
267 
268 static void add_padding_gcc(struct_typet &type, const namespacet &ns)
269 {
270  struct_typet::componentst &components = type.components();
271 
272  // First make bit-fields appear on byte boundaries
273  {
274  std::size_t bit_field_bits=0;
275 
276  for(struct_typet::componentst::iterator
277  it=components.begin();
278  it!=components.end();
279  it++)
280  {
281  if(it->type().id()==ID_c_bit_field &&
282  to_c_bit_field_type(it->type()).get_width()!=0)
283  {
284  // count the bits
285  const std::size_t width = to_c_bit_field_type(it->type()).get_width();
286  bit_field_bits+=width;
287  }
288  else if(bit_field_bits!=0)
289  {
290  // not on a byte-boundary?
291  if((bit_field_bits % config.ansi_c.char_width) != 0)
292  {
293  const std::size_t pad = config.ansi_c.char_width -
294  bit_field_bits % config.ansi_c.char_width;
295  it = pad_bit_field(components, it, pad);
296  }
297 
298  bit_field_bits=0;
299  }
300  }
301 
302  // Add padding at the end?
303  if((bit_field_bits % config.ansi_c.char_width) != 0)
304  {
305  const std::size_t pad =
306  config.ansi_c.char_width - bit_field_bits % config.ansi_c.char_width;
307  pad_bit_field(components, components.end(), pad);
308  }
309  }
310 
311  // Is the struct packed, without any alignment specification?
312  if(type.get_bool(ID_C_packed) &&
313  type.find(ID_C_alignment).is_nil())
314  return; // done
315 
316  mp_integer offset=0;
317  mp_integer max_alignment=0;
318  std::size_t bit_field_bits=0;
319 
320  for(struct_typet::componentst::iterator
321  it=components.begin();
322  it!=components.end();
323  it++)
324  {
325  const typet it_type=it->type();
326  mp_integer a=1;
327 
328  const bool packed=it_type.get_bool(ID_C_packed) ||
329  ns.follow(it_type).get_bool(ID_C_packed);
330 
331  if(it_type.id()==ID_c_bit_field)
332  {
333  a=alignment(to_c_bit_field_type(it_type).subtype(), ns);
334 
335  // A zero-width bit-field causes alignment to the base-type.
336  if(to_c_bit_field_type(it_type).get_width()==0)
337  {
338  }
339  else
340  {
341  // Otherwise, ANSI-C says that bit-fields do not get padded!
342  // We consider the type for max_alignment, however.
343  if(max_alignment<a)
344  max_alignment=a;
345 
346  std::size_t w=to_c_bit_field_type(it_type).get_width();
347  bit_field_bits += w;
348  const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
349  bit_field_bits %= config.ansi_c.char_width;
350  offset+=bytes;
351  continue;
352  }
353  }
354  else
355  a=alignment(it_type, ns);
356 
358  bit_field_bits == 0, "padding ensures offset at byte boundaries");
359 
360  // check minimum alignment
361  if(a<config.ansi_c.alignment && !packed)
363 
364  if(max_alignment<a)
365  max_alignment=a;
366 
367  if(a!=1)
368  {
369  // we may need to align it
370  const mp_integer displacement = offset % a;
371 
372  if(displacement!=0)
373  {
374  const mp_integer pad_bytes = a - displacement;
375  const std::size_t pad_bits =
376  integer2size_t(pad_bytes * config.ansi_c.char_width);
377  it = pad(components, it, pad_bits);
378  offset += pad_bytes;
379  }
380  }
381 
382  mp_integer size=pointer_offset_size(it_type, ns);
383 
384  if(size!=-1)
385  offset+=size;
386  }
387 
388  // any explicit alignment for the struct?
389  if(type.find(ID_C_alignment).is_not_nil())
390  {
391  const exprt &alignment=
392  static_cast<const exprt &>(type.find(ID_C_alignment));
393  if(alignment.id()!=ID_default)
394  {
395  exprt tmp=alignment;
396  simplify(tmp, ns);
397  mp_integer tmp_i;
398  if(!to_integer(tmp, tmp_i) && tmp_i>max_alignment)
399  max_alignment=tmp_i;
400  }
401  }
402  // Is the struct packed, without any alignment specification?
403  else if(type.get_bool(ID_C_packed))
404  return; // done
405 
406  // There may be a need for 'end of struct' padding.
407  // We use 'max_alignment'.
408 
409  if(max_alignment>1)
410  {
411  // we may need to align it
412  mp_integer displacement=offset%max_alignment;
413 
414  if(displacement!=0)
415  {
416  mp_integer pad_bytes = max_alignment - displacement;
417  std::size_t pad_bits =
418  integer2size_t(pad_bytes * config.ansi_c.char_width);
419  pad(components, components.end(), pad_bits);
420  }
421  }
422 }
423 
424 void add_padding(struct_typet &type, const namespacet &ns)
425 {
426  // padding depends greatly on compiler
428  add_padding_msvc(type, ns);
429  else
430  add_padding_gcc(type, ns);
431 }
432 
433 void add_padding(union_typet &type, const namespacet &ns)
434 {
435  mp_integer max_alignment_bits =
436  alignment(type, ns) * config.ansi_c.char_width;
437  mp_integer size_bits=0;
438 
439  // check per component, and ignore those without fixed size
440  for(const auto &c : type.components())
441  {
442  mp_integer s=pointer_offset_bits(c.type(), ns);
443  if(s>0)
444  size_bits=std::max(size_bits, s);
445  }
446 
447  // Is the union packed?
448  if(type.get_bool(ID_C_packed))
449  {
450  // The size needs to be a multiple of 1 char only.
451  max_alignment_bits = config.ansi_c.char_width;
452  }
453 
455  {
456  // Visual Studio pads up to the underlying width of
457  // any bit field.
458  for(const auto &c : type.components())
459  if(c.type().id() == ID_c_bit_field)
460  {
461  auto w = underlying_width(to_c_bit_field_type(c.type()), ns);
462  if(w.has_value() && w.value() > max_alignment_bits)
463  max_alignment_bits = w.value();
464  }
465  }
466 
467  // The size must be a multiple of the alignment, or
468  // we add a padding member to the union.
469 
470  if(size_bits%max_alignment_bits!=0)
471  {
472  mp_integer padding_bits=
473  max_alignment_bits-(size_bits%max_alignment_bits);
474 
475  unsignedbv_typet padding_type(
476  integer2size_t(size_bits+padding_bits));
477 
478  struct_typet::componentt component;
479  component.type()=padding_type;
480  component.set_name("$pad");
481  component.set_is_padding(true);
482 
483  type.components().push_back(component);
484  }
485 }
The type of an expression.
Definition: type.h:22
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
BigInt mp_integer
Definition: mp_arith.h:22
static struct_typet::componentst::iterator pad_bit_field(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition: padding.cpp:135
bool is_nil() const
Definition: irep.h:102
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
std::size_t alignment
Definition: config.h:69
void set_name(const irep_idt &name)
Definition: std_types.h:187
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:245
static optionalt< std::size_t > underlying_width(const c_bit_field_typet &type, const namespacet &ns)
Definition: padding.cpp:104
static void add_padding_msvc(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:168
std::vector< componentt > componentst
Definition: std_types.h:243
const componentst & components() const
Definition: std_types.h:245
static void add_padding_gcc(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:268
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
Structure type.
Definition: std_types.h:297
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
configt config
Definition: config.cpp:23
std::size_t char_width
Definition: config.h:33
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:74
Type for c bit fields.
Definition: std_types.h:1381
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
const irep_idt & id() const
Definition: irep.h:189
void set_is_padding(bool is_padding)
Definition: std_types.h:237
void add_padding(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:424
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition: padding.cpp:152
ANSI-C Language Type Checking.
flavourt mode
Definition: config.h:106
nonstd::optional< T > optionalt
Definition: optional.h:35
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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
Pointer Logic.
Base class for all expressions.
Definition: expr.h:42
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
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool simplify(exprt &expr, const namespacet &ns)