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 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:137
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
cpp_scopet
Definition: cpp_scope.h:21
cpp_typecheckt::anon_counter
unsigned anon_counter
Definition: cpp_typecheck.h:226
cpp_typecheckt::convert_function
void convert_function(symbolt &symbol)
Definition: cpp_typecheck_function.cpp:85
cpp_save_scopet
Definition: cpp_scopes.h:129
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:109
cpp_idt::this_expr
exprt this_expr
Definition: cpp_id.h:81
irept::make_nil
void make_nil()
Definition: irep.h:465
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:535
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
cpp_typecheckt::convert_parameter
void convert_parameter(const irep_idt &current_mode, code_typet::parametert &parameter)
Definition: cpp_typecheck_function.cpp:22
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:574
cpp_type2name.h
C++ Language Module.
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
cpp_typecheckt::dtor
codet dtor(const symbolt &symb, const symbol_exprt &this_expr)
produces destructor code for a class object
Definition: cpp_typecheck_destructor.cpp:51
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
c_qualifiers.h
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
cpp_scopest::put_into_scope
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
void_type
empty_typet void_type()
Definition: c_types.cpp:253
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
template_subtype
const typet & template_subtype(const typet &type)
Definition: cpp_template_type.h:50
cpp_idt::is_method
bool is_method
Definition: cpp_id.h:47
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
c_typecheck_baset::module
const irep_idt module
Definition: c_typecheck_base.h:69
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
code_typet::parametert::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:589
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
cpp_util.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:68
cpp_typecheckt::deferred_typechecking
std::unordered_set< irep_idt > deferred_typechecking
Definition: cpp_typecheck.h:595
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
code_typet
Base type of functions.
Definition: std_types.h:533
cpp_typecheckt::convert_parameters
void convert_parameters(const irep_idt &current_mode, code_typet &function_type)
Definition: cpp_typecheck_function.cpp:71
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
dstringt::empty
bool empty() const
Definition: dstring.h:88
cpp_typecheckt::function_identifier
irep_idt function_identifier(const typet &type)
for function overloading
Definition: cpp_typecheck_function.cpp:166
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
cpp_typecheck.h
C++ Language Type Checking.
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:579
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:69
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
cpp_idt::is_static_member
bool is_static_member
Definition: cpp_id.h:47
cpp_typecheckt::typecheck_code
void typecheck_code(codet &) override
Definition: cpp_typecheck_code.cpp:24
cpp_type2name
std::string cpp_type2name(const typet &type)
Definition: cpp_type2name.cpp:101
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:584
c_typecheck_baset::return_type
typet return_type
Definition: c_typecheck_base.h:153
code_typet::parametert
Definition: std_types.h:550
cpp_idt::prefix
std::string prefix
Definition: cpp_id.h:84
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
c_typecheck_baset::start_typecheck_code
virtual void start_typecheck_code()
Definition: c_typecheck_code.cpp:22
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:760
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:815
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
cpp_scopest::set_scope
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
cpp_template_type.h