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_struct_tag)
86  result = alignment(ns.follow_tag(to_struct_tag_type(type)), ns);
87  else if(type.id() == ID_union_tag)
88  result = alignment(ns.follow_tag(to_union_tag_type(type)), ns);
89  else if(type.id()==ID_symbol)
90  result=alignment(ns.follow(type), ns);
91  else if(type.id()==ID_c_bit_field)
92  {
93  // we align these according to the 'underlying type'
94  result=alignment(type.subtype(), ns);
95  }
96  else
97  result=1;
98 
99  // if an alignment had been provided and packing was requested, take
100  // the smallest alignment
101  if(a_int>0 && a_int<result)
102  result=a_int;
103 
104  return result;
105 }
106 
109 {
110  const typet &subtype = type.subtype();
111 
112  if(subtype.id() == ID_bool)
113  {
114  // This is the 'proper' bool.
115  return 1;
116  }
117  else if(
118  subtype.id() == ID_signedbv || subtype.id() == ID_unsignedbv ||
119  subtype.id() == ID_c_bool)
120  {
121  return to_bitvector_type(subtype).get_width();
122  }
123  else if(subtype.id() == ID_c_enum_tag)
124  {
125  // These point to an enum, which has a sub-subtype,
126  // which may be smaller or larger than int, and we thus have
127  // to check.
128  const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
129 
130  if(c_enum_type.id() == ID_c_enum)
131  return c_enum_type.subtype().get_size_t(ID_width);
132  else
133  return {};
134  }
135  else
136  return {};
137 }
138 
139 static struct_typet::componentst::iterator pad_bit_field(
140  struct_typet::componentst &components,
141  struct_typet::componentst::iterator where,
142  std::size_t pad_bits)
143 {
144  const c_bit_field_typet padding_type(
145  unsignedbv_typet(pad_bits), pad_bits);
146 
147  struct_typet::componentt component(
148  "$bit_field_pad" + std::to_string(where - components.begin()),
149  padding_type);
150 
151  component.set_is_padding(true);
152 
153  return std::next(components.insert(where, component));
154 }
155 
156 static struct_typet::componentst::iterator pad(
157  struct_typet::componentst &components,
158  struct_typet::componentst::iterator where,
159  std::size_t pad_bits)
160 {
161  const unsignedbv_typet padding_type(pad_bits);
162 
163  struct_typet::componentt component(
164  "$pad" + std::to_string(where - components.begin()),
165  padding_type);
166 
167  component.set_is_padding(true);
168 
169  return std::next(components.insert(where, component));
170 }
171 
172 static void add_padding_msvc(struct_typet &type, const namespacet &ns)
173 {
174  struct_typet::componentst &components=type.components();
175 
176  std::size_t bit_field_bits = 0, underlying_bits = 0;
177  mp_integer offset = 0;
178 
179  bool is_packed = type.get_bool(ID_C_packed);
180 
181  for(struct_typet::componentst::iterator it = components.begin();
182  it != components.end();
183  it++)
184  {
185  // there is exactly one case in which padding is not added:
186  // if we continue a bit-field with size>0 and the same underlying width
187 
188  if(
189  it->type().id() == ID_c_bit_field &&
190  to_c_bit_field_type(it->type()).get_width() != 0 &&
191  underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0) ==
192  underlying_bits)
193  {
194  // do not add padding, but count the bits
195  const auto width = to_c_bit_field_type(it->type()).get_width();
196  bit_field_bits += width;
197  }
198  else
199  {
200  // pad up any remaining bit field
201  if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
202  {
203  const std::size_t pad_bits =
204  underlying_bits - (bit_field_bits % underlying_bits);
205  it = pad_bit_field(components, it, pad_bits);
206  offset += (bit_field_bits + pad_bits) / config.ansi_c.char_width;
207  underlying_bits = bit_field_bits = 0;
208  }
209 
210  // pad up to underlying type unless the struct is packed
211  if(!is_packed)
212  {
213  const mp_integer a = alignment(it->type(), ns);
214  if(a > 1)
215  {
216  const mp_integer displacement = offset % a;
217 
218  if(displacement != 0)
219  {
220  const mp_integer pad_bytes = a - displacement;
221  std::size_t pad_bits =
222  integer2size_t(pad_bytes * config.ansi_c.char_width);
223  it = pad(components, it, pad_bits);
224  offset += pad_bytes;
225  }
226  }
227  }
228 
229  // do we start a new bit field?
230  if(it->type().id() == ID_c_bit_field)
231  {
232  underlying_bits =
233  underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0);
234  const auto width = to_c_bit_field_type(it->type()).get_width();
235  bit_field_bits += width;
236  }
237  else
238  {
239  // keep track of offset
240  const mp_integer size = pointer_offset_size(it->type(), ns);
241  if(size >= 1)
242  offset += size;
243  }
244  }
245  }
246 
247  // Add padding at the end?
248  // Bit-field
249  if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
250  {
251  const std::size_t pad =
252  underlying_bits - (bit_field_bits % underlying_bits);
253  pad_bit_field(components, components.end(), pad);
254  offset += (bit_field_bits + pad) / config.ansi_c.char_width;
255  }
256 
257  // alignment of the struct
258  // Note that this is done even if the struct is packed.
259  const mp_integer a = alignment(type, ns);
260  const mp_integer displacement = offset % a;
261 
262  if(displacement != 0)
263  {
264  const mp_integer pad_bytes = a - displacement;
265  const std::size_t pad_bits =
266  integer2size_t(pad_bytes * config.ansi_c.char_width);
267  pad(components, components.end(), pad_bits);
268  offset += pad_bytes;
269  }
270 }
271 
272 static void add_padding_gcc(struct_typet &type, const namespacet &ns)
273 {
274  struct_typet::componentst &components = type.components();
275 
276  // First make bit-fields appear on byte boundaries
277  {
278  std::size_t bit_field_bits=0;
279 
280  for(struct_typet::componentst::iterator
281  it=components.begin();
282  it!=components.end();
283  it++)
284  {
285  if(it->type().id()==ID_c_bit_field &&
286  to_c_bit_field_type(it->type()).get_width()!=0)
287  {
288  // count the bits
289  const std::size_t width = to_c_bit_field_type(it->type()).get_width();
290  bit_field_bits+=width;
291  }
292  else if(bit_field_bits!=0)
293  {
294  // not on a byte-boundary?
295  if((bit_field_bits % config.ansi_c.char_width) != 0)
296  {
297  const std::size_t pad = config.ansi_c.char_width -
298  bit_field_bits % config.ansi_c.char_width;
299  it = pad_bit_field(components, it, pad);
300  }
301 
302  bit_field_bits=0;
303  }
304  }
305 
306  // Add padding at the end?
307  if((bit_field_bits % config.ansi_c.char_width) != 0)
308  {
309  const std::size_t pad =
310  config.ansi_c.char_width - bit_field_bits % config.ansi_c.char_width;
311  pad_bit_field(components, components.end(), pad);
312  }
313  }
314 
315  // Is the struct packed, without any alignment specification?
316  if(type.get_bool(ID_C_packed) &&
317  type.find(ID_C_alignment).is_nil())
318  return; // done
319 
320  mp_integer offset=0;
321  mp_integer max_alignment=0;
322  std::size_t bit_field_bits=0;
323 
324  for(struct_typet::componentst::iterator
325  it=components.begin();
326  it!=components.end();
327  it++)
328  {
329  const typet it_type=it->type();
330  mp_integer a=1;
331 
332  const bool packed=it_type.get_bool(ID_C_packed) ||
333  ns.follow(it_type).get_bool(ID_C_packed);
334 
335  if(it_type.id()==ID_c_bit_field)
336  {
337  a=alignment(to_c_bit_field_type(it_type).subtype(), ns);
338 
339  // A zero-width bit-field causes alignment to the base-type.
340  if(to_c_bit_field_type(it_type).get_width()==0)
341  {
342  }
343  else
344  {
345  // Otherwise, ANSI-C says that bit-fields do not get padded!
346  // We consider the type for max_alignment, however.
347  if(max_alignment<a)
348  max_alignment=a;
349 
350  std::size_t w=to_c_bit_field_type(it_type).get_width();
351  bit_field_bits += w;
352  const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
353  bit_field_bits %= config.ansi_c.char_width;
354  offset+=bytes;
355  continue;
356  }
357  }
358  else
359  a=alignment(it_type, ns);
360 
362  bit_field_bits == 0, "padding ensures offset at byte boundaries");
363 
364  // check minimum alignment
365  if(a<config.ansi_c.alignment && !packed)
367 
368  if(max_alignment<a)
369  max_alignment=a;
370 
371  if(a!=1)
372  {
373  // we may need to align it
374  const mp_integer displacement = offset % a;
375 
376  if(displacement!=0)
377  {
378  const mp_integer pad_bytes = a - displacement;
379  const std::size_t pad_bits =
380  integer2size_t(pad_bytes * config.ansi_c.char_width);
381  it = pad(components, it, pad_bits);
382  offset += pad_bytes;
383  }
384  }
385 
386  mp_integer size=pointer_offset_size(it_type, ns);
387 
388  if(size!=-1)
389  offset+=size;
390  }
391 
392  // any explicit alignment for the struct?
393  if(type.find(ID_C_alignment).is_not_nil())
394  {
395  const exprt &alignment=
396  static_cast<const exprt &>(type.find(ID_C_alignment));
397  if(alignment.id()!=ID_default)
398  {
399  exprt tmp=alignment;
400  simplify(tmp, ns);
401  mp_integer tmp_i;
402  if(!to_integer(tmp, tmp_i) && tmp_i>max_alignment)
403  max_alignment=tmp_i;
404  }
405  }
406  // Is the struct packed, without any alignment specification?
407  else if(type.get_bool(ID_C_packed))
408  return; // done
409 
410  // There may be a need for 'end of struct' padding.
411  // We use 'max_alignment'.
412 
413  if(max_alignment>1)
414  {
415  // we may need to align it
416  mp_integer displacement=offset%max_alignment;
417 
418  if(displacement!=0)
419  {
420  mp_integer pad_bytes = max_alignment - displacement;
421  std::size_t pad_bits =
422  integer2size_t(pad_bytes * config.ansi_c.char_width);
423  pad(components, components.end(), pad_bits);
424  }
425  }
426 }
427 
428 void add_padding(struct_typet &type, const namespacet &ns)
429 {
430  // padding depends greatly on compiler
432  add_padding_msvc(type, ns);
433  else
434  add_padding_gcc(type, ns);
435 }
436 
437 void add_padding(union_typet &type, const namespacet &ns)
438 {
439  mp_integer max_alignment_bits =
440  alignment(type, ns) * config.ansi_c.char_width;
441  mp_integer size_bits=0;
442 
443  // check per component, and ignore those without fixed size
444  for(const auto &c : type.components())
445  {
446  mp_integer s=pointer_offset_bits(c.type(), ns);
447  if(s>0)
448  size_bits=std::max(size_bits, s);
449  }
450 
451  // Is the union packed?
452  if(type.get_bool(ID_C_packed))
453  {
454  // The size needs to be a multiple of 1 char only.
455  max_alignment_bits = config.ansi_c.char_width;
456  }
457 
459  {
460  // Visual Studio pads up to the underlying width of
461  // any bit field.
462  for(const auto &c : type.components())
463  if(c.type().id() == ID_c_bit_field)
464  {
465  auto w = underlying_width(to_c_bit_field_type(c.type()), ns);
466  if(w.has_value() && w.value() > max_alignment_bits)
467  max_alignment_bits = w.value();
468  }
469  }
470 
471  // The size must be a multiple of the alignment, or
472  // we add a padding member to the union.
473 
474  if(size_bits%max_alignment_bits!=0)
475  {
476  mp_integer padding_bits=
477  max_alignment_bits-(size_bits%max_alignment_bits);
478 
479  unsignedbv_typet padding_type(
480  integer2size_t(size_bits+padding_bits));
481 
482  struct_typet::componentt component;
483  component.type()=padding_type;
484  component.set_name("$pad");
485  component.set_is_padding(true);
486 
487  type.components().push_back(component);
488  }
489 }
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:1229
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:139
bool is_nil() const
Definition: irep.h:172
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
std::size_t alignment
Definition: config.h:69
void set_name(const irep_idt &name)
Definition: std_types.h:187
static optionalt< std::size_t > underlying_width(const c_bit_field_typet &type, const namespacet &ns)
Definition: padding.cpp:108
static void add_padding_msvc(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:172
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:272
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:80
Type for c bit fields.
Definition: std_types.h:1390
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:259
void set_is_padding(bool is_padding)
Definition: std_types.h:237
void add_padding(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:428
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition: padding.cpp:156
ANSI-C Language Type Checking.
flavourt mode
Definition: config.h:114
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
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 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 typet & follow(const typet &) const
Definition: namespace.cpp:55
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
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:1411
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:278
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool simplify(exprt &expr, const namespacet &ns)