cprover
padding.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: 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
23mp_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(to_array_type(type).element_type(), 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(to_c_enum_type(type).underlying_type(), 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(to_c_bit_field_type(type).underlying_type(), 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 &underlying_type = type.underlying_type();
108
109 if(underlying_type.id() == ID_bool)
110 {
111 // This is the 'proper' bool.
112 return 1;
113 }
114 else if(
115 underlying_type.id() == ID_signedbv ||
116 underlying_type.id() == ID_unsignedbv || underlying_type.id() == ID_c_bool)
117 {
118 return to_bitvector_type(underlying_type).get_width();
119 }
120 else if(underlying_type.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 =
126 ns.follow_tag(to_c_enum_tag_type(underlying_type));
127
128 if(!c_enum_type.is_incomplete())
129 return to_bitvector_type(c_enum_type.underlying_type()).get_width();
130 else
131 return {};
132 }
133 else
134 return {};
135}
136
137static struct_typet::componentst::iterator pad_bit_field(
138 struct_typet::componentst &components,
139 struct_typet::componentst::iterator where,
140 std::size_t pad_bits)
141{
142 const c_bit_field_typet padding_type(
143 unsignedbv_typet(pad_bits), pad_bits);
144
146 "$bit_field_pad" + std::to_string(where - components.begin()),
147 padding_type);
148
149 component.set_is_padding(true);
150
151 return std::next(components.insert(where, component));
152}
153
154static struct_typet::componentst::iterator pad(
155 struct_typet::componentst &components,
156 struct_typet::componentst::iterator where,
157 std::size_t pad_bits)
158{
159 const unsignedbv_typet padding_type(pad_bits);
160
162 "$pad" + std::to_string(where - components.begin()),
163 padding_type);
164
165 component.set_is_padding(true);
166
167 return std::next(components.insert(where, component));
168}
169
170static void add_padding_msvc(struct_typet &type, const namespacet &ns)
171{
172 struct_typet::componentst &components=type.components();
173
174 std::size_t bit_field_bits = 0, underlying_bits = 0;
175 mp_integer offset = 0;
176
177 bool is_packed = type.get_bool(ID_C_packed);
178
179 for(struct_typet::componentst::iterator it = components.begin();
180 it != components.end();
181 it++)
182 {
183 // there is exactly one case in which padding is not added:
184 // if we continue a bit-field with size>0 and the same underlying width
185
186 if(
187 it->type().id() == ID_c_bit_field &&
188 to_c_bit_field_type(it->type()).get_width() != 0 &&
189 underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0) ==
190 underlying_bits)
191 {
192 // do not add padding, but count the bits
193 const auto width = to_c_bit_field_type(it->type()).get_width();
194 bit_field_bits += width;
195 }
196 else if(
197 it->type().id() == ID_bool && underlying_bits == config.ansi_c.char_width)
198 {
199 ++bit_field_bits;
200 }
201 else
202 {
203 // pad up any remaining bit field
204 if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
205 {
206 const std::size_t pad_bits =
207 underlying_bits - (bit_field_bits % underlying_bits);
208 it = pad_bit_field(components, it, pad_bits);
209 offset += (bit_field_bits + pad_bits) / config.ansi_c.char_width;
210 underlying_bits = bit_field_bits = 0;
211 }
212 else
213 {
214 offset += bit_field_bits / config.ansi_c.char_width;
215 underlying_bits = bit_field_bits = 0;
216 }
217
218 // pad up to underlying type unless the struct is packed
219 if(!is_packed)
220 {
221 const mp_integer a = alignment(it->type(), ns);
222 if(a > 1)
223 {
224 const mp_integer displacement = offset % a;
225
226 if(displacement != 0)
227 {
228 const mp_integer pad_bytes = a - displacement;
229 std::size_t pad_bits =
230 numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
231 it = pad(components, it, pad_bits);
232 offset += pad_bytes;
233 }
234 }
235 }
236
237 // do we start a new bit field?
238 if(it->type().id() == ID_c_bit_field)
239 {
240 underlying_bits =
241 underlying_width(to_c_bit_field_type(it->type()), ns).value_or(0);
242 const auto width = to_c_bit_field_type(it->type()).get_width();
243 bit_field_bits += width;
244 }
245 else if(it->type().id() == ID_bool)
246 {
247 underlying_bits = config.ansi_c.char_width;
248 ++bit_field_bits;
249 }
250 else
251 {
252 // keep track of offset
253 const auto size = pointer_offset_size(it->type(), ns);
254 if(size.has_value() && *size >= 1)
255 offset += *size;
256 }
257 }
258 }
259
260 // Add padding at the end?
261 // Bit-field
262 if(underlying_bits != 0 && (bit_field_bits % underlying_bits) != 0)
263 {
264 const std::size_t pad =
265 underlying_bits - (bit_field_bits % underlying_bits);
266 pad_bit_field(components, components.end(), pad);
267 offset += (bit_field_bits + pad) / config.ansi_c.char_width;
268 }
269 else
270 offset += bit_field_bits / config.ansi_c.char_width;
271
272 // alignment of the struct
273 // Note that this is done even if the struct is packed.
274 const mp_integer a = alignment(type, ns);
275 const mp_integer displacement = offset % a;
276
277 if(displacement != 0)
278 {
279 const mp_integer pad_bytes = a - displacement;
280 const std::size_t pad_bits =
281 numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
282 pad(components, components.end(), pad_bits);
283 offset += pad_bytes;
284 }
285}
286
287static void add_padding_gcc(struct_typet &type, const namespacet &ns)
288{
289 struct_typet::componentst &components = type.components();
290
291 // First make bit-fields appear on byte boundaries
292 {
293 std::size_t bit_field_bits=0;
294
295 for(struct_typet::componentst::iterator
296 it=components.begin();
297 it!=components.end();
298 it++)
299 {
300 if(it->type().id()==ID_c_bit_field &&
301 to_c_bit_field_type(it->type()).get_width()!=0)
302 {
303 // count the bits
304 const std::size_t width = to_c_bit_field_type(it->type()).get_width();
305 bit_field_bits+=width;
306 }
307 else if(it->type().id() == ID_bool)
308 {
309 ++bit_field_bits;
310 }
311 else if(bit_field_bits!=0)
312 {
313 // not on a byte-boundary?
314 if((bit_field_bits % config.ansi_c.char_width) != 0)
315 {
316 const std::size_t pad = config.ansi_c.char_width -
317 bit_field_bits % config.ansi_c.char_width;
318 it = pad_bit_field(components, it, pad);
319 }
320
321 bit_field_bits=0;
322 }
323 }
324
325 // Add padding at the end?
326 if((bit_field_bits % config.ansi_c.char_width) != 0)
327 {
328 const std::size_t pad =
329 config.ansi_c.char_width - bit_field_bits % config.ansi_c.char_width;
330 pad_bit_field(components, components.end(), pad);
331 }
332 }
333
334 // Is the struct packed, without any alignment specification?
335 if(type.get_bool(ID_C_packed) &&
336 type.find(ID_C_alignment).is_nil())
337 return; // done
338
339 mp_integer offset=0;
340 mp_integer max_alignment=0;
341 std::size_t bit_field_bits=0;
342
343 for(struct_typet::componentst::iterator
344 it=components.begin();
345 it!=components.end();
346 it++)
347 {
348 const typet it_type=it->type();
349 mp_integer a=1;
350
351 const bool packed=it_type.get_bool(ID_C_packed) ||
352 ns.follow(it_type).get_bool(ID_C_packed);
353
354 if(it_type.id()==ID_c_bit_field)
355 {
356 a = alignment(to_c_bit_field_type(it_type).underlying_type(), ns);
357
358 // A zero-width bit-field causes alignment to the base-type.
359 if(to_c_bit_field_type(it_type).get_width()==0)
360 {
361 }
362 else
363 {
364 // Otherwise, ANSI-C says that bit-fields do not get padded!
365 // We consider the type for max_alignment, however.
366 if(max_alignment<a)
367 max_alignment=a;
368
369 std::size_t w=to_c_bit_field_type(it_type).get_width();
370 bit_field_bits += w;
371 const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
372 bit_field_bits %= config.ansi_c.char_width;
373 offset+=bytes;
374 continue;
375 }
376 }
377 else if(it_type.id() == ID_bool)
378 {
379 a = alignment(it_type, ns);
380 if(max_alignment < a)
381 max_alignment = a;
382
383 ++bit_field_bits;
384 const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
385 bit_field_bits %= config.ansi_c.char_width;
386 offset += bytes;
387 continue;
388 }
389 else
390 a=alignment(it_type, ns);
391
393 bit_field_bits == 0, "padding ensures offset at byte boundaries");
394
395 // check minimum alignment
396 if(a<config.ansi_c.alignment && !packed)
398
399 if(max_alignment<a)
400 max_alignment=a;
401
402 if(a!=1)
403 {
404 // we may need to align it
405 const mp_integer displacement = offset % a;
406
407 if(displacement!=0)
408 {
409 const mp_integer pad_bytes = a - displacement;
410 const std::size_t pad_bits =
411 numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
412 it = pad(components, it, pad_bits);
413 offset += pad_bytes;
414 }
415 }
416
417 auto size = pointer_offset_size(it_type, ns);
418
419 if(size.has_value())
420 offset += *size;
421 }
422
423 // any explicit alignment for the struct?
424 const exprt &alignment =
425 static_cast<const exprt &>(type.find(ID_C_alignment));
426 if(alignment.is_not_nil())
427 {
428 if(alignment.id()!=ID_default)
429 {
430 const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));
431
432 if(tmp_i.has_value() && *tmp_i > max_alignment)
433 max_alignment = *tmp_i;
434 }
435 }
436 // Is the struct packed, without any alignment specification?
437 else if(type.get_bool(ID_C_packed))
438 return; // done
439
440 // There may be a need for 'end of struct' padding.
441 // We use 'max_alignment'.
442
443 if(max_alignment>1)
444 {
445 // we may need to align it
446 mp_integer displacement=offset%max_alignment;
447
448 if(displacement!=0)
449 {
450 mp_integer pad_bytes = max_alignment - displacement;
451 std::size_t pad_bits =
452 numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
453 pad(components, components.end(), pad_bits);
454 }
455 }
456}
457
458void add_padding(struct_typet &type, const namespacet &ns)
459{
460 // padding depends greatly on compiler
462 add_padding_msvc(type, ns);
463 else
464 add_padding_gcc(type, ns);
465}
466
467void add_padding(union_typet &type, const namespacet &ns)
468{
469 mp_integer max_alignment_bits =
470 alignment(type, ns) * config.ansi_c.char_width;
471 mp_integer size_bits=0;
472
473 // check per component, and ignore those without fixed size
474 for(const auto &c : type.components())
475 {
476 auto s = pointer_offset_bits(c.type(), ns);
477 if(s.has_value())
478 size_bits = std::max(size_bits, *s);
479 }
480
481 // Is the union packed?
482 if(type.get_bool(ID_C_packed))
483 {
484 // The size needs to be a multiple of 1 char only.
485 max_alignment_bits = config.ansi_c.char_width;
486 }
487
489 {
490 // Visual Studio pads up to the underlying width of
491 // any bit field.
492 for(const auto &c : type.components())
493 if(c.type().id() == ID_c_bit_field)
494 {
495 auto w = underlying_width(to_c_bit_field_type(c.type()), ns);
496 if(w.has_value() && w.value() > max_alignment_bits)
497 max_alignment_bits = w.value();
498 }
499 }
500
501 // The size must be a multiple of the alignment, or
502 // we add a padding member to the union.
503
504 if(size_bits%max_alignment_bits!=0)
505 {
506 mp_integer padding_bits=
507 max_alignment_bits-(size_bits%max_alignment_bits);
508
509 unsignedbv_typet padding_type(
510 numeric_cast_v<std::size_t>(size_bits + padding_bits));
511
513 component.type()=padding_type;
514 component.set_name("$pad");
515 component.set_is_padding(true);
516
517 type.components().push_back(component);
518 }
519}
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
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:344
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
std::size_t get_width() const
Definition: std_types.h:864
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: c_types.h:20
const typet & underlying_type() const
Definition: c_types.h:30
struct configt::ansi_ct ansi_c
Base class for all expressions.
Definition: expr.h:54
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
The type of an expression, extends irept.
Definition: type.h:29
The union type.
Definition: c_types.h:125
Fixed-width bit-vector with unsigned binary interpretation.
configt config
Definition: config.cpp:25
nonstd::optional< T > optionalt
Definition: optional.h:35
static optionalt< std::size_t > underlying_width(const c_bit_field_typet &type, const namespacet &ns)
Definition: padding.cpp:105
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:23
static void add_padding_msvc(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:170
static void add_padding_gcc(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:287
void add_padding(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:458
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition: padding.cpp:154
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:137
ANSI-C Language Type Checking.
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.
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t alignment
Definition: config.h:165
std::size_t char_width
Definition: config.h:112
flavourt mode
Definition: config.h:222