cprover
cpp_typecheck_function.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 <util/c_types.h>
15 
16 #include <ansi-c/c_qualifiers.h>
17 
18 #include "cpp_template_type.h"
19 #include "cpp_type2name.h"
20 #include "cpp_util.h"
21 
23  const irep_idt &current_mode,
24  code_typet::parametert &parameter)
25 {
26  irep_idt base_name=id2string(parameter.get_base_name());
27 
28  if(base_name.empty())
29  {
30  base_name="#anon_arg"+std::to_string(anon_counter++);
31  parameter.set_base_name(base_name);
32  }
33 
36  id2string(base_name);
37 
38  parameter.set_identifier(identifier);
39 
40  // the parameter may already have been set up if dealing with virtual methods
41  const symbolt *check_symbol;
42  if(!lookup(identifier, check_symbol))
43  return;
44 
45  parameter_symbolt symbol;
46 
47  symbol.name=identifier;
48  symbol.base_name=parameter.get_base_name();
49  symbol.location=parameter.source_location();
50  symbol.mode = current_mode;
51  symbol.module=module;
52  symbol.type=parameter.type();
53  symbol.is_lvalue=!is_reference(symbol.type);
54 
55  INVARIANT(!symbol.base_name.empty(), "parameter has base name");
56 
57  symbolt *new_symbol;
58 
59  if(symbol_table.move(symbol, new_symbol))
60  {
62  error() << "cpp_typecheckt::convert_parameter: symbol_table.move(\""
63  << symbol.name << "\") failed" << eom;
64  throw 0;
65  }
66 
67  // put into scope
68  cpp_scopes.put_into_scope(*new_symbol);
69 }
70 
72  const irep_idt &current_mode,
73  code_typet &function_type)
74 {
75  code_typet::parameterst &parameters=
76  function_type.parameters();
77 
78  for(code_typet::parameterst::iterator
79  it=parameters.begin();
80  it!=parameters.end();
81  it++)
82  convert_parameter(current_mode, *it);
83 }
84 
86 {
87  code_typet &function_type=
89 
90  // only a prototype?
91  if(symbol.value.is_nil())
92  return;
93 
94  if(symbol.value.id() != ID_code)
95  {
96  error().source_location = symbol.location;
97  error() << "function '" << symbol.name << "' is initialized with "
98  << symbol.value.id() << eom;
99  throw 0;
100  }
101 
102  // enter appropriate scope
103  cpp_save_scopet saved_scope(cpp_scopes);
104  cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
105 
106  // fix the scope's prefix
107  function_scope.prefix=id2string(symbol.name)+"::";
108 
109  // genuine function definition -- do the parameter declarations
110  convert_parameters(symbol.mode, function_type);
111 
112  // create "this" if it's a non-static method
113  if(function_scope.is_method &&
114  !function_scope.is_static_member)
115  {
116  code_typet::parameterst &parameters=function_type.parameters();
117  assert(parameters.size()>=1);
118  code_typet::parametert &this_parameter_expr=parameters.front();
119  function_scope.this_expr = symbol_exprt{
120  this_parameter_expr.get_identifier(), this_parameter_expr.type()};
121  }
122  else
123  function_scope.this_expr.make_nil();
124 
125  // if it is a destructor, add the implicit code
126  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
127  {
128  const symbolt &msymb = lookup(symbol.type.get(ID_C_member_name));
129 
130  PRECONDITION(symbol.value.id() == ID_code);
131  PRECONDITION(symbol.value.get(ID_statement) == ID_block);
132 
133  if(
134  !symbol.value.has_operands() ||
135  !to_multi_ary_expr(symbol.value).op0().has_operands() ||
137  ID_already_typechecked)
138  {
139  symbol.value.copy_to_operands(
140  dtor(msymb, to_symbol_expr(function_scope.this_expr)));
141  }
142  }
143 
144  // do the function body
146 
147  // save current return type
148  typet old_return_type=return_type;
149 
150  return_type=function_type.return_type();
151 
152  // constructor, destructor?
153  if(return_type.id() == ID_constructor || return_type.id() == ID_destructor)
155 
156  typecheck_code(to_code(symbol.value));
157 
158  symbol.value.type()=symbol.type;
159 
160  return_type = old_return_type;
161 
162  deferred_typechecking.erase(symbol.name);
163 }
164 
167 {
168  const code_typet &function_type=
170 
171  const code_typet::parameterst &parameters=
172  function_type.parameters();
173 
174  std::string result;
175  bool first=true;
176 
177  result+='(';
178 
179  // the name of the function should not depend on
180  // the class name that is encoded in the type of this,
181  // but we must distinguish "const" and "non-const" member
182  // functions
183 
184  code_typet::parameterst::const_iterator it=
185  parameters.begin();
186 
187  if(it != parameters.end() && it->get_this())
188  {
189  const typet &pointer=it->type();
190  const typet &symbol =pointer.subtype();
191  if(symbol.get_bool(ID_C_constant))
192  result += "$const";
193  if(symbol.get_bool(ID_C_volatile))
194  result += "$volatile";
195  result += id2string(ID_this);
196  first=false;
197  it++;
198  }
199 
200  // we skipped the "this", on purpose!
201 
202  for(; it!=parameters.end(); it++)
203  {
204  if(first)
205  first=false;
206  else
207  result+=',';
208  typet tmp_type=it->type();
209  result+=cpp_type2name(it->type());
210  }
211 
212  result+=')';
213 
214  return result;
215 }
empty_typet void_type()
Definition: c_types.cpp:253
symbol_tablet & symbol_table
virtual void start_typecheck_code()
const irep_idt module
void set_base_name(const irep_idt &name)
Definition: std_types.h:790
const irep_idt & get_base_name() const
Definition: std_types.h:800
const irep_idt & get_identifier() const
Definition: std_types.h:795
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:785
Base type of functions.
Definition: std_types.h:744
std::vector< parametert > parameterst
Definition: std_types.h:746
const typet & return_type() const
Definition: std_types.h:850
const parameterst & parameters() const
Definition: std_types.h:860
exprt this_expr
Definition: cpp_id.h:81
std::string prefix
Definition: cpp_id.h:84
bool is_method
Definition: cpp_id.h:47
bool is_static_member
Definition: cpp_id.h:47
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
void typecheck_code(codet &) override
void convert_function(symbolt &symbol)
unsigned anon_counter
codet dtor(const symbolt &symb, const symbol_exprt &this_expr)
produces destructor code for a class object
std::unordered_set< irep_idt > deferred_typechecking
irep_idt function_identifier(const typet &type)
for function overloading
void convert_parameter(const irep_idt &current_mode, code_typet::parametert &parameter)
void convert_parameters(const irep_idt &current_mode, code_typet &function_type)
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:37
bool empty() const
Definition: dstring.h:88
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:133
const source_locationt & source_location() const
Definition: expr.h:234
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:464
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
exprt & op0()
Definition: std_expr.h:761
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
Expression to hold a symbol (variable)
Definition: std_expr.h:81
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
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
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
const typet & template_subtype(const typet &type)
std::string cpp_type2name(const typet &type)
C++ Language Module.
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:816
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:147
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.