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 <ansi-c/c_qualifiers.h>
15 
16 #include "cpp_template_type.h"
17 #include "cpp_type2name.h"
18 #include "cpp_util.h"
19 
21  const irep_idt &mode,
22  code_typet::parametert &parameter)
23 {
24  irep_idt base_name=id2string(parameter.get_base_name());
25 
26  if(base_name.empty())
27  {
28  base_name="#anon_arg"+std::to_string(anon_counter++);
29  parameter.set_base_name(base_name);
30  }
31 
33  id2string(base_name);
34 
35  parameter.set_identifier(identifier);
36 
37  // the parameter may already have been set up if dealing with virtual methods
38  const symbolt *check_symbol;
39  if(!lookup(identifier, check_symbol))
40  return;
41 
42  symbolt symbol;
43 
44  symbol.name=identifier;
45  symbol.base_name=parameter.get_base_name();
46  symbol.location=parameter.source_location();
47  symbol.mode=mode;
48  symbol.module=module;
49  symbol.type=parameter.type();
50  symbol.is_state_var=true;
51  symbol.is_lvalue=!is_reference(symbol.type);
52  symbol.is_parameter=true;
53 
54  INVARIANT(!symbol.base_name.empty(), "parameter has base name");
55 
56  symbolt *new_symbol;
57 
58  if(symbol_table.move(symbol, new_symbol))
59  {
61  error() << "cpp_typecheckt::convert_parameter: symbol_table.move(\""
62  << symbol.name << "\") failed" << eom;
63  throw 0;
64  }
65 
66  // put into scope
67  cpp_scopes.put_into_scope(*new_symbol);
68 }
69 
71  const irep_idt &mode,
72  code_typet &function_type)
73 {
74  code_typet::parameterst &parameters=
75  function_type.parameters();
76 
77  for(code_typet::parameterst::iterator
78  it=parameters.begin();
79  it!=parameters.end();
80  it++)
81  convert_parameter(mode, *it);
82 }
83 
85 {
86  code_typet &function_type=
88 
89  // only a prototype?
90  if(symbol.value.is_nil())
91  return;
92 
93  // if it is a destructor, add the implicit code
94  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
95  {
96  const symbolt &msymb=lookup(symbol.type.get(ID_C_member_name));
97 
98  assert(symbol.value.id()==ID_code);
99  assert(symbol.value.get(ID_statement)==ID_block);
100 
101  if(
102  !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
103  symbol.value.op0().op0().id() != ID_already_typechecked)
104  {
105  symbol.value.copy_to_operands(dtor(msymb));
106  }
107  }
108 
109  // enter appropriate scope
110  cpp_save_scopet saved_scope(cpp_scopes);
111  cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
112 
113  // fix the scope's prefix
114  function_scope.prefix=id2string(symbol.name)+"::";
115 
116  // genuine function definition -- do the parameter declarations
117  convert_parameters(symbol.mode, function_type);
118 
119  // create "this" if it's a non-static method
120  if(function_scope.is_method &&
121  !function_scope.is_static_member)
122  {
123  code_typet::parameterst &parameters=function_type.parameters();
124  assert(parameters.size()>=1);
125  code_typet::parametert &this_parameter_expr=parameters.front();
126  function_scope.this_expr=exprt(ID_symbol, this_parameter_expr.type());
127  function_scope.this_expr.set(
128  ID_identifier, this_parameter_expr.get(ID_C_identifier));
129  }
130  else
131  function_scope.this_expr.make_nil();
132 
133  // do the function body
135 
136  // save current return type
137  typet old_return_type=return_type;
138 
139  return_type=function_type.return_type();
140 
141  // constructor, destructor?
142  if(return_type.id()==ID_constructor ||
143  return_type.id()==ID_destructor)
145 
146  typecheck_code(to_code(symbol.value));
147 
148  symbol.value.type()=symbol.type;
149 
150  return_type = old_return_type;
151 }
152 
155 {
156  const code_typet &function_type=
158 
159  const code_typet::parameterst &parameters=
160  function_type.parameters();
161 
162  std::string result;
163  bool first=true;
164 
165  result+='(';
166 
167  // the name of the function should not depend on
168  // the class name that is encoded in the type of this,
169  // but we must distinguish "const" and "non-const" member
170  // functions
171 
172  code_typet::parameterst::const_iterator it=
173  parameters.begin();
174 
175  if(it!=parameters.end() &&
176  it->get_identifier()==ID_this)
177  {
178  const typet &pointer=it->type();
179  const typet &symbol =pointer.subtype();
180  if(symbol.get_bool(ID_C_constant))
181  result += "$const";
182  if(symbol.get_bool(ID_C_volatile))
183  result += "$volatile";
184  result+="this";
185  first=false;
186  it++;
187  }
188 
189  // we skipped the "this", on purpose!
190 
191  for(; it!=parameters.end(); it++)
192  {
193  if(first)
194  first=false;
195  else
196  result+=',';
197  typet tmp_type=it->type();
198  result+=cpp_type2name(it->type());
199  }
200 
201  result+=')';
202 
203  return result;
204 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
void convert_function(symbolt &symbol)
codet dtor(const symbolt &symb)
produces destructor code for a class object
Base type of functions.
Definition: std_types.h:751
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
exprt & op0()
Definition: expr.h:84
irep_idt mode
Language mode.
Definition: symbol.h:49
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
std::vector< parametert > parameterst
Definition: std_types.h:754
exprt value
Initial value of symbol.
Definition: symbol.h:34
bool is_static_member
Definition: cpp_id.h:48
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
void convert_parameter(const irep_idt &mode, code_typet::parametert &parameter)
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
typet & type()
Return the type of the expression.
Definition: expr.h:68
void typecheck_code(codet &) override
Symbol table entry.
Definition: symbol.h:27
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
const typet & template_subtype(const typet &type)
void set_base_name(const irep_idt &name)
Definition: std_types.h:823
symbol_tablet & symbol_table
std::string prefix
Definition: cpp_id.h:80
const irep_idt & id() const
Definition: irep.h:259
const irep_idt & get_base_name() const
Definition: std_types.h:833
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
const irep_idt mode
bool is_parameter
Definition: symbol.h:66
C++ Language Module.
source_locationt source_location
Definition: message.h:236
The empty type.
Definition: std_types.h:48
void convert_parameters(const irep_idt &mode, code_typet &function_type)
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
mstreamt & error() const
Definition: message.h:386
std::string cpp_type2name(const typet &type)
C++ Language Type Checking.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
unsigned anon_counter
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
virtual void start_typecheck_code()
exprt this_expr
Definition: cpp_id.h:77
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
static eomt eom
Definition: message.h:284
irep_idt function_identifier(const typet &type)
for function overloading
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:818
mstreamt & result() const
Definition: message.h:396
Base class for all expressions.
Definition: expr.h:54
bool is_state_var
Definition: symbol.h:61
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
const source_locationt & source_location() const
Definition: expr.h:228
bool is_method
Definition: cpp_id.h:48
const irep_idt module
void make_nil()
Definition: irep.h:315
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
const typet & subtype() const
Definition: type.h:38
bool empty() const
Definition: dstring.h:75
const typet & return_type() const
Definition: std_types.h:883
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
bool is_lvalue
Definition: symbol.h:66
cpp_scopest cpp_scopes