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