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  {
181  const bool has_array_ini = it->get_bool("#array_ini");
182  typecheck_expr(*it);
183  if(has_array_ini)
184  it->set("#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("#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("#reference");
316  symbol_expr.set("#lvalue", true);
317  code.op0().type().remove("#reference");
318 
319  side_effect_exprt assign(ID_assign);
320  assign.add_source_location() = code.source_location();
321  assign.copy_to_operands(symbol_expr, code.op0());
323  code_expressiont new_code(assign);
324  code.swap(new_code);
325  }
326  else
327  {
328  // it's a data member
329  already_typechecked(symbol_expr);
330 
331  exprt call=
332  cpp_constructor(code.source_location(), symbol_expr, code.operands());
333 
334  if(call.is_nil())
335  {
336  call=codet(ID_skip);
337  call.add_source_location()=code.source_location();
338  }
339 
340  code.swap(call);
341  }
342  }
343  else
344  {
346  error() << "invalid member initializer `"
347  << to_string(symbol_expr) << "'" << eom;
348  throw 0;
349  }
350  }
351 }
352 
354 {
355  if(code.operands().size()!=1)
356  {
358  error() << "declaration expected to have one operand" << eom;
359  throw 0;
360  }
361 
362  assert(code.op0().id()==ID_cpp_declaration);
363 
364  cpp_declarationt &declaration=
365  to_cpp_declaration(code.op0());
366 
367  typet &type=declaration.type();
368 
369  bool is_typedef=declaration.is_typedef();
370 
371  if(declaration.declarators().empty() || !has_auto(type))
372  typecheck_type(type);
373 
374  assert(type.is_not_nil());
375 
376  if(declaration.declarators().empty() &&
377  follow(type).get_bool(ID_C_is_anonymous))
378  {
379  if(follow(type).id()!=ID_union)
380  {
382  error() << "declaration statement does not declare anything"
383  << eom;
384  throw 0;
385  }
386 
387  convert_anonymous_union(declaration, code);
388  return;
389  }
390 
391  // mark as 'already typechecked'
393 
394  codet new_code(ID_decl_block);
395  new_code.reserve_operands(declaration.declarators().size());
396 
397  // Do the declarators (if any)
398  for(auto &declarator : declaration.declarators())
399  {
400  cpp_declarator_convertert cpp_declarator_converter(*this);
401  cpp_declarator_converter.is_typedef=is_typedef;
402 
403  const symbolt &symbol=
404  cpp_declarator_converter.convert(declaration, declarator);
405 
406  if(is_typedef)
407  continue;
408 
409  code_declt decl_statement(cpp_symbol_expr(symbol));
410  decl_statement.add_source_location()=symbol.location;
411 
412  // Do we have an initializer that's not code?
413  if(symbol.value.is_not_nil() &&
414  symbol.value.id()!=ID_code)
415  {
416  decl_statement.copy_to_operands(symbol.value);
418  has_auto(symbol.type) ||
419  follow(decl_statement.op1().type()) == follow(symbol.type),
420  "declarator type should match symbol type");
421  }
422 
423  new_code.move_to_operands(decl_statement);
424 
425  // is there a constructor to be called?
426  if(symbol.value.is_not_nil())
427  {
428  assert(declarator.find("init_args").is_nil());
429  if(symbol.value.id()==ID_code)
430  new_code.copy_to_operands(symbol.value);
431  }
432  else
433  {
434  exprt object_expr=cpp_symbol_expr(symbol);
435 
436  already_typechecked(object_expr);
437 
438  exprt constructor_call=
440  symbol.location,
441  object_expr,
442  declarator.init_args().operands());
443 
444  if(constructor_call.is_not_nil())
445  new_code.move_to_operands(constructor_call);
446  }
447  }
448 
449  code.swap(new_code);
450 }
451 
453 {
454  cpp_save_scopet saved_scope(cpp_scopes);
456 
458 }
C++ Language Type Checking.
const irep_idt & get_statement() const
Definition: std_code.h:39
The type of an expression.
Definition: type.h:22
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
void typecheck_type(typet &type)
A ‘switch’ instruction.
Definition: std_code.h:533
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
static bool has_auto(const typet &type)
exprt & op0()
Definition: expr.h:72
const exprt & cond() const
Definition: std_code.h:596
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_switch(code_switcht &code)
const exprt & cond() const
Definition: std_code.h:471
exprt & symbol()
Definition: std_code.h:266
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
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:1188
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:253
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
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:588
C++ Language Type Checking.
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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:1352
const exprt & value() const
Definition: std_code.h:541
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:1201
virtual std::string to_string(const typet &type)
cpp_scopet & new_block_scope()
Definition: cpp_scopes.cpp:16
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
An if-then-else.
Definition: std_code.h:461
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:164
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:257
An expression containing a side effect.
Definition: std_code.h:1238
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:214
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