cprover
Loading...
Searching...
No Matches
cpp_typecheck.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/pointer_expr.h>
16#include <util/symbol_table.h>
17
19
20#include "cpp_declarator.h"
21#include "cpp_util.h"
22#include "expr2cpp.h"
23
25{
26 if(item.is_declaration())
28 else if(item.is_linkage_spec())
29 convert(item.get_linkage_spec());
30 else if(item.is_namespace_spec())
31 convert(item.get_namespace_spec());
32 else if(item.is_using())
33 convert(item.get_using());
34 else if(item.is_static_assert())
35 convert(item.get_static_assert());
36 else
37 {
38 error().source_location=item.source_location();
39 error() << "unknown parse-tree element: " << item.id() << eom;
40 throw 0;
41 }
42}
43
46{
47 // default linkage is "automatic"
49
50 for(auto &item : cpp_parse_tree.items)
52
54
56
58
59 clean_up();
60}
61
63{
64 const exprt &this_expr=
66
67 CHECK_RETURN(this_expr.is_not_nil());
68 CHECK_RETURN(this_expr.type().id() == ID_pointer);
69
70 const typet &t = follow(to_pointer_type(this_expr.type()).base_type());
72 return to_struct_type(t);
73}
74
75std::string cpp_typecheckt::to_string(const exprt &expr)
76{
77 return expr2cpp(expr, *this);
78}
79
80std::string cpp_typecheckt::to_string(const typet &type)
81{
82 return type2cpp(type, *this);
83}
84
86 cpp_parse_treet &cpp_parse_tree,
87 symbol_table_baset &symbol_table,
88 const std::string &module,
89 message_handlert &message_handler)
90{
92 cpp_parse_tree, symbol_table, module, message_handler);
93 return cpp_typecheck.typecheck_main();
94}
95
97 exprt &expr,
98 message_handlert &message_handler,
99 const namespacet &ns)
100{
101 const unsigned errors_before=
102 message_handler.get_message_count(messaget::M_ERROR);
103
104 symbol_tablet symbol_table;
105 cpp_parse_treet cpp_parse_tree;
106
107 cpp_typecheckt cpp_typecheck(cpp_parse_tree, symbol_table,
108 ns.get_symbol_table(), "", message_handler);
109
110 try
111 {
112 cpp_typecheck.typecheck_expr(expr);
113 }
114
115 catch(int)
116 {
117 cpp_typecheck.error();
118 }
119
120 catch(const char *e)
121 {
122 cpp_typecheck.error() << e << messaget::eom;
123 }
124
125 catch(const std::string &e)
126 {
127 cpp_typecheck.error() << e << messaget::eom;
128 }
129
130 catch(const invalid_source_file_exceptiont &e)
131 {
132 cpp_typecheck.error().source_location = e.get_source_location();
133 cpp_typecheck.error() << e.get_reason() << messaget::eom;
134 }
135
136 return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
137}
138
154{
155 code_blockt init_block; // Dynamic Initialization Block
156
158
159 for(const irep_idt &d_it : dynamic_initializations)
160 {
161 symbolt &symbol = symbol_table.get_writeable_ref(d_it);
162
163 if(symbol.is_extern)
164 continue;
165
166 // PODs are always statically initialized
167 if(cpp_is_pod(symbol.type))
168 continue;
169
170 DATA_INVARIANT(symbol.is_static_lifetime, "should be static");
171 DATA_INVARIANT(!symbol.is_type, "should not be a type");
172 DATA_INVARIANT(symbol.type.id() != ID_code, "should not be code");
173
174 exprt symbol_expr=cpp_symbol_expr(symbol);
175
176 // initializer given?
177 if(symbol.value.is_not_nil())
178 {
179 // This will be a constructor call,
180 // which we execute.
181 init_block.add(to_code(symbol.value));
182
183 // Make it nil to get zero initialization by
184 // __CPROVER_initialize
185 symbol.value.make_nil();
186 }
187 else
188 {
189 // use default constructor
191
192 auto call = cpp_constructor(symbol.location, symbol_expr, ops);
193
194 if(call.has_value())
195 init_block.add(call.value());
196 }
197 }
198
200
201 // Create the dynamic initialization procedure
203 "#cpp_dynamic_initialization#" + id2string(module),
205 ID_cpp};
206 init_symbol.base_name="#cpp_dynamic_initialization#"+id2string(module);
207 init_symbol.value.swap(init_block);
208 init_symbol.module=module;
209
210 symbol_table.insert(std::move(init_symbol));
211
213}
214
216{
217 bool cont;
218
219 do
220 {
221 cont = false;
222
223 for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
224 {
225 const symbolt &symbol = it->second;
226
227 if(
228 symbol.value.id() == ID_cpp_not_typechecked &&
229 symbol.value.get_bool(ID_is_used))
230 {
231 DATA_INVARIANT(symbol.type.id() == ID_code, "must be code");
232 exprt value = symbol.value;
233
234 if(symbol.base_name=="operator=")
235 {
236 cpp_declaratort declarator;
237 declarator.add_source_location() = symbol.location;
239 lookup(symbol.type.get(ID_C_member_name)), declarator);
240 value.swap(declarator.value());
241 cont=true;
242 }
243 else if(symbol.value.operands().size()==1)
244 {
245 value = to_unary_expr(symbol.value).op();
246 cont=true;
247 }
248 else
249 UNREACHABLE; // Don't know what to do!
250
251 symbolt &writable_symbol = it.get_writeable_symbol();
252 writable_symbol.value.swap(value);
254 }
255 }
256 }
257 while(cont);
258
259 for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
260 {
261 if(it->second.value.id() == ID_cpp_not_typechecked)
262 it.get_writeable_symbol().value.make_nil();
263 }
264}
265
267{
268 auto it = symbol_table.begin();
269
270 while(it != symbol_table.end())
271 {
272 auto cur_it = it;
273 it++;
274
275 const symbolt &symbol=cur_it->second;
276
277 // erase templates and all member functions that have not been converted
278 if(
279 symbol.type.get_bool(ID_is_template) ||
281 {
283 continue;
284 }
285 else if(symbol.type.id()==ID_struct ||
286 symbol.type.id()==ID_union)
287 {
288 // remove methods from 'components'
290 to_struct_union_type(cur_it.get_writeable_symbol().type);
291
292 const struct_union_typet::componentst &components=
293 struct_union_type.components();
294
296 data_members.reserve(components.size());
297
300 (struct_union_type.add(ID_methods).get_sub());
301
302 function_members.reserve(components.size());
303
304 for(const auto &compo_it : components)
305 {
306 if(compo_it.get_bool(ID_is_static) ||
307 compo_it.get_bool(ID_is_type))
308 {
309 // skip it
310 }
311 else if(compo_it.type().id()==ID_code)
312 {
313 function_members.push_back(compo_it);
314 }
315 else
316 {
317 data_members.push_back(compo_it);
318 }
319 }
320
321 struct_union_type.components().swap(data_members);
322 }
323 }
324}
325
327{
328 return ::builtin_factory(identifier, symbol_table, get_message_handler());
329}
330
332{
333 if(expr.id() == ID_cpp_name || expr.id() == ID_cpp_declaration)
334 return true;
335
336 for(const exprt &op : expr.operands())
337 {
338 if(contains_cpp_name(op))
339 return true;
340 }
341 return false;
342}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
symbol_table_baset & symbol_table
A codet representing sequential composition of program statements.
Definition std_code.h:130
Base type of functions.
Definition std_types.h:539
exprt this_expr
Definition cpp_id.h:76
cpp_scopet & current_scope()
Definition cpp_scopes.h:32
void static_and_dynamic_initialization()
Initialization of static objects:
bool contains_cpp_name(const exprt &)
dynamic_initializationst dynamic_initializations
void convert_function(symbolt &symbol)
irep_idt current_linkage_spec
bool cpp_is_pod(const typet &type) const
void convert(cpp_linkage_spect &)
std::unordered_set< irep_idt > deferred_typechecking
void default_assignop_value(const symbolt &symbol, cpp_declaratort &declarator)
Generate code for the implicit default assignment operator.
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void typecheck() override
typechecking main method
bool builtin_factory(const irep_idt &)
std::string to_string(const typet &) override
bool disable_access_control
const struct_typet & this_struct_type()
cpp_parse_treet & cpp_parse_tree
cpp_scopest cpp_scopes
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:228
Thrown when we can't handle something in an input source file.
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
bool is_not_nil() const
Definition irep.h:380
void make_nil()
Definition irep.h:454
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
std::size_t get_message_count(unsigned level) const
Definition message.h:56
source_locationt source_location
Definition message.h:247
mstreamt & error() const
Definition message.h:399
message_handlert & get_message_handler()
Definition message.h:184
@ M_ERROR
Definition message.h:170
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition namespace.h:123
Structure type, corresponds to C style structs.
Definition std_types.h:231
Base type for structs and unions.
Definition std_types.h:62
std::vector< componentt > componentst
Definition std_types.h:140
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
virtual iteratort begin()=0
virtual iteratort end()=0
The symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
bool is_static_lifetime
Definition symbol.h:70
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
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
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.
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
C++ Language Type Checking.
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition cpp_util.cpp:14
std::string type2cpp(const typet &type, const namespacet &ns)
Definition expr2cpp.cpp:503
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition expr2cpp.cpp:496
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static std::unordered_set< irep_idt > init_symbol(const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
const codet & to_code(const exprt &expr)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
Author: Diffblue Ltd.