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({}, empty_typet());
29  typecheck_try_catch(code);
30  }
31  else if(statement==ID_member_initializer)
32  {
33  code.type() = code_typet({}, empty_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  {
181  const bool has_array_ini = it->get_bool(ID_C_array_ini);
182  typecheck_expr(*it);
183  if(has_array_ini)
184  it->set(ID_C_array_ini, true);
185  }
186 
187  // The initializer may be a data member (non-type)
188  // or a parent class (type).
189  // We ask for VAR only, as we get the parent classes via their
190  // constructor!
191  cpp_typecheck_fargst fargs;
192  fargs.in_use=true;
193  fargs.operands=code.operands();
194 
195  // We should only really resolve in qualified mode,
196  // no need to look into the parent.
197  // Plus, this should happen in class scope, not the scope of
198  // the constructor because of the constructor arguments.
199  exprt symbol_expr=
201 
202  if(symbol_expr.type().id()==ID_code)
203  {
204  const code_typet &code_type=to_code_type(symbol_expr.type());
205 
206  assert(code_type.parameters().size()>=1);
207 
208  // It's a parent. Call the constructor that we got.
209  side_effect_expr_function_callt function_call;
210 
211  function_call.function()=symbol_expr;
212  function_call.add_source_location()=code.source_location();
213  function_call.arguments().reserve(code.operands().size()+1);
214 
215  // we have to add 'this'
216  exprt this_expr = cpp_scopes.current_scope().this_expr;
217  assert(this_expr.is_not_nil());
218 
220  this_expr,
221  code_type.parameters().front().type());
222 
223  function_call.arguments().push_back(this_expr);
224 
225  forall_operands(it, code)
226  function_call.arguments().push_back(*it);
227 
228  // done building the expression, check the argument types
229  typecheck_function_call_arguments(function_call);
230 
231  if(symbol_expr.get_bool(ID_C_not_accessible))
232  {
233  irep_idt access = symbol_expr.get(ID_C_access);
234 
235  assert(access==ID_private ||
236  access==ID_protected ||
237  access=="noaccess");
238 
239  if(access==ID_private || access=="noaccess")
240  {
241  #if 0
243  str << "error: constructor of `"
244  << to_string(symbol_expr)
245  << "' is not accessible";
246  throw 0;
247  #endif
248  }
249  }
250 
251  code_expressiont code_expression;
252  code_expression.expression()=function_call;
253 
254  code.swap(code_expression);
255  }
256  else
257  {
258  // a reference member
259  if(symbol_expr.id() == ID_dereference &&
260  symbol_expr.op0().id() == ID_member &&
261  symbol_expr.get_bool(ID_C_implicit) == true)
262  {
263  // treat references as normal pointers
264  exprt tmp = symbol_expr.op0();
265  symbol_expr.swap(tmp);
266  }
267 
268  if(symbol_expr.id() == ID_symbol &&
269  symbol_expr.type().id()!=ID_code)
270  {
271  // maybe the name of the member collides with a parameter of the
272  // constructor
273  symbol_expr.make_nil();
274  cpp_typecheck_fargst fargs;
276  ID_dereference, cpp_scopes.current_scope().this_expr.type().subtype());
278  fargs.add_object(dereference);
279 
280  {
281  cpp_save_scopet cpp_saved_scope(cpp_scopes);
284  symbol_expr=resolve(member, cpp_typecheck_resolvet::wantt::VAR, fargs);
285  }
286 
287  if(symbol_expr.id() == ID_dereference &&
288  symbol_expr.op0().id() == ID_member &&
289  symbol_expr.get_bool(ID_C_implicit) == true)
290  {
291  // treat references as normal pointers
292  exprt tmp = symbol_expr.op0();
293  symbol_expr.swap(tmp);
294  }
295  }
296 
297  if(symbol_expr.id() == ID_member &&
298  symbol_expr.op0().id() == ID_dereference &&
299  symbol_expr.op0().op0() == cpp_scopes.current_scope().this_expr)
300  {
301  if(is_reference(symbol_expr.type()))
302  {
303  // it's a reference member
304  if(code.operands().size()!= 1)
305  {
307  error() << " reference `" << to_string(symbol_expr)
308  << "' expects one initializer" << eom;
309  throw 0;
310  }
311 
312  reference_initializer(code.op0(), symbol_expr.type());
313 
314  // assign the pointers
315  symbol_expr.type().remove(ID_C_reference);
316  symbol_expr.set(ID_C_lvalue, true);
317  code.op0().type().remove(ID_C_reference);
318 
319  side_effect_exprt assign(ID_assign, typet(), code.source_location());
320  assign.copy_to_operands(symbol_expr, code.op0());
322  code_expressiont new_code(assign);
323  code.swap(new_code);
324  }
325  else
326  {
327  // it's a data member
328  already_typechecked(symbol_expr);
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  if(declaration.declarators().empty() || !has_auto(type))
371  typecheck_type(type);
372 
373  assert(type.is_not_nil());
374 
375  if(declaration.declarators().empty() &&
376  follow(type).get_bool(ID_C_is_anonymous))
377  {
378  if(follow(type).id()!=ID_union)
379  {
381  error() << "declaration statement does not declare anything"
382  << eom;
383  throw 0;
384  }
385 
386  convert_anonymous_union(declaration, code);
387  return;
388  }
389 
390  // mark as 'already typechecked'
392 
393  codet new_code(ID_decl_block);
394  new_code.reserve_operands(declaration.declarators().size());
395 
396  // Do the declarators (if any)
397  for(auto &declarator : declaration.declarators())
398  {
399  cpp_declarator_convertert cpp_declarator_converter(*this);
400  cpp_declarator_converter.is_typedef=is_typedef;
401 
402  const symbolt &symbol=
403  cpp_declarator_converter.convert(declaration, declarator);
404 
405  if(is_typedef)
406  continue;
407 
408  code_declt decl_statement(cpp_symbol_expr(symbol));
409  decl_statement.add_source_location()=symbol.location;
410 
411  // Do we have an initializer that's not code?
412  if(symbol.value.is_not_nil() &&
413  symbol.value.id()!=ID_code)
414  {
415  decl_statement.copy_to_operands(symbol.value);
417  has_auto(symbol.type) ||
418  follow(decl_statement.op1().type()) == follow(symbol.type),
419  "declarator type should match symbol type");
420  }
421 
422  new_code.move_to_operands(decl_statement);
423 
424  // is there a constructor to be called?
425  if(symbol.value.is_not_nil())
426  {
427  assert(declarator.find("init_args").is_nil());
428  if(symbol.value.id()==ID_code)
429  new_code.copy_to_operands(symbol.value);
430  }
431  else
432  {
433  exprt object_expr=cpp_symbol_expr(symbol);
434 
435  already_typechecked(object_expr);
436 
437  exprt constructor_call=
439  symbol.location,
440  object_expr,
441  declarator.init_args().operands());
442 
443  if(constructor_call.is_not_nil())
444  new_code.move_to_operands(constructor_call);
445  }
446  }
447 
448  code.swap(new_code);
449 }
450 
452 {
453  cpp_save_scopet saved_scope(cpp_scopes);
455 
457 }
C++ Language Type Checking.
const irep_idt & get_statement() const
Definition: std_code.h:40
The type of an expression.
Definition: type.h:22
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
void typecheck_type(typet &type)
A ‘switch’ instruction.
Definition: std_code.h:538
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
static bool has_auto(const typet &type)
exprt & op0()
Definition: expr.h:72
const exprt & cond() const
Definition: std_code.h:617
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_switch(code_switcht &code)
const exprt & cond() const
Definition: std_code.h:476
exprt & symbol()
Definition: std_code.h:268
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
exprt::operandst operands
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:144
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
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:37
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
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
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:1220
virtual void typecheck_expr(exprt &expr)
const irep_idt & id() const
Definition: irep.h:259
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:254
virtual void typecheck_ifthenelse(code_ifthenelset &code)
const source_locationt & find_source_location() const
Definition: expr.cpp:246
void make_already_typechecked(typet &dest)
source_locationt source_location
Definition: message.h:214
The empty type.
Definition: std_types.h:54
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:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
#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:601
C++ Language Type Checking.
const typet & follow(const typet &) const
Definition: namespace.cpp:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:45
exprt this_expr
Definition: cpp_id.h:77
A function call side effect.
Definition: std_code.h:1395
const exprt & value() const
Definition: std_code.h:554
virtual void typecheck_decl(codet &code)
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)
void convert_anonymous_union(cpp_declarationt &declaration, codet &new_code)
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
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:125
virtual void typecheck_while(code_whilet &code)
const exprt & expression() const
Definition: std_code.h:1234
virtual std::string to_string(const typet &type)
cpp_scopet & new_block_scope()
Definition: cpp_scopes.cpp:16
void make_nil()
Definition: irep.h:315
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
An if-then-else.
Definition: std_code.h:466
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
virtual void typecheck_ifthenelse(code_ifthenelset &code)
A statement in a programming language.
Definition: std_code.h:21
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:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
An expression containing a side effect.
Definition: std_code.h:1271
operandst & operands()
Definition: expr.h:66
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:286
void reserve_operands(operandst::size_type n)
Definition: expr.h:96
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