CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/padding.cpp Source File

CBMC
Loading...
Searching...
No Matches
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>
20#include <util/pointer_offset_size.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?
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 {
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
104static std::optional<std::size_t>
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
137 static 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{
144
146 "$bit_field_pad" + std::to_string(where - components.begin()),
148
149 component.set_is_padding(true);
150
151 return std::next(components.insert(where, component));
152}
153
154 static struct_typet::componentst::iterator pad(
155 struct_typet::componentst &components,
156 struct_typet::componentst::iterator where,
157 std::size_t pad_bits)
158{
160
162 "$pad" + std::to_string(where - components.begin()),
164
165 component.set_is_padding(true);
166
167 return std::next(components.insert(where, component));
168}
169
170 static 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) ==
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(it->is_boolean() && underlying_bits == config.ansi_c.char_width)
197 {
199 }
200 else
201 {
202 // pad up any remaining bit field
204 {
205 const std::size_t pad_bits =
207 it = pad_bit_field(components, it, pad_bits);
208 offset += (bit_field_bits + pad_bits) / config.ansi_c.char_width;
210 }
211 else
212 {
213 offset += bit_field_bits / config.ansi_c.char_width;
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 {
228 std::size_t pad_bits =
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 {
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->is_boolean())
245 {
246 underlying_bits = config.ansi_c.char_width;
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
262 {
263 const std::size_t pad =
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 {
279 const std::size_t pad_bits =
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->is_boolean())
307 {
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
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 mp_integer offset=0;
335 std::size_t bit_field_bits=0;
336 const bool struct_is_packed = type.get_bool(ID_C_packed);
337
338 for(struct_typet::componentst::iterator
339 it=components.begin();
340 it!=components.end();
341 it++)
342 {
343 const typet it_type=it->type();
344 mp_integer a=1;
345
346 if(it_type.id()==ID_c_bit_field)
347 {
348 a = alignment(to_c_bit_field_type(it_type).underlying_type(), ns);
349
350 // A zero-width bit-field causes alignment to the base-type.
351 if(to_c_bit_field_type(it_type).get_width()==0)
352 {
353 }
354 else
355 {
356 // Otherwise, ANSI-C says that bit-fields do not get padded!
357 // We consider the type for max_alignment, however.
358 if(max_alignment<a)
360
361 std::size_t w=to_c_bit_field_type(it_type).get_width();
362 bit_field_bits += w;
363 const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
364 bit_field_bits %= config.ansi_c.char_width;
365 offset+=bytes;
366 continue;
367 }
368 }
369 else if(it_type.id() == ID_bool)
370 {
371 a = alignment(it_type, ns);
372 if(max_alignment < a)
374
376 const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
377 bit_field_bits %= config.ansi_c.char_width;
378 offset += bytes;
379 continue;
380 }
381 else
382 a=alignment(it_type, ns);
383
385 bit_field_bits == 0, "padding ensures offset at byte boundaries");
386
387 // check minimum alignment
388 if(
389 a < config.ansi_c.alignment && !it_type.get_bool(ID_C_packed) &&
390 (it_type.id() != ID_struct_tag ||
392 (it_type.id() != ID_union_tag ||
394 {
395 a=config.ansi_c.alignment;
396 }
397
398 if(max_alignment<a)
400
401 if(
402 a != 1 &&
403 (!struct_is_packed || it_type.find(ID_C_alignment).is_not_nil()))
404 {
405 // we may need to align it
406 const mp_integer displacement = offset % a;
407
408 if(displacement!=0)
409 {
411 const std::size_t pad_bits =
413 it = pad(components, it, pad_bits);
414 offset += pad_bytes;
415 }
416 }
417
418 auto size = pointer_offset_size(it_type, ns);
419
420 if(size.has_value())
421 offset += *size;
422 }
423
424 // any explicit alignment for the struct?
425 const exprt &alignment =
426 static_cast<const exprt &>(type.find(ID_C_alignment));
427 if(alignment.is_not_nil())
428 {
429 if(alignment.id()!=ID_default)
430 {
432
433 if(tmp_i.has_value() && *tmp_i > max_alignment)
435 }
436 }
437 // Is the struct packed, without any alignment specification?
438 else if(struct_is_packed)
439 return; // done
440
441 // There may be a need for 'end of struct' padding.
442 // We use 'max_alignment'.
443
444 if(max_alignment>1)
445 {
446 // we may need to align it
448
449 if(displacement!=0)
450 {
452 std::size_t pad_bits =
454 pad(components, components.end(), pad_bits);
455 }
456 }
457}
458
459 void add_padding(struct_typet &type, const namespacet &ns)
460{
461 // padding depends greatly on compiler
463 add_padding_msvc(type, ns);
464 else
465 add_padding_gcc(type, ns);
466}
467
468 void add_padding(union_typet &type, const namespacet &ns)
469{
471 alignment(type, ns) * config.ansi_c.char_width;
473
474 // check per component, and ignore those without fixed size
475 for(const auto &c : type.components())
476 {
477 auto s = pointer_offset_bits(c.type(), ns);
478 if(s.has_value())
479 size_bits = std::max(size_bits, *s);
480 }
481
482 // Is the union packed?
483 if(type.get_bool(ID_C_packed))
484 {
485 // The size needs to be a multiple of 1 char only.
486 max_alignment_bits = config.ansi_c.char_width;
487 }
488
490 {
491 // Visual Studio pads up to the underlying width of
492 // any bit field.
493 for(const auto &c : type.components())
494 if(c.type().id() == ID_c_bit_field)
495 {
496 auto w = underlying_width(to_c_bit_field_type(c.type()), ns);
497 if(w.has_value() && w.value() > max_alignment_bits)
498 max_alignment_bits = w.value();
499 }
500 }
501
502 // The size must be a multiple of the alignment, or
503 // we add a padding member to the union.
504
506 {
509
512
514 component.type()=padding_type;
515 component.set_name("$pad");
516 component.set_is_padding(true);
517
518 type.components().push_back(component);
519 }
520}
configt config
Definition config.cpp:25
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:80
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
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:377
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
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:57
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & id() const
Definition irep.h:388
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
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:230
Definition std_types.h:68
const componentst & components() const
Definition std_types.h:146
std::vector< componentt > componentst
Definition std_types.h:139
The type of an expression, extends irept.
Definition type.h:29
The union type.
Definition c_types.h:147
Fixed-width bit-vector with unsigned binary interpretation.
static std::optional< 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:286
void add_padding(struct_typet &type, const namespacet &ns)
Definition padding.cpp:459
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.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< 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:17
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:291
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:517
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:213
@ VISUAL_STUDIO

AltStyle によって変換されたページ (->オリジナル) /