cprover
expr_initializer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Expression Initialization
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "expr_initializer.h"
13 
14 #include "arith_tools.h"
15 #include "c_types.h"
16 #include "format_expr.h"
17 #include "format_type.h"
18 #include "invariant.h"
19 #include "message.h"
20 #include "namespace.h"
21 #include "pointer_offset_size.h"
22 #include "std_code.h"
23 #include "std_expr.h"
24 
25 template <bool nondet>
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 expr_initializer_rec(type, source_location);
42  }
43 
44 protected:
45  const namespacet &ns;
46 
48  const typet &type,
49  const source_locationt &source_location);
50 };
51 
52 template <bool nondet>
54  const typet &type,
55  const source_locationt &source_location)
56 {
57  const irep_idt &type_id=type.id();
58 
59  if(type_id==ID_unsignedbv ||
60  type_id==ID_signedbv ||
61  type_id==ID_pointer ||
62  type_id==ID_c_enum ||
63  type_id==ID_incomplete_c_enum ||
64  type_id==ID_c_bit_field ||
65  type_id==ID_bool ||
66  type_id==ID_c_bool ||
67  type_id==ID_floatbv ||
68  type_id==ID_fixedbv)
69  {
70  exprt result;
71  if(nondet)
72  result = side_effect_expr_nondett(type);
73  else
74  result = from_integer(0, type);
75 
76  result.add_source_location()=source_location;
77  return result;
78  }
79  else if(type_id==ID_rational ||
80  type_id==ID_real)
81  {
82  exprt result;
83  if(nondet)
84  result = side_effect_expr_nondett(type);
85  else
86  result = constant_exprt(ID_0, type);
87 
88  result.add_source_location()=source_location;
89  return result;
90  }
91  else if(type_id==ID_verilog_signedbv ||
92  type_id==ID_verilog_unsignedbv)
93  {
94  exprt result;
95  if(nondet)
96  result = side_effect_expr_nondett(type);
97  else
98  {
99  const std::size_t width = to_bitvector_type(type).get_width();
100  std::string value(width, '0');
101 
102  result = constant_exprt(value, type);
103  }
104 
105  result.add_source_location()=source_location;
106  return result;
107  }
108  else if(type_id==ID_complex)
109  {
110  exprt result;
111  if(nondet)
112  result = side_effect_expr_nondett(type);
113  else
114  {
115  exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);
116  result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));
117  }
118 
119  result.add_source_location()=source_location;
120  return result;
121  }
122  else if(type_id==ID_code)
123  {
124  error().source_location=source_location;
125  error() << "cannot initialize code-type" << eom;
126  throw 0;
127  }
128  else if(type_id==ID_array)
129  {
130  const array_typet &array_type=to_array_type(type);
131 
132  if(array_type.size().is_nil())
133  {
134  // we initialize this with an empty array
135 
136  array_exprt value(array_type);
137  value.type().id(ID_array);
138  value.type().set(ID_size, from_integer(0, size_type()));
139  value.add_source_location()=source_location;
140  return value;
141  }
142  else
143  {
144  exprt tmpval =
145  expr_initializer_rec(array_type.subtype(), source_location);
146 
147  mp_integer array_size;
148 
149  if(array_type.size().id()==ID_infinity)
150  {
151  if(nondet)
152  {
153  side_effect_expr_nondett result(type);
154  result.add_source_location() = source_location;
155  return result;
156  }
157 
158  array_of_exprt value(tmpval, array_type);
159  value.add_source_location()=source_location;
160  return value;
161  }
162  else if(to_integer(array_type.size(), array_size))
163  {
164  if(nondet)
165  {
166  side_effect_expr_nondett result(type);
167  result.add_source_location() = source_location;
168  return result;
169  }
170 
171  error().source_location=source_location;
172  error() << "failed to zero-initialize array of non-fixed size `"
173  << format(array_type.size()) << "'" << eom;
174  throw 0;
175  }
176 
178  array_size >= 0, "array should not have negative size");
179 
180  array_exprt value(array_type);
181  value.operands().resize(integer2size_t(array_size), tmpval);
182  value.add_source_location()=source_location;
183  return value;
184  }
185  }
186  else if(type_id==ID_vector)
187  {
188  const vector_typet &vector_type=to_vector_type(type);
189 
190  exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
191 
192  mp_integer vector_size;
193 
194  if(to_integer(vector_type.size(), vector_size))
195  {
196  if(nondet)
197  {
198  side_effect_expr_nondett result(type);
199  result.add_source_location() = source_location;
200  return result;
201  }
202 
203  error().source_location=source_location;
204  error() << "failed to zero-initialize vector of non-fixed size `"
205  << format(vector_type.size()) << "'" << eom;
206  throw 0;
207  }
208 
210  vector_size >= 0, "vector should not have negative size");
211 
212  vector_exprt value(vector_type);
213  value.operands().resize(integer2size_t(vector_size), tmpval);
214  value.add_source_location()=source_location;
215 
216  return value;
217  }
218  else if(type_id==ID_struct)
219  {
220  const struct_typet::componentst &components=
221  to_struct_type(type).components();
222 
223  struct_exprt value(type);
224 
225  value.operands().reserve(components.size());
226 
227  for(struct_typet::componentst::const_iterator
228  it=components.begin();
229  it!=components.end();
230  it++)
231  {
232  if(it->type().id()==ID_code)
233  {
234  constant_exprt code_value(ID_nil, it->type());
235  code_value.add_source_location()=source_location;
236  value.copy_to_operands(code_value);
237  }
238  else
239  value.copy_to_operands(
240  expr_initializer_rec(it->type(), source_location));
241  }
242 
243  value.add_source_location()=source_location;
244 
245  return value;
246  }
247  else if(type_id==ID_union)
248  {
249  const union_typet::componentst &components=
250  to_union_type(type).components();
251 
252  union_exprt value(type);
253 
254  union_typet::componentt component;
255  bool found=false;
256  mp_integer component_size=0;
257 
258  // we need to find the largest member
259 
260  for(struct_typet::componentst::const_iterator
261  it=components.begin();
262  it!=components.end();
263  it++)
264  {
265  // skip methods
266  if(it->type().id()==ID_code)
267  continue;
268 
269  mp_integer bits=pointer_offset_bits(it->type(), ns);
270 
271  if(bits>component_size)
272  {
273  component=*it;
274  found=true;
275  component_size=bits;
276  }
277  }
278 
279  value.add_source_location()=source_location;
280 
281  if(!found)
282  {
283  // stupid empty union
284  value.op()=nil_exprt();
285  }
286  else
287  {
288  value.set_component_name(component.get_name());
289  value.op()=
290  expr_initializer_rec(component.type(), source_location);
291  }
292 
293  return value;
294  }
295  else if(type_id==ID_symbol)
296  {
297  exprt result = expr_initializer_rec(ns.follow(type), source_location);
298  // we might have mangled the type for arrays, so keep that
299  if(ns.follow(type).id()!=ID_array)
300  result.type()=type;
301 
302  return result;
303  }
304  else if(type_id==ID_c_enum_tag)
305  {
306  return
307  expr_initializer_rec(
308  ns.follow_tag(to_c_enum_tag_type(type)),
309  source_location);
310  }
311  else if(type_id==ID_struct_tag)
312  {
313  return
314  expr_initializer_rec(
315  ns.follow_tag(to_struct_tag_type(type)),
316  source_location);
317  }
318  else if(type_id==ID_union_tag)
319  {
320  return
321  expr_initializer_rec(
322  ns.follow_tag(to_union_tag_type(type)),
323  source_location);
324  }
325  else if(type_id==ID_string)
326  {
327  exprt result;
328  if(nondet)
329  result = side_effect_expr_nondett(type);
330  else
331  result = constant_exprt(irep_idt(), type);
332 
333  result.add_source_location()=source_location;
334  return result;
335  }
336  else
337  {
338  error().source_location=source_location;
339  error() << "failed to initialize `" << format(type) << "'" << eom;
340  throw 0;
341  }
342 }
343 
345  const typet &type,
346  const source_locationt &source_location,
347  const namespacet &ns,
349 {
351  return z_i(type, source_location);
352 }
353 
355  const typet &type,
356  const source_locationt &source_location,
357  const namespacet &ns,
359 {
361  return z_i(type, source_location);
362 }
363 
365  const typet &type,
366  const source_locationt &source_location,
367  const namespacet &ns)
368 {
369  std::ostringstream oss;
370  stream_message_handlert mh(oss);
371 
372  try
373  {
374  expr_initializert<false> z_i(ns, mh);
375  return z_i(type, source_location);
376  }
377  catch(int)
378  {
379  throw oss.str();
380  }
381 }
382 
384  const typet &type,
385  const source_locationt &source_location,
386  const namespacet &ns)
387 {
388  std::ostringstream oss;
389  stream_message_handlert mh(oss);
390 
391  try
392  {
393  expr_initializert<true> z_i(ns, mh);
394  return z_i(type, source_location);
395  }
396  catch(int)
397  {
398  throw oss.str();
399  }
400 }
const irep_idt & get_name() const
Definition: std_types.h:182
The type of an expression.
Definition: type.h:22
exprt nondet_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:102
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1150
const exprt & op() const
Definition: std_expr.h:340
exprt expr_initializer_rec(const typet &type, const source_locationt &source_location)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
std::vector< componentt > componentst
Definition: std_types.h:243
const componentst & components() const
Definition: std_types.h:245
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
typet & type()
Definition: expr.h:56
unsignedbv_typet size_type()
Definition: c_types.cpp:58
A constant literal expression.
Definition: std_expr.h:4424
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:189
const namespacet & ns
The NIL expression.
Definition: std_expr.h:4510
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:603
A constant-size array type.
Definition: std_types.h:1629
union constructor from single element
Definition: std_expr.h:1730
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const exprt & size() const
Definition: std_types.h:1639
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1660
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:566
const exprt & size() const
Definition: std_types.h:1014
array constructor from single element
Definition: std_expr.h:1550
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
vector constructor from list of elements
Definition: std_expr.h:1684
exprt operator()(const typet &type, const source_locationt &source_location)
std::size_t get_width() const
Definition: std_types.h:1129
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:747
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
Pointer Logic.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
expr_initializert(const namespacet &_ns, message_handlert &_message_handler)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
const source_locationt & source_location() const
Definition: expr.h:125
const complex_typet & to_complex_type(const typet &type)
Cast a generic typet to a complex_typet.
Definition: std_types.h:1700
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1756
source_locationt & add_source_location()
Definition: expr.h:130
arrays with given size
Definition: std_types.h:1004
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
dstringt irep_idt
Definition: irep.h:31
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1815
array constructor from list of elements
Definition: std_expr.h:1617
complex constructor from a pair of numbers
Definition: std_expr.h:1861
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
static format_containert< T > format(const T &o)
Definition: format.h:35