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  // enter appropriate scope
95  cpp_save_scopet saved_scope(cpp_scopes);
96  cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
97 
98  // fix the scope's prefix
99  function_scope.prefix=id2string(symbol.name)+"::";
100 
101  // genuine function definition -- do the parameter declarations
102  convert_parameters(symbol.mode, function_type);
103 
104  // create "this" if it's a non-static method
105  if(function_scope.is_method &&
106  !function_scope.is_static_member)
107  {
108  code_typet::parameterst &parameters=function_type.parameters();
109  assert(parameters.size()>=1);
110  code_typet::parametert &this_parameter_expr=parameters.front();
111  function_scope.this_expr = symbol_exprt{
112  this_parameter_expr.get_identifier(), this_parameter_expr.type()};
113  }
114  else
115  function_scope.this_expr.make_nil();
116 
117  // if it is a destructor, add the implicit code
118  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
119  {
120  const symbolt &msymb = lookup(symbol.type.get(ID_C_member_name));
121 
122  PRECONDITION(symbol.value.id() == ID_code);
123  PRECONDITION(symbol.value.get(ID_statement) == ID_block);
124 
125  if(
126  !symbol.value.has_operands() ||
127  !to_multi_ary_expr(symbol.value).op0().has_operands() ||
129  ID_already_typechecked)
130  {
131  symbol.value.copy_to_operands(
132  dtor(msymb, to_symbol_expr(function_scope.this_expr)));
133  }
134  }
135 
136  // do the function body
138 
139  // save current return type
140  typet old_return_type=return_type;
141 
142  return_type=function_type.return_type();
143 
144  // constructor, destructor?
145  if(return_type.id() == ID_constructor || return_type.id() == ID_destructor)
147 
148  typecheck_code(to_code(symbol.value));
149 
150  symbol.value.type()=symbol.type;
151 
152  return_type = old_return_type;
153 
154  deferred_typechecking.erase(symbol.name);
155 }
156 
159 {
160  const code_typet &function_type=
162 
163  const code_typet::parameterst &parameters=
164  function_type.parameters();
165 
166  std::string result;
167  bool first=true;
168 
169  result+='(';
170 
171  // the name of the function should not depend on
172  // the class name that is encoded in the type of this,
173  // but we must distinguish "const" and "non-const" member
174  // functions
175 
176  code_typet::parameterst::const_iterator it=
177  parameters.begin();
178 
179  if(it != parameters.end() && it->get_this())
180  {
181  const typet &pointer=it->type();
182  const typet &symbol =pointer.subtype();
183  if(symbol.get_bool(ID_C_constant))
184  result += "$const";
185  if(symbol.get_bool(ID_C_volatile))
186  result += "$volatile";
187  result += id2string(ID_this);
188  first=false;
189  it++;
190  }
191 
192  // we skipped the "this", on purpose!
193 
194  for(; it!=parameters.end(); it++)
195  {
196  if(first)
197  first=false;
198  else
199  result+=',';
200  typet tmp_type=it->type();
201  result+=cpp_type2name(it->type());
202  }
203 
204  result+=')';
205 
206  return result;
207 }
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:150
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:82
irept::make_nil
void make_nil()
Definition: irep.h:475
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
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:782
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:50
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:82
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:48
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
c_typecheck_baset::module
const irep_idt module
Definition: c_typecheck_base.h:68
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
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:797
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
cpp_util.h
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
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:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:158
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
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:787
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
cpp_idt::is_static_member
bool is_static_member
Definition: cpp_id.h:48
cpp_typecheckt::typecheck_code
void typecheck_code(codet &) override
Definition: cpp_typecheck_code.cpp:23
cpp_type2name
std::string cpp_type2name(const typet &type)
Definition: cpp_type2name.cpp:97
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
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:792
c_typecheck_baset::return_type
typet return_type
Definition: c_typecheck_base.h:157
code_typet::parametert
Definition: std_types.h:753
cpp_idt::prefix
std::string prefix
Definition: cpp_id.h:85
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
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:21
parameter_symbolt
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:184
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:811
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:866
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
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
validation_modet::INVARIANT
@ INVARIANT
cpp_template_type.h