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 "namespace.h"
17 #include "pointer_offset_size.h"
18 #include "std_code.h"
19 #include "std_expr.h"
20 
21 template <bool nondet>
23 {
24 public:
25  explicit expr_initializert(const namespacet &_ns) : ns(_ns)
26  {
27  }
28 
30  const typet &type,
31  const source_locationt &source_location)
32  {
33  return expr_initializer_rec(type, source_location);
34  }
35 
36 protected:
37  const namespacet &ns;
38 
40  const typet &type,
41  const source_locationt &source_location);
42 };
43 
44 template <bool nondet>
46  const typet &type,
47  const source_locationt &source_location)
48 {
49  const irep_idt &type_id=type.id();
50 
51  if(type_id==ID_unsignedbv ||
52  type_id==ID_signedbv ||
53  type_id==ID_pointer ||
54  type_id==ID_c_enum ||
55  type_id==ID_incomplete_c_enum ||
56  type_id==ID_c_bit_field ||
57  type_id==ID_bool ||
58  type_id==ID_c_bool ||
59  type_id==ID_floatbv ||
60  type_id==ID_fixedbv)
61  {
62  exprt result;
63  if(nondet)
64  result = side_effect_expr_nondett(type, source_location);
65  else
66  result = from_integer(0, type);
67 
68  result.add_source_location()=source_location;
69  return result;
70  }
71  else if(type_id==ID_rational ||
72  type_id==ID_real)
73  {
74  exprt result;
75  if(nondet)
76  result = side_effect_expr_nondett(type, source_location);
77  else
78  result = constant_exprt(ID_0, type);
79 
80  result.add_source_location()=source_location;
81  return result;
82  }
83  else if(type_id==ID_verilog_signedbv ||
84  type_id==ID_verilog_unsignedbv)
85  {
86  exprt result;
87  if(nondet)
88  result = side_effect_expr_nondett(type, source_location);
89  else
90  {
91  const std::size_t width = to_bitvector_type(type).get_width();
92  std::string value(width, '0');
93 
94  result = constant_exprt(value, type);
95  }
96 
97  result.add_source_location()=source_location;
98  return result;
99  }
100  else if(type_id==ID_complex)
101  {
102  exprt result;
103  if(nondet)
104  result = side_effect_expr_nondett(type, source_location);
105  else
106  {
107  exprt sub_zero =
108  expr_initializer_rec(to_complex_type(type).subtype(), source_location);
109  if(sub_zero.is_nil())
110  return nil_exprt();
111 
112  result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));
113  }
114 
115  result.add_source_location()=source_location;
116  return result;
117  }
118  else if(type_id==ID_array)
119  {
120  const array_typet &array_type=to_array_type(type);
121 
122  if(array_type.size().is_nil())
123  {
124  // we initialize this with an empty array
125 
126  array_exprt value(array_type);
127  value.type().id(ID_array);
128  value.type().set(ID_size, from_integer(0, size_type()));
129  value.add_source_location()=source_location;
130  return std::move(value);
131  }
132  else
133  {
134  exprt tmpval =
135  expr_initializer_rec(array_type.subtype(), source_location);
136  if(tmpval.is_nil())
137  return nil_exprt();
138 
139  if(array_type.size().id()==ID_infinity)
140  {
141  if(nondet)
142  return side_effect_expr_nondett(type, source_location);
143 
144  array_of_exprt value(tmpval, array_type);
145  value.add_source_location()=source_location;
146  return std::move(value);
147  }
148 
149  const auto array_size = numeric_cast<mp_integer>(array_type.size());
150  if(!array_size.has_value())
151  {
152  if(nondet)
153  return side_effect_expr_nondett(type, source_location);
154  else
155  return nil_exprt();
156  }
157 
158  if(*array_size < 0)
159  return nil_exprt();
160 
161  array_exprt value(array_type);
162  value.operands().resize(numeric_cast_v<std::size_t>(*array_size), tmpval);
163  value.add_source_location()=source_location;
164  return std::move(value);
165  }
166  }
167  else if(type_id==ID_vector)
168  {
169  const vector_typet &vector_type=to_vector_type(type);
170 
171  exprt tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
172  if(tmpval.is_nil())
173  return nil_exprt();
174 
175  const mp_integer vector_size =
176  numeric_cast_v<mp_integer>(vector_type.size());
177 
178  if(vector_size < 0)
179  return nil_exprt();
180 
181  vector_exprt value(vector_type);
182  value.operands().resize(numeric_cast_v<std::size_t>(vector_size), tmpval);
183  value.add_source_location()=source_location;
184 
185  return std::move(value);
186  }
187  else if(type_id==ID_struct)
188  {
189  const struct_typet::componentst &components=
190  to_struct_type(type).components();
191 
192  struct_exprt value(type);
193 
194  value.operands().reserve(components.size());
195 
196  for(const auto &c : components)
197  {
198  if(c.type().id() == ID_code)
199  {
200  constant_exprt code_value(ID_nil, c.type());
201  code_value.add_source_location()=source_location;
202  value.add_to_operands(std::move(code_value));
203  }
204  else
205  {
206  const exprt member = expr_initializer_rec(c.type(), source_location);
207  if(member.is_nil())
208  return nil_exprt();
209 
210  value.add_to_operands(std::move(member));
211  }
212  }
213 
214  value.add_source_location()=source_location;
215 
216  return std::move(value);
217  }
218  else if(type_id==ID_union)
219  {
220  const union_typet::componentst &components=
221  to_union_type(type).components();
222 
223  union_exprt value(type);
224 
226  bool found=false;
227  mp_integer component_size=0;
228 
229  // we need to find the largest member
230 
231  for(const auto &c : components)
232  {
233  // skip methods
234  if(c.type().id() == ID_code)
235  continue;
236 
237  auto bits = pointer_offset_bits(c.type(), ns);
238 
239  if(bits.has_value() && *bits > component_size)
240  {
241  component = c;
242  found=true;
243  component_size = *bits;
244  }
245  }
246 
247  value.add_source_location()=source_location;
248 
249  if(!found)
250  {
251  // stupid empty union
252  value.op()=nil_exprt();
253  }
254  else
255  {
256  value.set_component_name(component.get_name());
257  value.op()=
258  expr_initializer_rec(component.type(), source_location);
259  if(value.op().is_nil())
260  return nil_exprt();
261  }
262 
263  return std::move(value);
264  }
265  else if(type_id == ID_symbol_type)
266  {
267  exprt result = expr_initializer_rec(ns.follow(type), source_location);
268  // we might have mangled the type for arrays, so keep that
269  if(ns.follow(type).id()!=ID_array)
270  result.type()=type;
271 
272  return result;
273  }
274  else if(type_id==ID_c_enum_tag)
275  {
276  return
277  expr_initializer_rec(
278  ns.follow_tag(to_c_enum_tag_type(type)),
279  source_location);
280  }
281  else if(type_id==ID_struct_tag)
282  {
283  exprt result = expr_initializer_rec(
284  ns.follow_tag(to_struct_tag_type(type)), source_location);
285 
286  // use the tag type
287  result.type() = type;
288 
289  return result;
290  }
291  else if(type_id==ID_union_tag)
292  {
293  exprt result = expr_initializer_rec(
294  ns.follow_tag(to_union_tag_type(type)), source_location);
295 
296  // use the tag type
297  result.type() = type;
298 
299  return result;
300  }
301  else if(type_id==ID_string)
302  {
303  exprt result;
304  if(nondet)
305  result = side_effect_expr_nondett(type, source_location);
306  else
307  result = constant_exprt(irep_idt(), type);
308 
309  result.add_source_location()=source_location;
310  return result;
311  }
312  else
313  return nil_exprt();
314 }
315 
323  const typet &type,
324  const source_locationt &source_location,
325  const namespacet &ns)
326 {
327  expr_initializert<false> z_i(ns);
328  const exprt result = z_i(type, source_location);
329  if(result.is_nil())
330  return {};
331  else
332  return result;
333 }
334 
343  const typet &type,
344  const source_locationt &source_location,
345  const namespacet &ns)
346 {
347  expr_initializert<true> z_i(ns);
348  const exprt result = z_i(type, source_location);
349  if(result.is_nil())
350  return {};
351  else
352  return result;
353 }
The type of an expression, extends irept.
Definition: type.h:27
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 typet to a bitvector_typet.
Definition: std_types.h:1158
const exprt & op() const
Definition: std_expr.h:371
optionalt< exprt > nondet_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create a non-deterministic value for type type, with all subtypes independently expanded as non-deter...
exprt expr_initializer_rec(const typet &type, const source_locationt &source_location)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
expr_initializert(const namespacet &_ns)
std::vector< componentt > componentst
Definition: std_types.h:203
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
unsignedbv_typet size_type()
Definition: c_types.cpp:58
A constant literal expression.
Definition: std_expr.h:4384
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
const namespacet & ns
The NIL expression.
Definition: std_expr.h:4461
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
The vector type.
Definition: std_types.h:1755
nonstd::optional< T > optionalt
Definition: optional.h:35
Union constructor from single element.
Definition: std_expr.h:1840
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const exprt & size() const
Definition: std_types.h:1765
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
const exprt & size() const
Definition: std_types.h:1010
Array constructor from single element.
Definition: std_expr.h:1678
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
Vector constructor from list of elements.
Definition: std_expr.h:1800
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
exprt operator()(const typet &type, const source_locationt &source_location)
std::size_t get_width() const
Definition: std_types.h:1117
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:737
Pointer Logic.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1838
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1868
source_locationt & add_source_location()
Definition: expr.h:233
Arrays with given size.
Definition: std_types.h:1000
dstringt irep_idt
Definition: irep.h:32
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
const typet & subtype() const
Definition: type.h:38
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Struct constructor from list of elements.
Definition: std_expr.h:1920
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:130
Array constructor from list of elements.
Definition: std_expr.h:1739
Complex constructor from a pair of numbers.
Definition: std_expr.h:1962
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286