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/arith_tools.h>
15 #include <util/pointer_expr.h>
16 #include <util/source_location.h>
17 
18 #include "cpp_convert_type.h"
20 #include "cpp_template_type.h"
21 #include "cpp_util.h"
22 #include "cpp_exception_id.h"
23 
25 {
26  const irep_idt &statement=code.get_statement();
27 
28  if(statement==ID_try_catch)
29  {
30  code.type() = empty_typet();
31  typecheck_try_catch(code);
32  }
33  else if(statement==ID_member_initializer)
34  {
35  code.type() = empty_typet();
37  }
38  else if(statement==ID_msc_if_exists ||
39  statement==ID_msc_if_not_exists)
40  {
41  }
42  else if(statement==ID_decl_block)
43  {
44  // type checked already
45  }
46  else if(statement == ID_expression)
47  {
48  if(
49  !code.has_operands() || code.op0().id() != ID_side_effect ||
50  to_side_effect_expr(code.op0()).get_statement() != ID_assign)
51  {
53  return;
54  }
55 
56  // as an extension, we support indexed access into signed/unsigned
57  // bitvectors, typically used with __CPROVER::(un)signedbv<N>
58  exprt &expr = code.op0();
59 
60  if(expr.operands().size() == 2)
61  {
62  auto &binary_expr = to_binary_expr(expr);
63 
64  if(binary_expr.op0().id() == ID_index)
65  {
66  exprt array = to_index_expr(binary_expr.op0()).array();
67  typecheck_expr(array);
68 
69  if(
70  array.type().id() == ID_signedbv ||
71  array.type().id() == ID_unsignedbv)
72  {
73  shl_exprt shl{from_integer(1, array.type()),
74  to_index_expr(binary_expr.op0()).index()};
75  exprt rhs = if_exprt{
76  equal_exprt{binary_expr.op1(), from_integer(0, array.type())},
77  bitand_exprt{array, bitnot_exprt{shl}},
78  bitor_exprt{array, shl}};
79  binary_expr.op0() = to_index_expr(binary_expr.op0()).array();
80  binary_expr.op1() = rhs;
81  }
82  }
83  }
84 
86  }
87  else
89 }
90 
92 {
93  bool first = true;
94 
95  for(auto &op : code.operands())
96  {
97  if(first)
98  {
99  // this is the 'try'
100  typecheck_code(to_code(op));
101  first = false;
102  }
103  else
104  {
105  // This is (one of) the catch clauses.
106  code_blockt &catch_block = to_code_block(to_code(op));
107 
108  // look at the catch operand
109  auto &statements = catch_block.statements();
110  PRECONDITION(!statements.empty());
111 
112  if(statements.front().get_statement() == ID_ellipsis)
113  {
114  statements.erase(statements.begin());
115 
116  // do body
117  typecheck_code(catch_block);
118  }
119  else
120  {
121  // turn references into non-references
122  {
123  code_declt &decl = to_code_decl(statements.front());
124  cpp_declarationt &cpp_declaration = to_cpp_declaration(decl.symbol());
125 
126  assert(cpp_declaration.declarators().size()==1);
127  cpp_declaratort &declarator=cpp_declaration.declarators().front();
128 
129  if(is_reference(declarator.type()))
130  declarator.type()=declarator.type().subtype();
131  }
132 
133  // typecheck the body
134  typecheck_code(catch_block);
135 
136  // the declaration is now in a decl_block
137  CHECK_RETURN(!catch_block.statements().empty());
138  CHECK_RETURN(
139  catch_block.statements().front().get_statement() == ID_decl_block);
140 
141  // get the declaration
142  const code_declt &code_decl =
143  to_code_decl(to_code(catch_block.statements().front().op0()));
144 
145  // get the type
146  const typet &type = code_decl.symbol().type();
147 
148  // annotate exception ID
149  op.set(ID_exception_id, cpp_exception_id(type, *this));
150  }
151  }
152  }
153 }
154 
156 {
157  // In addition to the C syntax, C++ also allows a declaration
158  // as condition. E.g.,
159  // if(void *p=...) ...
160 
161  if(code.cond().id()==ID_code)
162  {
163  typecheck_code(to_code(code.cond()));
164  }
165  else
167 }
168 
170 {
171  // In addition to the C syntax, C++ also allows a declaration
172  // as condition. E.g.,
173  // while(void *p=...) ...
174 
175  if(code.cond().id()==ID_code)
176  {
177  typecheck_code(to_code(code.cond()));
178  }
179  else
181 }
182 
184 {
185  // In addition to the C syntax, C++ also allows a declaration
186  // as condition. E.g.,
187  // switch(int i=...) ...
188 
189  exprt &value = to_code_switch(code).value();
190  if(value.id() == ID_code)
191  {
192  // we shall rewrite that into
193  // { int i=....; switch(i) .... }
194 
195  codet decl = to_code(value);
196  typecheck_decl(decl);
197 
198  assert(decl.get_statement()==ID_decl_block);
199  assert(decl.operands().size()==1);
200 
201  // replace declaration by its symbol
202  value = to_code_decl(to_code(to_unary_expr(decl).op())).symbol();
203 
205 
206  code_blockt code_block({to_code(decl.op0()), code});
207  code.swap(code_block);
208  }
209  else
211 }
212 
214 {
215  const cpp_namet &member=
216  to_cpp_name(code.find(ID_member));
217 
218  // Let's first typecheck the operands.
219  Forall_operands(it, code)
220  {
221  const bool has_array_ini = it->get_bool(ID_C_array_ini);
222  typecheck_expr(*it);
223  if(has_array_ini)
224  it->set(ID_C_array_ini, true);
225  }
226 
227  // The initializer may be a data member (non-type)
228  // or a parent class (type).
229  // We ask for VAR only, as we get the parent classes via their
230  // constructor!
231  cpp_typecheck_fargst fargs;
232  fargs.in_use=true;
233  fargs.operands=code.operands();
234 
235  // We should only really resolve in qualified mode,
236  // no need to look into the parent.
237  // Plus, this should happen in class scope, not the scope of
238  // the constructor because of the constructor arguments.
239  exprt symbol_expr=
241 
242  if(symbol_expr.type().id()==ID_code)
243  {
244  const code_typet &code_type=to_code_type(symbol_expr.type());
245 
246  assert(code_type.parameters().size()>=1);
247 
248  // It's a parent. Call the constructor that we got.
249  side_effect_expr_function_callt function_call(
250  symbol_expr, {}, uninitialized_typet{}, code.source_location());
251  function_call.arguments().reserve(code.operands().size()+1);
252 
253  // we have to add 'this'
254  exprt this_expr = cpp_scopes.current_scope().this_expr;
255  assert(this_expr.is_not_nil());
256 
258  this_expr,
259  code_type.parameters().front().type());
260 
261  function_call.arguments().push_back(this_expr);
262 
263  forall_operands(it, code)
264  function_call.arguments().push_back(*it);
265 
266  // done building the expression, check the argument types
267  typecheck_function_call_arguments(function_call);
268 
269  if(symbol_expr.get_bool(ID_C_not_accessible))
270  {
271  const irep_idt &access = symbol_expr.get(ID_C_access);
272  CHECK_RETURN(
273  access == ID_private || access == ID_protected ||
274  access == ID_noaccess);
275 
276  if(access == ID_private || access == ID_noaccess)
277  {
278  #if 0
280  str << "error: constructor of '"
281  << to_string(symbol_expr)
282  << "' is not accessible";
283  throw 0;
284  #endif
285  }
286  }
287 
288  code_expressiont code_expression(function_call);
289 
290  code.swap(code_expression);
291  }
292  else
293  {
294  // a reference member
295  if(
296  symbol_expr.id() == ID_dereference &&
297  to_dereference_expr(symbol_expr).pointer().id() == ID_member &&
298  symbol_expr.get_bool(ID_C_implicit))
299  {
300  // treat references as normal pointers
301  exprt tmp = to_dereference_expr(symbol_expr).pointer();
302  symbol_expr.swap(tmp);
303  }
304 
305  if(symbol_expr.id() == ID_symbol &&
306  symbol_expr.type().id()!=ID_code)
307  {
308  // maybe the name of the member collides with a parameter of the
309  // constructor
311  ID_dereference, cpp_scopes.current_scope().this_expr.type().subtype());
312  dereference.copy_to_operands(cpp_scopes.current_scope().this_expr);
313  cpp_typecheck_fargst deref_fargs;
314  deref_fargs.add_object(dereference);
315 
316  {
317  cpp_save_scopet cpp_saved_scope(cpp_scopes);
320  symbol_expr =
321  resolve(member, cpp_typecheck_resolvet::wantt::VAR, deref_fargs);
322  }
323 
324  if(
325  symbol_expr.id() == ID_dereference &&
326  to_dereference_expr(symbol_expr).pointer().id() == ID_member &&
327  symbol_expr.get_bool(ID_C_implicit))
328  {
329  // treat references as normal pointers
330  exprt tmp = to_dereference_expr(symbol_expr).pointer();
331  symbol_expr.swap(tmp);
332  }
333  }
334 
335  if(
336  symbol_expr.id() == ID_member &&
337  to_member_expr(symbol_expr).op().id() == ID_dereference &&
338  to_dereference_expr(to_member_expr(symbol_expr).op()).pointer() ==
340  {
341  if(is_reference(symbol_expr.type()))
342  {
343  // it's a reference member
344  if(code.operands().size()!= 1)
345  {
347  error() << " reference '" << to_string(symbol_expr)
348  << "' expects one initializer" << eom;
349  throw 0;
350  }
351 
352  reference_initializer(code.op0(), symbol_expr.type());
353 
354  // assign the pointers
355  symbol_expr.type().remove(ID_C_reference);
356  symbol_expr.set(ID_C_lvalue, true);
357  code.op0().type().remove(ID_C_reference);
358 
359  side_effect_exprt assign(
360  ID_assign,
361  {symbol_expr, code.op0()},
362  typet(),
363  code.source_location());
365  code_expressiont new_code(assign);
366  code.swap(new_code);
367  }
368  else
369  {
370  // it's a data member
372 
373  auto call =
374  cpp_constructor(code.source_location(), symbol_expr, code.operands());
375 
376  if(call.has_value())
377  code.swap(call.value());
378  else
379  {
380  auto source_location = code.source_location();
381  code = code_skipt();
382  code.add_source_location() = source_location;
383  }
384  }
385  }
386  else
387  {
389  error() << "invalid member initializer '" << to_string(symbol_expr) << "'"
390  << eom;
391  throw 0;
392  }
393  }
394 }
395 
397 {
398  if(code.operands().size()!=1)
399  {
401  error() << "declaration expected to have one operand" << eom;
402  throw 0;
403  }
404 
405  assert(code.op0().id()==ID_cpp_declaration);
406 
407  cpp_declarationt &declaration=
408  to_cpp_declaration(code.op0());
409 
410  typet &type=declaration.type();
411 
412  bool is_typedef=declaration.is_typedef();
413 
414  if(declaration.declarators().empty() || !has_auto(type))
415  typecheck_type(type);
416 
417  assert(type.is_not_nil());
418 
419  if(declaration.declarators().empty() &&
420  follow(type).get_bool(ID_C_is_anonymous))
421  {
422  if(type.id() != ID_union_tag)
423  {
425  error() << "declaration statement does not declare anything"
426  << eom;
427  throw 0;
428  }
429 
430  code = convert_anonymous_union(declaration);
431  return;
432  }
433 
434  // mark as 'already typechecked'
436 
437  codet new_code(ID_decl_block);
438  new_code.reserve_operands(declaration.declarators().size());
439 
440  // Do the declarators (if any)
441  for(auto &declarator : declaration.declarators())
442  {
443  cpp_declarator_convertert cpp_declarator_converter(*this);
444  cpp_declarator_converter.is_typedef=is_typedef;
445 
446  const symbolt &symbol=
447  cpp_declarator_converter.convert(declaration, declarator);
448 
449  if(is_typedef)
450  continue;
451 
452  if(!symbol.is_type && !symbol.is_extern && symbol.type.id() == ID_empty)
453  {
454  error().source_location = symbol.location;
455  error() << "void-typed symbol not permitted" << eom;
456  throw 0;
457  }
458 
459  code_declt decl_statement(cpp_symbol_expr(symbol));
460  decl_statement.add_source_location()=symbol.location;
461 
462  // Do we have an initializer that's not code?
463  if(symbol.value.is_not_nil() &&
464  symbol.value.id()!=ID_code)
465  {
466  decl_statement.copy_to_operands(symbol.value);
468  has_auto(symbol.type) ||
469  follow(decl_statement.op1().type()) == follow(symbol.type),
470  "declarator type should match symbol type");
471  }
472 
473  new_code.add_to_operands(std::move(decl_statement));
474 
475  // is there a constructor to be called?
476  if(symbol.value.is_not_nil())
477  {
479  declarator.find(ID_init_args).is_nil(),
480  "declarator should not have init_args");
481  if(symbol.value.id()==ID_code)
482  new_code.copy_to_operands(symbol.value);
483  }
484  else
485  {
486  exprt object_expr=cpp_symbol_expr(symbol);
487 
489 
490  auto constructor_call = cpp_constructor(
491  symbol.location, object_expr, declarator.init_args().operands());
492 
493  if(constructor_call.has_value())
494  new_code.add_to_operands(std::move(constructor_call.value()));
495  }
496  }
497 
498  code.swap(new_code);
499 }
500 
502 {
503  cpp_save_scopet saved_scope(cpp_scopes);
505 
507 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
static void make_already_typechecked(exprt &expr)
static void make_already_typechecked(typet &type)
exprt & op1()
Definition: expr.h:106
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
virtual void typecheck_block(code_blockt &code)
virtual void typecheck_code(codet &code)
virtual void typecheck_while(code_whilet &code)
virtual void typecheck_switch(codet &code)
virtual void typecheck_ifthenelse(code_ifthenelset &code)
A codet representing sequential composition of program statements.
Definition: std_code.h:170
code_operandst & statements()
Definition: std_code.h:178
A codet representing the declaration of a local variable.
Definition: std_code.h:402
symbol_exprt & symbol()
Definition: std_code.h:408
codet representation of an expression statement.
Definition: std_code.h:1842
codet representation of an if-then-else statement.
Definition: std_code.h:778
const exprt & cond() const
Definition: std_code.h:796
A codet representing a skip statement.
Definition: std_code.h:270
const exprt & value() const
Definition: std_code.h:873
Base type of functions.
Definition: std_types.h:744
const parameterst & parameters() const
Definition: std_types.h:860
codet representing a while statement.
Definition: std_code.h:928
const exprt & cond() const
Definition: std_code.h:935
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
exprt & op1()
Definition: expr.h:106
exprt & op0()
Definition: expr.h:103
const irep_idt & get_statement() const
Definition: std_code.h:71
const declaratorst & declarators() const
bool is_typedef() const
symbolt & convert(const typet &type, const cpp_storage_spect &storage_spec, const cpp_member_spect &member_spec, cpp_declaratort &declarator)
exprt this_expr
Definition: cpp_id.h:81
irep_idt class_identifier
Definition: cpp_id.h:80
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
cpp_scopet & new_block_scope()
Definition: cpp_scopes.cpp:16
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
id_mapt id_map
Definition: cpp_scopes.h:69
exprt::operandst operands
void add_object(const exprt &expr)
void typecheck_side_effect_assignment(side_effect_exprt &) override
void typecheck_type(typet &) override
void typecheck_switch(codet &) override
void typecheck_decl(codet &) override
void typecheck_code(codet &) override
void typecheck_member_initializer(codet &)
void typecheck_try_catch(codet &)
void typecheck_ifthenelse(code_ifthenelset &) override
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
static bool has_auto(const typet &type)
codet convert_anonymous_union(cpp_declarationt &declaration)
void typecheck_expr(exprt &) override
std::string to_string(const typet &) override
void typecheck_block(code_blockt &) override
void typecheck_while(code_whilet &) override
void make_ptr_typecast(exprt &expr, const typet &dest_type)
void typecheck_function_call_arguments(side_effect_expr_function_callt &) override
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
cpp_scopest cpp_scopes
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:
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:46
Equality.
Definition: std_expr.h:1140
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:179
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
exprt & op1()
Definition: expr.h:106
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:133
source_locationt & add_source_location()
Definition: expr.h:239
const source_locationt & source_location() const
Definition: expr.h:234
void reserve_operands(operandst::size_type n)
Definition: expr.h:128
typet & type()
Return the type of the expression.
Definition: expr.h:82
exprt & op0()
Definition: expr.h:103
operandst & operands()
Definition: expr.h:96
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:140
The trinary if-then-else operator.
Definition: std_expr.h:2087
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:452
void remove(const irep_namet &name)
Definition: irep.cpp:93
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
Left shift.
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
exprt::operandst & arguments()
Definition: std_code.h:2166
An expression containing a side effect.
Definition: std_code.h:1898
const irep_idt & get_statement() const
Definition: std_code.h:1920
Symbol table entry.
Definition: symbol.h:28
bool is_extern
Definition: symbol.h:66
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
exprt value
Initial value of symbol.
Definition: symbol.h:34
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
C++ Language Conversion.
cpp_declarationt & to_cpp_declaration(irept &irep)
C++ Language Type Checking.
irep_idt cpp_exception_id(const typet &src, const namespacet &ns)
turns a type into an exception ID
C++ Language Type Checking.
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:910
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:482
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:147
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949