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