cprover
cpp_typecheck_code.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/source_location.h>
15 
16 #include "cpp_convert_type.h"
18 #include "cpp_template_type.h"
19 #include "cpp_util.h"
20 #include "cpp_exception_id.h"
21 
23 {
24  const irep_idt &statement=code.get_statement();
25 
26  if(statement==ID_try_catch)
27  {
28  code.type()=code_typet();
29  typecheck_try_catch(code);
30  }
31  else if(statement==ID_member_initializer)
32  {
33  code.type()=code_typet();
35  }
36  else if(statement==ID_msc_if_exists ||
37  statement==ID_msc_if_not_exists)
38  {
39  }
40  else if(statement==ID_decl_block)
41  {
42  // type checked already
43  }
44  else
46 }
47 
49 {
50  codet::operandst &operands=code.operands();
51 
52  for(codet::operandst::iterator
53  it=operands.begin();
54  it!=operands.end();
55  it++)
56  {
57  if(it==operands.begin())
58  {
59  // this is the 'try'
60  typecheck_code(to_code(*it));
61  }
62  else
63  {
64  // This is (one of) the catch clauses.
65  codet &code=to_code_block(to_code(*it));
66 
67  // look at the catch operand
68  assert(!code.operands().empty());
69 
70  if(to_code(code.op0()).get_statement()==ID_ellipsis)
71  {
72  code.operands().erase(code.operands().begin());
73 
74  // do body
75  typecheck_code(code);
76  }
77  else
78  {
79  // turn references into non-references
80  {
81  assert(to_code(code.op0()).get_statement()==ID_decl);
82  cpp_declarationt &cpp_declaration=
84 
85  assert(cpp_declaration.declarators().size()==1);
86  cpp_declaratort &declarator=cpp_declaration.declarators().front();
87 
88  if(is_reference(declarator.type()))
89  declarator.type()=declarator.type().subtype();
90  }
91 
92  // typecheck the body
93  typecheck_code(code);
94 
95  // the declaration is now in a decl_block
96 
97  assert(!code.operands().empty());
98  assert(to_code(code.op0()).get_statement()==ID_decl_block);
99 
100  // get the declaration
101  const code_declt &code_decl=
102  to_code_decl(to_code(code.op0().op0()));
103 
104  // get the type
105  const typet &type=code_decl.op0().type();
106 
107  // annotate exception ID
108  it->set(ID_exception_id, cpp_exception_id(type, *this));
109  }
110  }
111  }
112 }
113 
115 {
116  // In addition to the C syntax, C++ also allows a declaration
117  // as condition. E.g.,
118  // if(void *p=...) ...
119 
120  if(code.cond().id()==ID_code)
121  {
122  typecheck_code(to_code(code.cond()));
123  }
124  else
126 }
127 
129 {
130  // In addition to the C syntax, C++ also allows a declaration
131  // as condition. E.g.,
132  // while(void *p=...) ...
133 
134  if(code.cond().id()==ID_code)
135  {
136  typecheck_code(to_code(code.cond()));
137  }
138  else
140 }
141 
143 {
144  // In addition to the C syntax, C++ also allows a declaration
145  // as condition. E.g.,
146  // switch(int i=...) ...
147 
148  if(code.value().id()==ID_code)
149  {
150  // we shall rewrite that into
151  // { int i=....; switch(i) .... }
152 
153  codet decl=to_code(code.value());
154  typecheck_decl(decl);
155 
156  assert(decl.get_statement()==ID_decl_block);
157  assert(decl.operands().size()==1);
158 
159  // replace declaration by its symbol
160  assert(decl.op0().op0().id()==ID_symbol);
161  code.value()=decl.op0().op0();
162 
164 
165  code_blockt code_block;
166  code_block.move_to_operands(decl.op0(), code);
167  code.swap(code_block);
168  }
169  else
171 }
172 
174 {
175  const cpp_namet &member=
176  to_cpp_name(code.find(ID_member));
177 
178  // Let's first typecheck the operands.
179  Forall_operands(it, code)
180  typecheck_expr(*it);
181 
182  // The initializer may be a data member (non-type)
183  // or a parent class (type).
184  // We ask for VAR only, as we get the parent classes via their
185  // constructor!
186  cpp_typecheck_fargst fargs;
187  fargs.in_use=true;
188  fargs.operands=code.operands();
189 
190  // We should only really resolve in qualified mode,
191  // no need to look into the parent.
192  // Plus, this should happen in class scope, not the scope of
193  // the constructor because of the constructor arguments.
194  exprt symbol_expr=
196 
197  if(symbol_expr.type().id()==ID_code)
198  {
199  const code_typet &code_type=to_code_type(symbol_expr.type());
200 
201  assert(code_type.parameters().size()>=1);
202 
203  // It's a parent. Call the constructor that we got.
204  side_effect_expr_function_callt function_call;
205 
206  function_call.function()=symbol_expr;
207  function_call.add_source_location()=code.source_location();
208  function_call.arguments().reserve(code.operands().size()+1);
209 
210  // we have to add 'this'
211  exprt this_expr = cpp_scopes.current_scope().this_expr;
212  assert(this_expr.is_not_nil());
213 
215  this_expr,
216  code_type.parameters().front().type());
217 
218  function_call.arguments().push_back(this_expr);
219 
220  forall_operands(it, code)
221  function_call.arguments().push_back(*it);
222 
223  // done building the expression, check the argument types
224  typecheck_function_call_arguments(function_call);
225 
226  if(symbol_expr.get_bool("#not_accessible"))
227  {
228  irep_idt access = symbol_expr.get(ID_C_access);
229 
230  assert(access==ID_private ||
231  access==ID_protected ||
232  access=="noaccess");
233 
234  if(access==ID_private || access=="noaccess")
235  {
236  #if 0
238  str << "error: constructor of `"
239  << to_string(symbol_expr)
240  << "' is not accessible";
241  throw 0;
242  #endif
243  }
244  }
245 
246  code_expressiont code_expression;
247  code_expression.expression()=function_call;
248 
249  code.swap(code_expression);
250  }
251  else
252  {
253  // a reference member
254  if(symbol_expr.id() == ID_dereference &&
255  symbol_expr.op0().id() == ID_member &&
256  symbol_expr.get_bool(ID_C_implicit) == true)
257  {
258  // treat references as normal pointers
259  exprt tmp = symbol_expr.op0();
260  symbol_expr.swap(tmp);
261  }
262 
263  if(symbol_expr.id() == ID_symbol &&
264  symbol_expr.type().id()!=ID_code)
265  {
266  // maybe the name of the member collides with a parameter of the
267  // constructor
268  symbol_expr.make_nil();
269  cpp_typecheck_fargst fargs;
271  ID_dereference, cpp_scopes.current_scope().this_expr.type().subtype());
273  fargs.add_object(dereference);
274 
275  {
276  cpp_save_scopet cpp_saved_scope(cpp_scopes);
279  symbol_expr=resolve(member, cpp_typecheck_resolvet::wantt::VAR, fargs);
280  }
281 
282  if(symbol_expr.id() == ID_dereference &&
283  symbol_expr.op0().id() == ID_member &&
284  symbol_expr.get_bool(ID_C_implicit) == true)
285  {
286  // treat references as normal pointers
287  exprt tmp = symbol_expr.op0();
288  symbol_expr.swap(tmp);
289  }
290  }
291 
292  if(symbol_expr.id() == ID_member &&
293  symbol_expr.op0().id() == ID_dereference &&
294  symbol_expr.op0().op0() == cpp_scopes.current_scope().this_expr)
295  {
296  if(is_reference(symbol_expr.type()))
297  {
298  // it's a reference member
299  if(code.operands().size()!= 1)
300  {
302  error() << " reference `" << to_string(symbol_expr)
303  << "' expects one initializer" << eom;
304  throw 0;
305  }
306 
307  reference_initializer(code.op0(), symbol_expr.type());
308 
309  // assign the pointers
310  symbol_expr.type().remove("#reference");
311  symbol_expr.set("#lvalue", true);
312  code.op0().type().remove("#reference");
313 
314  side_effect_exprt assign(ID_assign);
315  assign.add_source_location() = code.source_location();
316  assign.copy_to_operands(symbol_expr, code.op0());
318  code_expressiont new_code;
319  new_code.expression()=assign;
320  code.swap(new_code);
321  }
322  else
323  {
324  // it's a data member
325  already_typechecked(symbol_expr);
326 
327  Forall_operands(it, code)
328  already_typechecked(*it);
329 
330  exprt call=
331  cpp_constructor(code.source_location(), symbol_expr, code.operands());
332 
333  if(call.is_nil())
334  {
335  call=codet(ID_skip);
336  call.add_source_location()=code.source_location();
337  }
338 
339  code.swap(call);
340  }
341  }
342  else
343  {
345  error() << "invalid member initializer `"
346  << to_string(symbol_expr) << "'" << eom;
347  throw 0;
348  }
349  }
350 }
351 
353 {
354  if(code.operands().size()!=1)
355  {
357  error() << "declaration expected to have one operand" << eom;
358  throw 0;
359  }
360 
361  assert(code.op0().id()==ID_cpp_declaration);
362 
363  cpp_declarationt &declaration=
364  to_cpp_declaration(code.op0());
365 
366  typet &type=declaration.type();
367 
368  bool is_typedef=declaration.is_typedef();
369 
370  typecheck_type(type);
371  assert(type.is_not_nil());
372 
373  if(declaration.declarators().empty() &&
374  follow(type).get_bool(ID_C_is_anonymous))
375  {
376  if(follow(type).id()!=ID_union)
377  {
379  error() << "declaration statement does not declare anything"
380  << eom;
381  throw 0;
382  }
383 
384  convert_anonymous_union(declaration, code);
385  return;
386  }
387 
388  codet new_code(ID_decl_block);
389  new_code.reserve_operands(declaration.declarators().size());
390 
391  // Do the declarators (if any)
392  for(auto &declarator : declaration.declarators())
393  {
394  cpp_declarator_convertert cpp_declarator_converter(*this);
395  cpp_declarator_converter.is_typedef=is_typedef;
396 
397  const symbolt &symbol=
398  cpp_declarator_converter.convert(declaration, declarator);
399 
400  if(is_typedef)
401  continue;
402 
403  codet decl_statement(ID_decl);
404  decl_statement.reserve_operands(2);
405  decl_statement.add_source_location()=symbol.location;
406  decl_statement.copy_to_operands(cpp_symbol_expr(symbol));
407 
408  // Do we have an initializer that's not code?
409  if(symbol.value.is_not_nil() &&
410  symbol.value.id()!=ID_code)
411  {
412  decl_statement.copy_to_operands(symbol.value);
413  assert(follow(decl_statement.op1().type())==follow(symbol.type));
414  }
415 
416  new_code.move_to_operands(decl_statement);
417 
418  // is there a constructor to be called?
419  if(symbol.value.is_not_nil())
420  {
421  assert(declarator.find("init_args").is_nil());
422  if(symbol.value.id()==ID_code)
423  new_code.copy_to_operands(symbol.value);
424  }
425  else
426  {
427  exprt object_expr=cpp_symbol_expr(symbol);
428 
429  already_typechecked(object_expr);
430 
431  exprt constructor_call=
433  symbol.location,
434  object_expr,
435  declarator.init_args().operands());
436 
437  if(constructor_call.is_not_nil())
438  new_code.move_to_operands(constructor_call);
439  }
440  }
441 
442  code.swap(new_code);
443 }
444 
446 {
447  cpp_save_scopet saved_scope(cpp_scopes);
449 
451 }
452 
454 {
455  if(code.operands().size()!=2)
456  {
458  error() << "assignment statement expected to have two operands"
459  << eom;
460  throw 0;
461  }
462 
463  // turn into a side effect
464  side_effect_exprt expr(code.get(ID_statement));
465  expr.operands() = code.operands();
466  typecheck_expr(expr);
467 
468  code_expressiont code_expr;
469  code_expr.expression()=expr;
470  code_expr.add_source_location() = code.source_location();
471 
472  code.swap(code_expr);
473 }
C++ Language Type Checking.
const irep_idt & get_statement() const
Definition: std_code.h:37
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
void typecheck_type(typet &type)
A ‘switch’ instruction.
Definition: std_code.h:412
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
exprt & op0()
Definition: expr.h:84
const exprt & cond() const
Definition: std_code.h:465
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_switch(code_switcht &code)
const exprt & cond() const
Definition: std_code.h:360
exprt & symbol()
Definition: std_code.h:205
exprt::operandst operands
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:143
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
virtual void typecheck_code(codet &code)
exprt value
Initial value of symbol.
Definition: symbol.h:40
typet & type()
Definition: expr.h:60
void typecheck_assign(codet &code)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void typecheck_block(codet &code)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
An expression statement.
Definition: std_code.h:957
virtual void typecheck_expr(exprt &expr)
const irep_idt & id() const
Definition: irep.h:189
virtual void typecheck_try_catch(codet &code)
void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
exprt dereference(const exprt &pointer, const namespacet &ns)
Definition: dereference.h:88
A declaration of a local variable.
Definition: std_code.h:192
virtual void typecheck_ifthenelse(code_ifthenelset &code)
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
C++ Language Conversion.
C++ Language Type Checking.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
#define forall_operands(it, expr)
Definition: expr.h:17
irep_idt class_identifier
Definition: cpp_id.h:76
void add_object(const exprt &expr)
A ‘while’ instruction.
Definition: std_code.h:457
C++ Language Type Checking.
void typecheck_side_effect_assignment(side_effect_exprt &expr)
irep_idt cpp_exception_id(const typet &src, const namespacet &ns)
turns a type into an exception ID
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
Definition: cpp_typecheck.h:87
virtual void typecheck_switch(code_switcht &code)
virtual void typecheck_block(codet &code)
void make_ptr_typecast(exprt &expr, const typet &dest_type)
id_mapt id_map
Definition: cpp_scopes.h:69
std::vector< exprt > operandst
Definition: expr.h:49
exprt this_expr
Definition: cpp_id.h:77
A function call side effect.
Definition: std_code.h:1052
const exprt & value() const
Definition: std_code.h:420
virtual void typecheck_decl(codet &code)
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)
void convert_anonymous_union(cpp_declarationt &declaration, codet &new_code)
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
const source_locationt & source_location() const
Definition: expr.h:142
virtual void typecheck_while(code_whilet &code)
const exprt & expression() const
Definition: std_code.h:970
virtual std::string to_string(const typet &type)
cpp_scopet & new_block_scope()
Definition: cpp_scopes.cpp:16
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
An if-then-else.
Definition: std_code.h:350
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
virtual void typecheck_ifthenelse(code_ifthenelset &code)
A statement in a programming language.
Definition: std_code.h:19
exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
void remove(const irep_namet &name)
Definition: irep.cpp:270
const typet & subtype() const
Definition: type.h:31
An expression containing a side effect.
Definition: std_code.h:997
operandst & operands()
Definition: expr.h:70
virtual void typecheck_member_initializer(codet &code)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
codet cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
void reference_initializer(exprt &expr, const typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows: ...
virtual void typecheck_code(codet &code)
cpp_scopest cpp_scopes