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