CBMC
c_typecheck_initializer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Conversion / Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include <util/arith_tools.h>
13 #include <util/byte_operators.h>
14 #include <util/c_types.h>
15 #include <util/config.h>
16 #include <util/cprover_prefix.h>
17 #include <util/expr_initializer.h>
18 #include <util/std_types.h>
19 #include <util/string_constant.h>
20 #include <util/symbol_table_base.h>
21 
22 #include "anonymous_member.h"
23 #include "c_typecheck_base.h"
24 #include "type2name.h"
25 
27  exprt &initializer,
28  const typet &type,
29  bool force_constant)
30 {
31  exprt result=do_initializer_rec(initializer, type, force_constant);
32 
33  if(type.id()==ID_array)
34  {
35  const typet &result_type = result.type();
36  DATA_INVARIANT(result_type.id()==ID_array &&
37  to_array_type(result_type).size().is_not_nil(),
38  "any array must have a size");
39 
40  // we don't allow initialisation with symbols of array type
41  if(
42  result.id() != ID_array && result.id() != ID_array_of &&
43  result.id() != ID_compound_literal)
44  {
46  error() << "invalid array initializer " << to_string(result)
47  << eom;
48  throw 0;
49  }
50  }
51 
52  initializer=result;
53 }
54 
57  const exprt &value,
58  const typet &type,
59  bool force_constant)
60 {
61  if(
62  (type.id() == ID_struct_tag &&
63  follow_tag(to_struct_tag_type(type)).is_incomplete()) ||
64  (type.id() == ID_union_tag &&
65  follow_tag(to_union_tag_type(type)).is_incomplete()))
66  {
68  error() << "type '" << to_string(type)
69  << "' is still incomplete -- cannot initialize" << eom;
70  throw 0;
71  }
72 
73  if(value.id()==ID_initializer_list)
74  return do_initializer_list(value, type, force_constant);
75 
76  if(
77  value.id() == ID_array && value.get_bool(ID_C_string_constant) &&
78  type.id() == ID_array &&
79  (to_array_type(type).element_type().id() == ID_signedbv ||
80  to_array_type(type).element_type().id() == ID_unsignedbv) &&
81  to_bitvector_type(to_array_type(type).element_type()).get_width() ==
83  {
84  exprt tmp=value;
85 
86  // adjust char type
89 
90  Forall_operands(it, tmp)
91  it->type() = to_array_type(type).element_type();
92 
93  if(type.id() == ID_array && to_array_type(type).is_complete())
94  {
95  const auto &array_type = to_array_type(type);
96 
97  // check size
98  const auto array_size = numeric_cast<mp_integer>(array_type.size());
99  if(!array_size.has_value())
100  {
102  error() << "array size needs to be constant, got "
103  << to_string(array_type.size()) << eom;
104  throw 0;
105  }
106 
107  if(*array_size < 0)
108  {
110  error() << "array size must not be negative" << eom;
111  throw 0;
112  }
113 
114  if(mp_integer(tmp.operands().size()) > *array_size)
115  {
116  // cut off long strings. gcc does a warning for this
117  tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size));
118  tmp.type()=type;
119  }
120  else if(mp_integer(tmp.operands().size()) < *array_size)
121  {
122  // fill up
123  tmp.type()=type;
124  const auto zero = zero_initializer(
125  array_type.element_type(), value.source_location(), *this);
126  if(!zero.has_value())
127  {
129  error() << "cannot zero-initialize array with subtype '"
130  << to_string(array_type.element_type()) << "'" << eom;
131  throw 0;
132  }
133  tmp.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
134  }
135  }
136 
137  return tmp;
138  }
139 
140  if(
141  value.id() == ID_string_constant && type.id() == ID_array &&
142  (to_array_type(type).element_type().id() == ID_signedbv ||
143  to_array_type(type).element_type().id() == ID_unsignedbv) &&
144  to_bitvector_type(to_array_type(type).element_type()).get_width() ==
145  char_type().get_width())
146  {
147  // will go away, to be replaced by the above block
148 
150  // adjust char type
151  to_array_type(tmp1.type()).element_type() =
152  to_array_type(type).element_type();
153 
154  exprt tmp2=tmp1.to_array_expr();
155 
156  if(type.id() == ID_array && to_array_type(type).is_complete())
157  {
158  // check size
159  const auto array_size =
160  numeric_cast<mp_integer>(to_array_type(type).size());
161  if(!array_size.has_value())
162  {
164  error() << "array size needs to be constant, got "
165  << to_string(to_array_type(type).size()) << eom;
166  throw 0;
167  }
168 
169  if(*array_size < 0)
170  {
172  error() << "array size must not be negative" << eom;
173  throw 0;
174  }
175 
176  if(mp_integer(tmp2.operands().size()) > *array_size)
177  {
178  // cut off long strings. gcc does a warning for this
179  tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size));
180  tmp2.type()=type;
181  }
182  else if(mp_integer(tmp2.operands().size()) < *array_size)
183  {
184  // fill up
185  tmp2.type()=type;
186  const auto zero = zero_initializer(
187  to_array_type(type).element_type(), value.source_location(), *this);
188  if(!zero.has_value())
189  {
191  error() << "cannot zero-initialize array with subtype '"
192  << to_string(to_array_type(type).element_type()) << "'"
193  << eom;
194  throw 0;
195  }
196  tmp2.operands().resize(numeric_cast_v<std::size_t>(*array_size), *zero);
197  }
198  }
199 
200  return tmp2;
201  }
202 
203  if(type.id() == ID_array && to_array_type(type).size().is_nil())
204  {
206  error() << "type '" << to_string(type) << "' cannot be initialized with '"
207  << to_string(value) << "'" << eom;
208  throw 0;
209  }
210 
211  if(value.id()==ID_designated_initializer)
212  {
214  error() << "type '" << to_string(type)
215  << "' cannot be initialized with designated initializer" << eom;
216  throw 0;
217  }
218 
219  exprt result=value;
220  implicit_typecast(result, type);
221  return result;
222 }
223 
225 {
226  // this one doesn't need initialization
227  if(symbol.name.starts_with(CPROVER_PREFIX "constant_infinity"))
228  return;
229 
230  if(symbol.is_type)
231  return;
232 
233  if(symbol.value.is_not_nil())
234  {
235  typecheck_expr(symbol.value);
236  do_initializer(symbol.value, symbol.type, true);
237 
238  // A flexible array may have been initialized, which entails a type change.
239  // Note that the type equality test is important: we want to preserve
240  // annotations like typedefs or const-ness when the type is otherwise the
241  // same.
242  if(!symbol.is_macro && symbol.type != symbol.value.type())
243  symbol.type = symbol.value.type();
244  }
245 
246  if(symbol.is_macro)
247  make_constant(symbol.value);
248 }
249 
251  const typet &type,
252  designatort &designator)
253 {
254  designatort::entryt entry(type);
255 
256  if(auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(type))
257  {
258  const struct_typet &struct_type = follow_tag(*struct_tag_type);
259 
260  entry.size=struct_type.components().size();
261  entry.subtype.make_nil();
262  // only a top-level struct may end with a variable-length array
263  entry.vla_permitted=designator.empty();
264 
265  for(const auto &c : struct_type.components())
266  {
268  c.type().id() != ID_code, "struct member must not be of code type");
269 
270  if(
271  !c.get_is_padding() &&
272  (c.type().id() != ID_c_bit_field || !c.get_anonymous()))
273  {
274  entry.subtype = c.type();
275  break;
276  }
277 
278  ++entry.index;
279  }
280  }
281  else if(auto union_tag_type = type_try_dynamic_cast<union_tag_typet>(type))
282  {
283  const union_typet &union_type = follow_tag(*union_tag_type);
284 
285  if(union_type.components().empty())
286  {
287  entry.size=0;
288  entry.subtype.make_nil();
289  }
290  else
291  {
292  // The default is to initialize using the first member of the
293  // union.
294  entry.size=1;
295  entry.subtype=union_type.components().front().type();
296  }
297  }
298  else if(type.id() == ID_array)
299  {
300  const array_typet &array_type = to_array_type(type);
301 
302  if(array_type.size().is_nil())
303  {
304  entry.size=0;
305  entry.subtype = array_type.element_type();
306  }
307  else
308  {
309  const auto array_size = numeric_cast<mp_integer>(array_type.size());
310  if(!array_size.has_value())
311  {
312  error().source_location = array_type.size().source_location();
313  error() << "array has non-constant size '"
314  << to_string(array_type.size()) << "'" << eom;
315  throw 0;
316  }
317 
318  entry.size = numeric_cast_v<std::size_t>(*array_size);
319  entry.subtype = array_type.element_type();
320  }
321  }
322  else if(type.id() == ID_vector)
323  {
324  const vector_typet &vector_type = to_vector_type(type);
325 
326  const auto vector_size = numeric_cast<mp_integer>(vector_type.size());
327 
328  if(!vector_size.has_value())
329  {
330  error().source_location = vector_type.size().source_location();
331  error() << "vector has non-constant size '"
332  << to_string(vector_type.size()) << "'" << eom;
333  throw 0;
334  }
335 
336  entry.size = numeric_cast_v<std::size_t>(*vector_size);
337  entry.subtype = vector_type.element_type();
338  }
339  else
340  UNREACHABLE;
341 
342  designator.push_entry(entry);
343 }
344 
345 exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
346  exprt &result,
347  designatort &designator,
348  const exprt &initializer_list,
349  exprt::operandst::const_iterator init_it,
350  bool force_constant)
351 {
352  // copy the value, we may need to adjust it
353  exprt value=*init_it;
354 
355  PRECONDITION(!designator.empty());
356 
357  if(value.id()==ID_designated_initializer)
358  {
359  PRECONDITION(value.operands().size() == 1);
360 
361  designator=
363  designator.front().type,
364  static_cast<const exprt &>(value.find(ID_designator)));
365 
366  CHECK_RETURN(!designator.empty());
367 
368  // discard the return value
370  result, designator, value, value.operands().begin(), force_constant);
371  return ++init_it;
372  }
373 
374  exprt *dest=&result;
375 
376  // first phase: follow given designator
377 
378  for(size_t i=0; i<designator.size(); i++)
379  {
380  size_t index=designator[i].index;
381  const typet &type=designator[i].type;
382 
383  if(type.id() == ID_array || type.id() == ID_vector)
384  {
385  // zero_initializer may have built an array_of expression for a large
386  // array; as we have a designated initializer we need to have an array of
387  // individual objects
388  if(dest->id() == ID_array_of)
389  {
390  const array_typet array_type = to_array_type(dest->type());
391  const auto array_size = numeric_cast<mp_integer>(array_type.size());
392  if(!array_size.has_value())
393  {
395  error() << "cannot zero-initialize array with element type '"
396  << to_string(to_type_with_subtype(type).subtype()) << "'"
397  << eom;
398  throw 0;
399  }
400  const exprt zero = to_array_of_expr(*dest).what();
401  *dest = array_exprt{{}, array_type};
402  dest->operands().resize(numeric_cast_v<std::size_t>(*array_size), zero);
403  }
404 
405  if(index>=dest->operands().size())
406  {
407  if(
408  type.id() == ID_array && (to_array_type(type).size().is_zero() ||
409  to_array_type(type).size().is_nil()))
410  {
411  const typet &element_type = to_array_type(type).element_type();
412 
413  // we are willing to grow an incomplete or zero-sized array --
414  // do_initializer_list will fix up the resulting type
415  const auto zero =
416  zero_initializer(element_type, value.source_location(), *this);
417  if(!zero.has_value())
418  {
420  error() << "cannot zero-initialize array with element type '"
421  << to_string(element_type) << "'" << eom;
422  throw 0;
423  }
424  dest->operands().resize(
425  numeric_cast_v<std::size_t>(index) + 1, *zero);
426  }
427  else
428  {
430  error() << "array index designator " << index
431  << " out of bounds (" << dest->operands().size()
432  << ")" << eom;
433  throw 0;
434  }
435  }
436 
437  dest = &(dest->operands()[numeric_cast_v<std::size_t>(index)]);
438  }
439  else if(
440  auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(type))
441  {
442  const struct_typet::componentst &components =
443  follow_tag(*struct_tag_type).components();
444 
445  if(index>=dest->operands().size())
446  {
448  error() << "structure member designator " << index
449  << " out of bounds (" << dest->operands().size()
450  << ")" << eom;
451  throw 0;
452  }
453 
454  DATA_INVARIANT(index<components.size(),
455  "member designator is bounded by components size");
457  components[index].type().id() != ID_code,
458  "struct member must not be of code type");
460  !components[index].get_is_padding(),
461  "member designator points at non-padding member");
462 
463  dest=&(dest->operands()[index]);
464  }
465  else if(auto union_tag_type = type_try_dynamic_cast<union_tag_typet>(type))
466  {
467  const union_typet &union_type = follow_tag(*union_tag_type);
468 
469  const union_typet::componentst &components=
470  union_type.components();
471 
472  if(components.empty())
473  {
475  error() << "union member designator found for empty union" << eom;
476  throw 0;
477  }
478  else if(init_it != initializer_list.operands().begin())
479  {
481  {
483  error() << "too many initializers" << eom;
484  throw 0;
485  }
486  else
487  {
489  warning() << "excess elements in union initializer" << eom;
490 
491  return ++init_it;
492  }
493  }
494  else if(index >= components.size())
495  {
497  error() << "union member designator " << index << " out of bounds ("
498  << components.size() << ")" << eom;
499  throw 0;
500  }
501 
502  const union_typet::componentt &component = components[index];
503 
504  if(
505  dest->id() == ID_union &&
506  to_union_expr(*dest).get_component_name() == component.get_name())
507  {
508  // Already right union component. We can initialize multiple submembers,
509  // so do not overwrite this.
510  dest = &(to_union_expr(*dest).op());
511  }
512  else if(dest->id() == ID_union)
513  {
514  // The designated initializer does not initialize the maximum member,
515  // which the (default) zero initializer prepared. Replace this by a
516  // component-specific initializer; other bytes have an unspecified value
517  // (C Standard 6.2.6.1(7)). In practice, objects of static lifetime are
518  // fully zero initialized, so we just byte-update on top of the existing
519  // zero initializer.
520  const auto zero =
521  zero_initializer(component.type(), value.source_location(), *this);
522  if(!zero.has_value())
523  {
525  error() << "cannot zero-initialize union component of type '"
526  << to_string(component.type()) << "'" << eom;
527  throw 0;
528  }
529 
531  {
532  byte_update_exprt byte_update =
533  make_byte_update(*dest, from_integer(0, c_index_type()), *zero);
534  byte_update.add_source_location() = value.source_location();
535  *dest = std::move(byte_update);
536  dest = &(to_byte_update_expr(*dest).op2());
537  }
538  else
539  {
540  union_exprt union_expr(component.get_name(), *zero, type);
541  union_expr.add_source_location() = value.source_location();
542  *dest = std::move(union_expr);
543  dest = &(to_union_expr(*dest).op());
544  }
545  }
546  else if(
547  dest->id() == ID_byte_update_big_endian ||
548  dest->id() == ID_byte_update_little_endian)
549  {
550  // handle the byte update introduced by an earlier initializer (if
551  // current_symbol.is_static_lifetime)
552  byte_update_exprt &byte_update = to_byte_update_expr(*dest);
553  dest = &byte_update.op2();
554  }
555  }
556  else
557  UNREACHABLE;
558  }
559 
560  // second phase: assign value
561  // for this, we may need to go down, adding to the designator
562 
563  while(true)
564  {
565  // see what type we have to initialize
566 
567  const typet &type=designator.back().subtype;
568 
569  // do we initialize a scalar?
570  if(
571  type.id() != ID_struct_tag && type.id() != ID_union_tag &&
572  type.id() != ID_array && type.id() != ID_vector)
573  {
574  // The initializer for a scalar shall be a single expression,
575  // * optionally enclosed in braces. *
576 
577  if(value.id()==ID_initializer_list &&
578  value.operands().size()==1)
579  {
580  *dest =
581  do_initializer_rec(to_unary_expr(value).op(), type, force_constant);
582  }
583  else
584  *dest=do_initializer_rec(value, type, force_constant);
585 
586  DATA_INVARIANT(type == dest->type(), "matching types");
587 
588  return ++init_it; // done
589  }
590 
591  // union? The component in the zero initializer might
592  // not be the first one.
593  if(auto union_tag_type = type_try_dynamic_cast<union_tag_typet>(type))
594  {
595  const union_typet &union_type = follow_tag(*union_tag_type);
596 
597  const union_typet::componentst &components=
598  union_type.components();
599 
600  if(!components.empty())
601  {
603  union_type.components().front();
604 
605  const auto zero =
606  zero_initializer(component.type(), value.source_location(), *this);
607  if(!zero.has_value())
608  {
610  error() << "cannot zero-initialize union component of type '"
611  << to_string(component.type()) << "'" << eom;
612  throw 0;
613  }
614  union_exprt union_expr(component.get_name(), *zero, type);
615  union_expr.add_source_location()=value.source_location();
616  *dest=union_expr;
617  }
618  }
619 
620  // see what initializer we are given
621  if(value.id()==ID_initializer_list)
622  {
623  *dest=do_initializer_rec(value, type, force_constant);
624  return ++init_it; // done
625  }
626  else if(value.id()==ID_string_constant)
627  {
628  // We stop for initializers that are string-constants,
629  // which are like arrays. We only do so if we are to
630  // initialize an array of scalars.
631  if(
632  type.id() == ID_array &&
633  (to_array_type(type).element_type().id() == ID_signedbv ||
634  to_array_type(type).element_type().id() == ID_unsignedbv))
635  {
636  *dest=do_initializer_rec(value, type, force_constant);
637  return ++init_it; // done
638  }
639  }
640  else if(value.type() == type)
641  {
642  // a struct/union/vector can be initialized directly with
643  // an expression of the right type. This doesn't
644  // work with arrays, unfortunately.
645  if(
646  type.id() == ID_struct_tag || type.id() == ID_union_tag ||
647  type.id() == ID_vector)
648  {
649  *dest=value;
650  return ++init_it; // done
651  }
652  }
653 
655  type.id() == ID_struct_tag || type.id() == ID_union_tag ||
656  type.id() == ID_array || type.id() == ID_vector,
657  "full type must be composite");
658 
659  // we are initializing a compound type, and enter it!
660  // this may change the type, type might not be valid any more
661  const typet dest_type = type;
662  const bool vla_permitted=designator.back().vla_permitted;
663  designator_enter(type, designator);
664 
665  // GCC permits (though issuing a warning with -Wall) composite
666  // types built from flat initializer lists
667  if(dest->operands().empty())
668  {
670  warning() << "initialisation of " << dest_type.id()
671  << " requires initializer list, found " << value.id()
672  << " instead" << eom;
673 
674  // in case of a variable-length array consume all remaining
675  // initializer elements
676  if(vla_permitted &&
677  dest_type.id()==ID_array &&
678  (to_array_type(dest_type).size().is_zero() ||
679  to_array_type(dest_type).size().is_nil()))
680  {
681  value.id(ID_initializer_list);
682  value.operands().clear();
683  for( ; init_it!=initializer_list.operands().end(); ++init_it)
684  value.copy_to_operands(*init_it);
685  *dest=do_initializer_rec(value, dest_type, force_constant);
686 
687  return init_it;
688  }
689  else
690  {
692  error() << "cannot initialize type '" << to_string(dest_type)
693  << "' using value '" << to_string(value) << "'" << eom;
694  throw 0;
695  }
696  }
697 
698  dest = &(to_multi_ary_expr(*dest).op0());
699 
700  // we run into another loop iteration
701  }
702 
703  return ++init_it;
704 }
705 
707 {
708  PRECONDITION(!designator.empty());
709 
710  while(true)
711  {
712  designatort::entryt &entry=designator[designator.size()-1];
713 
714  entry.index++;
715 
716  if(entry.type.id() == ID_array && to_array_type(entry.type).size().is_nil())
717  return; // we will keep going forever
718 
719  if(entry.type.id() == ID_struct_tag && entry.index < entry.size)
720  {
721  // need to adjust subtype
722  const struct_typet &struct_type =
724  const struct_typet::componentst &components=
725  struct_type.components();
727  components.size() == entry.size, "matching component numbers");
728 
729  // we skip over any padding
730  // we also skip over anonymous members that are bit fields
731  while(entry.index < entry.size &&
732  (components[entry.index].get_is_padding() ||
733  (components[entry.index].get_anonymous() &&
734  components[entry.index].type().id() == ID_c_bit_field)))
735  {
736  entry.index++;
737  }
738 
739  if(entry.index<entry.size)
740  entry.subtype=components[entry.index].type();
741  }
742 
743  if(entry.index<entry.size)
744  return; // done
745 
746  if(designator.size()==1)
747  return; // done
748 
749  // pop entry
750  designator.pop_entry();
751 
752  INVARIANT(!designator.empty(), "designator had more than one entry");
753  }
754 }
755 
757  const typet &src_type,
758  const exprt &src)
759 {
760  PRECONDITION(!src.operands().empty());
761 
762  typet type=src_type;
763  designatort designator;
764 
765  for(const auto &d_op : src.operands())
766  {
767  designatort::entryt entry(type);
768 
769  if(entry.type.id() == ID_array)
770  {
771  if(d_op.id()!=ID_index)
772  {
773  error().source_location = d_op.source_location();
774  error() << "expected array index designator" << eom;
775  throw 0;
776  }
777 
778  exprt tmp_index = to_unary_expr(d_op).op();
779  make_constant_index(tmp_index);
780 
781  mp_integer index, size;
782 
783  if(to_integer(to_constant_expr(tmp_index), index))
784  {
786  error() << "expected constant array index designator" << eom;
787  throw 0;
788  }
789 
790  if(to_array_type(entry.type).size().is_nil())
791  size=0;
792  else if(
793  const auto size_opt =
794  numeric_cast<mp_integer>(to_array_type(entry.type).size()))
795  size = *size_opt;
796  else
797  {
799  error() << "expected constant array size" << eom;
800  throw 0;
801  }
802 
803  entry.index = numeric_cast_v<std::size_t>(index);
804  entry.size = numeric_cast_v<std::size_t>(size);
805  entry.subtype = to_array_type(entry.type).element_type();
806  }
807  else if(
808  auto struct_union_tag_type =
809  type_try_dynamic_cast<struct_or_union_tag_typet>(entry.type))
810  {
811  const struct_union_typet &struct_union_type =
812  follow_tag(*struct_union_tag_type);
813 
814  if(d_op.id()!=ID_member)
815  {
816  error().source_location = d_op.source_location();
817  error() << "expected member designator" << eom;
818  throw 0;
819  }
820 
821  const irep_idt &component_name=d_op.get(ID_component_name);
822 
823  if(struct_union_type.has_component(component_name))
824  {
825  // a direct member
826  entry.index=struct_union_type.component_number(component_name);
827  entry.size=struct_union_type.components().size();
828  entry.subtype=struct_union_type.components()[entry.index].type();
829  }
830  else
831  {
832  // We will search for anonymous members, in a loop. This isn't supported
833  // by GCC (unless the anonymous member is within an unnamed union or
834  // struct), but Visual Studio does allow it.
835 
836  bool found=false, repeat;
837  typet tmp_type=entry.type;
838 
839  do
840  {
841  repeat=false;
842  std::size_t number = 0;
843  const struct_union_typet::componentst &components =
845 
846  for(const auto &c : components)
847  {
848  if(c.get_name() == component_name)
849  {
850  // done!
851  entry.index=number;
852  entry.size=components.size();
853  entry.subtype = c.type();
854  entry.type=tmp_type;
855  }
856  else if(
857  c.get_anonymous() &&
858  (c.type().id() == ID_struct_tag ||
859  c.type().id() == ID_union_tag) &&
860  (config.ansi_c.mode ==
863  .find(ID_tag)
864  .is_nil()) &&
865  has_component_rec(c.type(), component_name, *this))
866  {
867  entry.index=number;
868  entry.size=components.size();
869  entry.subtype = c.type();
870  entry.type=tmp_type;
871  tmp_type=entry.subtype;
872  designator.push_entry(entry);
873  found=repeat=true;
874  break;
875  }
876 
877  ++number;
878  }
879  }
880  while(repeat);
881 
882  if(!found)
883  {
884  error().source_location = d_op.source_location();
885  error() << "failed to find struct component '" << component_name
886  << "' in initialization of '" << to_string(struct_union_type)
887  << "'" << eom;
888  throw 0;
889  }
890  }
891  }
892  else
893  {
894  error().source_location = d_op.source_location();
895  error() << "designated initializers cannot initialize '"
896  << to_string(entry.type) << "'" << eom;
897  throw 0;
898  }
899 
900  type=entry.subtype;
901  designator.push_entry(entry);
902  }
903 
904  INVARIANT(!designator.empty(), "expected an entry to be added");
905 
906  return designator;
907 }
908 
910  const exprt &value,
911  const typet &type,
912  bool force_constant)
913 {
914  PRECONDITION(value.id() == ID_initializer_list);
915 
916  // 6.7.9, 14: An array of character type may be initialized by a character
917  // string literal or UTF-8 string literal, optionally enclosed in braces.
918  if(
919  type.id() == ID_array && value.operands().size() >= 1 &&
920  to_multi_ary_expr(value).op0().id() == ID_string_constant &&
921  (to_array_type(type).element_type().id() == ID_signedbv ||
922  to_array_type(type).element_type().id() == ID_unsignedbv) &&
923  to_bitvector_type(to_array_type(type).element_type()).get_width() ==
924  char_type().get_width())
925  {
926  if(value.operands().size() > 1)
927  {
929  warning() << "ignoring excess initializers" << eom;
930  }
931 
932  return do_initializer_rec(
933  to_multi_ary_expr(value).op0(), type, force_constant);
934  }
935 
936  exprt result;
937  if(
938  type.id() == ID_struct_tag || type.id() == ID_union_tag ||
939  type.id() == ID_vector)
940  {
941  // start with zero everywhere
942  const auto zero = zero_initializer(type, value.source_location(), *this);
943  if(!zero.has_value())
944  {
946  error() << "cannot zero-initialize '" << to_string(type) << "'" << eom;
947  throw 0;
948  }
949  result = *zero;
950  }
951  else if(type.id() == ID_array)
952  {
953  if(to_array_type(type).size().is_nil())
954  {
955  // start with empty array
956  result = array_exprt({}, to_array_type(type));
957  result.add_source_location()=value.source_location();
958  }
959  else
960  {
961  // start with zero everywhere
962  const auto zero = zero_initializer(type, value.source_location(), *this);
963  if(!zero.has_value())
964  {
966  error() << "cannot zero-initialize '" << to_string(type) << "'" << eom;
967  throw 0;
968  }
969  result = *zero;
970  }
971  }
972  else if(type.id() == ID_complex)
973  {
974  // These may be initialized with an expression, an initializer list
975  // of size two, or an initializer list of size one.
976  if(value.operands().size() == 1)
977  {
978  return do_initializer_rec(
979  to_unary_expr(value).op(), type, force_constant);
980  }
981  else if(value.operands().size() == 2)
982  {
983  auto &complex_type = to_complex_type(type);
984  auto &subtype = complex_type.subtype();
985  auto real = do_initializer_rec(
986  to_binary_expr(value).op0(), subtype, force_constant);
987  auto imag = do_initializer_rec(
988  to_binary_expr(value).op1(), subtype, force_constant);
989  return complex_exprt(real, imag, complex_type)
991  }
992  else
993  {
994  throw errort().with_location(value.source_location())
995  << "too many initializers for '" << to_string(type) << "'";
996  }
997  }
998  else
999  {
1000  // The initializer for a scalar shall be a single expression,
1001  // * optionally enclosed in braces. *
1002 
1003  if(value.operands().size()==1)
1004  return do_initializer_rec(
1005  to_unary_expr(value).op(), type, force_constant);
1006 
1008  error() << "cannot initialize '" << to_string(type)
1009  << "' with an initializer list" << eom;
1010  throw 0;
1011  }
1012 
1013  designatort current_designator;
1014 
1015  designator_enter(type, current_designator);
1016 
1017  const exprt::operandst &operands=value.operands();
1018  for(exprt::operandst::const_iterator it=operands.begin();
1019  it!=operands.end(); ) // no ++it
1020  {
1022  result, current_designator, value, it, force_constant);
1023 
1024  // increase designator -- might go up
1025  increment_designator(current_designator);
1026  }
1027 
1028  if(auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(type))
1029  {
1030  const struct_typet &full_struct_type = follow_tag(*struct_tag_type);
1031  const struct_typet::componentst &components = full_struct_type.components();
1032  // make sure we didn't mess up index computation
1033  CHECK_RETURN(result.operands().size() == components.size());
1034 
1035  if(
1036  !components.empty() &&
1037  components.back().type().get_bool(ID_C_flexible_array_member))
1038  {
1039  const auto array_size = numeric_cast<mp_integer>(
1040  to_array_type(components.back().type()).size());
1041  array_exprt &init_array = to_array_expr(result.operands().back());
1042  if(
1043  !array_size.has_value() ||
1044  (*array_size <= 1 && init_array.operands().size() != *array_size))
1045  {
1046  struct_typet actual_struct_type = full_struct_type;
1047  array_typet &actual_array_type =
1048  to_array_type(actual_struct_type.components().back().type());
1049  actual_array_type.size() = from_integer(
1050  init_array.operands().size(), actual_array_type.index_type());
1051  actual_array_type.set(ID_C_flexible_array_member, true);
1052  init_array.type() = actual_array_type;
1053 
1054  // mimic bits of typecheck_compound_type to produce a new struct tag
1055  actual_struct_type.remove(ID_tag);
1056  std::string typestr = type2name(actual_struct_type, *this);
1057  irep_idt tag_identifier = "tag-#anon#" + typestr;
1058  type_symbolt compound_symbol{tag_identifier, actual_struct_type, mode};
1059  compound_symbol.base_name = "#anon#" + typestr;
1060  compound_symbol.location = value.source_location();
1061 
1062  // We might already have the same anonymous struct, which is fine as it
1063  // will be exactly the same type.
1064  symbol_table.insert(std::move(compound_symbol));
1065 
1066  result.type() = struct_tag_typet{tag_identifier};
1067  }
1068  }
1069  }
1070 
1071  if(type.id() == ID_array && to_array_type(type).size().is_nil())
1072  {
1073  // make complete by setting array size
1074  array_typet &array_type = to_array_type(result.type());
1075  array_type.size() =
1076  from_integer(result.operands().size(), array_type.index_type());
1077  }
1078 
1079  return result;
1080 }
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
configt config
Definition: config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
byte_update_exprt make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
Construct a byte_update_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
ANSI-C Language Type Checking.
bitvector_typet char_type()
Definition: c_types.cpp:106
bitvector_typet c_index_type()
Definition: c_types.cpp:16
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
Array constructor from list of elements.
Definition: std_expr.h:1621
const array_typet & type() const
Definition: std_expr.h:1628
exprt & what()
Definition: std_expr.h:1575
Arrays with given size.
Definition: std_types.h:807
typet index_type() const
The type of the index expressions into any instance of this type.
Definition: std_types.cpp:34
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:925
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
symbol_table_baset & symbol_table
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type ‘type’ with given value ‘value’
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
const irep_idt mode
virtual void make_constant(exprt &expr)
virtual std::string to_string(const exprt &expr)
void increment_designator(designatort &designator)
virtual exprt::operandst::const_iterator do_designated_initializer(exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant)
virtual void make_constant_index(exprt &expr)
designatort make_designator(const typet &type, const exprt &src)
void designator_enter(const typet &type, designatort &designator)
Complex constructor from a pair of numbers.
Definition: std_expr.h:1916
struct configt::ansi_ct ansi_c
const entryt & front() const
Definition: designator.h:41
size_t size() const
Definition: designator.h:37
void push_entry(const entryt &entry)
Definition: designator.h:45
const entryt & back() const
Definition: designator.h:40
bool empty() const
Definition: designator.h:36
void pop_entry()
Definition: designator.h:50
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition: dstring.h:95
Base class for all expressions.
Definition: expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:147
std::vector< exprt > operandst
Definition: expr.h:58
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition: expr.h:101
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:163
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
void remove(const irep_idt &name)
Definition: irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void make_nil()
Definition: irep.h:446
bool is_nil() const
Definition: irep.h:368
source_locationt source_location
Definition: message.h:239
mstreamt & error() const
Definition: message.h:391
mstreamt & warning() const
Definition: message.h:396
mstreamt & result() const
Definition: message.h:401
static eomt eom
Definition: message.h:289
exprt & op0()
Definition: std_expr.h:932
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
const array_typet & type() const
array_exprt to_array_expr() const
convert string into array constant
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Base type for structs and unions.
Definition: std_types.h:62
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
const componentst & components() const
Definition: std_types.h:147
std::size_t component_number(const irep_idt &component_name) const
Return the sequence number of the component with given name.
Definition: std_types.cpp:47
std::vector< componentt > componentst
Definition: std_types.h:140
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
bool is_macro
Definition: symbol.h:62
bool is_static_lifetime
Definition: symbol.h:70
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
exprt & op2()
Definition: expr.h:139
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:139
errort with_location(source_locationt _location) &&
Definition: typecheck.h:47
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
Union constructor from single element.
Definition: std_expr.h:1770
irep_idt get_component_name() const
Definition: std_expr.h:1778
The union type.
Definition: c_types.h:147
The vector type.
Definition: std_types.h:1061
const constant_exprt & size() const
Definition: std_types.cpp:286
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1077
#define CPROVER_PREFIX
#define Forall_operands(it, expr)
Definition: expr.h:27
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#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
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:97
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3050
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1665
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1816
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:987
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1603
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1113
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:1155
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 struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition: std_types.h:478
const string_constantt & to_string_constant(const exprt &expr)
flavourt mode
Definition: config.h:256
Author: Diffblue Ltd.
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:82
Type Naming for C.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208