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;
39 
40  // we trust it blindly, no matter how nonsensical
41  if(given_alignment.is_nil() ||
42  to_integer(given_alignment, a_int))
43  a_int=0;
44 
45  // alignment but no packing
46  if(a_int>0 && !type.get_bool(ID_C_packed))
47  return a_int;
48  // no alignment, packing
49  else if(a_int==0 && type.get_bool(ID_C_packed))
50  return 1;
51 
52  // compute default
53  mp_integer result;
54 
55  if(type.id()==ID_array)
56  result=alignment(type.subtype(), ns);
57  else if(type.id()==ID_struct || type.id()==ID_union)
58  {
59  const struct_union_typet::componentst &components=
61 
62  result=1;
63 
64  // get the max
65  // (should really be the smallest common denominator)
66  for(struct_union_typet::componentst::const_iterator
67  it=components.begin();
68  it!=components.end();
69  it++)
70  result=std::max(result, alignment(it->type(), ns));
71  }
72  else if(type.id()==ID_unsignedbv ||
73  type.id()==ID_signedbv ||
74  type.id()==ID_fixedbv ||
75  type.id()==ID_floatbv ||
76  type.id()==ID_c_bool)
77  {
78  std::size_t width=to_bitvector_type(type).get_width();
79  result=width%8?width/8+1:width/8;
80  }
81  else if(type.id()==ID_c_enum)
82  result=alignment(type.subtype(), ns);
83  else if(type.id()==ID_c_enum_tag)
84  result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns);
85  else if(type.id()==ID_pointer)
86  {
87  std::size_t width=config.ansi_c.pointer_width;
88  result=width%8?width/8+1:width/8;
89  }
90  else if(type.id()==ID_symbol)
91  result=alignment(ns.follow(type), ns);
92  else if(type.id()==ID_c_bit_field)
93  {
94  // we align these according to the 'underlying type'
95  result=alignment(type.subtype(), ns);
96  }
97  else
98  result=1;
99 
100  // if an alignment had been provided and packing was requested, take
101  // the smallest alignment
102  if(a_int>0 && a_int<result)
103  result=a_int;
104 
105  return result;
106 }
107 
108 void add_padding(struct_typet &type, const namespacet &ns)
109 {
110  struct_typet::componentst &components=type.components();
111 
112  // First do padding for bit-fields to make them
113  // appear on byte boundaries.
114 
115  {
116  std::size_t padding_counter=0;
117  std::size_t bit_field_bits=0;
118 
119  for(struct_typet::componentst::iterator
120  it=components.begin();
121  it!=components.end();
122  it++)
123  {
124  if(it->type().id()==ID_c_bit_field &&
125  to_c_bit_field_type(it->type()).get_width()!=0)
126  {
127  // count the bits
128  std::size_t width=to_c_bit_field_type(it->type()).get_width();
129  bit_field_bits+=width;
130  }
131  else if(bit_field_bits!=0)
132  {
133  // not on a byte-boundary?
134  if((bit_field_bits%8)!=0)
135  {
136  std::size_t pad=8-bit_field_bits%8;
137  c_bit_field_typet padding_type(unsignedbv_typet(pad), pad);
138 
139  struct_typet::componentt component;
140  component.type()=padding_type;
141  component.set_name(
142  "$bit_field_pad"+std::to_string(padding_counter++));
143  component.set_is_padding(true);
144 
145  it=components.insert(it, component);
146  it++; // skip over
147 
148  bit_field_bits+=pad;
149  }
150 
151  bit_field_bits=0;
152  }
153  }
154 
155  // Add padding at the end?
156  if((bit_field_bits%8)!=0)
157  {
158  std::size_t pad=8-bit_field_bits%8;
159  c_bit_field_typet padding_type(unsignedbv_typet(pad), pad);
160 
161  struct_typet::componentt component;
162  component.type()=padding_type;
163  component.set_name("$bit_field_pad"+std::to_string(padding_counter++));
164  component.set_is_padding(true);
165 
166  components.push_back(component);
167  }
168  }
169 
170  // Is the struct packed, without any alignment specification?
171  if(type.get_bool(ID_C_packed) &&
172  type.find(ID_C_alignment).is_nil())
173  return; // done
174 
175  mp_integer offset=0;
176  std::size_t padding_counter=0;
177  mp_integer max_alignment=0;
178  std::size_t bit_field_bits=0;
179 
180  for(struct_typet::componentst::iterator
181  it=components.begin();
182  it!=components.end();
183  it++)
184  {
185  const typet it_type=it->type();
186  mp_integer a=1;
187 
188  const bool packed=it_type.get_bool(ID_C_packed) ||
189  ns.follow(it_type).get_bool(ID_C_packed);
190 
191  if(it_type.id()==ID_c_bit_field)
192  {
193  a=alignment(to_c_bit_field_type(it_type).subtype(), ns);
194 
195  // A zero-width bit-field causes alignment to the base-type.
196  if(to_c_bit_field_type(it_type).get_width()==0)
197  {
198  }
199  else
200  {
201  // Otherwise, ANSI-C says that bit-fields do not get padded!
202  // We consider the type for max_alignment, however.
203  if(max_alignment<a)
204  max_alignment=a;
205 
206  std::size_t w=to_c_bit_field_type(it_type).get_width();
207  std::size_t bytes;
208  for(bytes=0; w>bit_field_bits; ++bytes, bit_field_bits+=8) {}
209  bit_field_bits-=w;
210  offset+=bytes;
211  continue;
212  }
213  }
214  else
215  a=alignment(it_type, ns);
216 
217  // check minimum alignment
218  if(a<config.ansi_c.alignment && !packed)
220 
221  if(max_alignment<a)
222  max_alignment=a;
223 
224  if(a!=1)
225  {
226  // we may need to align it
227  mp_integer displacement=offset%a;
228 
229  if(displacement!=0)
230  {
231  mp_integer pad=a-displacement;
232 
233  unsignedbv_typet padding_type;
234  padding_type.set_width(integer2unsigned(pad*8));
235 
236  struct_typet::componentt component;
237  component.type()=padding_type;
238  component.set_name("$pad"+std::to_string(padding_counter++));
239  component.set_is_padding(true);
240 
241  it=components.insert(it, component);
242  it++; // skip over
243 
244  offset+=pad;
245  }
246  }
247 
248  mp_integer size=pointer_offset_size(it_type, ns);
249 
250  if(size!=-1)
251  offset+=size;
252  }
253 
254  if(bit_field_bits!=0)
255  {
256  // these are now assumed to be multiples of 8
257  offset+=bit_field_bits/8;
258  }
259 
260  // any explicit alignment for the struct?
261  if(type.find(ID_C_alignment).is_not_nil())
262  {
263  const exprt &alignment=
264  static_cast<const exprt &>(type.find(ID_C_alignment));
265  if(alignment.id()!=ID_default)
266  {
267  exprt tmp=alignment;
268  simplify(tmp, ns);
269  mp_integer tmp_i;
270  if(!to_integer(tmp, tmp_i) && tmp_i>max_alignment)
271  max_alignment=tmp_i;
272  }
273  }
274  // Is the struct packed, without any alignment specification?
275  else if(type.get_bool(ID_C_packed))
276  return; // done
277 
278  // There may be a need for 'end of struct' padding.
279  // We use 'max_alignment'.
280 
281  if(max_alignment>1)
282  {
283  // we may need to align it
284  mp_integer displacement=offset%max_alignment;
285 
286  if(displacement!=0)
287  {
288  mp_integer pad=max_alignment-displacement;
289 
290  unsignedbv_typet padding_type;
291  padding_type.set_width(integer2unsigned(pad*8));
292 
293  // we insert after any final 'flexible member'
294  struct_typet::componentt component;
295  component.type()=padding_type;
296  component.set_name("$pad"+std::to_string(padding_counter++));
297  component.set_is_padding(true);
298 
299  components.push_back(component);
300  }
301  }
302 }
303 
304 void add_padding(union_typet &type, const namespacet &ns)
305 {
306  mp_integer max_alignment=alignment(type, ns)*8;
307  mp_integer size_bits=pointer_offset_bits(type, ns);
308 
309  if(size_bits<0)
310  throw "type of unknown size:\n"+type.pretty();
311 
312  union_typet::componentst &components=type.components();
313 
314  // Is the union packed?
315  if(type.get_bool(ID_C_packed))
316  {
317  // The size needs to be a multiple of 8 only.
318  max_alignment=8;
319  }
320 
321  // The size must be a multiple of the alignment, or
322  // we add a padding member to the union.
323 
324  if(size_bits%max_alignment!=0)
325  {
326  mp_integer padding=max_alignment-(size_bits%max_alignment);
327 
328  unsignedbv_typet padding_type;
329  padding_type.set_width(integer2unsigned(size_bits+padding));
330 
331  struct_typet::componentt component;
332  component.type()=padding_type;
333  component.set_name("$pad");
334  component.set_is_padding(true);
335 
336  components.push_back(component);
337  }
338 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
BigInt mp_integer
Definition: mp_arith.h:19
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
void set_name(const irep_idt &name)
Definition: std_types.h:184
unsigned alignment
Definition: config.h:68
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:60
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
configt config
Definition: config.cpp:21
Type for c bit fields.
Definition: std_types.h:1294
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
const irep_idt & id() const
Definition: irep.h:189
void set_is_padding(bool is_padding)
Definition: std_types.h:234
void add_padding(struct_typet &type, const namespacet &ns)
Definition: padding.cpp:108
ANSI-C Language Type Checking.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:717
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1319
std::size_t get_width() const
Definition: std_types.h:1030
Pointer Logic.
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
Base class for all expressions.
Definition: expr.h:46
The union type.
Definition: std_types.h:424
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const typet & subtype() const
Definition: type.h:31
unsigned pointer_width
Definition: config.h:36
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool simplify(exprt &expr, const namespacet &ns)
void set_width(std::size_t width)
Definition: std_types.h:1035
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051