cprover
cpp_typecheck.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 <algorithm>
15 
16 #include <util/arith_tools.h>
17 #include <util/source_location.h>
18 #include <util/symbol.h>
19 
21 #include <ansi-c/c_typecast.h>
22 
23 #include "expr2cpp.h"
24 #include "cpp_convert_type.h"
25 #include "cpp_declarator.h"
26 
28 {
29  if(item.is_declaration())
31  else if(item.is_linkage_spec())
32  convert(item.get_linkage_spec());
33  else if(item.is_namespace_spec())
35  else if(item.is_using())
36  convert(item.get_using());
37  else if(item.is_static_assert())
38  convert(item.get_static_assert());
39  else
40  {
42  error() << "unknown parse-tree element: " << item.id() << eom;
43  throw 0;
44  }
45 }
46 
49 {
50  // default linkage is "automatic"
51  current_linkage_spec=ID_auto;
52 
53  for(auto &item : cpp_parse_tree.items)
54  convert(item);
55 
57 
59 
60  clean_up();
61 }
62 
64 {
65  const exprt &this_expr=
67 
68  assert(this_expr.is_not_nil());
69  assert(this_expr.type().id()==ID_pointer);
70 
71  const typet &t=follow(this_expr.type().subtype());
72  assert(t.id()==ID_struct);
73  return to_struct_type(t);
74 }
75 
76 std::string cpp_typecheckt::to_string(const exprt &expr)
77 {
78  return expr2cpp(expr, *this);
79 }
80 
81 std::string cpp_typecheckt::to_string(const typet &type)
82 {
83  return type2cpp(type, *this);
84 }
85 
87  cpp_parse_treet &cpp_parse_tree,
88  symbol_tablet &symbol_table,
89  const std::string &module,
90  message_handlert &message_handler)
91 {
93  cpp_parse_tree, symbol_table, module, message_handler);
94  return cpp_typecheck.typecheck_main();
95 }
96 
98  exprt &expr,
99  message_handlert &message_handler,
100  const namespacet &ns)
101 {
102  const unsigned errors_before=
103  message_handler.get_message_count(messaget::M_ERROR);
104 
105  symbol_tablet symbol_table;
106  cpp_parse_treet cpp_parse_tree;
107 
108  cpp_typecheckt cpp_typecheck(cpp_parse_tree, symbol_table,
109  ns.get_symbol_table(), "", message_handler);
110 
111  try
112  {
113  cpp_typecheck.typecheck_expr(expr);
114  }
115 
116  catch(int)
117  {
118  cpp_typecheck.error();
119  }
120 
121  catch(const char *e)
122  {
123  cpp_typecheck.error() << e << messaget::eom;
124  }
125 
126  catch(const std::string &e)
127  {
128  cpp_typecheck.error() << e << messaget::eom;
129  }
130 
131  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
132 }
133 
149 {
150  code_blockt init_block; // Dynamic Initialization Block
151 
152  disable_access_control = true;
153 
154  for(const auto &d_it : dynamic_initializations)
155  {
156  symbolt &symbol=symbol_table.symbols.find(d_it)->second;
157 
158  if(symbol.is_extern)
159  continue;
160 
161  // PODs are always statically initialized
162  if(cpp_is_pod(symbol.type))
163  continue;
164 
165  assert(symbol.is_static_lifetime);
166  assert(!symbol.is_type);
167  assert(symbol.type.id()!=ID_code);
168 
169  exprt symbol_expr=cpp_symbol_expr(symbol);
170 
171  // initializer given?
172  if(symbol.value.is_not_nil())
173  {
174  // This will be a constructor call,
175  // which we execute.
176  assert(symbol.value.id()==ID_code);
177  init_block.copy_to_operands(symbol.value);
178 
179  // Make it nil to get zero initialization by
180  // __CPROVER_initialize
181  symbol.value.make_nil();
182  }
183  else
184  {
185  // use default constructor
186  exprt::operandst ops;
187 
188  codet call=
189  cpp_constructor(symbol.location, symbol_expr, ops);
190 
191  if(call.is_not_nil())
192  init_block.move_to_operands(call);
193  }
194  }
195 
196  dynamic_initializations.clear();
197 
198  // block_sini.move_to_operands(block_dini);
199 
200  // Create the dynamic initialization procedure
201  symbolt init_symbol;
202 
203  init_symbol.name="#cpp_dynamic_initialization#"+id2string(module);
204  init_symbol.base_name="#cpp_dynamic_initialization#"+id2string(module);
205  init_symbol.value.swap(init_block);
206  init_symbol.mode=ID_cpp;
207  init_symbol.module=module;
208  init_symbol.type=code_typet();
209  init_symbol.type.add(ID_return_type)=typet(ID_constructor);
210  init_symbol.is_type=false;
211  init_symbol.is_macro=false;
212 
213  symbol_table.move(init_symbol);
214 
216 }
217 
219 {
220  bool cont;
221 
222  do
223  {
224  cont = false;
225 
227  {
228  symbolt &symbol=s_it->second;
229 
230  if(symbol.value.id()=="cpp_not_typechecked" &&
231  symbol.value.get_bool("is_used"))
232  {
233  assert(symbol.type.id()==ID_code);
234 
235  if(symbol.base_name=="operator=")
236  {
237  cpp_declaratort declarator;
238  declarator.add_source_location() = symbol.location;
240  lookup(symbol.type.get(ID_C_member_name)), declarator);
241  symbol.value.swap(declarator.value());
242  convert_function(symbol);
243  cont=true;
244  }
245  else if(symbol.value.operands().size()==1)
246  {
247  exprt tmp = symbol.value.op0();
248  symbol.value.swap(tmp);
249  convert_function(symbol);
250  cont=true;
251  }
252  else
253  assert(0); // Don't know what to do!
254  }
255  }
256  }
257  while(cont);
258 
260  {
261  symbolt &symbol=s_it->second;
262  if(symbol.value.id()=="cpp_not_typechecked")
263  symbol.value.make_nil();
264  }
265 }
266 
268 {
269  symbol_tablet::symbolst::iterator it=symbol_table.symbols.begin();
270 
271  while(it!=symbol_table.symbols.end())
272  {
273  symbol_tablet::symbolst::iterator cur_it = it;
274  it++;
275 
276  symbolt &symbol = cur_it->second;
277 
278  // erase templates
279  if(symbol.type.get_bool(ID_is_template))
280  {
281  symbol_table.symbols.erase(cur_it);
282  continue;
283  }
284  else if(symbol.type.id()==ID_struct ||
285  symbol.type.id()==ID_union)
286  {
287  // remove methods from 'components'
288  struct_union_typet &struct_union_type=
289  to_struct_union_type(symbol.type);
290 
291  const struct_union_typet::componentst &components=
292  struct_union_type.components();
293 
294  struct_union_typet::componentst data_members;
295  data_members.reserve(components.size());
296 
297  struct_union_typet::componentst &function_members=
299  (struct_union_type.add(ID_methods).get_sub());
300 
301  function_members.reserve(components.size());
302 
303  for(const auto &compo_it : components)
304  {
305  if(compo_it.get_bool(ID_is_static) ||
306  compo_it.get_bool(ID_is_type))
307  {
308  // skip it
309  }
310  else if(compo_it.type().id()==ID_code)
311  {
312  function_members.push_back(compo_it);
313  }
314  else
315  {
316  data_members.push_back(compo_it);
317  }
318  }
319 
320  struct_union_type.components().swap(data_members);
321  }
322  }
323 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
void convert_function(symbolt &symbol)
bool is_using() const
Definition: cpp_item.h:121
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Linking: Zero Initialization.
Base type of functions.
Definition: std_types.h:734
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
Symbol table entry.
cpp_usingt & get_using()
Definition: cpp_item.h:109
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:91
exprt & op0()
Definition: expr.h:84
irep_idt mode
Language mode.
Definition: symbol.h:55
bool is_static_assert() const
Definition: cpp_item.h:140
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
std::vector< componentt > componentst
Definition: std_types.h:240
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
exprt value
Initial value of symbol.
Definition: symbol.h:40
const componentst & components() const
Definition: std_types.h:242
void static_and_dynamic_initialization()
Initialization of static objects:
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
typet & type()
Definition: expr.h:60
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
C++ Language Type Checking.
bool is_static_lifetime
Definition: symbol.h:70
subt & get_sub()
Definition: irep.h:245
void convert(cpp_linkage_spect &)
symbol_tablet & symbol_table
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
#define Forall_symbols(it, expr)
Definition: symbol_table.h:32
void default_assignop_value(const symbolt &symbol, cpp_declaratort &declarator)
Generate code for the implicit default assignment operator.
bool is_declaration() const
Definition: cpp_item.h:46
bool is_namespace_spec() const
Definition: cpp_item.h:96
const irep_idt & id() const
Definition: irep.h:189
cpp_namespace_spect & get_namespace_spec()
Definition: cpp_item.h:84
symbolst symbols
Definition: symbol_table.h:57
virtual void typecheck()
typechecking main method
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:505
source_locationt source_location
Definition: message.h:175
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
cpp_parse_treet & cpp_parse_tree
C++ Language Conversion.
cpp_static_assertt & get_static_assert()
Definition: cpp_item.h:134
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
C++ Language Type Checking.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
exprt this_expr
Definition: cpp_id.h:77
bool is_extern
Definition: symbol.h:71
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
cpp_declarationt & to_cpp_declaration(irept &irep)
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
void do_not_typechecked()
irep_idt current_linkage_spec
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:512
Base class for all expressions.
Definition: expr.h:46
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
const source_locationt & source_location() const
Definition: cpp_item.h:145
irept & add(const irep_namet &name)
Definition: irep.cpp:306
virtual std::string to_string(const typet &type)
cpp_linkage_spect & get_linkage_spec()
Definition: cpp_item.h:59
const irep_idt module
void make_nil()
Definition: irep.h:243
const struct_typet & this_struct_type()
dynamic_initializationst dynamic_initializations
bool disable_access_control
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
A statement in a programming language.
Definition: std_code.h:19
exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
bool is_type
Definition: symbol.h:66
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
bool is_macro
Definition: symbol.h:66
codet cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
bool is_linkage_spec() const
Definition: cpp_item.h:71
cpp_scopest cpp_scopes
unsigned get_message_count(unsigned level) const
Definition: message.h:47