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/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
20 #include <util/simplify_expr.h>
21 
22 mp_integer alignment(const typet &type, const namespacet &ns)
23 {
24  // we need to consider a number of different cases:
25  // - alignment specified in the source, which will be recorded in
26  // ID_C_alignment
27  // - alignment induced by packing ("The alignment of a member will
28  // be on a boundary that is either a multiple of n or a multiple of
29  // the size of the member, whichever is smaller."); both
30  // ID_C_alignment and ID_C_packed will be set
31  // - natural alignment, when neither ID_C_alignment nor ID_C_packed
32  // are set
33  // - dense packing with only ID_C_packed set.
34 
35  // is the alignment given?
36  const exprt &given_alignment=
37  static_cast<const exprt &>(type.find(ID_C_alignment));
38 
39  mp_integer a_int = 0;
40 
41  // we trust it blindly, no matter how nonsensical
42  if(given_alignment.is_not_nil())
43  {
44  const auto a = numeric_cast<mp_integer>(given_alignment);
45  if(a.has_value())
46  a_int = *a;
47  }
48 
49  // alignment but no packing
50  if(a_int>0 && !type.get_bool(ID_C_packed))
51  return a_int;
52  // no alignment, packing
53  else if(a_int==0 && type.get_bool(ID_C_packed))
54  return 1;
55 
56  // compute default
57  mp_integer result;
58 
59  if(type.id()==ID_array)
60  result=alignment(type.subtype(), ns);
61  else if(type.id()==ID_struct || type.id()==ID_union)
62  {
63  result=1;
64 
65  // get the max
66  // (should really be the smallest common denominator)
67  for(const auto &c : to_struct_union_type(type).components())
68  result = std::max(result, alignment(c.type(), ns));
69  }
70  else if(type.id()==ID_unsignedbv ||
71  type.id()==ID_signedbv ||
72  type.id()==ID_fixedbv ||
73  type.id()==ID_floatbv ||
74  type.id()==ID_c_bool ||
75  type.id()==ID_pointer)
76  {
77  result = *pointer_offset_size(type, ns);
78  }
79  else if(type.id()==ID_c_enum)
80  result=alignment(type.subtype(), ns);
81  else if(type.id()==ID_c_enum_tag)
82  result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns);
83  else if(type.id() == ID_struct_tag)
84  result = alignment(ns.follow_tag(to_struct_tag_type(type)), ns);
85  else if(type.id() == ID_union_tag)
86  result = alignment(ns.follow_tag(to_union_tag_type(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 auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
125 
126  if(!c_enum_type.is_incomplete())
127  return to_bitvector_type(c_enum_type.subtype()).get_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 
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 
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 if(
195  it->type().id() == ID_bool && underlying_bits == config.ansi_c.char_width)
196  {
197  ++bit_field_bits;
198  }
199  else
200  {
201  // pad up any remaining bit field
202  if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
203  {
204  const std::size_t pad_bits =
205  underlying_bits - (bit_field_bits % underlying_bits);
206  it = pad_bit_field(components, it, pad_bits);
207  offset += (bit_field_bits + pad_bits) / config.ansi_c.char_width;
208  underlying_bits = bit_field_bits = 0;
209  }
210  else
211  {
212  offset += bit_field_bits / config.ansi_c.char_width;
213  underlying_bits = bit_field_bits = 0;
214  }
215 
216  // pad up to underlying type unless the struct is packed
217  if(!is_packed)
218  {
219  const mp_integer a = alignment(it->type(), ns);
220  if(a > 1)
221  {
222  const mp_integer displacement = offset % a;
223 
224  if(displacement != 0)
225  {
226  const mp_integer pad_bytes = a - displacement;
227  std::size_t pad_bits =
228  numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
229  it = pad(components, it, pad_bits);
230  offset += pad_bytes;
231  }
232  }
233  }
234 
235  // do we start a new bit field?
236  if(it->type().id() == ID_c_bit_field)
237  {
238  underlying_bits =
239  underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0);
240  const auto width = to_c_bit_field_type(it->type()).get_width();
241  bit_field_bits += width;
242  }
243  else if(it->type().id() == ID_bool)
244  {
245  underlying_bits = config.ansi_c.char_width;
246  ++bit_field_bits;
247  }
248  else
249  {
250  // keep track of offset
251  const auto size = pointer_offset_size(it->type(), ns);
252  if(size.has_value() && *size >= 1)
253  offset += *size;
254  }
255  }
256  }
257 
258  // Add padding at the end?
259  // Bit-field
260  if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
261  {
262  const std::size_t pad =
263  underlying_bits - (bit_field_bits % underlying_bits);
264  pad_bit_field(components, components.end(), pad);
265  offset += (bit_field_bits + pad) / config.ansi_c.char_width;
266  }
267  else
268  offset += bit_field_bits / config.ansi_c.char_width;
269 
270  // alignment of the struct
271  // Note that this is done even if the struct is packed.
272  const mp_integer a = alignment(type, ns);
273  const mp_integer displacement = offset % a;
274 
275  if(displacement != 0)
276  {
277  const mp_integer pad_bytes = a - displacement;
278  const std::size_t pad_bits =
279  numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
280  pad(components, components.end(), pad_bits);
281  offset += pad_bytes;
282  }
283 }
284 
285 static void add_padding_gcc(struct_typet &type, const namespacet &ns)
286 {
287  struct_typet::componentst &components = type.components();
288 
289  // First make bit-fields appear on byte boundaries
290  {
291  std::size_t bit_field_bits=0;
292 
293  for(struct_typet::componentst::iterator
294  it=components.begin();
295  it!=components.end();
296  it++)
297  {
298  if(it->type().id()==ID_c_bit_field &&
299  to_c_bit_field_type(it->type()).get_width()!=0)
300  {
301  // count the bits
302  const std::size_t width = to_c_bit_field_type(it->type()).get_width();
303  bit_field_bits+=width;
304  }
305  else if(it->type().id() == ID_bool)
306  {
307  ++bit_field_bits;
308  }
309  else if(bit_field_bits!=0)
310  {
311  // not on a byte-boundary?
312  if((bit_field_bits % config.ansi_c.char_width) != 0)
313  {
314  const std::size_t pad = config.ansi_c.char_width -
315  bit_field_bits % config.ansi_c.char_width;
316  it = pad_bit_field(components, it, pad);
317  }
318 
319  bit_field_bits=0;
320  }
321  }
322 
323  // Add padding at the end?
324  if((bit_field_bits % config.ansi_c.char_width) != 0)
325  {
326  const std::size_t pad =
327  config.ansi_c.char_width - bit_field_bits % config.ansi_c.char_width;
328  pad_bit_field(components, components.end(), pad);
329  }
330  }
331 
332  // Is the struct packed, without any alignment specification?
333  if(type.get_bool(ID_C_packed) &&
334  type.find(ID_C_alignment).is_nil())
335  return; // done
336 
337  mp_integer offset=0;
338  mp_integer max_alignment=0;
339  std::size_t bit_field_bits=0;
340 
341  for(struct_typet::componentst::iterator
342  it=components.begin();
343  it!=components.end();
344  it++)
345  {
346  const typet it_type=it->type();
347  mp_integer a=1;
348 
349  const bool packed=it_type.get_bool(ID_C_packed) ||
350  ns.follow(it_type).get_bool(ID_C_packed);
351 
352  if(it_type.id()==ID_c_bit_field)
353  {
354  a=alignment(to_c_bit_field_type(it_type).subtype(), ns);
355 
356  // A zero-width bit-field causes alignment to the base-type.
357  if(to_c_bit_field_type(it_type).get_width()==0)
358  {
359  }
360  else
361  {
362  // Otherwise, ANSI-C says that bit-fields do not get padded!
363  // We consider the type for max_alignment, however.
364  if(max_alignment<a)
365  max_alignment=a;
366 
367  std::size_t w=to_c_bit_field_type(it_type).get_width();
368  bit_field_bits += w;
369  const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
370  bit_field_bits %= config.ansi_c.char_width;
371  offset+=bytes;
372  continue;
373  }
374  }
375  else if(it_type.id() == ID_bool)
376  {
377  a = alignment(it_type, ns);
378  if(max_alignment < a)
379  max_alignment = a;
380 
381  ++bit_field_bits;
382  const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
383  bit_field_bits %= config.ansi_c.char_width;
384  offset += bytes;
385  continue;
386  }
387  else
388  a=alignment(it_type, ns);
389 
391  bit_field_bits == 0, "padding ensures offset at byte boundaries");
392 
393  // check minimum alignment
394  if(a<config.ansi_c.alignment && !packed)
396 
397  if(max_alignment<a)
398  max_alignment=a;
399 
400  if(a!=1)
401  {
402  // we may need to align it
403  const mp_integer displacement = offset % a;
404 
405  if(displacement!=0)
406  {
407  const mp_integer pad_bytes = a - displacement;
408  const std::size_t pad_bits =
409  numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
410  it = pad(components, it, pad_bits);
411  offset += pad_bytes;
412  }
413  }
414 
415  auto size = pointer_offset_size(it_type, ns);
416 
417  if(size.has_value())
418  offset += *size;
419  }
420 
421  // any explicit alignment for the struct?
422  const exprt &alignment =
423  static_cast<const exprt &>(type.find(ID_C_alignment));
424  if(alignment.is_not_nil())
425  {
426  if(alignment.id()!=ID_default)
427  {
428  const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));
429 
430  if(tmp_i.has_value() && *tmp_i > max_alignment)
431  max_alignment = *tmp_i;
432  }
433  }
434  // Is the struct packed, without any alignment specification?
435  else if(type.get_bool(ID_C_packed))
436  return; // done
437 
438  // There may be a need for 'end of struct' padding.
439  // We use 'max_alignment'.
440 
441  if(max_alignment>1)
442  {
443  // we may need to align it
444  mp_integer displacement=offset%max_alignment;
445 
446  if(displacement!=0)
447  {
448  mp_integer pad_bytes = max_alignment - displacement;
449  std::size_t pad_bits =
450  numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
451  pad(components, components.end(), pad_bits);
452  }
453  }
454 }
455 
456 void add_padding(struct_typet &type, const namespacet &ns)
457 {
458  // padding depends greatly on compiler
460  add_padding_msvc(type, ns);
461  else
462  add_padding_gcc(type, ns);
463 }
464 
465 void add_padding(union_typet &type, const namespacet &ns)
466 {
467  mp_integer max_alignment_bits =
468  alignment(type, ns) * config.ansi_c.char_width;
469  mp_integer size_bits=0;
470 
471  // check per component, and ignore those without fixed size
472  for(const auto &c : type.components())
473  {
474  auto s = pointer_offset_bits(c.type(), ns);
475  if(s.has_value())
476  size_bits = std::max(size_bits, *s);
477  }
478 
479  // Is the union packed?
480  if(type.get_bool(ID_C_packed))
481  {
482  // The size needs to be a multiple of 1 char only.
483  max_alignment_bits = config.ansi_c.char_width;
484  }
485 
487  {
488  // Visual Studio pads up to the underlying width of
489  // any bit field.
490  for(const auto &c : type.components())
491  if(c.type().id() == ID_c_bit_field)
492  {
493  auto w = underlying_width(to_c_bit_field_type(c.type()), ns);
494  if(w.has_value() && w.value() > max_alignment_bits)
495  max_alignment_bits = w.value();
496  }
497  }
498 
499  // The size must be a multiple of the alignment, or
500  // we add a padding member to the union.
501 
502  if(size_bits%max_alignment_bits!=0)
503  {
504  mp_integer padding_bits=
505  max_alignment_bits-(size_bits%max_alignment_bits);
506 
507  unsignedbv_typet padding_type(
508  numeric_cast_v<std::size_t>(size_bits + padding_bits));
509 
511  component.type()=padding_type;
512  component.set_name("$pad");
513  component.set_is_padding(true);
514 
515  type.components().push_back(component);
516  }
517 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
pointer_offset_size.h
Pointer Logic.
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:208
typet
The type of an expression, extends irept.
Definition: type.h:28
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:112
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:168
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:150
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
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
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:114
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:391
add_padding
void add_padding(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:456
underlying_width
static optionalt< std::size_t > underlying_width(const c_bit_field_typet &type, const namespacet &ns)
Definition: padding.cpp:104
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: c_types.h:19
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: c_types.h:317
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
pad
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition: padding.cpp:152
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
alignment
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:22
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:468
union_typet
The union type.
Definition: c_types.h:112
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:285
config
configt config
Definition: config.cpp:24
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
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:135
struct_union_typet::componentt
Definition: std_types.h:63
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: c_types.h:47
configt::ansi_ct::mode
flavourt mode
Definition: config.h:196
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
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:52
config.h
c_types.h
padding.h
ANSI-C Language Type Checking.