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, source_location);
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, source_location);
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, source_location);
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, source_location);
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  return side_effect_expr_nondett(type, source_location);
153 
154  array_of_exprt value(tmpval, array_type);
155  value.add_source_location()=source_location;
156  return value;
157  }
158  else if(to_integer(array_type.size(), array_size))
159  {
160  if(nondet)
161  return side_effect_expr_nondett(type, source_location);
162 
163  error().source_location=source_location;
164  error() << "failed to zero-initialize array of non-fixed size `"
165  << format(array_type.size()) << "'" << eom;
166  throw 0;
167  }
168 
170  array_size >= 0, "array should not have negative size");
171 
172  array_exprt value(array_type);
173  value.operands().resize(integer2size_t(array_size), tmpval);
174  value.add_source_location()=source_location;
175  return value;
176  }
177  }
178  else if(type_id==ID_vector)
179  {
180  const vector_typet &vector_type=to_vector_type(type);
181 
182  exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
183 
184  mp_integer vector_size;
185 
186  if(to_integer(vector_type.size(), vector_size))
187  {
188  if(nondet)
189  return side_effect_expr_nondett(type, source_location);
190 
191  error().source_location=source_location;
192  error() << "failed to zero-initialize vector of non-fixed size `"
193  << format(vector_type.size()) << "'" << eom;
194  throw 0;
195  }
196 
198  vector_size >= 0, "vector should not have negative size");
199 
200  vector_exprt value(vector_type);
201  value.operands().resize(integer2size_t(vector_size), tmpval);
202  value.add_source_location()=source_location;
203 
204  return value;
205  }
206  else if(type_id==ID_struct)
207  {
208  const struct_typet::componentst &components=
209  to_struct_type(type).components();
210 
211  struct_exprt value(type);
212 
213  value.operands().reserve(components.size());
214 
215  for(struct_typet::componentst::const_iterator
216  it=components.begin();
217  it!=components.end();
218  it++)
219  {
220  if(it->type().id()==ID_code)
221  {
222  constant_exprt code_value(ID_nil, it->type());
223  code_value.add_source_location()=source_location;
224  value.copy_to_operands(code_value);
225  }
226  else
227  value.copy_to_operands(
228  expr_initializer_rec(it->type(), source_location));
229  }
230 
231  value.add_source_location()=source_location;
232 
233  return value;
234  }
235  else if(type_id==ID_union)
236  {
237  const union_typet::componentst &components=
238  to_union_type(type).components();
239 
240  union_exprt value(type);
241 
242  union_typet::componentt component;
243  bool found=false;
244  mp_integer component_size=0;
245 
246  // we need to find the largest member
247 
248  for(struct_typet::componentst::const_iterator
249  it=components.begin();
250  it!=components.end();
251  it++)
252  {
253  // skip methods
254  if(it->type().id()==ID_code)
255  continue;
256 
257  mp_integer bits=pointer_offset_bits(it->type(), ns);
258 
259  if(bits>component_size)
260  {
261  component=*it;
262  found=true;
263  component_size=bits;
264  }
265  }
266 
267  value.add_source_location()=source_location;
268 
269  if(!found)
270  {
271  // stupid empty union
272  value.op()=nil_exprt();
273  }
274  else
275  {
276  value.set_component_name(component.get_name());
277  value.op()=
278  expr_initializer_rec(component.type(), source_location);
279  }
280 
281  return value;
282  }
283  else if(type_id==ID_symbol)
284  {
285  exprt result = expr_initializer_rec(ns.follow(type), source_location);
286  // we might have mangled the type for arrays, so keep that
287  if(ns.follow(type).id()!=ID_array)
288  result.type()=type;
289 
290  return result;
291  }
292  else if(type_id==ID_c_enum_tag)
293  {
294  return
295  expr_initializer_rec(
296  ns.follow_tag(to_c_enum_tag_type(type)),
297  source_location);
298  }
299  else if(type_id==ID_struct_tag)
300  {
301  return
302  expr_initializer_rec(
303  ns.follow_tag(to_struct_tag_type(type)),
304  source_location);
305  }
306  else if(type_id==ID_union_tag)
307  {
308  return
309  expr_initializer_rec(
310  ns.follow_tag(to_union_tag_type(type)),
311  source_location);
312  }
313  else if(type_id==ID_string)
314  {
315  exprt result;
316  if(nondet)
317  result = side_effect_expr_nondett(type, source_location);
318  else
319  result = constant_exprt(irep_idt(), type);
320 
321  result.add_source_location()=source_location;
322  return result;
323  }
324  else
325  {
326  error().source_location=source_location;
327  error() << "failed to initialize `" << format(type) << "'" << eom;
328  throw 0;
329  }
330 }
331 
333  const typet &type,
334  const source_locationt &source_location,
335  const namespacet &ns,
337 {
339  return z_i(type, source_location);
340 }
341 
343  const typet &type,
344  const source_locationt &source_location,
345  const namespacet &ns,
347 {
349  return z_i(type, source_location);
350 }
351 
353  const typet &type,
354  const source_locationt &source_location,
355  const namespacet &ns)
356 {
357  std::ostringstream oss;
358  stream_message_handlert mh(oss);
359 
360  try
361  {
362  expr_initializert<false> z_i(ns, mh);
363  return z_i(type, source_location);
364  }
365  catch(int)
366  {
367  throw oss.str();
368  }
369 }
370 
372  const typet &type,
373  const source_locationt &source_location,
374  const namespacet &ns)
375 {
376  std::ostringstream oss;
377  stream_message_handlert mh(oss);
378 
379  try
380  {
381  expr_initializert<true> z_i(ns, mh);
382  return z_i(type, source_location);
383  }
384  catch(int)
385  {
386  throw oss.str();
387  }
388 }
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:172
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1159
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:4422
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
const namespacet & ns
The NIL expression.
Definition: std_expr.h:4508
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:1638
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:1648
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a struct_tag_typet.
Definition: std_types.h:566
const exprt & size() const
Definition: std_types.h:1023
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
exprt operator()(const typet &type, const source_locationt &source_location)
std::size_t get_width() const
Definition: std_types.h:1138
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:1054
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:1709
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:1013
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:32
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:278
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:286
static format_containert< T > format(const T &o)
Definition: format.h:35