cprover
Loading...
Searching...
No Matches
cpp_typecheck_code.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: 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/bitvector_expr.h>
16#include <util/pointer_expr.h>
18
20#include "cpp_exception_id.h"
21#include "cpp_typecheck_fargs.h"
22#include "cpp_util.h"
23
25{
26 const irep_idt &statement=code.get_statement();
27
28 if(statement==ID_try_catch)
29 {
30 code.type() = empty_typet();
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{
77 binary_expr.op1(), from_integer(0, binary_expr.op1().type())},
78 bitand_exprt{array, bitnot_exprt{shl}},
79 bitor_exprt{array, shl}};
80 binary_expr.op0() = to_index_expr(binary_expr.op0()).array();
81 binary_expr.op1() = rhs;
82 }
83 }
84 }
85
87 }
88 else
90}
91
93{
94 bool first = true;
95
96 for(auto &op : code.operands())
97 {
98 if(first)
99 {
100 // this is the 'try'
102 first = false;
103 }
104 else
105 {
106 // This is (one of) the catch clauses.
107 code_blockt &catch_block = to_code_block(to_code(op));
108
109 // look at the catch operand
110 auto &statements = catch_block.statements();
111 PRECONDITION(!statements.empty());
112
113 if(statements.front().get_statement() == ID_ellipsis)
114 {
115 statements.erase(statements.begin());
116
117 // do body
118 typecheck_code(catch_block);
119 }
120 else
121 {
122 // turn references into non-references
123 {
124 code_frontend_declt &decl = to_code_frontend_decl(statements.front());
125 cpp_declarationt &cpp_declaration = to_cpp_declaration(decl.symbol());
126
127 PRECONDITION(cpp_declaration.declarators().size() == 1);
128 cpp_declaratort &declarator=cpp_declaration.declarators().front();
129
130 if(is_reference(declarator.type()))
131 declarator.type() =
132 to_reference_type(declarator.type()).base_type();
133 }
134
135 // typecheck the body
136 typecheck_code(catch_block);
137
138 // the declaration is now in a decl_block
139 CHECK_RETURN(!catch_block.statements().empty());
141 catch_block.statements().front().get_statement() == ID_decl_block);
142
143 // get the declaration
145 to_code(catch_block.statements().front().op0()));
146
147 // get the type
148 const typet &type = code_decl.symbol().type();
149
150 // annotate exception ID
151 op.set(ID_exception_id, cpp_exception_id(type, *this));
152 }
153 }
154 }
155}
156
158{
159 // In addition to the C syntax, C++ also allows a declaration
160 // as condition. E.g.,
161 // if(void *p=...) ...
162
163 if(code.cond().id()==ID_code)
164 {
165 typecheck_code(to_code(code.cond()));
166 }
167 else
169}
170
172{
173 // In addition to the C syntax, C++ also allows a declaration
174 // as condition. E.g.,
175 // while(void *p=...) ...
176
177 if(code.cond().id()==ID_code)
178 {
179 typecheck_code(to_code(code.cond()));
180 }
181 else
183}
184
186{
187 // In addition to the C syntax, C++ also allows a declaration
188 // as condition. E.g.,
189 // switch(int i=...) ...
190
191 exprt &value = to_code_switch(code).value();
192 if(value.id() == ID_code)
193 {
194 // we shall rewrite that into
195 // { int i=....; switch(i) .... }
196
197 codet decl = to_code(value);
198 typecheck_decl(decl);
199
200 CHECK_RETURN(decl.get_statement() == ID_decl_block);
201 CHECK_RETURN(decl.operands().size() == 1);
202
203 // replace declaration by its symbol
204 value = to_code_frontend_decl(to_code(to_unary_expr(decl).op())).symbol();
205
207
208 code_blockt code_block({to_code(decl.op0()), code});
209 code.swap(code_block);
210 }
211 else
213}
214
216{
217 const cpp_namet &member=
218 to_cpp_name(code.find(ID_member));
219
220 // Let's first typecheck the operands.
221 Forall_operands(it, code)
222 {
223 const bool has_array_ini = it->get_bool(ID_C_array_ini);
224 typecheck_expr(*it);
225 if(has_array_ini)
226 it->set(ID_C_array_ini, true);
227 }
228
229 // The initializer may be a data member (non-type)
230 // or a parent class (type).
231 // We ask for VAR only, as we get the parent classes via their
232 // constructor!
234 fargs.in_use=true;
235 fargs.operands=code.operands();
236
237 // We should only really resolve in qualified mode,
238 // no need to look into the parent.
239 // Plus, this should happen in class scope, not the scope of
240 // the constructor because of the constructor arguments.
241 exprt symbol_expr=
243
244 if(symbol_expr.type().id()==ID_code)
245 {
246 const code_typet &code_type=to_code_type(symbol_expr.type());
247
249 code_type.parameters().size() >= 1, "at least one parameter");
250
251 // It's a parent. Call the constructor that we got.
253 symbol_expr, {}, uninitialized_typet{}, code.source_location());
254 function_call.arguments().reserve(code.operands().size()+1);
255
256 // we have to add 'this'
258 PRECONDITION(this_expr.is_not_nil());
259
261 this_expr,
262 code_type.parameters().front().type());
263
264 function_call.arguments().push_back(this_expr);
265
266 for(const auto &op : as_const(code).operands())
267 function_call.arguments().push_back(op);
268
269 // done building the expression, check the argument types
271
272 if(symbol_expr.get_bool(ID_C_not_accessible))
273 {
274 const irep_idt &access = symbol_expr.get(ID_C_access);
276 access == ID_private || access == ID_protected ||
277 access == ID_noaccess);
278
279 if(access == ID_private || access == ID_noaccess)
280 {
281 #if 0
283 str << "error: constructor of '"
284 << to_string(symbol_expr)
285 << "' is not accessible";
286 throw 0;
287 #endif
288 }
289 }
290
291 code_expressiont code_expression(function_call);
292
293 code.swap(code_expression);
294 }
295 else
296 {
297 // a reference member
298 if(
299 symbol_expr.id() == ID_dereference &&
300 to_dereference_expr(symbol_expr).pointer().id() == ID_member &&
301 symbol_expr.get_bool(ID_C_implicit))
302 {
303 // treat references as normal pointers
304 exprt tmp = to_dereference_expr(symbol_expr).pointer();
305 symbol_expr.swap(tmp);
306 }
307
308 if(symbol_expr.id() == ID_symbol &&
309 symbol_expr.type().id()!=ID_code)
310 {
311 // maybe the name of the member collides with a parameter of the
312 // constructor
314 ID_dereference,
316 .base_type());
317 dereference.copy_to_operands(cpp_scopes.current_scope().this_expr);
318 cpp_typecheck_fargst deref_fargs;
319 deref_fargs.add_object(dereference);
320
321 {
322 cpp_save_scopet cpp_saved_scope(cpp_scopes);
325 symbol_expr =
326 resolve(member, cpp_typecheck_resolvet::wantt::VAR, deref_fargs);
327 }
328
329 if(
330 symbol_expr.id() == ID_dereference &&
331 to_dereference_expr(symbol_expr).pointer().id() == ID_member &&
332 symbol_expr.get_bool(ID_C_implicit))
333 {
334 // treat references as normal pointers
335 exprt tmp = to_dereference_expr(symbol_expr).pointer();
336 symbol_expr.swap(tmp);
337 }
338 }
339
340 if(
341 symbol_expr.id() == ID_member &&
342 to_member_expr(symbol_expr).op().id() == ID_dereference &&
343 to_dereference_expr(to_member_expr(symbol_expr).op()).pointer() ==
345 {
346 if(is_reference(symbol_expr.type()))
347 {
348 // it's a reference member
349 if(code.operands().size()!= 1)
350 {
352 error() << " reference '" << to_string(symbol_expr)
353 << "' expects one initializer" << eom;
354 throw 0;
355 }
356
357 reference_initializer(code.op0(), symbol_expr.type());
358
359 // assign the pointers
360 symbol_expr.type().remove(ID_C_reference);
361 symbol_expr.set(ID_C_lvalue, true);
362 code.op0().type().remove(ID_C_reference);
363
364 side_effect_exprt assign(
365 ID_assign,
366 {symbol_expr, code.op0()},
367 typet(),
368 code.source_location());
370 code_expressiont new_code(assign);
371 code.swap(new_code);
372 }
373 else
374 {
375 // it's a data member
377
378 auto call =
379 cpp_constructor(code.source_location(), symbol_expr, code.operands());
380
381 if(call.has_value())
382 code.swap(call.value());
383 else
384 {
385 auto source_location = code.source_location();
386 code = code_skipt();
387 code.add_source_location() = source_location;
388 }
389 }
390 }
391 else
392 {
394 error() << "invalid member initializer '" << to_string(symbol_expr) << "'"
395 << eom;
396 throw 0;
397 }
398 }
399}
400
402{
403 if(code.operands().size()!=1)
404 {
406 error() << "declaration expected to have one operand" << eom;
407 throw 0;
408 }
409
410 PRECONDITION(code.op0().id() == ID_cpp_declaration);
411
412 cpp_declarationt &declaration=
413 to_cpp_declaration(code.op0());
414
415 typet &type=declaration.type();
416
417 bool is_typedef=declaration.is_typedef();
418
419 if(declaration.declarators().empty() || !has_auto(type))
420 typecheck_type(type);
421
422 CHECK_RETURN(type.is_not_nil());
423
424 if(declaration.declarators().empty() &&
425 follow(type).get_bool(ID_C_is_anonymous))
426 {
427 if(type.id() != ID_union_tag)
428 {
430 error() << "declaration statement does not declare anything"
431 << eom;
432 throw 0;
433 }
434
435 code = convert_anonymous_union(declaration);
436 return;
437 }
438
439 // mark as 'already typechecked'
441
442 codet new_code(ID_decl_block);
443 new_code.reserve_operands(declaration.declarators().size());
444
445 // Do the declarators (if any)
446 for(auto &declarator : declaration.declarators())
447 {
448 cpp_declarator_convertert cpp_declarator_converter(*this);
449 cpp_declarator_converter.is_typedef=is_typedef;
450
451 const symbolt &symbol=
452 cpp_declarator_converter.convert(declaration, declarator);
453
454 if(is_typedef)
455 continue;
456
457 if(!symbol.is_type && !symbol.is_extern && symbol.type.id() == ID_empty)
458 {
459 error().source_location = symbol.location;
460 error() << "void-typed symbol not permitted" << eom;
461 throw 0;
462 }
463
464 code_frontend_declt decl_statement(cpp_symbol_expr(symbol));
465 decl_statement.add_source_location()=symbol.location;
466
467 // Do we have an initializer that's not code?
468 if(symbol.value.is_not_nil() &&
469 symbol.value.id()!=ID_code)
470 {
471 decl_statement.copy_to_operands(symbol.value);
473 has_auto(symbol.type) ||
474 follow(decl_statement.op1().type()) == follow(symbol.type),
475 "declarator type should match symbol type");
476 }
477
478 new_code.add_to_operands(std::move(decl_statement));
479
480 // is there a constructor to be called?
481 if(symbol.value.is_not_nil())
482 {
484 declarator.find(ID_init_args).is_nil(),
485 "declarator should not have init_args");
486 if(symbol.value.id()==ID_code)
487 new_code.copy_to_operands(symbol.value);
488 }
489 else
490 {
491 exprt object_expr=cpp_symbol_expr(symbol);
492
494
495 auto constructor_call = cpp_constructor(
496 symbol.location, object_expr, declarator.init_args().operands());
497
498 if(constructor_call.has_value())
499 new_code.add_to_operands(std::move(constructor_call.value()));
500 }
501 }
502
503 code.swap(new_code);
504}
505
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
API to expression classes for bitvectors.
static void make_already_typechecked(exprt &expr)
static void make_already_typechecked(typet &type)
exprt & op1()
Definition expr.h:128
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:130
code_operandst & statements()
Definition std_code.h:138
codet representation of an expression statement.
Definition std_code.h:1394
A codet representing the declaration of a local variable.
Definition std_code.h:347
symbol_exprt & symbol()
Definition std_code.h:354
codet representation of an if-then-else statement.
Definition std_code.h:460
const exprt & cond() const
Definition std_code.h:478
A codet representing a skip statement.
Definition std_code.h:322
const exprt & value() const
Definition std_code.h:555
Base type of functions.
Definition std_types.h:539
const parameterst & parameters() const
Definition std_types.h:655
codet representing a while statement.
Definition std_code.h:610
const exprt & cond() const
Definition std_code.h:617
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
const irep_idt & get_statement() const
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:76
irep_idt class_identifier
Definition cpp_id.h:75
void go_to(cpp_idt &id)
Definition cpp_scopes.h:103
cpp_scopet & new_block_scope()
id_mapt id_map
Definition cpp_scopes.h:68
cpp_scopet & current_scope()
Definition cpp_scopes.h:32
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)
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:39
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:155
void reserve_operands(operandst::size_type n)
Definition expr.h:150
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
The trinary if-then-else operator.
Definition std_expr.h:2323
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:95
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
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:49
const typet & base_type() const
The type of the data what we point to.
Left shift.
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
exprt::operandst & arguments()
Definition std_code.h:1718
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
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:29
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.
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:27
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.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const code_switcht & to_code_switch(const codet &code)
Definition std_code.h:592
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition std_code.h:429
const codet & to_code(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:660
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744