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