cprover
cpp_instantiate_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 "cpp_typecheck.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #endif
17 
18 #include <util/arith_tools.h>
19 #include <util/base_exceptions.h>
20 #include <util/simplify_expr.h>
21 
22 #include <util/c_types.h>
23 
24 #include "cpp_type2name.h"
25 
27  const cpp_template_args_tct &template_args)
28 {
29  // quick hack
30  std::string result="<";
31  bool first=true;
32 
33  const cpp_template_args_tct::argumentst &arguments=
34  template_args.arguments();
35 
36  for(cpp_template_args_tct::argumentst::const_iterator
37  it=arguments.begin();
38  it!=arguments.end();
39  it++)
40  {
41  if(first)
42  first=false;
43  else
44  result+=',';
45 
46  const exprt expr=*it;
47 
48  assert(expr.id()!="ambiguous");
49 
50  if(expr.id()==ID_type)
51  {
52  const typet &type=expr.type();
53  if(type.id()==ID_symbol)
54  result+=type.get_string(ID_identifier);
55  else
56  result+=cpp_type2name(type);
57  }
58  else // expression
59  {
60  exprt e=expr;
61  make_constant(e);
62 
63  // this must be a constant, which includes true/false
64  mp_integer i;
65 
66  if(e.is_true())
67  i=1;
68  else if(e.is_false())
69  i=0;
70  else if(to_integer(e, i))
71  {
72  error().source_location=it->find_source_location();
73  error() << "template argument expression expected to be "
74  << "scalar constant, but got `"
75  << to_string(e) << "'" << eom;
76  throw 0;
77  }
78 
80  }
81  }
82 
83  result+='>';
84 
85  return result;
86 }
87 
89 {
90  for(instantiation_stackt::const_iterator
91  s_it=instantiation_stack.begin();
92  s_it!=instantiation_stack.end();
93  s_it++)
94  {
95  const symbolt &symbol=lookup(s_it->identifier);
96  out << "instantiating `" << symbol.pretty_name << "' with <";
97 
98  forall_expr(a_it, s_it->full_template_args.arguments())
99  {
100  if(a_it!=s_it->full_template_args.arguments().begin())
101  out << ", ";
102 
103  if(a_it->id()==ID_type)
104  out << to_string(a_it->type());
105  else
106  out << to_string(*a_it);
107  }
108 
109  out << "> at " << s_it->source_location << '\n';
110  }
111 }
112 
114  const source_locationt &source_location,
115  const symbolt &template_symbol,
116  const cpp_template_args_tct &specialization_template_args,
117  const cpp_template_args_tct &full_template_args)
118 {
119  // we should never get 'unassigned' here
120  assert(!full_template_args.has_unassigned());
121 
122  // do we have args?
123  if(full_template_args.arguments().empty())
124  {
125  error().source_location=source_location;
126  error() << "`" << template_symbol.base_name
127  << "' is a template; thus, expected template arguments"
128  << eom;
129  throw 0;
130  }
131 
132  // produce new symbol name
133  std::string suffix=template_suffix(full_template_args);
134 
135  cpp_scopet *template_scope=
136  static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
137 
139  template_scope!=nullptr, nullptr_exceptiont, "template_scope is null");
140 
141  irep_idt identifier=
142  id2string(template_scope->prefix)+
143  "tag-"+id2string(template_symbol.base_name)+
144  id2string(suffix);
145 
146  // already there?
147  symbol_tablet::symbolst::const_iterator s_it=
148  symbol_table.symbols.find(identifier);
149  if(s_it!=symbol_table.symbols.end())
150  return s_it->second;
151 
152  // Create as incomplete_struct, but mark as
153  // "template_class_instance", to be elaborated later.
154  symbolt new_symbol;
155  new_symbol.name=identifier;
156  new_symbol.pretty_name=template_symbol.pretty_name;
157  new_symbol.location=template_symbol.location;
158  new_symbol.type=typet(ID_incomplete_struct);
159  new_symbol.type.set(ID_tag, template_symbol.type.find(ID_tag));
160  if(template_symbol.type.get_bool(ID_C_class))
161  new_symbol.type.set(ID_C_class, true);
162  new_symbol.type.set(ID_template_class_instance, true);
163  new_symbol.type.add_source_location()=template_symbol.location;
164  new_symbol.type.set(
165  "specialization_template_args", specialization_template_args);
166  new_symbol.type.set("full_template_args", full_template_args);
167  new_symbol.type.set(ID_identifier, template_symbol.name);
168  new_symbol.mode=template_symbol.mode;
169  new_symbol.base_name=template_symbol.base_name;
170  new_symbol.is_type=true;
171 
172  symbolt *s_ptr;
173  symbol_table.move(new_symbol, s_ptr);
174 
175  // put into template scope
176  cpp_idt &id=cpp_scopes.put_into_scope(*s_ptr, *template_scope);
177 
179  id.is_scope=true;
180  id.prefix=template_scope->prefix+
181  id2string(s_ptr->base_name)+
182  id2string(suffix)+"::";
183  id.class_identifier=s_ptr->name;
184  id.id_class=cpp_idt::id_classt::CLASS;
185 
186  return *s_ptr;
187 }
188 
191  const typet &type)
192 {
193  if(type.id()!=ID_symbol)
194  return;
195 
196  const symbolt &symbol = lookup(to_symbol_type(type));
197 
198  // Make a copy, as instantiate will destroy the symbol type!
199  const typet t_type=symbol.type;
200 
201  if(t_type.id()==ID_incomplete_struct &&
202  t_type.get_bool(ID_template_class_instance))
203  {
205  type.source_location(),
206  lookup(t_type.get(ID_identifier)),
207  static_cast<const cpp_template_args_tct &>(
208  t_type.find("specialization_template_args")),
209  static_cast<const cpp_template_args_tct &>(
210  t_type.find("full_template_args")));
211  }
212 }
213 
218 #define MAX_DEPTH 50
219 
221  const source_locationt &source_location,
222  const symbolt &template_symbol,
223  const cpp_template_args_tct &specialization_template_args,
224  const cpp_template_args_tct &full_template_args,
225  const typet &specialization)
226 {
227 #ifdef DEBUG
228  std::cout << "instantiate_template: " << template_symbol.name << '\n';
229 #endif
230 
231  if(instantiation_stack.size()==MAX_DEPTH)
232  {
233  error().source_location=source_location;
234  error() << "reached maximum template recursion depth ("
235  << MAX_DEPTH << ")" << eom;
236  throw 0;
237  }
238 
240  instantiation_stack.back().source_location=source_location;
241  instantiation_stack.back().identifier=template_symbol.name;
242  instantiation_stack.back().full_template_args=full_template_args;
243 
244 #ifdef DEBUG
245  std::cout << "L: " << source_location << '\n';
246  std::cout << "I: " << template_symbol.name << '\n';
247 #endif
248 
250 
251  bool specialization_given=specialization.is_not_nil();
252 
253  // we should never get 'unassigned' here
254  assert(!specialization_template_args.has_unassigned());
255  assert(!full_template_args.has_unassigned());
256 
257 #ifdef DEBUG
258  std::cout << "A: <";
259  forall_expr(it, specialization_template_args.arguments())
260  {
261  if(it!=specialization_template_args.arguments().begin())
262  std::cout << ", ";
263  if(it->id()==ID_type)
264  std::cout << to_string(it->type());
265  else
266  std::cout << to_string(*it);
267  }
268  std::cout << ">\n\n";
269 #endif
270 
271  // do we have arguments?
272  if(full_template_args.arguments().empty())
273  {
274  error().source_location=source_location;
275  error() << "`" << template_symbol.base_name
276  << "' is a template; thus, expected template arguments"
277  << eom;
278  throw 0;
279  }
280 
281  // produce new symbol name
282  std::string suffix=template_suffix(full_template_args);
283 
284  // we need the template scope to see the template parameters
285  cpp_scopet *template_scope=
286  static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
287 
288  if(template_scope==nullptr)
289  {
290  error().source_location=source_location;
291  error() << "identifier: " << template_symbol.name << '\n'
292  << "template instantiation error: scope not found" << eom;
293  throw 0;
294  }
295 
296  // produce new declaration
297  cpp_declarationt new_decl=to_cpp_declaration(template_symbol.type);
298 
299  // The new one is not a template any longer, but we remember the
300  // template type that was used.
301  template_typet template_type=new_decl.template_type();
302  new_decl.remove(ID_is_template);
303  new_decl.remove(ID_template_type);
304  new_decl.set(ID_C_template, template_symbol.name);
305  new_decl.set(ID_C_template_arguments, specialization_template_args);
306 
307  // save old scope
308  cpp_save_scopet saved_scope(cpp_scopes);
309 
310  // mapping from template parameters to values/types
311  template_map.build(template_type, specialization_template_args);
312 
313  // enter the template scope
314  cpp_scopes.go_to(*template_scope);
315 
316  // Is it a template method?
317  // It's in the scope of a class, and not a class itself.
318  bool is_template_method=
320  new_decl.type().id()!=ID_struct;
321 
322  irep_idt class_name;
323 
324  if(is_template_method)
326 
327  // sub-scope for fixing the prefix
328  std::string subscope_name=id2string(template_scope->identifier)+suffix;
329 
330  // let's see if we have the instance already
331  cpp_scopest::id_mapt::iterator scope_it=
332  cpp_scopes.id_map.find(subscope_name);
333 
334  if(scope_it!=cpp_scopes.id_map.end())
335  {
336  cpp_scopet &scope=cpp_scopes.get_scope(subscope_name);
337 
339  scope.lookup(template_symbol.base_name, cpp_scopet::SCOPE_ONLY, id_set);
340 
341  if(id_set.size()==1)
342  {
343  // It has already been instantiated!
344  const cpp_idt &cpp_id = **id_set.begin();
345 
346  assert(cpp_id.id_class == cpp_idt::id_classt::CLASS ||
348 
349  const symbolt &symb=lookup(cpp_id.identifier);
350 
351  // continue if the type is incomplete only
352  if(cpp_id.id_class==cpp_idt::id_classt::CLASS &&
353  symb.type.id()==ID_struct)
354  return symb;
355  else if(symb.value.is_not_nil())
356  return symb;
357  }
358 
359  cpp_scopes.go_to(scope);
360  }
361  else
362  {
363  // set up a scope as subscope of the template scope
364  cpp_scopet &sub_scope=
365  cpp_scopes.current_scope().new_scope(subscope_name);
367  sub_scope.prefix=template_scope->get_parent().prefix;
368  sub_scope.suffix=suffix;
369  sub_scope.add_using_scope(template_scope->get_parent());
370  cpp_scopes.go_to(sub_scope);
371  cpp_scopes.id_map.insert(
372  cpp_scopest::id_mapt::value_type(subscope_name, &sub_scope));
373  }
374 
375  // store the information that the template has
376  // been instantiated using these arguments
377  {
378  // need non-const handle on template symbol
379  symbolt &s=*symbol_table.get_writeable(template_symbol.name);
380  irept &instantiated_with=s.value.add("instantiated_with");
381  instantiated_with.get_sub().push_back(specialization_template_args);
382  }
383 
384  #ifdef DEBUG
385  std::cout << "CLASS MAP:\n";
386  template_map.print(std::cout);
387  #endif
388 
389  // fix the type
390  {
391  typet declaration_type=new_decl.type();
392 
393  // specialization?
394  if(specialization_given)
395  {
396  if(declaration_type.id()==ID_struct)
397  {
398  declaration_type=specialization;
399  declaration_type.add_source_location()=source_location;
400  }
401  else
402  {
403  irept tmp=specialization;
404  new_decl.declarators()[0].swap(tmp);
405  }
406  }
407 
408  template_map.apply(declaration_type);
409  new_decl.type().swap(declaration_type);
410  }
411 
412  if(new_decl.type().id()==ID_struct)
413  {
414  // a class template
416 
417  // also instantiate all the template methods
418  const exprt &template_methods=
419  static_cast<const exprt &>(
420  template_symbol.value.find("template_methods"));
421 
422  for(auto &tm : template_methods.operands())
423  {
424  saved_scope.restore();
425 
426  cpp_declarationt method_decl=
427  static_cast<const cpp_declarationt &>(
428  static_cast<const irept &>(tm));
429 
430  // copy the type of the template method
431  template_typet method_type=
432  method_decl.template_type();
433 
434  // do template parameters
435  // this also sets up the template scope of the method
436  cpp_scopet &method_scope=
437  typecheck_template_parameters(method_type);
438 
439  cpp_scopes.go_to(method_scope);
440 
441  // mapping from template arguments to values/types
442  template_map.build(method_type, specialization_template_args);
443 #ifdef DEBUG
444  std::cout << "METHOD MAP:\n";
445  template_map.print(std::cout);
446 #endif
447 
448  method_decl.remove(ID_template_type);
449  method_decl.remove(ID_is_template);
450 
451  convert(method_decl);
452  }
453 
454  const irep_idt& new_symb_id = new_decl.type().get(ID_identifier);
455  symbolt &new_symb = symbol_table.get_writeable_ref(new_symb_id);
456 
457  // add template arguments to type in order to retrieve template map when
458  // typechecking function body
459  new_symb.type.set(ID_C_template, template_type);
460  new_symb.type.set(ID_C_template_arguments, specialization_template_args);
461 
462 #ifdef DEBUG
463  std::cout << "instance symbol: " << new_symb.name << "\n\n";
464  std::cout << "template type: " << template_type.pretty() << "\n\n";
465 #endif
466 
467  return new_symb;
468  }
469 
470  if(is_template_method)
471  {
472  symbolt &symb=*symbol_table.get_writeable(class_name);
473 
474  assert(new_decl.declarators().size() == 1);
475 
476  if(new_decl.member_spec().is_virtual())
477  {
479  error() << "invalid use of `virtual' in template declaration"
480  << eom;
481  throw 0;
482  }
483 
484  if(new_decl.is_typedef())
485  {
487  error() << "template declaration for typedef" << eom;
488  throw 0;
489  }
490 
491  if(new_decl.storage_spec().is_extern() ||
492  new_decl.storage_spec().is_auto() ||
493  new_decl.storage_spec().is_register() ||
494  new_decl.storage_spec().is_mutable())
495  {
497  error() << "invalid storage class specified for template field"
498  << eom;
499  throw 0;
500  }
501 
502  bool is_static=new_decl.storage_spec().is_static();
503  irep_idt access = new_decl.get(ID_C_access);
504 
505  assert(!access.empty());
506  assert(symb.type.id()==ID_struct);
507 
509  symb,
510  new_decl,
511  new_decl.declarators()[0],
513  access,
514  is_static,
515  false,
516  false);
517 
518  return lookup(to_struct_type(symb.type).components().back().get(ID_name));
519  }
520 
521  // not a class template, not a class template method,
522  // it must be a function template!
523 
524  assert(new_decl.declarators().size()==1);
525 
527 
528  const symbolt &symb=
529  lookup(new_decl.declarators()[0].get(ID_identifier));
530 
531  return symb;
532 }
bool is_typedef() const
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition: invariant.h:216
void apply(exprt &dest) const
BigInt mp_integer
Definition: mp_arith.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
bool is_mutable() const
const cpp_storage_spect & storage_spec() const
void lookup(const irep_idt &base_name, lookup_kindt kind, id_sett &id_set)
Definition: cpp_scope.cpp:29
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
void convert_non_template_declaration(cpp_declarationt &declaration)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
virtual void make_constant(exprt &expr)
irep_idt mode
Language mode.
Definition: symbol.h:52
instantiation_stackt instantiation_stack
exprt::operandst argumentst
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=typet(ID_nil))
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
Definition: cpp_scope.cpp:200
#define forall_expr(it, expr)
Definition: expr.h:28
bool is_auto() const
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
bool is_false() const
Definition: expr.cpp:131
cpp_scopet & get_parent() const
Definition: cpp_scope.h:89
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
void show_instantiation_stack(std::ostream &)
exprt value
Initial value of symbol.
Definition: symbol.h:37
const componentst & components() const
Definition: std_types.h:245
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
template_mapt template_map
bool is_true() const
Definition: expr.cpp:124
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
bool is_register() const
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
void build(const template_typet &template_type, const cpp_template_args_tct &template_args)
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
cpp_scopet & typecheck_template_parameters(template_typet &type)
const cpp_member_spect & member_spec() const
std::string suffix
Definition: cpp_id.h:80
subt & get_sub()
Definition: irep.h:317
void convert(cpp_linkage_spect &)
void typecheck_compound_declarator(const symbolt &symbol, const cpp_declarationt &declaration, cpp_declaratort &declarator, struct_typet::componentst &components, const irep_idt &access, bool is_static, bool is_typedef, bool is_mutable)
symbol_tablet & symbol_table
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:87
std::string prefix
Definition: cpp_id.h:80
const irep_idt & id() const
Definition: irep.h:259
void elaborate_class_template(const typet &type)
elaborate class template instances
const declaratorst & declarators() const
bool is_extern() const
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
C++ Language Module.
source_locationt source_location
Definition: message.h:214
irep_idt identifier
Definition: cpp_id.h:73
id_classt id_class
Definition: cpp_id.h:51
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
bool is_static() const
std::string cpp_type2name(const typet &type)
Base class for tree-like data structures with sharing.
Definition: irep.h:156
C++ Language Type Checking.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const symbolst & symbols
std::string template_suffix(const cpp_template_args_tct &template_args)
bool is_class() const
Definition: cpp_id.h:53
id_mapt id_map
Definition: cpp_scopes.h:69
const source_locationt & source_location() const
Definition: type.h:97
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
cpp_declarationt & to_cpp_declaration(irept &irep)
mstreamt & result() const
Definition: message.h:312
const symbolt & class_template_symbol(const source_locationt &source_location, const symbolt &template_symbol, const cpp_template_args_tct &specialization_template_args, const cpp_template_args_tct &full_template_args)
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
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
virtual std::string to_string(const typet &type)
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
void swap(irept &irep)
Definition: irep.h:303
cpp_scopet & get_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:81
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
Definition: cpp_id.h:28
void remove(const irep_namet &name)
Definition: irep.cpp:270
operandst & operands()
Definition: expr.h:66
template_typet & template_type()
#define MAX_DEPTH
Generic exception types primarily designed for use with invariants.
bool empty() const
Definition: dstring.h:73
std::set< cpp_idt * > id_sett
Definition: cpp_scope.h:28
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:136
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
void add_using_scope(cpp_scopet &other)
Definition: cpp_scope.h:110
bool is_virtual() const
void print(std::ostream &out) const
cpp_scopest cpp_scopes