CBMC
cpp_typecheck_template.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 <util/base_exceptions.h> // IWYU pragma: keep
13 #include <util/simplify_expr.h>
14 #include <util/symbol_table_base.h>
15 
16 #include "cpp_convert_type.h"
18 #include "cpp_template_args.h"
19 #include "cpp_template_type.h"
20 #include "cpp_type2name.h"
21 #include "cpp_typecheck.h"
22 
24  const template_typet &old_type,
25  template_typet &new_type)
26 {
27  const template_typet::template_parameterst &old_parameters=
28  old_type.template_parameters();
30  new_type.template_parameters();
31 
32  for(std::size_t i=0; i<new_parameters.size(); i++)
33  {
34  if(i<old_parameters.size() &&
35  old_parameters[i].has_default_argument() &&
36  !new_parameters[i].has_default_argument())
37  {
38  // TODO The default may depend on previous parameters!!
39  new_parameters[i].default_argument()=old_parameters[i].default_argument();
40  }
41  }
42 }
43 
45  cpp_declarationt &declaration)
46 {
47  // Do template parameters. This also sets up the template scope.
48  cpp_scopet &template_scope=
50 
51  typet &type=declaration.type();
52  template_typet &template_type=declaration.template_type();
53 
54  bool has_body=type.find(ID_body).is_not_nil();
55 
56  const cpp_namet &cpp_name=
57  static_cast<const cpp_namet &>(type.find(ID_tag));
58 
59  if(cpp_name.is_nil())
60  {
62  error() << "class templates must not be anonymous" << eom;
63  throw 0;
64  }
65 
66  if(!cpp_name.is_simple_name())
67  {
69  error() << "simple name expected as class template tag" << eom;
70  throw 0;
71  }
72 
73  irep_idt base_name=cpp_name.get_base_name();
74 
75  const cpp_template_args_non_tct &partial_specialization_args=
76  declaration.partial_specialization_args();
77 
78  const irep_idt symbol_name=
80  base_name, template_type, partial_specialization_args);
81 
82  #if 0
83  // Check if the name is already used by a different template
84  // in the same scope.
85  {
86  const auto id_set=
88  base_name,
90  cpp_scopet::TEMPLATE);
91 
92  if(!id_set.empty())
93  {
94  const symbolt &previous=lookup((*id_set.begin())->identifier);
95  if(previous.name!=symbol_name || id_set.size()>1)
96  {
98  str << "template declaration of '" << base_name.c_str()
99  << " does not match previous declaration\n";
100  str << "location of previous definition: " << previous.location;
101  throw 0;
102  }
103  }
104  }
105  #endif
106 
107  // check if we have it already
108 
109  if(const auto maybe_symbol=symbol_table.get_writeable(symbol_name))
110  {
111  // there already
112  symbolt &previous_symbol=*maybe_symbol;
113  cpp_declarationt &previous_declaration=
114  to_cpp_declaration(previous_symbol.type);
115 
116  bool previous_has_body=
117  previous_declaration.type().find(ID_body).is_not_nil();
118 
119  // check if we have 2 bodies
120  if(has_body && previous_has_body)
121  {
123  error() << "template struct '" << base_name << "' defined previously\n"
124  << "location of previous definition: " << previous_symbol.location
125  << eom;
126  throw 0;
127  }
128 
129  if(has_body)
130  {
131  // We replace the template!
132  // We have to retain any default parameters from the previous declaration.
134  previous_declaration.template_type(),
135  declaration.template_type());
136 
137  previous_symbol.type.swap(declaration);
138 
139  #if 0
140  std::cout << "*****\n";
141  std::cout << *cpp_scopes.id_map[symbol_name];
142  std::cout << "*****\n";
143  std::cout << "II: " << symbol_name << '\n';
144  #endif
145 
146  // We also replace the template scope (the old one could be deleted).
147  cpp_scopes.id_map[symbol_name]=&template_scope;
148 
149  // We also fix the parent scope in order to see the new
150  // template arguments
151  }
152  else
153  {
154  // just update any default arguments
156  declaration.template_type(),
157  previous_declaration.template_type());
158  }
159 
160  INVARIANT(
161  cpp_scopes.id_map[symbol_name]->is_template_scope(),
162  "symbol should be in template scope");
163 
164  return;
165  }
166 
167  // it's not there yet
168 
169  symbolt symbol{symbol_name, typet{}, ID_cpp};
170  symbol.base_name=base_name;
171  symbol.location=cpp_name.source_location();
172  symbol.module=module;
173  symbol.type.swap(declaration);
174  symbol.value = exprt(ID_template_decls);
175 
176  symbol.pretty_name=
177  cpp_scopes.current_scope().prefix+id2string(symbol.base_name);
178 
179  symbolt *new_symbol;
180  if(symbol_table.move(symbol, new_symbol))
181  {
182  error().source_location=symbol.location;
183  error() << "cpp_typecheckt::typecheck_compound_type: "
184  << "symbol_table.move() failed"
185  << eom;
186  throw 0;
187  }
188 
189  // put into current scope
190  cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol);
192  id.prefix=cpp_scopes.current_scope().prefix+
193  id2string(new_symbol->base_name);
194 
195  // link the template symbol with the template scope
196  cpp_scopes.id_map[symbol_name]=&template_scope;
197 
198  INVARIANT(
199  cpp_scopes.id_map[symbol_name]->is_template_scope(),
200  "symbol should be in template scope");
201 }
202 
205  cpp_declarationt &declaration)
206 {
207  PRECONDITION(declaration.declarators().size() == 1);
208 
209  cpp_declaratort &declarator=declaration.declarators()[0];
210  const cpp_namet &cpp_name = declarator.name();
211 
212  // do template arguments
213  // this also sets up the template scope
214  cpp_scopet &template_scope=
216 
217  if(!cpp_name.is_simple_name())
218  {
219  error().source_location=declaration.source_location();
220  error() << "function template must have simple name" << eom;
221  throw 0;
222  }
223 
224  irep_idt base_name=cpp_name.get_base_name();
225 
226  template_typet &template_type=declaration.template_type();
227 
228  typet function_type=
229  declarator.merge_type(declaration.type());
230 
232 
233  irep_idt symbol_name=
235  base_name,
236  template_type,
237  function_type);
238 
239  bool has_value=declarator.find(ID_value).is_not_nil();
240 
241  // check if we have it already
242 
243  symbolt *previous_symbol = symbol_table.get_writeable(symbol_name);
244 
245  if(previous_symbol)
246  {
247  bool previous_has_value = to_cpp_declaration(previous_symbol->type)
248  .declarators()[0]
249  .find(ID_value)
250  .is_not_nil();
251 
252  if(has_value && previous_has_value)
253  {
255  error() << "function template symbol '" << base_name
256  << "' declared previously\n"
257  << "location of previous definition: "
258  << previous_symbol->location << eom;
259  throw 0;
260  }
261 
262  if(has_value)
263  {
264  previous_symbol->type.swap(declaration);
265  cpp_scopes.id_map[symbol_name]=&template_scope;
266  }
267 
268  // todo: the old template scope now is useless,
269  // and thus, we could delete it
270  return;
271  }
272 
273  symbolt symbol{symbol_name, typet{}, ID_cpp};
274  symbol.base_name=base_name;
275  symbol.location=cpp_name.source_location();
276  symbol.module=module;
277  symbol.type.swap(declaration);
278  symbol.pretty_name=
279  cpp_scopes.current_scope().prefix+id2string(symbol.base_name);
280 
281  symbolt *new_symbol;
282  if(symbol_table.move(symbol, new_symbol))
283  {
284  error().source_location=symbol.location;
285  error() << "cpp_typecheckt::typecheck_compound_type: "
286  << "symbol_table.move() failed"
287  << eom;
288  throw 0;
289  }
290 
291  // put into scope
292  cpp_idt &id=cpp_scopes.put_into_scope(*new_symbol);
294  id.prefix=cpp_scopes.current_scope().prefix+
295  id2string(new_symbol->base_name);
296 
297  // link the template symbol with the template scope
298  cpp_scopes.id_map[symbol_name] = &template_scope;
299  INVARIANT(
300  template_scope.is_template_scope(), "symbol should be in template scope");
301 }
302 
305  cpp_declarationt &declaration)
306 {
307  PRECONDITION(declaration.declarators().size() == 1);
308 
309  cpp_declaratort &declarator=declaration.declarators()[0];
310  const cpp_namet &cpp_name = declarator.name();
311 
312  PRECONDITION(cpp_name.is_qualified() || cpp_name.has_template_args());
313 
314  // must be of the form: name1<template_args>::name2
315  // or: name1<template_args>::operator X
316  if(cpp_name.get_sub().size()==4 &&
317  cpp_name.get_sub()[0].id()==ID_name &&
318  cpp_name.get_sub()[1].id()==ID_template_args &&
319  cpp_name.get_sub()[2].id()=="::" &&
320  cpp_name.get_sub()[3].id()==ID_name)
321  {
322  }
323  else if(cpp_name.get_sub().size()==5 &&
324  cpp_name.get_sub()[0].id()==ID_name &&
325  cpp_name.get_sub()[1].id()==ID_template_args &&
326  cpp_name.get_sub()[2].id()=="::" &&
327  cpp_name.get_sub()[3].id()==ID_operator)
328  {
329  }
330  else
331  {
332  return; // TODO
333 
334 #if 0
336  error() << "bad template name" << eom;
337  throw 0;
338 #endif
339  }
340 
341  // let's find the class template this function template belongs to.
342  const auto id_set = cpp_scopes.current_scope().lookup(
343  cpp_name.get_sub().front().get(ID_identifier),
344  cpp_scopet::SCOPE_ONLY, // look only in current scope
345  cpp_scopet::id_classt::TEMPLATE); // must be template
346 
347  if(id_set.empty())
348  {
351  error() << "class template '"
352  << cpp_name.get_sub().front().get(ID_identifier) << "' not found"
353  << eom;
354  throw 0;
355  }
356  else if(id_set.size()>1)
357  {
359  error() << "class template '"
360  << cpp_name.get_sub().front().get(ID_identifier) << "' is ambiguous"
361  << eom;
362  throw 0;
363  }
364  else if((*(id_set.begin()))->id_class!=cpp_idt::id_classt::TEMPLATE)
365  {
366  // std::cerr << *(*id_set.begin()) << '\n';
368  error() << "class template '"
369  << cpp_name.get_sub().front().get(ID_identifier)
370  << "' is not a template" << eom;
371  throw 0;
372  }
373 
374  const cpp_idt &cpp_id=**(id_set.begin());
375  symbolt &template_symbol = symbol_table.get_writeable_ref(cpp_id.identifier);
376 
377  exprt &template_methods =
378  static_cast<exprt &>(template_symbol.value.add(ID_template_methods));
379 
380  template_methods.copy_to_operands(declaration);
381 
382  // save current scope
383  cpp_save_scopet cpp_saved_scope(cpp_scopes);
384 
385  const irept &instantiated_with =
386  template_symbol.value.add(ID_instantiated_with);
387 
388  for(std::size_t i=0; i<instantiated_with.get_sub().size(); i++)
389  {
390  const cpp_template_args_tct &tc_template_args=
391  static_cast<const cpp_template_args_tct &>(
392  instantiated_with.get_sub()[i]);
393 
394  cpp_declarationt decl_tmp=declaration;
395 
396  // do template arguments
397  // this also sets up the template scope of the method
398  cpp_scopet &method_scope=
400 
401  cpp_scopes.go_to(method_scope);
402 
403  // mapping from template arguments to values/types
404  template_map.build(decl_tmp.template_type(), tc_template_args);
405 
406  decl_tmp.remove(ID_template_type);
407  decl_tmp.remove(ID_is_template);
408 
409  convert(decl_tmp);
410  cpp_saved_scope.restore();
411  }
412 }
413 
415  const irep_idt &base_name,
416  const template_typet &template_type,
417  const cpp_template_args_non_tct &partial_specialization_args)
418 {
419  std::string identifier=
421  "template."+id2string(base_name) + "<";
422 
423  int counter=0;
424 
425  // these are probably not needed -- templates
426  // should be unique in a namespace
427  for(template_typet::template_parameterst::const_iterator
428  it=template_type.template_parameters().begin();
429  it!=template_type.template_parameters().end();
430  it++)
431  {
432  if(counter!=0)
433  identifier+=',';
434 
435  if(it->id()==ID_type)
436  identifier+="Type"+std::to_string(counter);
437  else
438  identifier+="Non_Type"+std::to_string(counter);
439 
440  counter++;
441  }
442 
443  identifier += ">";
444 
445  if(!partial_specialization_args.arguments().empty())
446  {
447  identifier+="_specialized_to_<";
448 
449  counter=0;
450  for(cpp_template_args_non_tct::argumentst::const_iterator
451  it=partial_specialization_args.arguments().begin();
452  it!=partial_specialization_args.arguments().end();
453  it++, counter++)
454  {
455  if(counter!=0)
456  identifier+=',';
457 
458  // These are not yet typechecked, as they may depend
459  // on unassigned template parameters.
460 
461  if(it->id() == ID_type || it->id() == ID_ambiguous)
462  identifier+=cpp_type2name(it->type());
463  else
464  identifier+=cpp_expr2name(*it);
465  }
466 
467  identifier+='>';
468  }
469 
470  return identifier;
471 }
472 
474  const irep_idt &base_name,
475  const template_typet &template_type,
476  const typet &function_type)
477 {
478  // we first build something without function arguments
479  cpp_template_args_non_tct partial_specialization_args;
480  std::string identifier=
481  class_template_identifier(base_name, template_type,
482  partial_specialization_args);
483 
484  // we must also add the signature of the function to the identifier
485  identifier+=cpp_type2name(function_type);
486 
487  return identifier;
488 }
489 
491  cpp_declarationt &declaration)
492 {
493  cpp_save_scopet saved_scope(cpp_scopes);
494 
495  typet &type=declaration.type();
496 
497  PRECONDITION(type.id() == ID_struct);
498 
499  cpp_namet &cpp_name=
500  static_cast<cpp_namet &>(type.add(ID_tag));
501 
502  if(cpp_name.is_qualified())
503  {
505  error() << "qualifiers not expected here" << eom;
506  throw 0;
507  }
508 
509  if(cpp_name.get_sub().size()!=2 ||
510  cpp_name.get_sub()[0].id()!=ID_name ||
511  cpp_name.get_sub()[1].id()!=ID_template_args)
512  {
513  // currently we are more restrictive
514  // than the standard
516  error() << "bad template-class-specialization name" << eom;
517  throw 0;
518  }
519 
520  irep_idt base_name=
521  cpp_name.get_sub()[0].get(ID_identifier);
522 
523  // copy the template arguments
524  const cpp_template_args_non_tct template_args_non_tc=
525  to_cpp_template_args_non_tc(cpp_name.get_sub()[1]);
526 
527  // Remove the template arguments from the name.
528  cpp_name.get_sub().pop_back();
529 
530  // get the template symbol
531 
532  auto id_set = cpp_scopes.current_scope().lookup(
534 
535  // remove any specializations
536  for(cpp_scopest::id_sett::iterator
537  it=id_set.begin();
538  it!=id_set.end();
539  ) // no it++
540  {
541  cpp_scopest::id_sett::iterator next=it;
542  next++;
543 
544  if(lookup((*it)->identifier).type.find(ID_specialization_of).is_not_nil())
545  id_set.erase(it);
546 
547  it=next;
548  }
549 
550  // only one should be left
551  if(id_set.empty())
552  {
554  error() << "class template '" << base_name << "' not found" << eom;
555  throw 0;
556  }
557  else if(id_set.size()>1)
558  {
560  error() << "class template '" << base_name << "' is ambiguous" << eom;
561  throw 0;
562  }
563 
564  symbol_table_baset::symbolst::const_iterator s_it =
565  symbol_table.symbols.find((*id_set.begin())->identifier);
566 
567  CHECK_RETURN(s_it != symbol_table.symbols.end());
568 
569  const symbolt &template_symbol=s_it->second;
570 
571  if(!template_symbol.type.get_bool(ID_is_template))
572  {
574  error() << "expected a template" << eom;
575  }
576 
577  #if 0
578  // is this partial specialization?
579  if(declaration.template_type().parameters().empty())
580  {
581  // typecheck arguments -- these are for the 'primary' template!
582  cpp_template_args_tct template_args_tc=
584  declaration.source_location(),
585  to_cpp_declaration(template_symbol.type).template_type(),
586  template_args_non_tc);
587 
588  // Full specialization, i.e., template<>.
589  // We instantiate.
591  cpp_name.source_location(),
592  template_symbol,
593  template_args_tc,
594  type);
595  }
596  else // NOLINT(readability/braces)
597  #endif
598 
599  {
600  // partial specialization -- we typecheck
601  declaration.partial_specialization_args()=template_args_non_tc;
602  declaration.set_specialization_of(template_symbol.name);
603 
604  typecheck_class_template(declaration);
605  }
606 }
607 
609  cpp_declarationt &declaration)
610 {
611  cpp_save_scopet saved_scope(cpp_scopes);
612 
613  if(declaration.declarators().size()!=1 ||
614  declaration.declarators().front().type().id()!=ID_function_type)
615  {
616  error().source_location=declaration.type().source_location();
617  error() << "expected function template specialization" << eom;
618  throw 0;
619  }
620 
621  PRECONDITION(declaration.declarators().size() == 1);
622  cpp_declaratort declarator=declaration.declarators().front();
623  cpp_namet &cpp_name=declarator.name();
624 
625  // There is specialization (instantiation with template arguments)
626  // but also function overloading (no template arguments)
627 
628  PRECONDITION(!cpp_name.get_sub().empty());
629 
630  if(cpp_name.get_sub().back().id()==ID_template_args)
631  {
632  // proper specialization with arguments
633  if(cpp_name.get_sub().size()!=2 ||
634  cpp_name.get_sub()[0].id()!=ID_name ||
635  cpp_name.get_sub()[1].id()!=ID_template_args)
636  {
637  // currently we are more restrictive
638  // than the standard
640  error() << "bad template-function-specialization name" << eom;
641  throw 0;
642  }
643 
644  std::string base_name=
645  cpp_name.get_sub()[0].get(ID_identifier).c_str();
646 
647  const auto id_set =
649 
650  if(id_set.empty())
651  {
653  error() << "template function '" << base_name << "' not found" << eom;
654  throw 0;
655  }
656  else if(id_set.size()>1)
657  {
659  error() << "template function '" << base_name << "' is ambiguous" << eom;
660  throw 0;
661  }
662 
663  const symbolt &template_symbol=
664  lookup((*id_set.begin())->identifier);
665 
666  cpp_template_args_tct template_args=
668  declaration.source_location(),
669  template_symbol,
670  to_cpp_template_args_non_tc(cpp_name.get_sub()[1]));
671 
672  cpp_name.get_sub().pop_back();
673 
674  typet specialization;
675  specialization.swap(declarator);
676 
678  cpp_name.source_location(),
679  template_symbol,
680  template_args,
681  template_args,
682  specialization);
683  }
684  else
685  {
686  // Just overloading, but this is still a template
687  // for disambiguation purposes!
688  // http://www.gotw.ca/publications/mill17.htm
689  cpp_declarationt new_declaration=declaration;
690 
691  new_declaration.remove(ID_template_type);
692  new_declaration.remove(ID_is_template);
693  new_declaration.set(ID_C_template, ""); // todo, get identifier
694 
695  convert_non_template_declaration(new_declaration);
696  }
697 }
698 
700  template_typet &type)
701 {
702  cpp_save_scopet cpp_saved_scope(cpp_scopes);
703 
704  PRECONDITION(type.id() == ID_template);
705 
706  std::string id_suffix="template::"+std::to_string(template_counter++);
707 
708  // produce a new scope for the template parameters
709  cpp_scopet &template_scope = cpp_scopes.current_scope().new_scope(id_suffix);
711 
712  cpp_scopes.go_to(template_scope);
713 
714  // put template parameters into this scope
716  type.template_parameters();
717 
718  unsigned anon_count=0;
719 
720  for(template_typet::template_parameterst::iterator
721  it=parameters.begin();
722  it!=parameters.end();
723  it++)
724  {
725  exprt &parameter=*it;
726 
727  cpp_declarationt declaration;
728  declaration.swap(static_cast<cpp_declarationt &>(parameter));
729 
730  cpp_declarator_convertert cpp_declarator_converter(*this);
731 
732  // there must be _one_ declarator
733  PRECONDITION(declaration.declarators().size() == 1);
734 
735  cpp_declaratort &declarator=declaration.declarators().front();
736 
737  // it may be anonymous
738  if(declarator.name().is_nil())
739  declarator.name() = cpp_namet("anon#" + std::to_string(++anon_count));
740 
741  #if 1
742  // The declarator needs to be just a name
743  if(declarator.name().get_sub().size()!=1 ||
744  declarator.name().get_sub().front().id()!=ID_name)
745  {
746  error().source_location=declaration.source_location();
747  error() << "template parameter must be simple name" << eom;
748  throw 0;
749  }
750 
752 
753  irep_idt base_name=declarator.name().get_sub().front().get(ID_identifier);
754  irep_idt identifier=scope.prefix+id2string(base_name);
755 
756  // add to scope
757  cpp_idt &id=scope.insert(base_name);
758  id.identifier=identifier;
760 
761  // is it a type or not?
762  if(declaration.get_bool(ID_is_type))
763  {
764  parameter = type_exprt(template_parameter_symbol_typet(identifier));
765  parameter.type().add_source_location()=declaration.find_source_location();
766  }
767  else
768  {
769  // The type is not checked, as it might depend
770  // on earlier parameters.
771  parameter = symbol_exprt(identifier, declaration.type());
772  }
773 
774  // There might be a default type or default value.
775  // We store it for later, as it can't be typechecked now
776  // because of possible dependencies on earlier parameters!
777  if(declarator.value().is_not_nil())
778  parameter.add(ID_C_default_value)=declarator.value();
779 
780  #else
781  // is it a type or not?
782  cpp_declarator_converter.is_typedef=declaration.get_bool(ID_is_type);
783 
784  // say it a template parameter
785  cpp_declarator_converter.is_template_parameter=true;
786 
787  // There might be a default type or default value.
788  // We store it for later, as it can't be typechecked now
789  // because of possible dependencies on earlier parameters!
790  exprt default_value=declarator.value();
791  declarator.value().make_nil();
792 
793  const symbolt &symbol=
794  cpp_declarator_converter.convert(declaration, declarator);
795 
796  if(cpp_declarator_converter.is_typedef)
797  {
798  parameter = exprt(ID_type, struct_tag_typet(symbol.name));
799  parameter.type().add_source_location()=declaration.find_location();
800  }
801  else
802  parameter=symbol.symbol_expr();
803 
804  // set (non-typechecked) default value
805  if(default_value.is_not_nil())
806  parameter.add(ID_C_default_value)=default_value;
807 
808  parameter.add_source_location()=declaration.find_location();
809  #endif
810  }
811 
812  return template_scope;
813 }
814 
818  const source_locationt &source_location,
819  const symbolt &template_symbol,
820  const cpp_template_args_non_tct &template_args)
821 {
822  // old stuff
823  PRECONDITION(template_args.id() != ID_already_typechecked);
824 
825  PRECONDITION(template_symbol.type.get_bool(ID_is_template));
826 
827  const template_typet &template_type=
828  to_cpp_declaration(template_symbol.type).template_type();
829 
830  // bad re-cast, but better than copying the args one by one
832  (const cpp_template_args_tct &)(template_args);
833 
835  result.arguments();
836 
837  const template_typet::template_parameterst &parameters=
838  template_type.template_parameters();
839 
840  if(parameters.size()<args.size())
841  {
842  error().source_location=source_location;
843  error() << "too many template arguments (expected "
844  << parameters.size() << ", but got "
845  << args.size() << ")" << eom;
846  throw 0;
847  }
848 
849  // we will modify the template map
850  template_mapt old_template_map;
851  old_template_map=template_map;
852 
853  // check for default arguments
854  for(std::size_t i=0; i<parameters.size(); i++)
855  {
856  const template_parametert &parameter=parameters[i];
857  cpp_save_scopet cpp_saved_scope(cpp_scopes);
858 
859  if(i>=args.size())
860  {
861  // Check for default argument for the parameter.
862  // These may depend on previous arguments.
863  if(!parameter.has_default_argument())
864  {
865  error().source_location=source_location;
866  error() << "not enough template arguments (expected "
867  << parameters.size() << ", but got " << args.size()
868  << ")" << eom;
869  throw 0;
870  }
871 
872  args.push_back(parameter.default_argument());
873 
874  // these need to be typechecked in the scope of the template,
875  // not in the current scope!
876  cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
878  template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
879  cpp_scopes.go_to(*template_scope);
880  }
881 
882  DATA_INVARIANT(i < args.size(), "i must be in bounds");
883 
884  exprt &arg=args[i];
885 
886  if(parameter.id()==ID_type)
887  {
888  if(arg.id()==ID_type)
889  {
890  typecheck_type(arg.type());
891  }
892  else if(arg.id() == ID_ambiguous)
893  {
894  typecheck_type(arg.type());
895  typet t=arg.type();
896  arg=exprt(ID_type, t);
897  }
898  else
899  {
901  error() << "expected type, but got expression" << eom;
902  throw 0;
903  }
904  }
905  else // expression
906  {
907  if(arg.id()==ID_type)
908  {
910  error() << "expected expression, but got type" << eom;
911  throw 0;
912  }
913  else if(arg.id() == ID_ambiguous)
914  {
915  exprt e;
916  e.swap(arg.type());
917  arg.swap(e);
918  }
919 
920  typet type=parameter.type();
921 
922  // First check the parameter type (might have earlier
923  // type parameters in it). Needs to be checked in scope
924  // of template.
925  {
926  cpp_save_scopet cpp_saved_scope_before_parameter_typecheck(cpp_scopes);
927  cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
929  template_scope!=nullptr,
931  "template_scope is null");
932  cpp_scopes.go_to(*template_scope);
933  typecheck_type(type);
934  }
935 
936  // Now check the argument to match that.
937  typecheck_expr(arg);
938  simplify(arg, *this);
939  implicit_typecast(arg, type);
940  }
941 
942  // Set right away -- this is for the benefit of default
943  // arguments and later parameters whose type might
944  // depend on an earlier parameter.
945 
946  template_map.set(parameter, arg);
947  }
948 
949  // restore template map
950  template_map.swap(old_template_map);
951 
952  // now the numbers should match
954  args.size() == parameters.size(),
955  "argument and parameter numbers must match");
956 
957  return result;
958 }
959 
961  cpp_declarationt &declaration)
962 {
963  PRECONDITION(declaration.is_template());
964 
965  if(declaration.member_spec().is_virtual())
966  {
967  error().source_location=declaration.source_location();
968  error() << "invalid use of 'virtual' in template declaration"
969  << eom;
970  throw 0;
971  }
972 
973  if(declaration.is_typedef())
974  {
975  error().source_location=declaration.source_location();
976  error() << "template declaration for typedef" << eom;
977  throw 0;
978  }
979 
980  typet &type=declaration.type();
981 
982  // there are
983  // 1) function templates
984  // 2) class templates
985  // 3) template members of class templates (static or methods)
986  // 4) variable templates (C++14)
987 
988  if(declaration.is_class_template())
989  {
990  // there should not be declarators
991  if(!declaration.declarators().empty())
992  {
993  error().source_location=declaration.source_location();
994  error() << "class template not expected to have declarators"
995  << eom;
996  throw 0;
997  }
998 
999  // it needs to be a class template
1000  if(type.id()!=ID_struct)
1001  {
1002  error().source_location=declaration.source_location();
1003  error() << "expected class template" << eom;
1004  throw 0;
1005  }
1006 
1007  // Is it class template specialization?
1008  // We can tell if there are template arguments in the class name,
1009  // like template<...> class tag<stuff> ...
1010  if((static_cast<const cpp_namet &>(
1011  type.find(ID_tag))).has_template_args())
1012  {
1014  return;
1015  }
1016 
1017  typecheck_class_template(declaration);
1018  return;
1019  }
1020  // maybe function template, maybe class template member, maybe
1021  // template variable
1022  else
1023  {
1024  // there should be declarators in either case
1025  if(declaration.declarators().empty())
1026  {
1027  error().source_location=declaration.source_location();
1028  error() << "non-class template is expected to have a declarator"
1029  << eom;
1030  throw 0;
1031  }
1032 
1033  // Is it function template specialization?
1034  // Only full specialization is allowed!
1035  if(declaration.template_type().template_parameters().empty())
1036  {
1038  return;
1039  }
1040 
1041  // Explicit qualification is forbidden for function templates,
1042  // which we can use to distinguish them.
1043 
1045  declaration.declarators().size() >= 1, "declarator required");
1046 
1047  cpp_declaratort &declarator=declaration.declarators()[0];
1048  const cpp_namet &cpp_name = declarator.name();
1049 
1050  if(cpp_name.is_qualified() ||
1051  cpp_name.has_template_args())
1052  return typecheck_class_template_member(declaration);
1053 
1054  // must be function template
1055  typecheck_function_template(declaration);
1056  return;
1057  }
1058 }
Generic exception types primarily designed for use with invariants.
symbol_table_baset & symbol_table
const irep_idt module
const declaratorst & declarators() const
void set_specialization_of(const irep_idt &id)
bool is_template() const
const cpp_member_spect & member_spec() const
bool is_class_template() const
template_typet & template_type()
cpp_template_args_non_tct & partial_specialization_args()
bool is_typedef() const
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
cpp_namet & name()
typet merge_type(const typet &declaration_type) const
Definition: cpp_id.h:23
irep_idt identifier
Definition: cpp_id.h:72
std::string prefix
Definition: cpp_id.h:79
id_classt id_class
Definition: cpp_id.h:45
bool is_template_scope() const
Definition: cpp_id.h:67
bool is_virtual() const
bool is_qualified() const
Definition: cpp_name.h:109
irep_idt get_base_name() const
Definition: cpp_name.cpp:14
const source_locationt & source_location() const
Definition: cpp_name.h:73
bool has_template_args() const
Definition: cpp_name.h:124
bool is_simple_name() const
Definition: cpp_name.h:89
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
id_mapt id_map
Definition: cpp_scopes.h:68
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
Definition: cpp_scope.cpp:190
@ SCOPE_ONLY
Definition: cpp_scope.h:30
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition: cpp_scope.h:32
cpp_idt & insert(const irep_idt &_base_name)
Definition: cpp_scope.h:52
exprt::operandst argumentst
std::string class_template_identifier(const irep_idt &base_name, const template_typet &template_type, const cpp_template_args_non_tct &partial_specialization_args)
void typecheck_type(typet &) override
template_mapt template_map
std::string function_template_identifier(const irep_idt &base_name, const template_typet &template_type, const typet &function_type)
void convert_template_declaration(cpp_declarationt &declaration)
void implicit_typecast(exprt &expr, const typet &type) override
void salvage_default_arguments(const template_typet &old_type, template_typet &new_type)
void convert_non_template_declaration(cpp_declarationt &declaration)
void typecheck_function_template(cpp_declarationt &declaration)
typecheck function templates
unsigned template_counter
void typecheck_class_template_member(cpp_declarationt &declaration)
typecheck class template members; these can be methods or static members
cpp_template_args_tct typecheck_template_args(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_non_tct &template_args)
void convert(cpp_linkage_spect &)
void typecheck_expr(exprt &) override
cpp_scopet & typecheck_template_parameters(template_typet &type)
void typecheck_class_template(cpp_declarationt &declaration)
const symbolt & instantiate_template(const source_locationt &source_location, const symbolt &symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args, const typet &specialization=uninitialized_typet{})
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:92
void convert_template_function_or_member_specialization(cpp_declarationt &declaration)
void convert_class_template_specialization(cpp_declarationt &declaration)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
void swap(dstringt &b)
Definition: dstring.h:162
const char * c_str() const
Definition: dstring.h:116
size_t size() const
Definition: dstring.h:121
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
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
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:448
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
void swap(irept &irep)
Definition: irep.h:434
irept & add(const irep_idt &name)
Definition: irep.cpp:103
bool is_nil() const
Definition: irep.h:368
source_locationt source_location
Definition: message.h:239
mstreamt & error() const
Definition: message.h:391
mstreamt & result() const
Definition: message.h:401
message_handlert & get_message_handler()
Definition: message.h:183
static eomt eom
Definition: message.h:289
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
Expression to hold a symbol (variable)
Definition: std_expr.h:131
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
void set(const template_parametert &parameter, const exprt &value)
void swap(template_mapt &template_map)
Definition: template_map.h:37
template_parameterst & template_parameters()
std::vector< template_parametert > template_parameterst
An expression denoting a type.
Definition: std_expr.h:2964
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:72
source_locationt & add_source_location()
Definition: type.h:77
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
C++ Language Conversion.
cpp_declarationt & to_cpp_declaration(irept &irep)
C++ Language Type Checking.
C++ Language Type Checking.
cpp_template_args_non_tct & to_cpp_template_args_non_tc(irept &irep)
std::string cpp_type2name(const typet &type)
std::string cpp_expr2name(const exprt &expr)
C++ Language Module.
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool simplify(exprt &expr, const namespacet &ns)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:407
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#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
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
a template parameter symbol that is a type
Author: Diffblue Ltd.