cprover
Loading...
Searching...
No Matches
expr_initializer.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Expression Initialization
4
5Author: 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
21template <bool nondet>
23{
24public:
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
35protected:
36 const namespacet &ns;
37
39 const typet &type,
40 const source_locationt &source_location);
41};
42
43template <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 =
132 expr_initializer_rec(array_type.element_type(), 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 =
164 expr_initializer_rec(vector_type.element_type(), source_location);
165 if(!tmpval.has_value())
166 return {};
167
168 const mp_integer vector_size =
169 numeric_cast_v<mp_integer>(vector_type.size());
170
171 if(vector_size < 0)
172 return {};
173
174 vector_exprt value({}, vector_type);
175 value.operands().resize(numeric_cast_v<std::size_t>(vector_size), *tmpval);
176 value.add_source_location()=source_location;
177
178 return std::move(value);
179 }
180 else if(type_id==ID_struct)
181 {
182 const struct_typet::componentst &components=
184
185 struct_exprt value({}, type);
186
187 value.operands().reserve(components.size());
188
189 for(const auto &c : components)
190 {
191 if(c.type().id() == ID_code)
192 {
193 constant_exprt code_value(ID_nil, c.type());
194 code_value.add_source_location()=source_location;
195 value.add_to_operands(std::move(code_value));
196 }
197 else
198 {
199 const auto member = expr_initializer_rec(c.type(), source_location);
200 if(!member.has_value())
201 return {};
202
203 value.add_to_operands(std::move(*member));
204 }
205 }
206
207 value.add_source_location()=source_location;
208
209 return std::move(value);
210 }
211 else if(type_id==ID_union)
212 {
213 const union_typet &union_type = to_union_type(type);
214
215 if(union_type.components().empty())
216 {
217 empty_union_exprt value{type};
218 value.add_source_location() = source_location;
219 return std::move(value);
220 }
221
222 const auto &widest_member = union_type.find_widest_union_component(ns);
223 if(!widest_member.has_value())
224 return {};
225
226 auto component_value =
227 expr_initializer_rec(widest_member->first.type(), source_location);
228
229 if(!component_value.has_value())
230 return {};
231
232 union_exprt value{widest_member->first.get_name(), *component_value, type};
233 value.add_source_location() = source_location;
234
235 return std::move(value);
236 }
237 else if(type_id==ID_c_enum_tag)
238 {
239 auto result = expr_initializer_rec(
240 ns.follow_tag(to_c_enum_tag_type(type)), source_location);
241
242 if(!result.has_value())
243 return {};
244
245 // use the tag type
246 result->type() = type;
247
248 return *result;
249 }
250 else if(type_id==ID_struct_tag)
251 {
252 auto result = expr_initializer_rec(
253 ns.follow_tag(to_struct_tag_type(type)), source_location);
254
255 if(!result.has_value())
256 return {};
257
258 // use the tag type
259 result->type() = type;
260
261 return *result;
262 }
263 else if(type_id==ID_union_tag)
264 {
265 auto result = expr_initializer_rec(
266 ns.follow_tag(to_union_tag_type(type)), source_location);
267
268 if(!result.has_value())
269 return {};
270
271 // use the tag type
272 result->type() = type;
273
274 return *result;
275 }
276 else if(type_id==ID_string)
277 {
278 exprt result;
279 if(nondet)
280 result = side_effect_expr_nondett(type, source_location);
281 else
282 result = constant_exprt(irep_idt(), type);
283
284 result.add_source_location()=source_location;
285 return result;
286 }
287 else
288 return {};
289}
290
298 const typet &type,
299 const source_locationt &source_location,
300 const namespacet &ns)
301{
302 return expr_initializert<false>(ns)(type, source_location);
303}
304
313 const typet &type,
314 const source_locationt &source_location,
315 const namespacet &ns)
316{
317 return expr_initializert<true>(ns)(type, source_location);
318}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
unsignedbv_typet size_type()
Definition c_types.cpp:68
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:344
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:202
Array constructor from list of elements.
Definition std_expr.h:1476
const array_typet & type() const
Definition std_expr.h:1483
Array constructor from single element.
Definition std_expr.h:1411
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
std::size_t get_width() const
Definition std_types.h:864
Complex constructor from a pair of numbers.
Definition std_expr.h:1761
A constant literal expression.
Definition std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1677
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
operandst & operands()
Definition expr.h:92
source_locationt & add_source_location()
Definition expr.h:235
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
Struct constructor from list of elements.
Definition std_expr.h:1722
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:29
source_locationt & add_source_location()
Definition type.h:79
Union constructor from single element.
Definition std_expr.h:1611
The union type.
Definition c_types.h:125
optionalt< std::pair< struct_union_typet::componentt, mp_integer > > find_widest_union_component(const namespacet &ns) const
Determine the member of maximum bit width in a union type.
Definition c_types.cpp:318
Vector constructor from list of elements.
Definition std_expr.h:1575
The vector type.
Definition std_types.h:996
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1006
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
Pointer Logic.
BigInt mp_integer
Definition smt_terms.h:12
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1040
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1082
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832