CBMC
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 "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 {
27 public:
28  explicit expr_initializert(const namespacet &_ns) : ns(_ns)
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 
40 protected:
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 
56  if(type_id==ID_unsignedbv ||
57  type_id==ID_signedbv ||
58  type_id==ID_pointer ||
59  type_id==ID_c_enum ||
60  type_id==ID_c_bit_field ||
61  type_id==ID_bool ||
62  type_id==ID_c_bool ||
63  type_id==ID_floatbv ||
64  type_id==ID_fixedbv)
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 ||
78  type_id==ID_real)
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  }
91  else if(type_id==ID_verilog_signedbv ||
92  type_id==ID_verilog_unsignedbv)
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  {
117  auto sub_zero = expr_initializer_rec(
118  to_complex_type(type).subtype(), source_location, init_expr);
119  if(!sub_zero.has_value())
120  return {};
121 
122  result = complex_exprt(*sub_zero, *sub_zero, to_complex_type(type));
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  {
132  const array_typet &array_type=to_array_type(type);
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  {
145  auto tmpval = expr_initializer_rec(
146  array_type.element_type(), source_location, init_expr);
147  if(!tmpval.has_value())
148  return {};
149 
150  const auto array_size = numeric_cast<mp_integer>(array_type.size());
151  if(
152  array_type.size().id() == ID_infinity || !array_size.has_value() ||
153  *array_size > MAX_FLATTENED_ARRAY_SIZE)
154  {
155  if(init_expr.id() == ID_nondet)
156  return side_effect_expr_nondett(type, source_location);
157 
158  array_of_exprt value(*tmpval, array_type);
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(
168  numeric_cast_v<std::size_t>(*array_size), *tmpval);
169  value.add_source_location()=source_location;
170  return std::move(value);
171  }
172  }
173  else if(type_id==ID_vector)
174  {
175  const vector_typet &vector_type=to_vector_type(type);
176 
177  auto tmpval = expr_initializer_rec(
178  vector_type.element_type(), source_location, init_expr);
179  if(!tmpval.has_value())
180  return {};
181 
182  const mp_integer vector_size =
183  numeric_cast_v<mp_integer>(vector_type.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 
235  auto component_value = expr_initializer_rec(
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 
308 std::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 
324 std::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 
340 std::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 
354 static 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(
362  can_cast_type<signedbv_typet>(out_type) ||
364  {
365  return typecast_exprt::conditional_cast(expr, out_type);
366  }
367  return make_byte_extract(expr, from_integer(0, char_type()), out_type);
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 =
387  type_try_dynamic_cast<bitvector_typet>(init_byte_expr.type());
388  // Fail if `init_byte_expr` is not a bitvector of maximum 8 bits or a boolean.
389  PRECONDITION(
390  (init_type_as_bitvector &&
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
395  const auto simplified_init_expr = simplify_expr(init_byte_expr, ns);
396  if(const auto output_bv = type_try_dynamic_cast<bitvector_typet>(output_type))
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 =
407  to_constant_expr(simplified_init_expr).get_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 &&
418  get_bvrep_bit(init_value, init_size, source_index);
419  });
420 
421  return constant_exprt{output_value, output_type};
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.
434  typet operation_type = unsignedbv_typet{output_bv->get_width()};
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).
438  const exprt casted_init_byte_expr = typecast_exprt::conditional_cast(
440  init_byte_expr, unsignedbv_typet{init_type_as_bitvector->get_width()}),
441  operation_type);
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(
447  casted_init_byte_expr,
449  }
450  return cast_or_reinterpret(
451  values.size() == 1 ? values[0]
452  : multi_ary_exprt(ID_bitor, values, operation_type),
453  output_type);
454  }
455 
456  // Anything else. We don't know what to do with it. So, just cast.
457  return typecast_exprt::conditional_cast(init_byte_expr, output_type);
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.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_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 union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:184
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
Array constructor from list of elements.
Definition: std_expr.h:1616
const array_typet & type() const
Definition: std_expr.h:1623
Array constructor from single element.
Definition: std_expr.h:1553
Arrays with given size.
Definition: std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & size() const
Definition: std_types.h:840
std::size_t get_width() const
Definition: std_types.h:920
Complex constructor from a pair of numbers.
Definition: std_expr.h:1911
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2987
const irep_idt & get_value() const
Definition: std_expr.h:2995
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:1829
std::optional< exprt > expr_initializer_rec(const typet &type, const source_locationt &source_location, const exprt &init_expr)
std::optional< exprt > operator()(const typet &type, const source_locationt &source_location, const exprt &init_expr)
const namespacet & ns
expr_initializert(const namespacet &_ns)
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
source_locationt & add_source_location()
Definition: expr.h:236
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
const irep_idt & id() const
Definition: irep.h:384
bool is_nil() const
Definition: irep.h:364
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:912
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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:1872
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
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:1765
The union type.
Definition: c_types.h:147
std::optional< 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:300
Fixed-width bit-vector with unsigned binary interpretation.
Vector constructor from list of elements.
Definition: std_expr.h:1729
The vector type.
Definition: std_types.h:1052
const constant_exprt & size() const
Definition: std_types.cpp:270
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1068
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...
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 > 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...
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
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.
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)
BigInt mp_integer
Definition: smt_terms.h:17
#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:3037
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1104
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:888
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1146
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
std::size_t char_width
Definition: config.h:140
Author: Diffblue Ltd.
#define size_type
Definition: unistd.c:347
dstringt irep_idt