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 
62 
63  clean_up();
64 }
65 
67 {
68  const exprt &this_expr=
70 
71  assert(this_expr.is_not_nil());
72  assert(this_expr.type().id()==ID_pointer);
73 
74  const typet &t=follow(this_expr.type().subtype());
75  assert(t.id()==ID_struct);
76  return to_struct_type(t);
77 }
78 
79 std::string cpp_typecheckt::to_string(const exprt &expr)
80 {
81  return expr2cpp(expr, *this);
82 }
83 
84 std::string cpp_typecheckt::to_string(const typet &type)
85 {
86  return type2cpp(type, *this);
87 }
88 
90  cpp_parse_treet &cpp_parse_tree,
91  symbol_tablet &symbol_table,
92  const std::string &module,
93  message_handlert &message_handler)
94 {
96  cpp_parse_tree, symbol_table, module, message_handler);
97  return cpp_typecheck.typecheck_main();
98 }
99 
101  exprt &expr,
102  message_handlert &message_handler,
103  const namespacet &ns)
104 {
105  const unsigned errors_before=
106  message_handler.get_message_count(messaget::M_ERROR);
107 
108  symbol_tablet symbol_table;
109  cpp_parse_treet cpp_parse_tree;
110 
111  cpp_typecheckt cpp_typecheck(cpp_parse_tree, symbol_table,
112  ns.get_symbol_table(), "", message_handler);
113 
114  try
115  {
116  cpp_typecheck.typecheck_expr(expr);
117  }
118 
119  catch(int)
120  {
121  cpp_typecheck.error();
122  }
123 
124  catch(const char *e)
125  {
126  cpp_typecheck.error() << e << messaget::eom;
127  }
128 
129  catch(const std::string &e)
130  {
131  cpp_typecheck.error() << e << messaget::eom;
132  }
133 
134  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
135 }
136 
152 {
153  code_blockt init_block; // Dynamic Initialization Block
154 
155  disable_access_control = true;
156 
157  for(const irep_idt &d_it : dynamic_initializations)
158  {
159  const symbolt &symbol = symbol_table.lookup_ref(d_it);
160 
161  if(symbol.is_extern)
162  continue;
163 
164  // PODs are always statically initialized
165  if(cpp_is_pod(symbol.type))
166  continue;
167 
168  assert(symbol.is_static_lifetime);
169  assert(!symbol.is_type);
170  assert(symbol.type.id()!=ID_code);
171 
172  exprt symbol_expr=cpp_symbol_expr(symbol);
173 
174  // initializer given?
175  if(symbol.value.is_not_nil())
176  {
177  // This will be a constructor call,
178  // which we execute.
179  init_block.add(to_code(symbol.value));
180 
181  // Make it nil to get zero initialization by
182  // __CPROVER_initialize
184  }
185  else
186  {
187  // use default constructor
188  exprt::operandst ops;
189 
190  auto call = cpp_constructor(symbol.location, symbol_expr, ops);
191 
192  if(call.has_value())
193  init_block.add(call.value());
194  }
195  }
196 
197  dynamic_initializations.clear();
198 
199  // Create the dynamic initialization procedure
200  symbolt init_symbol;
201 
202  init_symbol.name="#cpp_dynamic_initialization#"+id2string(module);
203  init_symbol.base_name="#cpp_dynamic_initialization#"+id2string(module);
204  init_symbol.value.swap(init_block);
205  init_symbol.mode=ID_cpp;
206  init_symbol.module=module;
207  init_symbol.type = code_typet({}, typet(ID_constructor));
208  init_symbol.is_type=false;
209  init_symbol.is_macro=false;
210 
211  symbol_table.insert(std::move(init_symbol));
212 
214 }
215 
217 {
218  bool cont;
219 
220  do
221  {
222  cont = false;
223 
224  for(const auto &named_symbol : symbol_table.symbols)
225  {
226  const symbolt &symbol=named_symbol.second;
227 
228  if(
229  symbol.value.id() == ID_cpp_not_typechecked &&
230  symbol.value.get_bool(ID_is_used))
231  {
232  assert(symbol.type.id()==ID_code);
233  exprt value = symbol.value;
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  value.swap(declarator.value());
242  cont=true;
243  }
244  else if(symbol.value.operands().size()==1)
245  {
246  value = to_unary_expr(symbol.value).op();
247  cont=true;
248  }
249  else
250  UNREACHABLE; // Don't know what to do!
251 
252  symbolt &writable_symbol =
253  symbol_table.get_writeable_ref(named_symbol.first);
254  writable_symbol.value.swap(value);
255  convert_function(writable_symbol);
256  }
257  }
258  }
259  while(cont);
260 
261  for(const auto &named_symbol : symbol_table.symbols)
262  {
263  if(named_symbol.second.value.id() == 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 and all member functions that have not been converted
280  if(
281  symbol.type.get_bool(ID_is_template) ||
282  deferred_typechecking.find(symbol.name) != deferred_typechecking.end())
283  {
284  symbol_table.erase(cur_it);
285  continue;
286  }
287  else if(symbol.type.id()==ID_struct ||
288  symbol.type.id()==ID_union)
289  {
290  // remove methods from 'components'
291  struct_union_typet &struct_union_type=to_struct_union_type(
292  symbol_table.get_writeable_ref(cur_it->first).type);
293 
294  const struct_union_typet::componentst &components=
295  struct_union_type.components();
296 
297  struct_union_typet::componentst data_members;
298  data_members.reserve(components.size());
299 
300  struct_union_typet::componentst &function_members=
302  (struct_union_type.add(ID_methods).get_sub());
303 
304  function_members.reserve(components.size());
305 
306  for(const auto &compo_it : components)
307  {
308  if(compo_it.get_bool(ID_is_static) ||
309  compo_it.get_bool(ID_is_type))
310  {
311  // skip it
312  }
313  else if(compo_it.type().id()==ID_code)
314  {
315  function_members.push_back(compo_it);
316  }
317  else
318  {
319  data_members.push_back(compo_it);
320  }
321  }
322 
323  struct_union_type.components().swap(data_members);
324  }
325  }
326 }
327 
329 {
331 }
332 
334 {
335  if(expr.id() == ID_cpp_name || expr.id() == ID_cpp_declaration)
336  return true;
337 
338  for(const exprt &op : expr.operands())
339  {
340  if(contains_cpp_name(op))
341  return true;
342  }
343  return false;
344 }
cpp_typecheckt::convert
void convert(cpp_linkage_spect &)
Definition: cpp_typecheck_linkage_spec.cpp:14
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
cpp_parse_treet
Definition: cpp_parse_tree.h:20
arith_tools.h
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
cpp_typecheckt::convert_function
void convert_function(symbolt &symbol)
Definition: cpp_typecheck_function.cpp:85
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
cpp_typecheckt::typecheck_method_bodies
void typecheck_method_bodies()
Definition: cpp_typecheck_method_bodies.cpp:18
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:109
cpp_idt::this_expr
exprt this_expr
Definition: cpp_id.h:82
irept::make_nil
void make_nil()
Definition: irep.h:475
typet
The type of an expression, extends irept.
Definition: type.h:29
cpp_typecheckt::this_struct_type
const struct_typet & this_struct_type()
Definition: cpp_typecheck.cpp:66
to_cpp_declaration
cpp_declarationt & to_cpp_declaration(irept &irep)
Definition: cpp_declaration.h:148
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
cpp_typecheckt::clean_up
void clean_up()
Definition: cpp_typecheck.cpp:268
builtin_factory
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
Definition: builtin_factory.cpp:98
cpp_typecheckt::builtin_factory
bool builtin_factory(const irep_idt &)
Definition: cpp_typecheck.cpp:328
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
cpp_typecheckt::default_assignop_value
void default_assignop_value(const symbolt &symbol, cpp_declaratort &declarator)
Generate code for the implicit default assignment operator.
Definition: cpp_typecheck_constructor.cpp:345
cpp_typecheckt::current_linkage_spec
irep_idt current_linkage_spec
Definition: cpp_typecheck.h:112
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
cpp_typecheckt::cpp_constructor
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
Definition: cpp_constructor.cpp:25
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
expr2cpp.h
messaget::eom
static eomt eom
Definition: message.h:297
expr2cpp
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:492
cpp_typecheckt::static_and_dynamic_initialization
void static_and_dynamic_initialization()
Initialization of static objects:
Definition: cpp_typecheck.cpp:151
cpp_typecheckt::contains_cpp_name
bool contains_cpp_name(const exprt &)
Definition: cpp_typecheck.cpp:333
cpp_itemt::source_location
const source_locationt & source_location() const
Definition: cpp_item.h:145
cpp_typecheck
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Definition: cpp_typecheck.cpp:89
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
cpp_itemt::get_linkage_spec
cpp_linkage_spect & get_linkage_spec()
Definition: cpp_item.h:59
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
c_typecheck_baset::module
const irep_idt module
Definition: c_typecheck_base.h:68
expr_initializer.h
Expression Initialization.
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
cpp_itemt::get_using
cpp_usingt & get_using()
Definition: cpp_item.h:109
cpp_itemt::is_linkage_spec
bool is_linkage_spec() const
Definition: cpp_item.h:71
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
type2cpp
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:499
cpp_symbol_expr
symbol_exprt cpp_symbol_expr(const symbolt &symbol)
Definition: cpp_util.cpp:14
messaget::M_ERROR
@ M_ERROR
Definition: message.h:170
source_location.h
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:67
cpp_typecheckt::deferred_typechecking
std::unordered_set< irep_idt > deferred_typechecking
Definition: cpp_typecheck.h:595
irept::swap
void swap(irept &irep)
Definition: irep.h:463
code_typet
Base type of functions.
Definition: std_types.h:736
cpp_typecheckt
Definition: cpp_typecheck.h:45
cpp_convert_type.h
C++ Language Conversion.
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
cpp_typecheckt::cpp_parse_tree
cpp_parse_treet & cpp_parse_tree
Definition: cpp_typecheck.h:111
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
cpp_declarator.h
C++ Language Type Checking.
cpp_itemt::is_static_assert
bool is_static_assert() const
Definition: cpp_item.h:140
cpp_typecheck.h
C++ Language Type Checking.
builtin_factory.h
cpp_itemt::is_using
bool is_using() const
Definition: cpp_item.h:121
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
c_typecast.h
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
cpp_typecheckt::do_not_typechecked
void do_not_typechecked()
Definition: cpp_typecheck.cpp:216
irept::get_sub
subt & get_sub()
Definition: irep.h:477
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
cpp_itemt::is_namespace_spec
bool is_namespace_spec() const
Definition: cpp_item.h:96
cpp_declaratort::value
exprt & value()
Definition: cpp_declarator.h:42
cpp_itemt::get_static_assert
cpp_static_assertt & get_static_assert()
Definition: cpp_item.h:134
symbol_tablet::erase
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
Definition: symbol_table.cpp:92
cpp_typecheckt::to_string
std::string to_string(const typet &) override
Definition: cpp_typecheck.cpp:84
exprt::operands
operandst & operands()
Definition: expr.h:95
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
cpp_itemt::get_namespace_spec
cpp_namespace_spect & get_namespace_spec()
Definition: cpp_item.h:84
cpp_typecheckt::dynamic_initializations
dynamic_initializationst dynamic_initializations
Definition: cpp_typecheck.h:593
cpp_typecheckt::disable_access_control
bool disable_access_control
Definition: cpp_typecheck.h:594
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
cpp_parse_treet::items
itemst items
Definition: cpp_parse_tree.h:25
cpp_itemt
Definition: cpp_item.h:24
cpp_declaratort
Definition: cpp_declarator.h:20
message_handlert::get_message_count
std::size_t get_message_count(unsigned level) const
Definition: message.h:56
cpp_typecheckt::typecheck
void typecheck() override
typechecking main method
Definition: cpp_typecheck.cpp:49
cpp_itemt::is_declaration
bool is_declaration() const
Definition: cpp_item.h:46