CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_declarator_converter.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
13
14#include <util/c_types.h>
17#include <util/std_types.h>
19
20#include "cpp_type2name.h"
21#include "cpp_typecheck.h"
22#include "cpp_typecheck_fargs.h"
23
26 is_typedef(false),
27 is_template(false),
28 is_template_parameter(false),
29 is_friend(false),
30 linkage_spec(_cpp_typecheck.current_linkage_spec),
32 is_code(false)
33{
34}
35
38 const cpp_storage_spect &storage_spec,
39 const cpp_member_spect &member_spec,
40 cpp_declaratort &declarator)
41{
42 PRECONDITION(declaration_type.is_not_nil());
43
44 if(declaration_type.id()=="cpp-cast-operator")
45 {
46 typet type;
47 type.swap(declarator.name().get_sub().back());
48 declarator.type().add_subtype() = type;
49 cpp_typecheck.typecheck_type(type);
50 cpp_namet::namet name("(" + cpp_type2name(type) + ")");
51 declarator.name().get_sub().back().swap(name);
52 }
53
54 PRECONDITION(declarator.id() == ID_cpp_declarator);
57
60
62
63 // run resolver on scope
64 {
66
68
69 cpp_typecheck_resolve.resolve_scope(
70 declarator.name(), base_name, template_args);
71
72 cpp_scopet *friend_scope = nullptr;
73
74 if(is_friend)
75 {
76 friend_scope = &cpp_typecheck.cpp_scopes.current_scope();
77 save_scope.restore();
78 }
79
80 scope=&cpp_typecheck.cpp_scopes.current_scope();
81
82 // check the declarator-part of the type, in the current scope
83 if(declarator.value().is_nil() || !cpp_typecheck.has_auto(final_type))
84 cpp_typecheck.typecheck_type(final_type);
85
86 if(friend_scope)
88 }
89
91
92 // global-scope arrays must have fixed size
94 cpp_typecheck.check_fixed_size_array(final_type);
95
97
98 if(is_typedef)
100
101 // first see if it is a member
103 {
104 // it's a member! it must be declared already, unless it's a friend
105
106 typet &method_qualifier=
107 static_cast<typet &>(declarator.method_qualifier());
108
109 // adjust template type
111 {
113 typet tmp;
116 }
117
118 // try static first
119 auto maybe_symbol=
120 cpp_typecheck.symbol_table.get_writeable(final_identifier);
121
122 if(!maybe_symbol)
123 {
124 // adjust type if it's a non-static member function
125 if(final_type.id()==ID_code)
126 {
128 cpp_typecheck.cpp_scopes.go_to(*scope);
129
130 cpp_typecheck.add_this_to_method_type(
133 method_qualifier);
134 }
135
137
138 // try again
139 maybe_symbol=cpp_typecheck.symbol_table.get_writeable(final_identifier);
140 if(!maybe_symbol && is_friend)
141 {
143 convert_new_symbol(final_storage_spec, member_spec, declarator);
144 // mark it as weak so that the full declaration can replace the symbol
145 friend_symbol.is_weak = true;
146 return friend_symbol;
147 }
148 else if(!maybe_symbol)
149 {
150 cpp_typecheck.error().source_location=
151 declarator.name().source_location();
152 cpp_typecheck.error()
153 << "member '" << base_name << "' not found in scope '"
154 << scope->identifier << "'" << messaget::eom;
155 throw 0;
156 }
157 }
158
159 symbolt &symbol=*maybe_symbol;
160
161 combine_types(declarator.name().source_location(), final_type, symbol);
162 enforce_rules(symbol);
163
164 // If it is a constructor, we take care of the
165 // object initialization
166 if(
167 final_type.id() == ID_code &&
168 to_code_type(final_type).return_type().id() == ID_constructor)
169 {
170 const cpp_namet &name=declarator.name();
171
172 exprt symbol_expr=
173 cpp_typecheck.resolve(
174 name,
177
178 if(symbol_expr.id() != ID_type)
179 {
180 cpp_typecheck.error().source_location=name.source_location();
181 cpp_typecheck.error() << "expected type" << messaget::eom;
182 throw 0;
183 }
184
185 irep_idt identifier=symbol_expr.type().get(ID_identifier);
186 const symbolt &symb=cpp_typecheck.lookup(identifier);
187 const struct_typet &type = to_struct_type(symb.type);
188
189 if(declarator.find(ID_member_initializers).is_nil())
191
192 cpp_typecheck.check_member_initializers(
193 type.bases(), type.components(), declarator.member_initializers());
194
195 cpp_typecheck.full_member_initialization(
196 type, declarator.member_initializers());
197 }
198
199 if(!final_storage_spec.is_extern())
200 symbol.is_extern=false;
201
202 // initializer?
203 handle_initializer(symbol, declarator);
204
205 return symbol;
206 }
207 else
208 {
209 // no, it's no way a method
210
211 // we won't allow the constructor/destructor type
212 if(final_type.id()==ID_code &&
213 to_code_type(final_type).return_type().id()==ID_constructor)
214 {
215 cpp_typecheck.error().source_location=declarator.name().source_location();
216 cpp_typecheck.error() << "function must have return type"
217 << messaget::eom;
218 throw 0;
219 }
220
221 // already there?
222 const auto maybe_symbol=
223 cpp_typecheck.symbol_table.get_writeable(final_identifier);
224 if(!maybe_symbol)
225 return convert_new_symbol(final_storage_spec, member_spec, declarator);
226 symbolt &symbol=*maybe_symbol;
227
228 if(!final_storage_spec.is_extern())
229 symbol.is_extern = false;
230
231 if(declarator.get_bool(ID_C_template_case))
232 return symbol;
233
234 combine_types(declarator.name().source_location(), final_type, symbol);
235 enforce_rules(symbol);
236
237 // initializer?
238 handle_initializer(symbol, declarator);
239
240 if(symbol.type.id()=="cpp-template-type")
241 {
242 const auto id_set = scope->lookup_identifier(
244
245 if(id_set.empty())
246 {
247 cpp_idt &identifier=
248 cpp_typecheck.cpp_scopes.put_into_scope(symbol, *scope);
250 }
251 }
252
253 return symbol;
254 }
255}
256
258 const source_locationt &source_location,
259 const typet &decl_type,
260 symbolt &symbol)
261{
262 if(symbol.type.id()==decl_type.id() &&
263 decl_type.id()==ID_code)
264 {
265 // functions need special treatment due
266 // to argument names, default values, and inlined-ness
269
270 if(decl_code_type.get_inlined())
271 symbol_code_type.set_inlined(true);
272
273 if(decl_code_type.return_type()==symbol_code_type.return_type() &&
274 decl_code_type.parameters().size()==symbol_code_type.parameters().size())
275 {
276 for(std::size_t i=0; i<decl_code_type.parameters().size(); i++)
277 {
279 decl_code_type.parameters()[i];
281 symbol_code_type.parameters()[i];
282
283 // first check type
284 if(decl_parameter.type()!=symbol_parameter.type())
285 {
286 // The 'this' parameter of virtual functions mismatches
287 if(i != 0 || !symbol_code_type.get_bool(ID_C_is_virtual))
288 {
289 cpp_typecheck.error().source_location=source_location;
290 cpp_typecheck.error()
291 << "symbol '" << symbol.display_name() << "': parameter "
292 << (i + 1) << " type mismatch\n"
293 << "previous type: "
294 << cpp_typecheck.to_string(symbol_parameter.type())
295 << "\nnew type: "
296 << cpp_typecheck.to_string(decl_parameter.type())
297 << messaget::eom;
298 throw 0;
299 }
300 }
301
302 if(symbol.value.is_nil())
303 {
304 symbol_parameter.set_base_name(decl_parameter.get_base_name());
305 // set an empty identifier when no body is available
306 symbol_parameter.set_identifier(irep_idt());
307 symbol_parameter.add_source_location()=
308 decl_parameter.source_location();
309 }
310 }
311
312 // ok
313 return;
314 }
315 }
316 else if(symbol.type==decl_type)
317 return; // ok
318 else if(
319 symbol.type.id() == ID_array &&
320 to_array_type(symbol.type).size().is_nil() && decl_type.id() == ID_array &&
321 to_array_type(symbol.type).element_type() ==
322 to_array_type(decl_type).element_type())
323 {
324 symbol.type = decl_type;
325 return; // ok
326 }
327
328 cpp_typecheck.error().source_location=source_location;
329 cpp_typecheck.error() << "symbol '" << symbol.display_name()
330 << "' already declared with different type:\n"
331 << "original: " << cpp_typecheck.to_string(symbol.type)
332 << "\n new: " << cpp_typecheck.to_string(final_type)
333 << messaget::eom;
334 throw 0;
335}
336
338{
339 // enforce rules for operator overloading
341
342 // enforce rules about main()
343 main_function_rules(symbol);
344}
345
347 symbolt &symbol,
348 cpp_declaratort &declarator)
349{
350 exprt &value=declarator.value();
351
352 // moves member initializers into 'value' - only methods have these
353 if(symbol.type.id() == ID_code)
354 cpp_typecheck.move_member_initializers(
355 declarator.member_initializers(), to_code_type(symbol.type), value);
356
357 // any initializer to be done?
358 if(value.is_nil())
359 return;
360
361 if(symbol.is_extern)
362 {
363 // the symbol is really located here
364 symbol.is_extern=false;
365 }
366
367 if(symbol.value.is_nil())
368 {
369 // no initial value yet
370 symbol.value.swap(value);
371
372 if(!is_code)
373 cpp_typecheck.convert_initializer(symbol);
374 }
375 else
376 {
377#if 0
378 cpp_typecheck.error().source_location=source_location;
379
380 if(is_code)
381 {
382 cpp_typecheck.error() << "body of function '"
383 << symbol.display_name()
384 << "' has already been defined" << messaget::eom;
385 }
386 else
387 {
388 cpp_typecheck.error() << "symbol '"
389 << symbol.display_name()
390 << "' already has an initializer" << messaget::eom;
391 }
392
393 throw 0;
394#endif
395 }
396}
397
399{
400 std::string identifier=id2string(base_name);
401
402 // main is always "C" linkage, as a matter of principle
403 if(is_code && base_name == ID_main && scope->prefix.empty())
404 {
406 }
407
408 if(is_code)
409 {
410 if(linkage_spec==ID_C)
411 {
412 // fine as is
413 }
414 else if(linkage_spec==ID_auto ||
416 {
417 // Is there already an `extern "C"' function with the same name
418 // and the same signature?
419 symbol_table_baset::symbolst::const_iterator c_it =
420 cpp_typecheck.symbol_table.symbols.find(identifier);
421
422 if(c_it!=cpp_typecheck.symbol_table.symbols.end() &&
423 c_it->second.type.id()==ID_code &&
424 cpp_typecheck.function_identifier(final_type)==
425 cpp_typecheck.function_identifier(c_it->second.type))
426 {
427 // leave as is, no decoration
428 }
429 else
430 {
431 // add C++ decoration
432 identifier+=id2string(cpp_typecheck.function_identifier(final_type));
433 }
434 }
435 }
436
437 final_identifier = scope->prefix + identifier;
438}
439
441 const cpp_storage_spect &storage_spec,
442 const cpp_member_spect &member_spec,
443 cpp_declaratort &declarator)
444{
445 irep_idt pretty_name=get_pretty_name();
446
447 symbolt symbol{
451 symbol.base_name=base_name;
452 symbol.value=declarator.value();
453 symbol.location=declarator.name().source_location();
454 symbol.is_extern = storage_spec.is_extern();
455 symbol.is_parameter = declarator.get_is_parameter();
456 symbol.is_weak = storage_spec.is_weak();
457 symbol.module=cpp_typecheck.module;
458 symbol.is_type=is_typedef;
459 symbol.is_macro=is_typedef && !is_template_parameter;
460 symbol.pretty_name=pretty_name;
461
462 if(is_code && !symbol.is_type)
463 {
464 // it is a function
465 symbol.is_static_lifetime = false;
466 symbol.is_thread_local = false;
467
468 symbol.is_file_local = storage_spec.is_static();
469
470 if(member_spec.is_inline())
471 to_code_type(symbol.type).set_inlined(true);
472
473 if(symbol.value.is_nil())
474 {
475 // we don't need the identifiers
476 for(auto &parameter : to_code_type(symbol.type).parameters())
477 parameter.set_identifier(irep_idt());
478 }
479 }
480 else
481 {
482 symbol.is_lvalue = !is_reference(symbol.type) &&
483 !(symbol.type.get_bool(ID_C_constant) &&
484 is_number(symbol.type) && symbol.value.is_constant());
485
486 symbol.is_static_lifetime =
487 !symbol.is_macro && !symbol.is_type &&
488 (cpp_typecheck.cpp_scopes.current_scope().is_global_scope() ||
489 storage_spec.is_static());
490
491 symbol.is_thread_local =
492 (!symbol.is_static_lifetime && !storage_spec.is_extern()) ||
493 storage_spec.is_thread_local();
494
495 symbol.is_file_local =
496 symbol.is_macro ||
497 (!cpp_typecheck.cpp_scopes.current_scope().is_global_scope() &&
498 !storage_spec.is_extern()) ||
499 (cpp_typecheck.cpp_scopes.current_scope().is_global_scope() &&
500 storage_spec.is_static()) ||
501 symbol.is_parameter;
502 }
503
504 if(symbol.is_static_lifetime)
505 cpp_typecheck.dynamic_initializations.push_back(symbol.name);
506
507 // move early, it must be visible before doing any value
508 symbolt *new_symbol;
509
510 if(cpp_typecheck.symbol_table.move(symbol, new_symbol))
511 {
512 cpp_typecheck.error().source_location=symbol.location;
513 cpp_typecheck.error()
514 << "cpp_typecheckt::convert_declarator: symbol_table.move() failed"
515 << messaget::eom;
516 throw 0;
517 }
518
519 if(!is_code)
520 {
521 const auto id_set = cpp_typecheck.cpp_scopes.current_scope().lookup(
523
524 for(const auto &id_ptr : id_set)
525 {
526 const cpp_idt &id = *id_ptr;
527 // the name is already in the scope
528 // this is ok if they belong to different categories
529
530 if(!id.is_class() && !id.is_enum())
531 {
532 cpp_typecheck.error().source_location=new_symbol->location;
533 cpp_typecheck.error()
534 << "'" << base_name << "' already in scope" << messaget::eom;
535 throw 0;
536 }
537 }
538 }
539
540 // put into scope
541 cpp_idt &identifier=
542 cpp_typecheck.cpp_scopes.put_into_scope(*new_symbol, *scope, is_friend);
543
544 if(is_template)
546 else if(is_template_parameter)
548 else if(is_typedef)
550 else
552
553 // do the value
554 if(!new_symbol->is_type)
555 {
556 if(is_code && declarator.type().id()!=ID_template)
557 cpp_typecheck.add_method_body(new_symbol);
558
559 if(!is_code)
560 cpp_typecheck.convert_initializer(*new_symbol);
561 }
562
563 enforce_rules(*new_symbol);
564
565 return *new_symbol;
566}
567
569{
570 if(is_code)
571 {
572 const irept::subt &parameters=
573 final_type.find(ID_parameters).get_sub();
574
575 std::string result=scope->prefix+id2string(base_name)+"(";
576
577 for(auto it = parameters.begin(); it != parameters.end(); ++it)
578 {
579 const typet &parameter_type = ((exprt &)*it).type();
580
581 if(it!=parameters.begin())
582 result+=", ";
583
584 result+=cpp_typecheck.to_string(parameter_type);
585 }
586
587 result+=')';
588
589 return result;
590 }
591
593}
594
599
601 const symbolt &symbol)
602{
603 if(symbol.name==ID_main)
604 {
605 if(symbol.type.id()!=ID_code)
606 {
607 cpp_typecheck.error().source_location=symbol.location;
608 cpp_typecheck.error() << "main must be function" << messaget::eom;
609 throw 0;
610 }
611
612 const typet &return_type=
613 to_code_type(symbol.type).return_type();
614
615 if(return_type!=signed_int_type())
616 {
617 // Too many embedded compilers ignore this rule.
618 #if 0
619 cpp_typecheck.error().source_location=symbol.location;
620 throw "main must return int";
621 #endif
622 }
623 }
624}
signedbv_typet signed_int_type()
Definition c_types.cpp:22
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base type of functions.
Definition std_types.h:583
void handle_initializer(symbolt &symbol, cpp_declaratort &declarator)
symbolt & convert_new_symbol(const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
bool is_code_type(const typet &type) const
void operator_overloading_rules(const symbolt &symbol)
cpp_declarator_convertert(class cpp_typecheckt &_cpp_typecheck)
void combine_types(const source_locationt &source_location, const typet &decl_type, symbolt &symbol)
void main_function_rules(const symbolt &symbol)
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
class cpp_typecheckt & cpp_typecheck
void enforce_rules(const symbolt &symbol)
irept & member_initializers()
typet merge_type(const typet &declaration_type) const
cpp_namet & name()
irept & method_qualifier()
bool get_is_parameter() const
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_inline() const
const source_locationt & source_location() const
Definition cpp_name.h:73
bool is_global_scope() const
Definition cpp_scope.h:82
id_sett lookup_identifier(const irep_idt &id, cpp_idt::id_classt identifier_class)
bool is_static() const
bool is_thread_local() const
bool is_extern() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
bool is_not_nil() const
Definition irep.h:372
subt & get_sub()
Definition irep.h:448
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
static eomt eom
Definition message.h:289
Structure type, corresponds to C style structs.
Definition std_types.h:231
const basest & bases() const
Get the collection of base classes/structs.
Definition std_types.h:262
const componentst & components() const
Definition std_types.h:147
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
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
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
exprt value
Initial value of symbol.
Definition symbol.h:34
const typet & subtype() const
The type of an expression, extends irept.
Definition type.h:29
typet & add_subtype()
Definition type.h:53
C++ Language Type Checking.
template_typet & to_template_type(typet &type)
std::string cpp_type2name(const typet &type)
C++ Language Module.
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
C++ Language Type Checking.
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
bool is_reference(const typet &type)
Returns true if the type is a reference.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
Author: Diffblue Ltd.
dstringt irep_idt