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  bool first = true;
51 
52  for(auto &op : code.operands())
53  {
54  if(first)
55  {
56  // this is the 'try'
58  first = false;
59  }
60  else
61  {
62  // This is (one of) the catch clauses.
63  code_blockt &catch_block = to_code_block(to_code(op));
64 
65  // look at the catch operand
66  auto &statements = catch_block.statements();
67  PRECONDITION(!statements.empty());
68 
69  if(statements.front().get_statement() == ID_ellipsis)
70  {
71  statements.erase(statements.begin());
72 
73  // do body
74  typecheck_code(catch_block);
75  }
76  else
77  {
78  // turn references into non-references
79  {
80  code_declt &decl = to_code_decl(statements.front());
81  cpp_declarationt &cpp_declaration = to_cpp_declaration(decl.symbol());
82 
83  assert(cpp_declaration.declarators().size()==1);
84  cpp_declaratort &declarator=cpp_declaration.declarators().front();
85 
86  if(is_reference(declarator.type()))
87  declarator.type()=declarator.type().subtype();
88  }
89 
90  // typecheck the body
91  typecheck_code(catch_block);
92 
93  // the declaration is now in a decl_block
94  CHECK_RETURN(!catch_block.statements().empty());
96  catch_block.statements().front().get_statement() == ID_decl_block);
97 
98  // get the declaration
99  const code_declt &code_decl =
100  to_code_decl(to_code(catch_block.statements().front().op0()));
101 
102  // get the type
103  const typet &type = code_decl.symbol().type();
104 
105  // annotate exception ID
106  op.set(ID_exception_id, cpp_exception_id(type, *this));
107  }
108  }
109  }
110 }
111 
113 {
114  // In addition to the C syntax, C++ also allows a declaration
115  // as condition. E.g.,
116  // if(void *p=...) ...
117 
118  if(code.cond().id()==ID_code)
119  {
120  typecheck_code(to_code(code.cond()));
121  }
122  else
124 }
125 
127 {
128  // In addition to the C syntax, C++ also allows a declaration
129  // as condition. E.g.,
130  // while(void *p=...) ...
131 
132  if(code.cond().id()==ID_code)
133  {
134  typecheck_code(to_code(code.cond()));
135  }
136  else
138 }
139 
141 {
142  // In addition to the C syntax, C++ also allows a declaration
143  // as condition. E.g.,
144  // switch(int i=...) ...
145 
146  if(code.value().id()==ID_code)
147  {
148  // we shall rewrite that into
149  // { int i=....; switch(i) .... }
150 
151  codet decl=to_code(code.value());
152  typecheck_decl(decl);
153 
154  assert(decl.get_statement()==ID_decl_block);
155  assert(decl.operands().size()==1);
156 
157  // replace declaration by its symbol
158  assert(decl.op0().op0().id()==ID_symbol);
159  code.value()=decl.op0().op0();
160 
162 
163  code_blockt code_block({to_code(decl.op0()), code});
164  code.swap(code_block);
165  }
166  else
168 }
169 
171 {
172  const cpp_namet &member=
173  to_cpp_name(code.find(ID_member));
174 
175  // Let's first typecheck the operands.
176  Forall_operands(it, code)
177  {
178  const bool has_array_ini = it->get_bool(ID_C_array_ini);
179  typecheck_expr(*it);
180  if(has_array_ini)
181  it->set(ID_C_array_ini, true);
182  }
183 
184  // The initializer may be a data member (non-type)
185  // or a parent class (type).
186  // We ask for VAR only, as we get the parent classes via their
187  // constructor!
188  cpp_typecheck_fargst fargs;
189  fargs.in_use=true;
190  fargs.operands=code.operands();
191 
192  // We should only really resolve in qualified mode,
193  // no need to look into the parent.
194  // Plus, this should happen in class scope, not the scope of
195  // the constructor because of the constructor arguments.
196  exprt symbol_expr=
198 
199  if(symbol_expr.type().id()==ID_code)
200  {
201  const code_typet &code_type=to_code_type(symbol_expr.type());
202 
203  assert(code_type.parameters().size()>=1);
204 
205  // It's a parent. Call the constructor that we got.
206  side_effect_expr_function_callt function_call;
207 
208  function_call.function()=symbol_expr;
209  function_call.add_source_location()=code.source_location();
210  function_call.arguments().reserve(code.operands().size()+1);
211 
212  // we have to add 'this'
213  exprt this_expr = cpp_scopes.current_scope().this_expr;
214  assert(this_expr.is_not_nil());
215 
217  this_expr,
218  code_type.parameters().front().type());
219 
220  function_call.arguments().push_back(this_expr);
221 
222  forall_operands(it, code)
223  function_call.arguments().push_back(*it);
224 
225  // done building the expression, check the argument types
226  typecheck_function_call_arguments(function_call);
227 
228  if(symbol_expr.get_bool(ID_C_not_accessible))
229  {
230  const irep_idt &access = symbol_expr.get(ID_C_access);
231  CHECK_RETURN(
232  access == ID_private || access == ID_protected ||
233  access == ID_noaccess);
234 
235  if(access == ID_private || access == ID_noaccess)
236  {
237  #if 0
239  str << "error: constructor of `"
240  << to_string(symbol_expr)
241  << "' is not accessible";
242  throw 0;
243  #endif
244  }
245  }
246 
247  code_expressiont code_expression;
248  code_expression.expression()=function_call;
249 
250  code.swap(code_expression);
251  }
252  else
253  {
254  // a reference member
255  if(
256  symbol_expr.id() == ID_dereference &&
257  symbol_expr.op0().id() == ID_member &&
258  symbol_expr.get_bool(ID_C_implicit))
259  {
260  // treat references as normal pointers
261  exprt tmp = symbol_expr.op0();
262  symbol_expr.swap(tmp);
263  }
264 
265  if(symbol_expr.id() == ID_symbol &&
266  symbol_expr.type().id()!=ID_code)
267  {
268  // maybe the name of the member collides with a parameter of the
269  // constructor
271  ID_dereference, cpp_scopes.current_scope().this_expr.type().subtype());
273  cpp_typecheck_fargst deref_fargs;
274  deref_fargs.add_object(dereference);
275 
276  {
277  cpp_save_scopet cpp_saved_scope(cpp_scopes);
280  symbol_expr =
281  resolve(member, cpp_typecheck_resolvet::wantt::VAR, deref_fargs);
282  }
283 
284  if(
285  symbol_expr.id() == ID_dereference &&
286  symbol_expr.op0().id() == ID_member &&
287  symbol_expr.get_bool(ID_C_implicit))
288  {
289  // treat references as normal pointers
290  exprt tmp = symbol_expr.op0();
291  symbol_expr.swap(tmp);
292  }
293  }
294 
295  if(symbol_expr.id() == ID_member &&
296  symbol_expr.op0().id() == ID_dereference &&
297  symbol_expr.op0().op0() == cpp_scopes.current_scope().this_expr)
298  {
299  if(is_reference(symbol_expr.type()))
300  {
301  // it's a reference member
302  if(code.operands().size()!= 1)
303  {
305  error() << " reference `" << to_string(symbol_expr)
306  << "' expects one initializer" << eom;
307  throw 0;
308  }
309 
310  reference_initializer(code.op0(), symbol_expr.type());
311 
312  // assign the pointers
313  symbol_expr.type().remove(ID_C_reference);
314  symbol_expr.set(ID_C_lvalue, true);
315  code.op0().type().remove(ID_C_reference);
316 
317  side_effect_exprt assign(ID_assign, typet(), code.source_location());
318  assign.copy_to_operands(symbol_expr, code.op0());
320  code_expressiont new_code(assign);
321  code.swap(new_code);
322  }
323  else
324  {
325  // it's a data member
326  already_typechecked(symbol_expr);
327 
328  auto call =
329  cpp_constructor(code.source_location(), symbol_expr, code.operands());
330 
331  if(call.has_value())
332  code.swap(call.value());
333  else
334  {
335  auto source_location = code.source_location();
336  code = code_skipt();
337  code.add_source_location() = source_location;
338  }
339  }
340  }
341  else
342  {
344  error() << "invalid member initializer `"
345  << to_string(symbol_expr) << "'" << eom;
346  throw 0;
347  }
348  }
349 }
350 
352 {
353  if(code.operands().size()!=1)
354  {
356  error() << "declaration expected to have one operand" << eom;
357  throw 0;
358  }
359 
360  assert(code.op0().id()==ID_cpp_declaration);
361 
362  cpp_declarationt &declaration=
363  to_cpp_declaration(code.op0());
364 
365  typet &type=declaration.type();
366 
367  bool is_typedef=declaration.is_typedef();
368 
369  if(declaration.declarators().empty() || !has_auto(type))
370  typecheck_type(type);
371 
372  assert(type.is_not_nil());
373 
374  if(declaration.declarators().empty() &&
375  follow(type).get_bool(ID_C_is_anonymous))
376  {
377  if(follow(type).id()!=ID_union)
378  {
380  error() << "declaration statement does not declare anything"
381  << eom;
382  throw 0;
383  }
384 
385  convert_anonymous_union(declaration, code);
386  return;
387  }
388 
389  // mark as 'already typechecked'
391 
392  codet new_code(ID_decl_block);
393  new_code.reserve_operands(declaration.declarators().size());
394 
395  // Do the declarators (if any)
396  for(auto &declarator : declaration.declarators())
397  {
398  cpp_declarator_convertert cpp_declarator_converter(*this);
399  cpp_declarator_converter.is_typedef=is_typedef;
400 
401  const symbolt &symbol=
402  cpp_declarator_converter.convert(declaration, declarator);
403 
404  if(is_typedef)
405  continue;
406 
407  code_declt decl_statement(cpp_symbol_expr(symbol));
408  decl_statement.add_source_location()=symbol.location;
409 
410  // Do we have an initializer that's not code?
411  if(symbol.value.is_not_nil() &&
412  symbol.value.id()!=ID_code)
413  {
414  decl_statement.copy_to_operands(symbol.value);
416  has_auto(symbol.type) ||
417  follow(decl_statement.op1().type()) == follow(symbol.type),
418  "declarator type should match symbol type");
419  }
420 
421  new_code.move_to_operands(decl_statement);
422 
423  // is there a constructor to be called?
424  if(symbol.value.is_not_nil())
425  {
427  declarator.find(ID_init_args).is_nil(),
428  "declarator should not have init_args");
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  auto constructor_call = cpp_constructor(
439  symbol.location, object_expr, declarator.init_args().operands());
440 
441  if(constructor_call.has_value())
442  new_code.move_to_operands(constructor_call.value());
443  }
444  }
445 
446  code.swap(new_code);
447 }
448 
450 {
451  cpp_save_scopet saved_scope(cpp_scopes);
453 
455 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
cpp_idt::class_identifier
irep_idt class_identifier
Definition: cpp_id.h:76
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
exprt::move_to_operands
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Definition: expr.cpp:29
typet::subtype
const typet & subtype() const
Definition: type.h:38
cpp_declarationt::is_typedef
bool is_typedef() const
Definition: cpp_declaration.h:135
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
code_whilet
codet representing a while statement.
Definition: std_code.h:767
cpp_typecheck_fargst
Definition: cpp_typecheck_fargs.h:22
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
cpp_save_scopet
Definition: cpp_scopes.h:128
c_typecheck_baset::typecheck_while
virtual void typecheck_while(code_whilet &code)
Definition: c_typecheck_code.cpp:716
cpp_scopest::id_map
id_mapt id_map
Definition: cpp_scopes.h:69
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:109
cpp_idt::this_expr
exprt this_expr
Definition: cpp_id.h:77
already_typechecked
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
cpp_exception_id
irep_idt cpp_exception_id(const typet &src, const namespacet &ns)
turns a type into an exception ID
Definition: cpp_exception_id.cpp:94
typet
The type of an expression, extends irept.
Definition: type.h:27
cpp_typecheckt::typecheck_while
void typecheck_while(code_whilet &) override
Definition: cpp_typecheck_code.cpp:126
to_cpp_declaration
cpp_declarationt & to_cpp_declaration(irept &irep)
Definition: cpp_declaration.h:148
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
cpp_typecheckt::typecheck_side_effect_assignment
void typecheck_side_effect_assignment(side_effect_exprt &) override
Definition: cpp_typecheck_expr.cpp:2426
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1691
cpp_typecheckt::typecheck_block
void typecheck_block(code_blockt &) override
Definition: cpp_typecheck_code.cpp:449
cpp_typecheck_fargst::operands
exprt::operandst operands
Definition: cpp_typecheck_fargs.h:26
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
cpp_typecheckt::convert_anonymous_union
void convert_anonymous_union(cpp_declarationt &declaration, codet &new_code)
Definition: cpp_typecheck_declaration.cpp:34
cpp_declarator_convertert::convert
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
Definition: cpp_declarator_converter.cpp:34
exprt
Base class for all expressions.
Definition: expr.h:54
cpp_typecheckt::cpp_constructor
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
Definition: cpp_constructor.cpp:25
exprt::op0
exprt & op0()
Definition: expr.h:84
cpp_typecheckt::typecheck_decl
void typecheck_decl(codet &) override
Definition: cpp_typecheck_code.cpp:351
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:642
messaget::eom
static eomt eom
Definition: message.h:284
cpp_typecheckt::typecheck_switch
void typecheck_switch(code_switcht &) override
Definition: cpp_typecheck_code.cpp:140
cpp_typecheckt::typecheck_try_catch
void typecheck_try_catch(codet &)
Definition: cpp_typecheck_code.cpp:48
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:614
cpp_declarationt::declarators
const declaratorst & declarators() const
Definition: cpp_declaration.h:64
cpp_exception_id.h
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:159
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
messaget::error
mstreamt & error() const
Definition: message.h:386
empty_typet
The empty type.
Definition: std_types.h:48
cpp_util.h
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
cpp_typecheckt::reference_initializer
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:
Definition: cpp_typecheck_conversions.cpp:1561
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
cpp_declarator_convertert
Definition: cpp_declarator_converter.h:25
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
cpp_declarator_convertert::is_typedef
bool is_typedef
Definition: cpp_declarator_converter.h:31
cpp_symbol_expr
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
c_typecheck_baset::make_already_typechecked
void make_already_typechecked(typet &dest)
Definition: c_typecheck_base.h:228
cpp_typecheckt::typecheck_function_call_arguments
void typecheck_function_call_arguments(side_effect_expr_function_callt &) override
Definition: cpp_typecheck_expr.cpp:2258
exprt::op1
exprt & op1()
Definition: expr.h:87
cpp_typecheckt::make_ptr_typecast
void make_ptr_typecast(exprt &expr, const typet &dest_type)
Definition: cpp_typecheck_compound_type.cpp:1689
source_location.h
cpp_typecheckt::typecheck_ifthenelse
void typecheck_ifthenelse(code_ifthenelset &) override
Definition: cpp_typecheck_code.cpp:112
c_typecheck_baset::typecheck_code
virtual void typecheck_code(codet &code)
Definition: c_typecheck_code.cpp:24
irept::swap
void swap(irept &irep)
Definition: irep.h:303
cpp_typecheck_fargst::in_use
bool in_use
Definition: cpp_typecheck_fargs.h:25
code_typet
Base type of functions.
Definition: std_types.h:751
cpp_convert_type.h
code_whilet::cond
const exprt & cond() const
Definition: std_code.h:783
cpp_declarationt
Definition: cpp_declaration.h:23
irept::id
const irep_idt & id() const
Definition: irep.h:259
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:269
cpp_typecheck_fargst::add_object
void add_object(const exprt &expr)
Definition: cpp_typecheck_fargs.h:51
cpp_scopest::go_to
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
cpp_typecheck.h
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:360
c_typecheck_baset::typecheck_switch
virtual void typecheck_switch(code_switcht &code)
Definition: c_typecheck_code.cpp:685
cpp_scopest::new_block_scope
cpp_scopet & new_block_scope()
Definition: cpp_scopes.cpp:16
code_switcht::value
const exprt & value() const
Definition: std_code.h:721
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2684
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
code_skipt
A codet representing a skip statement.
Definition: std_code.h:237
cpp_typecheckt::typecheck_code
void typecheck_code(codet &) override
Definition: cpp_typecheck_code.cpp:22
cpp_typecheckt::typecheck_member_initializer
void typecheck_member_initializer(codet &)
Definition: cpp_typecheck_code.cpp:170
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
code_switcht
codet representing a switch statement.
Definition: std_code.h:705
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
side_effect_expr_function_callt::arguments
exprt::operandst & arguments()
Definition: std_code.h:1754
cpp_typecheckt::has_auto
static bool has_auto(const typet &type)
Definition: cpp_typecheck_compound_type.cpp:64
cpp_typecheck_resolvet::wantt::VAR
@ VAR
dereference
exprt dereference(const exprt &pointer, const namespacet &ns)
Dereference the given pointer-expression.
Definition: dereference.h:75
c_typecheck_baset::typecheck_ifthenelse
virtual void typecheck_ifthenelse(code_ifthenelset &code)
Definition: c_typecheck_code.cpp:582
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
code_expressiont::expression
const exprt & expression() const
Definition: std_code.h:1518
cpp_typecheckt::to_string
std::string to_string(const typet &) override
Definition: cpp_typecheck.cpp:84
side_effect_expr_function_callt::function
exprt & function()
Definition: std_code.h:1744
exprt::operands
operandst & operands()
Definition: expr.h:78
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:56
cpp_typecheckt::resolve
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:88
exprt::reserve_operands
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
cpp_namet
Definition: cpp_name.h:16
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
cpp_declaratort
Definition: cpp_declarator.h:19
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1560
to_cpp_name
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:144
c_typecheck_baset::typecheck_block
virtual void typecheck_block(code_blockt &code)
Definition: c_typecheck_code.cpp:184
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1504
cpp_template_type.h
cpp_declarator_converter.h
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470