cprover
zero_initializer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Linking: Zero Initialization
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "zero_initializer.h"
13 
14 #include <sstream>
15 
16 #include <util/namespace.h>
17 #include <util/message.h>
18 #include <util/arith_tools.h>
19 #include <util/std_types.h>
20 #include <util/std_expr.h>
22 
23 #include <util/c_types.h>
24 #include <ansi-c/expr2c.h>
25 
27 {
28 public:
30  const namespacet &_ns,
31  message_handlert &_message_handler):
32  messaget(_message_handler),
33  ns(_ns)
34  {
35  }
36 
38  const typet &type,
39  const source_locationt &source_location)
40  {
41  return zero_initializer_rec(type, source_location);
42  }
43 
44 protected:
45  const namespacet &ns;
46 
47  std::string to_string(const exprt &src)
48  {
49  return expr2c(src, ns);
50  }
51 
52  std::string to_string(const typet &src)
53  {
54  return type2c(src, ns);
55  }
56 
58  const typet &type,
59  const source_locationt &source_location);
60 };
61 
63  const typet &type,
64  const source_locationt &source_location)
65 {
66  const irep_idt &type_id=type.id();
67 
68  if(type_id==ID_unsignedbv ||
69  type_id==ID_signedbv ||
70  type_id==ID_pointer ||
71  type_id==ID_c_enum ||
72  type_id==ID_incomplete_c_enum ||
73  type_id==ID_c_bit_field ||
74  type_id==ID_bool ||
75  type_id==ID_c_bool ||
76  type_id==ID_floatbv ||
77  type_id==ID_fixedbv)
78  {
79  exprt result=from_integer(0, type);
80  result.add_source_location()=source_location;
81  return result;
82  }
83  else if(type_id==ID_rational ||
84  type_id==ID_real)
85  {
86  constant_exprt result(ID_0, type);
87  result.add_source_location()=source_location;
88  return result;
89  }
90  else if(type_id==ID_verilog_signedbv ||
91  type_id==ID_verilog_unsignedbv)
92  {
93  std::size_t width=to_bitvector_type(type).get_width();
94  std::string value(width, '0');
95 
96  constant_exprt result(value, type);
97  result.add_source_location()=source_location;
98  return result;
99  }
100  else if(type_id==ID_complex)
101  {
102  exprt sub_zero=zero_initializer_rec(type.subtype(), source_location);
103  complex_exprt result(sub_zero, sub_zero, to_complex_type(type));
104  result.add_source_location()=source_location;
105  return result;
106  }
107  else if(type_id==ID_code)
108  {
109  error().source_location=source_location;
110  error() << "cannot zero-initialize code-type" << eom;
111  throw 0;
112  }
113  else if(type_id==ID_array)
114  {
115  const array_typet &array_type=to_array_type(type);
116 
117  if(array_type.size().is_nil())
118  {
119  // we initialize this with an empty array
120 
121  array_exprt value(array_type);
122  value.type().id(ID_array);
123  value.type().set(ID_size, from_integer(0, size_type()));
124  value.add_source_location()=source_location;
125  return value;
126  }
127  else
128  {
129  exprt tmpval=zero_initializer_rec(array_type.subtype(), source_location);
130 
131  mp_integer array_size;
132 
133  if(array_type.size().id()==ID_infinity)
134  {
135  exprt value(ID_array_of, type);
136  value.copy_to_operands(tmpval);
137  value.add_source_location()=source_location;
138  return value;
139  }
140  else if(to_integer(array_type.size(), array_size))
141  {
142  error().source_location=source_location;
143  error() << "failed to zero-initialize array of non-fixed size `"
144  << to_string(array_type.size()) << "'" << eom;
145  throw 0;
146  }
147 
148  if(array_size<0)
149  {
150  error().source_location=source_location;
151  error() << "failed to zero-initialize array of with negative size"
152  << eom;
153  throw 0;
154  }
155 
156  array_exprt value(array_type);
157  value.operands().resize(integer2unsigned(array_size), tmpval);
158  value.add_source_location()=source_location;
159  return value;
160  }
161  }
162  else if(type_id==ID_vector)
163  {
164  const vector_typet &vector_type=to_vector_type(type);
165 
166  exprt tmpval=zero_initializer_rec(vector_type.subtype(), source_location);
167 
168  mp_integer vector_size;
169 
170  if(to_integer(vector_type.size(), vector_size))
171  {
172  error().source_location=source_location;
173  error() << "failed to zero-initialize vector of non-fixed size `"
174  << to_string(vector_type.size()) << "'" << eom;
175  throw 0;
176  }
177 
178  if(vector_size<0)
179  {
180  error().source_location=source_location;
181  error() << "failed to zero-initialize vector of with negative size"
182  << eom;
183  throw 0;
184  }
185 
186  vector_exprt value(vector_type);
187  value.operands().resize(integer2unsigned(vector_size), tmpval);
188  value.add_source_location()=source_location;
189 
190  return value;
191  }
192  else if(type_id==ID_struct)
193  {
194  const struct_typet::componentst &components=
195  to_struct_type(type).components();
196 
197  exprt value(ID_struct, type);
198 
199  value.operands().reserve(components.size());
200 
201  for(struct_typet::componentst::const_iterator
202  it=components.begin();
203  it!=components.end();
204  it++)
205  {
206  if(it->type().id()==ID_code)
207  {
208  constant_exprt code_value(it->type());
209  code_value.set_value(ID_nil);
210  code_value.add_source_location()=source_location;
211  value.copy_to_operands(code_value);
212  }
213  else
214  value.copy_to_operands(
215  zero_initializer_rec(it->type(), source_location));
216  }
217 
218  value.add_source_location()=source_location;
219 
220  return value;
221  }
222  else if(type_id==ID_union)
223  {
224  const union_typet::componentst &components=
225  to_union_type(type).components();
226 
227  union_exprt value(type);
228 
229  union_typet::componentt component;
230  bool found=false;
231  mp_integer component_size=0;
232 
233  // we need to find the largest member
234 
235  for(struct_typet::componentst::const_iterator
236  it=components.begin();
237  it!=components.end();
238  it++)
239  {
240  // skip methods
241  if(it->type().id()==ID_code)
242  continue;
243 
244  mp_integer bits=pointer_offset_bits(it->type(), ns);
245 
246  if(bits>component_size)
247  {
248  component=*it;
249  found=true;
250  component_size=bits;
251  }
252  }
253 
254  value.add_source_location()=source_location;
255 
256  if(!found)
257  {
258  // stupid empty union
259  value.op()=nil_exprt();
260  }
261  else
262  {
263  value.set_component_name(component.get_name());
264  value.op()=
265  zero_initializer_rec(component.type(), source_location);
266  }
267 
268  return value;
269  }
270  else if(type_id==ID_symbol)
271  {
272  exprt result=zero_initializer_rec(ns.follow(type), source_location);
273  // we might have mangled the type for arrays, so keep that
274  if(ns.follow(type).id()!=ID_array)
275  result.type()=type;
276 
277  return result;
278  }
279  else if(type_id==ID_c_enum_tag)
280  {
281  return
284  source_location);
285  }
286  else if(type_id==ID_struct_tag)
287  {
288  return
291  source_location);
292  }
293  else if(type_id==ID_union_tag)
294  {
295  return
298  source_location);
299  }
300  else if(type_id==ID_string)
301  {
302  return constant_exprt(irep_idt(), type);
303  }
304  else
305  {
306  error().source_location=source_location;
307  error() << "failed to zero-initialize `" << to_string(type)
308  << "'" << eom;
309  throw 0;
310  }
311 }
312 
314  const typet &type,
315  const source_locationt &source_location,
316  const namespacet &ns,
318 {
319  zero_initializert z_i(ns, message_handler);
320  return z_i(type, source_location);
321 }
322 
324  const typet &type,
325  const source_locationt &source_location,
326  const namespacet &ns)
327 {
328  std::ostringstream oss;
329  stream_message_handlert mh(oss);
330 
331  try
332  {
333  zero_initializert z_i(ns, mh);
334  return z_i(type, source_location);
335  }
336  catch(int)
337  {
338  throw oss.str();
339  }
340 }
const irep_idt & get_name() const
Definition: std_types.h:179
The type of an expression.
Definition: type.h:20
mstreamt & result()
Definition: message.h:233
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
BigInt mp_integer
Definition: mp_arith.h:19
Linking: Zero Initialization.
bool is_nil() const
Definition: irep.h:103
std::string to_string(const typet &src)
const exprt & op() const
Definition: std_expr.h:258
std::string to_string(const exprt &src)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
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
unsignedbv_typet size_type()
Definition: c_types.cpp:57
A constant literal expression.
Definition: std_expr.h:3685
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
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
The NIL expression.
Definition: std_expr.h:3764
source_locationt source_location
Definition: message.h:175
A constant-size array type.
Definition: std_types.h:1554
union constructor from single element
Definition: std_expr.h:1389
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const exprt & size() const
Definition: std_types.h:1568
zero_initializert(const namespacet &_ns, message_handlert &_message_handler)
std::string type2c(const typet &type, const namespacet &ns)
Definition: expr2c.cpp:3882
const exprt & size() const
Definition: std_types.h:915
vector constructor from list of elements
Definition: std_expr.h:1349
std::size_t get_width() const
Definition: std_types.h:1030
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
const namespacet & ns
API to type classes.
exprt zero_initializer_rec(const typet &type, const source_locationt &source_location)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:536
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:573
Base class for all expressions.
Definition: expr.h:46
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3874
mstreamt & error()
Definition: message.h:223
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1415
source_locationt & add_source_location()
Definition: expr.h:147
arrays with given size
Definition: std_types.h:901
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
Definition: std_types.h:1629
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1589
message_handlert * message_handler
Definition: message.h:259
array constructor from list of elements
Definition: std_expr.h:1309
complex constructor from a pair of numbers
Definition: std_expr.h:1504
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
exprt operator()(const typet &type, const source_locationt &source_location)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051