CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 "bitvector_expr.h"
16#include "byte_operators.h"
17#include "c_types.h"
18#include "config.h"
19#include "magic.h"
20#include "namespace.h" // IWYU pragma: keep
21#include "simplify_expr.h"
22#include "std_code.h"
23#include "symbol_table.h"
24
26{
27public:
29 {
30 }
31
32 std::optional<exprt> operator()(
33 const typet &type,
34 const source_locationt &source_location,
35 const exprt &init_expr)
36 {
37 return expr_initializer_rec(type, source_location, init_expr);
38 }
39
40protected:
41 const namespacet &ns;
42
43 std::optional<exprt> expr_initializer_rec(
44 const typet &type,
45 const source_locationt &source_location,
46 const exprt &init_expr);
47};
48
50 const typet &type,
51 const source_locationt &source_location,
52 const exprt &init_expr)
53{
54 const irep_idt &type_id=type.id();
55
65 {
66 exprt result;
67 if(init_expr.id() == ID_nondet)
68 result = side_effect_expr_nondett(type, source_location);
69 else if(init_expr.is_zero())
70 result = from_integer(0, type);
71 else
72 result = duplicate_per_byte(init_expr, type, ns);
73
74 result.add_source_location()=source_location;
75 return result;
76 }
77 else if(type_id==ID_rational ||
79 {
80 exprt result;
81 if(init_expr.id() == ID_nondet)
82 result = side_effect_expr_nondett(type, source_location);
83 else if(init_expr.is_zero())
84 result = constant_exprt(ID_0, type);
85 else
86 result = duplicate_per_byte(init_expr, type, ns);
87
88 result.add_source_location()=source_location;
89 return result;
90 }
93 {
94 exprt result;
95 if(init_expr.id() == ID_nondet)
96 result = side_effect_expr_nondett(type, source_location);
97 else if(init_expr.is_zero())
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 else
105 result = duplicate_per_byte(init_expr, type, ns);
106
107 result.add_source_location()=source_location;
108 return result;
109 }
110 else if(type_id==ID_complex)
111 {
112 exprt result;
113 if(init_expr.id() == ID_nondet)
114 result = side_effect_expr_nondett(type, source_location);
115 else if(init_expr.is_zero())
116 {
118 to_complex_type(type).subtype(), source_location, init_expr);
119 if(!sub_zero.has_value())
120 return {};
121
123 }
124 else
125 result = duplicate_per_byte(init_expr, type, ns);
126
127 result.add_source_location()=source_location;
128 return result;
129 }
130 else if(type_id==ID_array)
131 {
133
134 if(array_type.size().is_nil())
135 {
136 // we initialize this with an empty array
137
138 array_exprt value({}, array_type);
139 value.type().size() = from_integer(0, size_type());
140 value.add_source_location()=source_location;
141 return std::move(value);
142 }
143 else
144 {
146 array_type.element_type(), source_location, init_expr);
147 if(!tmpval.has_value())
148 return {};
149
151 if(
152 array_type.size().id() == ID_infinity || !array_size.has_value() ||
154 {
155 if(init_expr.id() == ID_nondet)
156 return side_effect_expr_nondett(type, source_location);
157
159 value.add_source_location()=source_location;
160 return std::move(value);
161 }
162
163 if(*array_size < 0)
164 return {};
165
166 array_exprt value({}, array_type);
167 value.operands().resize(
169 value.add_source_location()=source_location;
170 return std::move(value);
171 }
172 }
173 else if(type_id==ID_vector)
174 {
176
178 vector_type.element_type(), source_location, init_expr);
179 if(!tmpval.has_value())
180 return {};
181
182 const mp_integer vector_size =
184
185 if(vector_size < 0)
186 return {};
187
188 vector_exprt value({}, vector_type);
189 value.operands().resize(numeric_cast_v<std::size_t>(vector_size), *tmpval);
190 value.add_source_location()=source_location;
191
192 return std::move(value);
193 }
194 else if(type_id==ID_struct)
195 {
196 const struct_typet::componentst &components=
197 to_struct_type(type).components();
198
199 struct_exprt value({}, type);
200
201 value.operands().reserve(components.size());
202
203 for(const auto &c : components)
204 {
206 c.type().id() != ID_code, "struct member must not be of code type");
207
208 const auto member =
209 expr_initializer_rec(c.type(), source_location, init_expr);
210 if(!member.has_value())
211 return {};
212
213 value.add_to_operands(std::move(*member));
214 }
215
216 value.add_source_location()=source_location;
217
218 return std::move(value);
219 }
220 else if(type_id==ID_union)
221 {
222 const union_typet &union_type = to_union_type(type);
223
224 if(union_type.components().empty())
225 {
226 empty_union_exprt value{type};
227 value.add_source_location() = source_location;
228 return std::move(value);
229 }
230
231 const auto &widest_member = union_type.find_widest_union_component(ns);
232 if(!widest_member.has_value())
233 return {};
234
236 widest_member->first.type(), source_location, init_expr);
237
238 if(!component_value.has_value())
239 return {};
240
241 union_exprt value{widest_member->first.get_name(), *component_value, type};
242 value.add_source_location() = source_location;
243
244 return std::move(value);
245 }
246 else if(type_id==ID_c_enum_tag)
247 {
248 auto result = expr_initializer_rec(
249 ns.follow_tag(to_c_enum_tag_type(type)), source_location, init_expr);
250
251 if(!result.has_value())
252 return {};
253
254 // use the tag type
255 result->type() = type;
256
257 return *result;
258 }
259 else if(type_id==ID_struct_tag)
260 {
261 auto result = expr_initializer_rec(
262 ns.follow_tag(to_struct_tag_type(type)), source_location, init_expr);
263
264 if(!result.has_value())
265 return {};
266
267 // use the tag type
268 result->type() = type;
269
270 return *result;
271 }
272 else if(type_id==ID_union_tag)
273 {
274 auto result = expr_initializer_rec(
275 ns.follow_tag(to_union_tag_type(type)), source_location, init_expr);
276
277 if(!result.has_value())
278 return {};
279
280 // use the tag type
281 result->type() = type;
282
283 return *result;
284 }
285 else if(type_id==ID_string)
286 {
287 exprt result;
288 if(init_expr.id() == ID_nondet)
289 result = side_effect_expr_nondett(type, source_location);
290 else if(init_expr.is_zero())
291 result = constant_exprt(irep_idt(), type);
292 else
293 result = duplicate_per_byte(init_expr, type, ns);
294
295 result.add_source_location()=source_location;
296 return result;
297 }
298 else
299 return {};
300}
301
308std::optional<exprt> zero_initializer(
309 const typet &type,
310 const source_locationt &source_location,
311 const namespacet &ns)
312{
313 return expr_initializert(ns)(
314 type, source_location, constant_exprt(ID_0, char_type()));
315}
316
324std::optional<exprt> nondet_initializer(
325 const typet &type,
326 const source_locationt &source_location,
327 const namespacet &ns)
328{
329 return expr_initializert(ns)(type, source_location, exprt(ID_nondet));
330}
331
340std::optional<exprt> expr_initializer(
341 const typet &type,
342 const source_locationt &source_location,
343 const namespacet &ns,
344 const exprt &init_byte_expr)
345{
346 return expr_initializert(ns)(type, source_location, init_byte_expr);
347}
348
354static exprt cast_or_reinterpret(const exprt &expr, const typet &out_type)
355{
356 // Same type --> no cast
357 if(expr.type() == out_type)
358 {
359 return expr;
360 }
361 if(
364 {
366 }
368}
369
382 const exprt &init_byte_expr,
383 const typet &output_type,
384 const namespacet &ns)
385{
386 const auto init_type_as_bitvector =
388 // Fail if `init_byte_expr` is not a bitvector of maximum 8 bits or a boolean.
391 init_type_as_bitvector->get_width() <= config.ansi_c.char_width) ||
392 init_byte_expr.type().id() == ID_bool);
393 // Simplify init_expr to enable faster duplication when simplifiable to a
394 // constant expr
397 {
398 const auto out_width = output_bv->get_width();
399 // Replicate `simplified_init_expr` enough times until it completely fills
400 // `output_type`.
401
402 // We've got a constant. So, precompute the value of the constant.
403 if(simplified_init_expr.is_constant())
404 {
405 const auto init_size = init_type_as_bitvector->get_width();
406 const irep_idt init_value =
408
409 // Create a new BV of `output_type` size with its representation being the
410 // replication of the simplified_init_expr (padded with 0) enough times to
411 // fill.
412 const auto output_value =
413 make_bvrep(out_width, [&init_size, &init_value](std::size_t index) {
414 // Index modded by 8 to access the i-th bit of init_value
415 const auto source_index = index % config.ansi_c.char_width;
416 // If the modded i-th bit exists get it, otherwise add 0 padding.
417 return source_index < init_size &&
419 });
420
422 }
423
424 const size_t size =
425 (out_width + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
426
427 // We haven't got a constant. So, build the expression using shift-and-or.
428 exprt::operandst values;
429
430 // When doing the replication we extend the init_expr to the output size to
431 // compute the bitwise or. To avoid that the sign is extended too we change
432 // the type of the output to an unsigned bitvector with the same size as the
433 // output type.
435 // To avoid sign-extension during cast we first cast to an unsigned version
436 // of the same bv type, then we extend it to the output type (adding 0
437 // padding).
442
443 values.push_back(casted_init_byte_expr);
444 for(size_t i = 1; i < size; ++i)
445 {
446 values.push_back(shl_exprt(
448 from_integer(config.ansi_c.char_width * i, size_type())));
449 }
450 return cast_or_reinterpret(
451 values.size() == 1 ? values[0]
454 }
455
456 // Anything else. We don't know what to do with it. So, just cast.
458}
configt config
Definition config.cpp:25
irep_idt make_bvrep(const std::size_t width, const std::function< bool(std::size_t)> f)
construct a bit-vector representation from a functor
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
API to expression classes for bitvectors.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
bitvector_typet char_type()
Definition c_types.cpp:106
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:377
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Array constructor from list of elements.
Definition std_expr.h:1621
const array_typet & type() const
Definition std_expr.h:1628
Array constructor from single element.
Definition std_expr.h:1558
Arrays with given size.
Definition std_types.h:807
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition std_expr.h:3117
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1834
std::optional< exprt > expr_initializer_rec(const typet &type, const source_locationt &source_location, const exprt &init_expr)
const namespacet & ns
expr_initializert(const namespacet &_ns)
std::optional< exprt > operator()(const typet &type, const source_locationt &source_location, const exprt &init_expr)
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:236
const irep_idt & id() const
Definition irep.h:388
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Left shift.
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:1877
std::vector< componentt > componentst
Definition std_types.h:140
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
source_locationt & add_source_location()
Definition type.h:77
Union constructor from single element.
Definition std_expr.h:1770
The union type.
Definition c_types.h:147
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Definition std_expr.h:1734
The vector type.
Definition std_types.h:1064
exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type, const namespacet &ns)
Builds an expression of the given output type with each of its bytes initialized to the given initial...
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
static exprt cast_or_reinterpret(const exprt &expr, const typet &out_type)
Typecast the input to the output if this is a signed/unsigned bv.
std::optional< exprt > expr_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, const exprt &init_byte_expr)
Create a value for type type, with all subtype bytes initialized to the given value.
std::optional< 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.
Magic numbers used throughout the codebase.
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition magic.h:11
exprt simplify_expr(exprt src, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
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:518
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
Author: Diffblue Ltd.
#define size_type
Definition unistd.c:186
dstringt irep_idt