CBMC
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 <util/c_types.h>
13 #include <util/symbol_table_base.h>
14 
15 #include "cpp_template_type.h"
16 #include "cpp_type2name.h"
17 #include "cpp_typecheck.h"
18 
20  const irep_idt &current_mode,
21  code_typet::parametert &parameter)
22 {
23  irep_idt base_name=id2string(parameter.get_base_name());
24 
25  if(base_name.empty())
26  {
27  base_name="#anon_arg"+std::to_string(anon_counter++);
28  parameter.set_base_name(base_name);
29  }
30 
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  parameter_symbolt symbol;
43 
44  symbol.name=identifier;
45  symbol.base_name=parameter.get_base_name();
46  symbol.location=parameter.source_location();
47  symbol.mode = current_mode;
48  symbol.module=module;
49  symbol.type=parameter.type();
50  symbol.is_lvalue=!is_reference(symbol.type);
51 
52  INVARIANT(!symbol.base_name.empty(), "parameter has base name");
53 
54  symbolt *new_symbol;
55 
56  if(symbol_table.move(symbol, new_symbol))
57  {
59  error() << "cpp_typecheckt::convert_parameter: symbol_table.move(\""
60  << symbol.name << "\") failed" << eom;
61  throw 0;
62  }
63 
64  // put into scope
65  cpp_scopes.put_into_scope(*new_symbol);
66 }
67 
69  const irep_idt &current_mode,
70  code_typet &function_type)
71 {
72  code_typet::parameterst &parameters=
73  function_type.parameters();
74 
75  for(code_typet::parameterst::iterator
76  it=parameters.begin();
77  it!=parameters.end();
78  it++)
79  convert_parameter(current_mode, *it);
80 }
81 
83 {
84  code_typet &function_type=
86 
87  // only a prototype?
88  if(symbol.value.is_nil())
89  return;
90 
91  if(symbol.value.id() != ID_code)
92  {
93  error().source_location = symbol.location;
94  error() << "function '" << symbol.name << "' is initialized with "
95  << symbol.value.id() << eom;
96  throw 0;
97  }
98 
99  // enter appropriate scope
100  cpp_save_scopet saved_scope(cpp_scopes);
101  cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
102 
103  // fix the scope's prefix
104  function_scope.prefix=id2string(symbol.name)+"::";
105 
106  // genuine function definition -- do the parameter declarations
107  convert_parameters(symbol.mode, function_type);
108 
109  // create "this" if it's a non-static method
110  if(function_scope.is_method &&
111  !function_scope.is_static_member)
112  {
113  code_typet::parameterst &parameters=function_type.parameters();
114  DATA_INVARIANT(parameters.size() >= 1, "parameters expected");
115  code_typet::parametert &this_parameter_expr=parameters.front();
116  function_scope.this_expr = symbol_exprt{
117  this_parameter_expr.get_identifier(), this_parameter_expr.type()};
118  }
119  else
120  function_scope.this_expr.make_nil();
121 
122  // if it is a destructor, add the implicit code
123  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
124  {
125  const symbolt &msymb = lookup(symbol.type.get(ID_C_member_name));
126 
127  PRECONDITION(symbol.value.id() == ID_code);
128  PRECONDITION(symbol.value.get(ID_statement) == ID_block);
129 
130  if(
131  !symbol.value.has_operands() ||
132  !to_multi_ary_expr(symbol.value).op0().has_operands() ||
134  ID_already_typechecked)
135  {
136  symbol.value.copy_to_operands(
137  dtor(msymb, to_symbol_expr(function_scope.this_expr)));
138  }
139  }
140 
141  // do the function body
143 
144  // save current return type
145  typet old_return_type=return_type;
146 
147  return_type=function_type.return_type();
148 
149  // constructor, destructor?
150  if(return_type.id() == ID_constructor || return_type.id() == ID_destructor)
152 
153  typecheck_code(to_code(symbol.value));
154 
155  symbol.value.type()=symbol.type;
156 
157  return_type = old_return_type;
158 
159  deferred_typechecking.erase(symbol.name);
160 }
161 
164 {
165  const code_typet &function_type=
167 
168  const code_typet::parameterst &parameters=
169  function_type.parameters();
170 
171  std::string result;
172  bool first=true;
173 
174  result+='(';
175 
176  // the name of the function should not depend on
177  // the class name that is encoded in the type of this,
178  // but we must distinguish "const" and "non-const" member
179  // functions
180 
181  code_typet::parameterst::const_iterator it=
182  parameters.begin();
183 
184  if(it != parameters.end() && it->get_this())
185  {
186  const typet &pointer=it->type();
187  const typet &symbol = to_pointer_type(pointer).base_type();
188  if(symbol.get_bool(ID_C_constant))
189  result += "$const";
190  if(symbol.get_bool(ID_C_volatile))
191  result += "$volatile";
192  result += id2string(ID_this);
193  first=false;
194  it++;
195  }
196 
197  // we skipped the "this", on purpose!
198 
199  for(; it!=parameters.end(); it++)
200  {
201  if(first)
202  first=false;
203  else
204  result+=',';
205  typet tmp_type=it->type();
206  result+=cpp_type2name(it->type());
207  }
208 
209  result+=')';
210 
211  return result;
212 }
empty_typet void_type()
Definition: c_types.cpp:245
symbol_table_baset & symbol_table
virtual void start_typecheck_code()
const irep_idt module
void set_base_name(const irep_idt &name)
Definition: std_types.h:629
const irep_idt & get_base_name() const
Definition: std_types.h:639
const irep_idt & get_identifier() const
Definition: std_types.h:634
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:624
Base type of functions.
Definition: std_types.h:583
std::vector< parametert > parameterst
Definition: std_types.h:585
const typet & return_type() const
Definition: std_types.h:689
const parameterst & parameters() const
Definition: std_types.h:699
exprt this_expr
Definition: cpp_id.h:76
std::string prefix
Definition: cpp_id.h:79
bool is_method
Definition: cpp_id.h:42
bool is_static_member
Definition: cpp_id.h:42
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:87
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
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
Definition: cpp_typecheck.h:92
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:163
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const irep_idt & id() const
Definition: irep.h:384
void make_nil()
Definition: irep.h:442
bool is_nil() const
Definition: irep.h:364
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:932
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:179
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
Expression to hold a symbol (variable)
Definition: std_expr.h:131
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
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:72
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:29
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:40
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:144
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const codet & to_code(const exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:987
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Author: Diffblue Ltd.