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 auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
124 
125  if(!c_enum_type.is_incomplete())
126  return to_bitvector_type(c_enum_type.subtype()).get_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 if(
194  it->type().id() == ID_bool && underlying_bits == config.ansi_c.char_width)
195  {
196  ++bit_field_bits;
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  else
210  {
211  offset += bit_field_bits / config.ansi_c.char_width;
212  underlying_bits = bit_field_bits = 0;
213  }
214 
215  // pad up to underlying type unless the struct is packed
216  if(!is_packed)
217  {
218  const mp_integer a = alignment(it->type(), ns);
219  if(a > 1)
220  {
221  const mp_integer displacement = offset % a;
222 
223  if(displacement != 0)
224  {
225  const mp_integer pad_bytes = a - displacement;
226  std::size_t pad_bits =
227  numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
228  it = pad(components, it, pad_bits);
229  offset += pad_bytes;
230  }
231  }
232  }
233 
234  // do we start a new bit field?
235  if(it->type().id() == ID_c_bit_field)
236  {
237  underlying_bits =
238  underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0);
239  const auto width = to_c_bit_field_type(it->type()).get_width();
240  bit_field_bits += width;
241  }
242  else if(it->type().id() == ID_bool)
243  {
244  underlying_bits = config.ansi_c.char_width;
245  ++bit_field_bits;
246  }
247  else
248  {
249  // keep track of offset
250  const auto size = pointer_offset_size(it->type(), ns);
251  if(size.has_value() && *size >= 1)
252  offset += *size;
253  }
254  }
255  }
256 
257  // Add padding at the end?
258  // Bit-field
259  if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
260  {
261  const std::size_t pad =
262  underlying_bits - (bit_field_bits % underlying_bits);
263  pad_bit_field(components, components.end(), pad);
264  offset += (bit_field_bits + pad) / config.ansi_c.char_width;
265  }
266  else
267  offset += bit_field_bits / config.ansi_c.char_width;
268 
269  // alignment of the struct
270  // Note that this is done even if the struct is packed.
271  const mp_integer a = alignment(type, ns);
272  const mp_integer displacement = offset % a;
273 
274  if(displacement != 0)
275  {
276  const mp_integer pad_bytes = a - displacement;
277  const std::size_t pad_bits =
278  numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
279  pad(components, components.end(), pad_bits);
280  offset += pad_bytes;
281  }
282 }
283 
284 static void add_padding_gcc(struct_typet &type, const namespacet &ns)
285 {
286  struct_typet::componentst &components = type.components();
287 
288  // First make bit-fields appear on byte boundaries
289  {
290  std::size_t bit_field_bits=0;
291 
292  for(struct_typet::componentst::iterator
293  it=components.begin();
294  it!=components.end();
295  it++)
296  {
297  if(it->type().id()==ID_c_bit_field &&
298  to_c_bit_field_type(it->type()).get_width()!=0)
299  {
300  // count the bits
301  const std::size_t width = to_c_bit_field_type(it->type()).get_width();
302  bit_field_bits+=width;
303  }
304  else if(it->type().id() == ID_bool)
305  {
306  ++bit_field_bits;
307  }
308  else if(bit_field_bits!=0)
309  {
310  // not on a byte-boundary?
311  if((bit_field_bits % config.ansi_c.char_width) != 0)
312  {
313  const std::size_t pad = config.ansi_c.char_width -
314  bit_field_bits % config.ansi_c.char_width;
315  it = pad_bit_field(components, it, pad);
316  }
317 
318  bit_field_bits=0;
319  }
320  }
321 
322  // Add padding at the end?
323  if((bit_field_bits % config.ansi_c.char_width) != 0)
324  {
325  const std::size_t pad =
326  config.ansi_c.char_width - bit_field_bits % config.ansi_c.char_width;
327  pad_bit_field(components, components.end(), pad);
328  }
329  }
330 
331  // Is the struct packed, without any alignment specification?
332  if(type.get_bool(ID_C_packed) &&
333  type.find(ID_C_alignment).is_nil())
334  return; // done
335 
336  mp_integer offset=0;
337  mp_integer max_alignment=0;
338  std::size_t bit_field_bits=0;
339 
340  for(struct_typet::componentst::iterator
341  it=components.begin();
342  it!=components.end();
343  it++)
344  {
345  const typet it_type=it->type();
346  mp_integer a=1;
347 
348  const bool packed=it_type.get_bool(ID_C_packed) ||
349  ns.follow(it_type).get_bool(ID_C_packed);
350 
351  if(it_type.id()==ID_c_bit_field)
352  {
353  a=alignment(to_c_bit_field_type(it_type).subtype(), ns);
354 
355  // A zero-width bit-field causes alignment to the base-type.
356  if(to_c_bit_field_type(it_type).get_width()==0)
357  {
358  }
359  else
360  {
361  // Otherwise, ANSI-C says that bit-fields do not get padded!
362  // We consider the type for max_alignment, however.
363  if(max_alignment<a)
364  max_alignment=a;
365 
366  std::size_t w=to_c_bit_field_type(it_type).get_width();
367  bit_field_bits += w;
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  }
374  else if(it_type.id() == ID_bool)
375  {
376  a = alignment(it_type, ns);
377  if(max_alignment < a)
378  max_alignment = a;
379 
380  ++bit_field_bits;
381  const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
382  bit_field_bits %= config.ansi_c.char_width;
383  offset += bytes;
384  continue;
385  }
386  else
387  a=alignment(it_type, ns);
388 
390  bit_field_bits == 0, "padding ensures offset at byte boundaries");
391 
392  // check minimum alignment
393  if(a<config.ansi_c.alignment && !packed)
395 
396  if(max_alignment<a)
397  max_alignment=a;
398 
399  if(a!=1)
400  {
401  // we may need to align it
402  const mp_integer displacement = offset % a;
403 
404  if(displacement!=0)
405  {
406  const mp_integer pad_bytes = a - displacement;
407  const std::size_t pad_bits =
408  numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
409  it = pad(components, it, pad_bits);
410  offset += pad_bytes;
411  }
412  }
413 
414  auto size = pointer_offset_size(it_type, ns);
415 
416  if(size.has_value())
417  offset += *size;
418  }
419 
420  // any explicit alignment for the struct?
421  const exprt &alignment =
422  static_cast<const exprt &>(type.find(ID_C_alignment));
423  if(alignment.is_not_nil())
424  {
425  if(alignment.id()!=ID_default)
426  {
427  const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));
428 
429  if(tmp_i.has_value() && *tmp_i > max_alignment)
430  max_alignment = *tmp_i;
431  }
432  }
433  // Is the struct packed, without any alignment specification?
434  else if(type.get_bool(ID_C_packed))
435  return; // done
436 
437  // There may be a need for 'end of struct' padding.
438  // We use 'max_alignment'.
439 
440  if(max_alignment>1)
441  {
442  // we may need to align it
443  mp_integer displacement=offset%max_alignment;
444 
445  if(displacement!=0)
446  {
447  mp_integer pad_bytes = max_alignment - displacement;
448  std::size_t pad_bits =
449  numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
450  pad(components, components.end(), pad_bits);
451  }
452  }
453 }
454 
455 void add_padding(struct_typet &type, const namespacet &ns)
456 {
457  // padding depends greatly on compiler
459  add_padding_msvc(type, ns);
460  else
461  add_padding_gcc(type, ns);
462 }
463 
464 void add_padding(union_typet &type, const namespacet &ns)
465 {
466  mp_integer max_alignment_bits =
467  alignment(type, ns) * config.ansi_c.char_width;
468  mp_integer size_bits=0;
469 
470  // check per component, and ignore those without fixed size
471  for(const auto &c : type.components())
472  {
473  auto s = pointer_offset_bits(c.type(), ns);
474  if(s.has_value())
475  size_bits = std::max(size_bits, *s);
476  }
477 
478  // Is the union packed?
479  if(type.get_bool(ID_C_packed))
480  {
481  // The size needs to be a multiple of 1 char only.
482  max_alignment_bits = config.ansi_c.char_width;
483  }
484 
486  {
487  // Visual Studio pads up to the underlying width of
488  // any bit field.
489  for(const auto &c : type.components())
490  if(c.type().id() == ID_c_bit_field)
491  {
492  auto w = underlying_width(to_c_bit_field_type(c.type()), ns);
493  if(w.has_value() && w.value() > max_alignment_bits)
494  max_alignment_bits = w.value();
495  }
496  }
497 
498  // The size must be a multiple of the alignment, or
499  // we add a padding member to the union.
500 
501  if(size_bits%max_alignment_bits!=0)
502  {
503  mp_integer padding_bits=
504  max_alignment_bits-(size_bits%max_alignment_bits);
505 
506  unsignedbv_typet padding_type(
507  numeric_cast_v<std::size_t>(size_bits + padding_bits));
508 
510  component.type()=padding_type;
511  component.set_name("$pad");
512  component.set_is_padding(true);
513 
514  type.components().push_back(component);
515  }
516 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
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:555
pointer_offset_size.h
Pointer Logic.
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:721
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
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:209
typet
The type of an expression, extends irept.
Definition: type.h:29
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
exprt
Base class for all expressions.
Definition: expr.h:53
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:135
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:70
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
configt::ansi_c
struct configt::ansi_ct ansi_c
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1216
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:34
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
add_padding
void add_padding(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:455
underlying_width
static optionalt< std::size_t > underlying_width(const c_bit_field_typet &type, const namespacet &ns)
Definition: padding.cpp:103
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:511
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:1443
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
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:1471
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
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
alignment
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:515
union_typet
The union type.
Definition: std_types.h:393
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:284
config
configt config
Definition: config.cpp:24
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
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:64
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
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:89
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
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:1089
padding.h
ANSI-C Language Type Checking.