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