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