cprover
cpp_typecheck_constructor.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_typecheck.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/std_code.h>
16 #include <util/std_expr.h>
17 
18 #include <util/c_types.h>
19 
20 #include "cpp_util.h"
21 
25 static void copy_parent(
26  const source_locationt &source_location,
27  const irep_idt &parent_base_name,
28  const irep_idt &arg_name,
29  exprt &block)
30 {
31  block.operands().push_back(codet());
32 
33  codet &code=to_code(block.operands().back());
34  code.add_source_location()=source_location;
35 
36  code.set_statement(ID_assign);
37  code.operands().push_back(exprt(ID_dereference));
38 
39  code.op0().operands().push_back(exprt("explicit-typecast"));
40 
41  exprt &op0=code.op0().op0();
42 
43  op0.operands().push_back(exprt("cpp-this"));
44  op0.type()=
45  pointer_type(cpp_namet(parent_base_name, source_location).as_type());
46  op0.add_source_location()=source_location;
47 
48  code.operands().push_back(exprt("explicit-typecast"));
49  exprt &op1=code.op1();
50 
51  op1.type() =
52  pointer_type(cpp_namet(parent_base_name, source_location).as_type());
53  op1.type().set(ID_C_reference, true);
54  op1.type().subtype().set(ID_C_constant, true);
55 
56  op1.operands().push_back(exprt(ID_cpp_name));
57  op1.op0().get_sub().push_back(irept(ID_name));
58  op1.op0().get_sub().back().set(ID_identifier, arg_name);
59  op1.op0().get_sub().back().set(ID_C_source_location, source_location);
60  op1.add_source_location()=source_location;
61 }
62 
66 static void copy_member(
67  const source_locationt &source_location,
68  const irep_idt &member_base_name,
69  const irep_idt &arg_name,
70  exprt &block)
71 {
72  block.operands().push_back(exprt(ID_code));
73  exprt &code=block.operands().back();
74 
75  code.set(ID_statement, ID_expression);
76  code.add(ID_type)=typet(ID_code);
77  code.operands().push_back(exprt(ID_side_effect));
78  code.op0().set(ID_statement, ID_assign);
79  code.op0().operands().push_back(exprt(ID_cpp_name));
80  code.add_source_location()=source_location;
81 
82  exprt &op0=code.op0().op0();
83  op0.add_source_location()=source_location;
84 
85  op0.get_sub().push_back(irept(ID_name));
86  op0.get_sub().back().set(ID_identifier, member_base_name);
87  op0.get_sub().back().set(ID_C_source_location, source_location);
88 
89  code.op0().operands().push_back(exprt(ID_member));
90 
91  exprt &op1=code.op0().op1();
92 
93  op1.add(ID_component_cpp_name).id(ID_cpp_name);
94  op1.add(ID_component_cpp_name).get_sub().push_back(irept(ID_name));
95  op1.add(ID_component_cpp_name).get_sub().back().set(
96  ID_identifier, member_base_name);
97  op1.add(ID_component_cpp_name).get_sub().back().set(
98  ID_C_source_location, source_location);
99 
100  op1.operands().push_back(exprt(ID_cpp_name));
101  op1.op0().get_sub().push_back(irept(ID_name));
102  op1.op0().get_sub().back().set(ID_identifier, arg_name);
103  op1.op0().get_sub().back().set(ID_C_source_location, source_location);
104  op1.add_source_location()=source_location;
105 }
106 
111 static void copy_array(
112  const source_locationt &source_location,
113  const irep_idt &member_base_name,
114  mp_integer i,
115  const irep_idt &arg_name,
116  exprt &block)
117 {
118  // Build the index expression
119  exprt constant=from_integer(i, index_type());
120 
121  block.operands().push_back(exprt(ID_code));
122  exprt &code=block.operands().back();
123  code.add_source_location()=source_location;
124 
125  code.set(ID_statement, ID_expression);
126  code.add(ID_type)=typet(ID_code);
127  code.operands().push_back(exprt(ID_side_effect));
128  code.op0().set(ID_statement, ID_assign);
129  code.op0().operands().push_back(exprt(ID_index));
130  exprt &op0=code.op0().op0();
131  op0.operands().push_back(exprt(ID_cpp_name));
132  op0.add_source_location()=source_location;
133 
134  op0.op0().get_sub().push_back(irept(ID_name));
135  op0.op0().get_sub().back().set(ID_identifier, member_base_name);
136  op0.op0().get_sub().back().set(ID_C_source_location, source_location);
137  op0.copy_to_operands(constant);
138 
139  code.op0().operands().push_back(exprt(ID_index));
140 
141  exprt &op1=code.op0().op1();
142  op1.operands().push_back(exprt(ID_member));
143  op1.op0().add(ID_component_cpp_name).id(ID_cpp_name);
144  op1.op0().add(ID_component_cpp_name).get_sub().push_back(irept(ID_name));
145  op1.op0().add(ID_component_cpp_name).get_sub().back().set(
146  ID_identifier, member_base_name);
147  op1.op0().add(ID_component_cpp_name).get_sub().back().set(
148  ID_C_source_location, source_location);
149 
150  op1.op0().operands().push_back(exprt(ID_cpp_name));
151  op1.op0().op0().get_sub().push_back(irept(ID_name));
152  op1.op0().op0().get_sub().back().set(ID_identifier, arg_name);
153  op1.op0().op0().get_sub().back().set(ID_C_source_location, source_location);
154  op1.copy_to_operands(constant);
155 
156  op1.add_source_location()=source_location;
157 }
158 
161  const source_locationt &source_location,
162  const irep_idt &base_name,
163  cpp_declarationt &ctor) const
164 {
165  exprt name(ID_name);
166  name.set(ID_identifier, base_name);
167  name.add_source_location()=source_location;
168 
169  cpp_declaratort decl;
170  decl.name().id(ID_cpp_name);
171  decl.name().move_to_sub(name);
172  decl.type()=typet(ID_function_type);
173  decl.type().subtype().make_nil();
174  decl.add_source_location()=source_location;
175 
176  decl.value().id(ID_code);
177  decl.value().type()=typet(ID_code);
178  decl.value().set(ID_statement, ID_block);
179  decl.add("cv").make_nil();
180  decl.add("throw_decl").make_nil();
181 
182  ctor.type().id(ID_constructor);
183  ctor.add(ID_storage_spec).id(ID_cpp_storage_spec);
184  ctor.move_to_operands(decl);
185  ctor.add_source_location()=source_location;
186 }
187 
190  const symbolt &symbol,
191  cpp_declarationt &cpctor) const
192 {
193  source_locationt source_location=symbol.type.source_location();
194 
195  source_location.set_function(
196  id2string(symbol.base_name)+
197  "::"+id2string(symbol.base_name)+
198  "(const "+id2string(symbol.base_name)+" &)");
199 
200  // Produce default constructor first
201  default_ctor(source_location, symbol.base_name, cpctor);
202  cpp_declaratort &decl0=cpctor.declarators()[0];
203 
204  std::string param_identifier("ref");
205 
206  // Compound name
207  irept comp_name(ID_name);
208  comp_name.set(ID_identifier, symbol.base_name);
209  comp_name.set(ID_C_source_location, source_location);
210 
211  cpp_namet cppcomp;
212  cppcomp.move_to_sub(comp_name);
213 
214  // Parameter name
215  exprt param_name(ID_name);
216  param_name.add_source_location()=source_location;
217  param_name.set(ID_identifier, param_identifier);
218 
219  cpp_namet cpp_parameter;
220  cpp_parameter.move_to_sub(param_name);
221 
222  // Parameter declarator
223  cpp_declaratort parameter_tor;
224  parameter_tor.add(ID_value).make_nil();
225  parameter_tor.set(ID_name, cpp_parameter);
226  parameter_tor.type()=reference_type(nil_typet());
227  parameter_tor.add_source_location()=source_location;
228 
229  // Parameter declaration
230  cpp_declarationt parameter_decl;
231  parameter_decl.set(ID_type, ID_merged_type);
232  typet::subtypest &sub=parameter_decl.type().subtypes();
233  sub.push_back(
234  static_cast<const typet &>(static_cast<const irept &>(cppcomp)));
235  irept constnd(ID_const);
236  sub.push_back(static_cast<const typet &>(constnd));
237  parameter_decl.move_to_operands(parameter_tor);
238  parameter_decl.add_source_location()=source_location;
239 
240  // Add parameter to function type
241  decl0.add(ID_type).add(ID_parameters).get_sub().push_back(parameter_decl);
242  decl0.add_source_location()=source_location;
243 
244  irept &initializers=decl0.add(ID_member_initializers);
245  initializers.id(ID_member_initializers);
246 
247  cpp_declaratort &declarator=static_cast<cpp_declaratort &>(cpctor.op0());
248  exprt &block=declarator.value();
249 
250  // First, we need to call the parent copy constructors
251  const irept &bases=symbol.type.find(ID_bases);
252  forall_irep(parent_it, bases.get_sub())
253  {
254  assert(parent_it->id()==ID_base);
255  assert(parent_it->get(ID_type)==ID_symbol);
256 
257  const symbolt &parsymb=
258  lookup(parent_it->find(ID_type).get(ID_identifier));
259 
260  if(cpp_is_pod(parsymb.type))
261  copy_parent(source_location, parsymb.base_name, param_identifier, block);
262  else
263  {
264  irep_idt ctor_name=parsymb.base_name;
265 
266  // Call the parent default copy constructor
267  exprt name(ID_name);
268  name.set(ID_identifier, ctor_name);
269  name.add_source_location()=source_location;
270 
271  cpp_namet cppname;
272  cppname.move_to_sub(name);
273 
274  codet mem_init(ID_member_initializer);
275  mem_init.add_source_location()=source_location;
276  mem_init.set(ID_member, cppname);
277  mem_init.copy_to_operands(
278  static_cast<const exprt &>(static_cast<const irept &>(cpp_parameter)));
279  initializers.move_to_sub(mem_init);
280  }
281  }
282 
283  // Then, we add the member initializers
284  const struct_typet::componentst &components=
285  to_struct_type(symbol.type).components();
286  for(struct_typet::componentst::const_iterator mem_it=components.begin();
287  mem_it!=components.end(); mem_it++)
288  {
289  // Take care of virtual tables
290  if(mem_it->get_bool("is_vtptr"))
291  {
292  exprt name(ID_name);
293  name.set(ID_identifier, mem_it->get(ID_base_name));
294  name.add_source_location()=source_location;
295 
296  cpp_namet cppname;
297  cppname.move_to_sub(name);
298 
299  const symbolt &virtual_table_symbol_type =
300  lookup(mem_it->type().subtype().get(ID_identifier));
301 
302  const symbolt &virtual_table_symbol_var = lookup(
303  id2string(virtual_table_symbol_type.name) + "@" +
304  id2string(symbol.name));
305 
306  exprt var=virtual_table_symbol_var.symbol_expr();
307  address_of_exprt address(var);
308  assert(address.type()==mem_it->type());
309 
310  already_typechecked(address);
311 
312  exprt ptrmember(ID_ptrmember);
313  ptrmember.set(ID_component_name, mem_it->get(ID_name));
314  ptrmember.operands().push_back(exprt("cpp-this"));
315 
316  code_assignt assign(ptrmember, address);
317  initializers.move_to_sub(assign);
318  continue;
319  }
320 
321  if( mem_it->get_bool("from_base")
322  || mem_it->get_bool(ID_is_type)
323  || mem_it->get_bool(ID_is_static)
324  || mem_it->type().id()==ID_code)
325  continue;
326 
327  irep_idt mem_name=mem_it->get(ID_base_name);
328 
329  exprt name(ID_name);
330  name.set(ID_identifier, mem_name);
331  name.add_source_location()=source_location;
332 
333  cpp_namet cppname;
334  cppname.move_to_sub(name);
335 
336  codet mem_init(ID_member_initializer);
337  mem_init.set(ID_member, cppname);
338  mem_init.add_source_location()=source_location;
339 
340  exprt memberexpr(ID_member);
341  memberexpr.set(ID_component_cpp_name, cppname);
342  memberexpr.copy_to_operands(
343  static_cast<const exprt &>(static_cast<const irept &>(cpp_parameter)));
344  memberexpr.add_source_location()=source_location;
345 
346  if(mem_it->type().id()==ID_array)
347  memberexpr.set("#array_ini", true);
348 
349  mem_init.move_to_operands(memberexpr);
350  initializers.move_to_sub(mem_init);
351  }
352 }
353 
356  const symbolt &symbol,
357  cpp_declarationt &cpctor)
358 {
359  source_locationt source_location=symbol.type.source_location();
360 
361  source_location.set_function(
362  id2string(symbol.base_name)
363  + "& "+
364  id2string(symbol.base_name)+
365  "::operator=( const "+id2string(symbol.base_name)+"&)");
366 
367  std::string arg_name("ref");
368 
369  cpctor.add(ID_storage_spec).id(ID_cpp_storage_spec);
370  cpctor.type().id(ID_symbol);
371  cpctor.type().add(ID_identifier).id(symbol.name);
372  cpctor.operands().push_back(exprt(ID_cpp_declarator));
373  cpctor.add_source_location()=source_location;
374 
375  cpp_declaratort &declarator=(cpp_declaratort&) cpctor.op0();
376  declarator.add_source_location()=source_location;
377 
378  cpp_namet &declarator_name=declarator.name();
379  typet &declarator_type=declarator.type();
380 
381  declarator_type.add_source_location()=source_location;
382 
383  declarator_name.id(ID_cpp_name);
384  declarator_name.get_sub().push_back(irept(ID_operator));
385  declarator_name.get_sub().push_back(irept("="));
386 
387  declarator_type.id(ID_function_type);
388  declarator_type.subtype()=reference_type(nil_typet());
389  declarator_type.subtype().add("#qualifier").make_nil();
390 
391  exprt &args=static_cast<exprt&>(declarator.type().add(ID_parameters));
392  args.add_source_location()=source_location;
393 
394  args.get_sub().push_back(irept(ID_cpp_declaration));
395 
396  cpp_declarationt &args_decl=
397  static_cast<cpp_declarationt&>(args.get_sub().back());
398 
399  typet::subtypest &args_decl_type_sub=args_decl.type().subtypes();
400 
401  args_decl.type().id(ID_merged_type);
402  args_decl_type_sub.push_back(typet(ID_cpp_name));
403  args_decl_type_sub.back().get_sub().push_back(irept(ID_name));
404  args_decl_type_sub.back().get_sub().back().set(
405  ID_identifier, symbol.base_name);
406  args_decl_type_sub.back().get_sub().back().set(
407  ID_C_source_location, source_location);
408 
409  args_decl_type_sub.push_back(typet(ID_const));
410  args_decl.operands().push_back(exprt(ID_cpp_declarator));
411  args_decl.add_source_location()=source_location;
412 
413  cpp_declaratort &args_decl_declor=
414  static_cast<cpp_declaratort&>(args_decl.operands().back());
415 
416  args_decl_declor.name().id(ID_cpp_name);
417  args_decl_declor.name().get_sub().push_back(irept(ID_name));
418  args_decl_declor.name().get_sub().back().add(ID_identifier).id(arg_name);
419  args_decl_declor.add_source_location()=source_location;
420 
421  args_decl_declor.type()=pointer_type(typet(ID_nil));
422  args_decl_declor.type().set(ID_C_reference, true);
423  args_decl_declor.value().make_nil();
424 }
425 
428  const symbolt &symbol,
429  cpp_declaratort &declarator)
430 {
431  // save source location
432  source_locationt source_location=declarator.source_location();
433  declarator.make_nil();
434 
435  declarator.value().add_source_location()=source_location;
436  declarator.value().id(ID_code);
437  declarator.value().set(ID_statement, ID_block);
438  declarator.value().type()=code_typet();
439 
440  exprt &block=declarator.value();
441 
442  std::string arg_name("ref");
443 
444  // First, we copy the parents
445  const irept &bases=symbol.type.find(ID_bases);
446 
447  forall_irep(parent_it, bases.get_sub())
448  {
449  assert(parent_it->id()==ID_base);
450  assert(parent_it->get(ID_type)==ID_symbol);
451 
452  const symbolt &symb=
453  lookup(parent_it->find(ID_type).get(ID_identifier));
454 
455  copy_parent(source_location, symb.base_name, arg_name, block);
456  }
457 
458  // Then, we copy the members
459  const irept &components=symbol.type.find(ID_components);
460 
461  forall_irep(mem_it, components.get_sub())
462  {
463  if(mem_it->get_bool(ID_from_base) ||
464  mem_it->get_bool(ID_is_type) ||
465  mem_it->get_bool(ID_is_static) ||
466  mem_it->get_bool("is_vtptr") ||
467  mem_it->get(ID_type)==ID_code)
468  continue;
469 
470  irep_idt mem_name=mem_it->get(ID_base_name);
471 
472  if(mem_it->get(ID_type)==ID_array)
473  {
474  const exprt &size_expr=
475  to_array_type((typet&)mem_it->find(ID_type)).size();
476 
477  if(size_expr.id()==ID_infinity)
478  {
479  // error().source_location=object);
480  // err << "cannot copy array of infinite size\n";
481  // throw 0;
482  continue;
483  }
484 
485  mp_integer size;
486  bool to_int=to_integer(size_expr, size);
487  CHECK_RETURN(!to_int);
488  CHECK_RETURN(size>=0);
489 
490  exprt::operandst empty_operands;
491  for(mp_integer i=0; i < size; ++i)
492  copy_array(source_location, mem_name, i, arg_name, block);
493  }
494  else
495  copy_member(source_location, mem_name, arg_name, block);
496  }
497 
498  // Finally we add the return statement
499  block.operands().push_back(exprt(ID_code));
500  exprt &ret_code=declarator.value().operands().back();
501  ret_code.operands().push_back(exprt(ID_dereference));
502  ret_code.op0().operands().push_back(exprt("cpp-this"));
503  ret_code.set(ID_statement, ID_return);
504  ret_code.type()=code_typet();
505 }
506 
515  const irept &bases,
516  const struct_typet::componentst &components,
517  const irept &initializers)
518 {
519  assert(initializers.id()==ID_member_initializers);
520 
521  forall_irep(init_it, initializers.get_sub())
522  {
523  const irept &initializer=*init_it;
524  assert(initializer.is_not_nil());
525 
526  assert(initializer.get(ID_member)==ID_cpp_name);
527 
528  const cpp_namet &member_name=
529  to_cpp_name(initializer.find(ID_member));
530 
531  bool has_template_args=member_name.has_template_args();
532 
533  if(has_template_args)
534  {
535  // it has to be a parent constructor
536  typet member_type=(typet&) initializer.find(ID_member);
537  typecheck_type(member_type);
538 
539  // check for a direct parent
540  bool ok=false;
541  forall_irep(parent_it, bases.get_sub())
542  {
543  assert(parent_it->get(ID_type)==ID_symbol);
544 
545  if(member_type.get(ID_identifier)
546  ==parent_it->find(ID_type).get(ID_identifier))
547  {
548  ok=true;
549  break;
550  }
551  }
552 
553  if(!ok)
554  {
555  error().source_location=member_name.source_location();
556  error() << "invalid initializer `" << member_name.to_string()
557  << "'" << eom;
558  throw 0;
559  }
560  return;
561  }
562 
563  irep_idt base_name=member_name.get_base_name();
564  bool ok=false;
565 
566  for(struct_typet::componentst::const_iterator
567  c_it=components.begin();
568  c_it!=components.end();
569  c_it++)
570  {
571  if(c_it->get(ID_base_name)!=base_name)
572  continue;
573 
574  // Data member
575  if(!c_it->get_bool(ID_from_base) &&
576  !c_it->get_bool(ID_is_static) &&
577  c_it->get(ID_type)!=ID_code)
578  {
579  ok=true;
580  break;
581  }
582 
583  // Maybe it is a parent constructor?
584  if(c_it->get_bool("is_type"))
585  {
586  typet type=static_cast<const typet&>(c_it->find(ID_type));
587  if(type.id()!=ID_symbol)
588  continue;
589 
590  const symbolt &symb=lookup(type.get(ID_identifier));
591  if(symb.type.id()!=ID_struct)
592  break;
593 
594  // check for a direct parent
595  forall_irep(parent_it, bases.get_sub())
596  {
597  assert(parent_it->get(ID_type)==ID_symbol);
598  if(symb.name==parent_it->find(ID_type).get(ID_identifier))
599  {
600  ok=true;
601  break;
602  }
603  }
604  continue;
605  }
606 
607  // Parent constructor
608  if(c_it->get_bool(ID_from_base) &&
609  !c_it->get_bool(ID_is_type) &&
610  !c_it->get_bool(ID_is_static) &&
611  c_it->get(ID_type)==ID_code &&
612  c_it->find(ID_type).get(ID_return_type)==ID_constructor)
613  {
614  typet member_type=(typet&) initializer.find(ID_member);
615  typecheck_type(member_type);
616 
617  // check for a direct parent
618  forall_irep(parent_it, bases.get_sub())
619  {
620  assert(parent_it->get(ID_type)==ID_symbol);
621 
622  if(member_type.get(ID_identifier)==
623  parent_it->find(ID_type).get(ID_identifier))
624  {
625  ok=true;
626  break;
627  }
628  }
629  break;
630  }
631  }
632 
633  if(!ok)
634  {
635  error().source_location=member_name.source_location();
636  error() << "invalid initializer `" << base_name << "'" << eom;
637  throw 0;
638  }
639  }
640 }
641 
651  const struct_union_typet &struct_union_type,
652  irept &initializers)
653 {
654  const struct_union_typet::componentst &components=
655  struct_union_type.components();
656 
657  assert(initializers.id()==ID_member_initializers);
658 
659  irept final_initializers(ID_member_initializers);
660 
661  if(struct_union_type.id()==ID_struct)
662  {
663  // First, if we are the most-derived object, then
664  // we need to construct the virtual bases
665  std::list<irep_idt> vbases;
666  get_virtual_bases(to_struct_type(struct_union_type), vbases);
667 
668  if(!vbases.empty())
669  {
670  // TODO(tautschnig): this code doesn't seem to make much sense as the
671  // ifthenelse only gets to have two operands (instead of three)
672  codet cond(ID_ifthenelse);
673 
674  {
675  cpp_namet most_derived;
676  most_derived.get_sub().push_back(irept(ID_name));
677  most_derived.get_sub().back().set(ID_identifier, "@most_derived");
678 
679  exprt tmp;
680  tmp.swap(most_derived);
681  cond.move_to_operands(tmp);
682  }
683 
684  code_blockt block;
685 
686  while(!vbases.empty())
687  {
688  const symbolt &symb=lookup(vbases.front());
689  if(!cpp_is_pod(symb.type))
690  {
691  // default initializer
692  irept name(ID_name);
693  name.set(ID_identifier, symb.base_name);
694 
695  cpp_namet cppname;
696  cppname.move_to_sub(name);
697 
698  codet mem_init(ID_member_initializer);
699  mem_init.set(ID_member, cppname);
700  block.move_to_sub(mem_init);
701  }
702  vbases.pop_front();
703  }
704  cond.move_to_operands(block);
705  final_initializers.move_to_sub(cond);
706  }
707 
708  const irept &bases=struct_union_type.find(ID_bases);
709 
710  // Subsequently, we need to call the non-POD parent constructors
711  forall_irep(parent_it, bases.get_sub())
712  {
713  assert(parent_it->id()==ID_base);
714  assert(parent_it->get(ID_type)==ID_symbol);
715 
716  const symbolt &ctorsymb=
717  lookup(parent_it->find(ID_type).get(ID_identifier));
718 
719  if(cpp_is_pod(ctorsymb.type))
720  continue;
721 
722  irep_idt ctor_name=ctorsymb.base_name;
723 
724  // Check if the initialization list of the constructor
725  // explicitly calls the parent constructor.
726  bool found=false;
727 
728  forall_irep(m_it, initializers.get_sub())
729  {
730  irept initializer=*m_it;
731 
732  assert(initializer.get(ID_member)==ID_cpp_name);
733 
734  const cpp_namet &member_name=
735  to_cpp_name(initializer.find(ID_member));
736 
737  bool has_template_args=member_name.has_template_args();
738 
739  if(!has_template_args)
740  {
741  irep_idt base_name=member_name.get_base_name();
742 
743  // check if the initializer is a data
744  bool is_data=false;
745 
746  for(struct_typet::componentst::const_iterator c_it =
747  components.begin(); c_it!=components.end(); c_it++)
748  {
749  if(c_it->get(ID_base_name)==base_name &&
750  c_it->get(ID_type)!=ID_code &&
751  !c_it->get_bool(ID_is_type))
752  {
753  is_data=true;
754  break;
755  }
756  }
757 
758  if(is_data)
759  continue;
760  }
761 
762  typet member_type=
763  static_cast<const typet&>(initializer.find(ID_member));
764 
765  typecheck_type(member_type);
766 
767  if(member_type.id()!=ID_symbol)
768  break;
769 
770  if(parent_it->find(ID_type).get(ID_identifier)==
771  member_type.get(ID_identifier))
772  {
773  final_initializers.move_to_sub(initializer);
774  found=true;
775  break;
776  }
777  }
778 
779  // Call the parent default constructor
780  if(!found)
781  {
782  irept name(ID_name);
783  name.set(ID_identifier, ctor_name);
784 
785  cpp_namet cppname;
786  cppname.move_to_sub(name);
787 
788  codet mem_init(ID_member_initializer);
789  mem_init.set(ID_member, cppname);
790  final_initializers.move_to_sub(mem_init);
791  }
792 
793  if(parent_it->get_bool(ID_virtual))
794  {
795  // TODO(tautschnig): this code doesn't seem to make much sense as the
796  // ifthenelse only gets to have two operands (instead of three)
797  codet cond(ID_ifthenelse);
798 
799  {
800  cpp_namet most_derived;
801  most_derived.get_sub().push_back(irept(ID_name));
802  most_derived.get_sub().back().set(ID_identifier, "@most_derived");
803 
804  exprt tmp;
805  tmp.swap(most_derived);
806  cond.move_to_operands(tmp);
807  }
808 
809  {
810  codet tmp(ID_member_initializer);
811  tmp.swap(final_initializers.get_sub().back());
812  cond.move_to_operands(tmp);
813  final_initializers.get_sub().back().swap(cond);
814  }
815  }
816  }
817  }
818 
819  // Then, we add the member initializers
820  for(struct_typet::componentst::const_iterator mem_it =
821  components.begin(); mem_it!=components.end(); mem_it++)
822  {
823  // Take care of virtual tables
824  if(mem_it->get_bool("is_vtptr"))
825  {
826  exprt name(ID_name);
827  name.set(ID_identifier, mem_it->get(ID_base_name));
828  name.add_source_location()=mem_it->source_location();
829 
830  cpp_namet cppname;
831  cppname.move_to_sub(name);
832 
833  const symbolt &virtual_table_symbol_type =
834  lookup(mem_it->type().subtype().get(ID_identifier));
835 
836  const symbolt &virtual_table_symbol_var =
837  lookup(id2string(virtual_table_symbol_type.name) + "@" +
838  id2string(struct_union_type.get(ID_name)));
839 
840  exprt var=virtual_table_symbol_var.symbol_expr();
841  address_of_exprt address(var);
842  assert(address.type()==mem_it->type());
843 
844  already_typechecked(address);
845 
846  exprt ptrmember(ID_ptrmember);
847  ptrmember.set(ID_component_name, mem_it->get(ID_name));
848  ptrmember.operands().push_back(exprt("cpp-this"));
849 
850  code_assignt assign(ptrmember, address);
851  final_initializers.move_to_sub(assign);
852  continue;
853  }
854 
855  if( mem_it->get_bool(ID_from_base)
856  || mem_it->type().id()==ID_code
857  || mem_it->get_bool(ID_is_type)
858  || mem_it->get_bool(ID_is_static))
859  continue;
860 
861  irep_idt mem_name=mem_it->get(ID_base_name);
862 
863  // Check if the initialization list of the constructor
864  // explicitly initializes the data member
865  bool found=false;
866  Forall_irep(m_it, initializers.get_sub())
867  {
868  irept &initializer=*m_it;
869 
870  if(initializer.get(ID_member)!=ID_cpp_name)
871  continue;
872  cpp_namet &member_name=(cpp_namet&) initializer.add(ID_member);
873 
874  if(member_name.has_template_args())
875  continue; // base-type initializer
876 
877  irep_idt base_name=member_name.get_base_name();
878 
879  if(mem_name==base_name)
880  {
881  final_initializers.move_to_sub(initializer);
882  found=true;
883  break;
884  }
885  }
886 
887  // If the data member is a reference, it must be explicitly
888  // initialized
889  if(!found &&
890  mem_it->find(ID_type).id()==ID_pointer &&
891  mem_it->find(ID_type).get_bool(ID_C_reference))
892  {
893  error().source_location=mem_it->source_location();
894  error() << "reference must be explicitly initialized" << eom;
895  throw 0;
896  }
897 
898  // If the data member is not POD and is not explicitly initialized,
899  // then its default constructor is called.
900  if(!found && !cpp_is_pod((const typet &)(mem_it->find(ID_type))))
901  {
902  irept name(ID_name);
903  name.set(ID_identifier, mem_name);
904 
905  cpp_namet cppname;
906  cppname.move_to_sub(name);
907 
908  codet mem_init(ID_member_initializer);
909  mem_init.set(ID_member, cppname);
910  final_initializers.move_to_sub(mem_init);
911  }
912  }
913 
914  initializers.swap(final_initializers);
915 }
916 
919 bool cpp_typecheckt::find_cpctor(const symbolt &symbol) const
920 {
921  const struct_typet &struct_type=to_struct_type(symbol.type);
922  const struct_typet::componentst &components=struct_type.components();
923 
924  for(struct_typet::componentst::const_iterator
925  cit=components.begin();
926  cit!=components.end();
927  cit++)
928  {
929  // Skip non-ctor
930  const struct_typet::componentt &component=*cit;
931 
932  if(component.type().id()!=ID_code ||
933  to_code_type(component.type()).return_type().id() !=ID_constructor)
934  continue;
935 
936  // Skip inherited constructor
937  if(component.get_bool(ID_from_base))
938  continue;
939 
940  const code_typet &code_type=to_code_type(component.type());
941 
942  const code_typet::parameterst &parameters=code_type.parameters();
943 
944  // First parameter is the 'this' pointer. Therefore, copy
945  // constructors have at least two parameters
946  if(parameters.size() < 2)
947  continue;
948 
949  const code_typet::parametert &parameter1=parameters[1];
950 
951  const typet &parameter1_type=parameter1.type();
952 
953  if(!is_reference(parameter1_type))
954  continue;
955 
956  if(parameter1_type.subtype().get(ID_identifier)!=symbol.name)
957  continue;
958 
959  bool defargs=true;
960  for(std::size_t i=2; i<parameters.size(); i++)
961  {
962  if(parameters[i].default_value().is_nil())
963  {
964  defargs=false;
965  break;
966  }
967  }
968 
969  if(defargs)
970  return true;
971  }
972 
973  return false;
974 }
975 
976 bool cpp_typecheckt::find_assignop(const symbolt &symbol) const
977 {
978  const struct_typet &struct_type=to_struct_type(symbol.type);
979  const struct_typet::componentst &components=struct_type.components();
980 
981  for(std::size_t i=0; i < components.size(); i++)
982  {
983  const struct_typet::componentt &component=components[i];
984 
985  if(component.get(ID_base_name)!="operator=")
986  continue;
987 
988  if(component.get_bool(ID_is_static))
989  continue;
990 
991  if(component.get_bool(ID_from_base))
992  continue;
993 
994  const code_typet &code_type=to_code_type(component.type());
995 
996  const code_typet::parameterst &args=code_type.parameters();
997 
998  if(args.size()!=2)
999  continue;
1000 
1001  const code_typet::parametert &arg1=args[1];
1002 
1003  const typet &arg1_type=arg1.type();
1004 
1005  if(!is_reference(arg1_type))
1006  continue;
1007 
1008  if(arg1_type.subtype().get(ID_identifier)!=symbol.name)
1009  continue;
1010 
1011  return true;
1012  }
1013 
1014  return false;
1015 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
bool find_cpctor(const symbolt &symbol) const
void set_function(const irep_idt &function)
BigInt mp_integer
Definition: mp_arith.h:22
void typecheck_type(typet &type)
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
static void copy_parent(const source_locationt &source_location, const irep_idt &parent_base_name, const irep_idt &arg_name, exprt &block)
exprt & op0()
Definition: expr.h:72
void move_to_sub(irept &irep)
Definition: irep.cpp:204
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
void full_member_initialization(const struct_union_typet &struct_union_type, irept &initializers)
Build the full initialization list of the constructor.
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:144
std::vector< componentt > componentst
Definition: std_types.h:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
subtypest & subtypes()
Definition: type.h:58
std::vector< parametert > parameterst
Definition: std_types.h:767
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
void check_member_initializers(const irept &bases, const struct_typet::componentst &components, const irept &initializers)
Check a constructor initialization-list.
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
static void copy_member(const source_locationt &source_location, const irep_idt &member_base_name, const irep_idt &arg_name, exprt &block)
subt & get_sub()
Definition: irep.h:245
void default_assignop_value(const symbolt &symbol, cpp_declaratort &declarator)
Generate code for the implicit default assignment operator.
const irep_idt & id() const
Definition: irep.h:189
const declaratorst & declarators() const
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:248
bool has_template_args() const
Definition: cpp_name.h:122
source_locationt source_location
Definition: message.h:214
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
API to expression classes.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
Base class for tree-like data structures with sharing.
Definition: irep.h:86
C++ Language Type Checking.
bitvector_typet index_type()
Definition: c_types.cpp:16
#define Forall_irep(it, irep)
Definition: irep.h:65
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
Operator to return the address of an object.
Definition: std_expr.h:3170
std::vector< typet > subtypest
Definition: type.h:56
void default_assignop(const symbolt &symbol, cpp_declarationt &cpctor)
Generate declaration of the implicit default assignment operator.
void default_cpctor(const symbolt &, cpp_declarationt &cpctor) const
Generate code for implicit default copy constructor.
std::vector< exprt > operandst
Definition: expr.h:45
const source_locationt & source_location() const
Definition: type.h:97
irep_idt get_base_name() const
Definition: cpp_name.cpp:17
typet type
Type of symbol.
Definition: symbol.h:34
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
void default_ctor(const source_locationt &source_location, const irep_idt &base_name, cpp_declarationt &ctor) const
Generate code for implicit default constructors.
void set_statement(const irep_idt &statement)
Definition: std_code.h:34
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
bool find_assignop(const symbolt &symbol) const
Base class for all expressions.
Definition: expr.h:42
void get_virtual_bases(const struct_typet &type, std::list< irep_idt > &vbases) const
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
source_locationt & add_source_location()
Definition: type.h:102
const source_locationt & source_location() const
Definition: expr.h:125
irept & add(const irep_namet &name)
Definition: irep.cpp:306
The NIL type.
Definition: std_types.h:44
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
cpp_namet & name()
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
A statement in a programming language.
Definition: std_code.h:21
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static void copy_array(const source_locationt &source_location, const irep_idt &member_base_name, mp_integer i, const irep_idt &arg_name, exprt &block)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
#define forall_irep(it, irep)
Definition: irep.h:61