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