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