cprover
cpp_typecheck_type.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/source_location.h>
15 #include <util/simplify_expr.h>
16 #include <util/c_types.h>
17 
18 #include <ansi-c/c_qualifiers.h>
19 
20 #include "cpp_convert_type.h"
21 #include "expr2cpp.h"
22 
24 {
25  assert(!type.id().empty());
26  assert(type.is_not_nil());
27 
28  try
29  {
31  }
32 
33  catch(const char *err)
34  {
36  error() << err << eom;
37  throw 0;
38  }
39 
40  catch(const std::string &err)
41  {
43  error() << err << eom;
44  throw 0;
45  }
46 
47  if(type.id()==ID_cpp_name)
48  {
49  c_qualifierst qualifiers(type);
50 
51  cpp_namet cpp_name;
52  cpp_name.swap(type);
53 
54  exprt symbol_expr=resolve(
55  cpp_name,
58 
59  if(symbol_expr.id()!=ID_type)
60  {
62  error() << "error: expected type" << eom;
63  throw 0;
64  }
65 
66  type=symbol_expr.type();
67  assert(type.is_not_nil());
68 
69  if(type.get_bool(ID_C_constant))
70  qualifiers.is_constant = true;
71 
72  qualifiers.write(type);
73  }
74  else if(type.id()==ID_struct ||
75  type.id()==ID_union)
76  {
78  }
79  else if(type.id()==ID_pointer)
80  {
81  c_qualifierst qualifiers(type);
82 
83  // the pointer/reference might have a qualifier,
84  // but do subtype first
85  typecheck_type(type.subtype());
86 
87  // Check if it is a pointer-to-member
88  if(type.find("to-member").is_not_nil())
89  {
90  // these can point either to data members or member functions
91  // of a class
92 
93  typet &class_object=static_cast<typet &>(type.add("to-member"));
94 
95  if(class_object.id()==ID_cpp_name)
96  {
97  assert(class_object.get_sub().back().id()=="::");
98  class_object.get_sub().pop_back();
99  }
100 
101  typecheck_type(class_object);
102 
103  // there may be parameters if this is a pointer to member function
104  if(type.subtype().id()==ID_code)
105  {
106  irept::subt &parameters=type.subtype().add(ID_parameters).get_sub();
107 
108  if(parameters.empty() ||
109  parameters.front().get(ID_C_base_name)!=ID_this)
110  {
111  // Add 'this' to the parameters
112  exprt a0(ID_parameter);
113  a0.set(ID_C_base_name, ID_this);
114  a0.type()=pointer_type(class_object);
115  parameters.insert(parameters.begin(), a0);
116  }
117  }
118  }
119 
120  if(type.get_bool(ID_C_constant))
121  qualifiers.is_constant = true;
122 
123  qualifiers.write(type);
124  }
125  else if(type.id()==ID_array)
126  {
127  exprt &size_expr=to_array_type(type).size();
128 
129  if(size_expr.is_not_nil())
130  {
131  typecheck_expr(size_expr);
132  simplify(size_expr, *this);
133  }
134 
135  typecheck_type(type.subtype());
136 
137  if(type.subtype().get_bool(ID_C_constant))
138  type.set(ID_C_constant, true);
139 
140  if(type.subtype().get_bool(ID_C_volatile))
141  type.set(ID_C_volatile, true);
142  }
143  else if(type.id()==ID_vector)
144  {
146  }
147  else if(type.id()==ID_code)
148  {
149  code_typet &code_type=to_code_type(type);
150  typecheck_type(code_type.return_type());
151 
152  code_typet::parameterst &parameters=code_type.parameters();
153 
154  for(auto &param : parameters)
155  {
156  typecheck_type(param.type());
157 
158  // see if there is a default value
159  if(param.has_default_value())
160  {
161  typecheck_expr(param.default_value());
162  implicit_typecast(param.default_value(), param.type());
163  }
164  }
165  }
166  else if(type.id()==ID_template)
167  {
168  typecheck_type(type.subtype());
169  }
170  else if(type.id()==ID_c_enum)
171  {
172  typecheck_enum_type(type);
173  }
174  else if(type.id()==ID_c_enum_tag)
175  {
176  }
177  else if(type.id()==ID_c_bit_field)
178  {
180  }
181  else if(
182  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
183  type.id() == ID_bool || type.id() == ID_c_bool || type.id() == ID_floatbv ||
184  type.id() == ID_fixedbv || type.id() == ID_empty)
185  {
186  }
187  else if(type.id() == ID_symbol_type)
188  {
189  }
190  else if(type.id() == ID_struct_tag)
191  {
192  }
193  else if(type.id() == ID_union_tag)
194  {
195  }
196  else if(type.id()==ID_constructor ||
197  type.id()==ID_destructor)
198  {
199  }
200  else if(type.id()=="cpp-cast-operator")
201  {
202  }
203  else if(type.id()=="cpp-template-type")
204  {
205  }
206  else if(type.id()==ID_typeof)
207  {
208  exprt e=static_cast<const exprt &>(type.find(ID_expr_arg));
209 
210  if(e.is_nil())
211  {
212  typet tmp_type=
213  static_cast<const typet &>(type.find(ID_type_arg));
214 
215  if(tmp_type.id()==ID_cpp_name)
216  {
217  // this may be ambiguous -- it can be either a type or
218  // an expression
219 
220  cpp_typecheck_fargst fargs;
221 
222  exprt symbol_expr=resolve(
223  to_cpp_name(static_cast<const irept &>(tmp_type)),
225  fargs);
226 
227  type=symbol_expr.type();
228  }
229  else
230  {
231  typecheck_type(tmp_type);
232  type=tmp_type;
233  }
234  }
235  else
236  {
237  typecheck_expr(e);
238  type=e.type();
239  }
240  }
241  else if(type.id()==ID_decltype)
242  {
243  exprt e=static_cast<const exprt &>(type.find(ID_expr_arg));
244  typecheck_expr(e);
245 
246  if(e.type().id() == ID_c_bit_field)
247  type = e.type().subtype();
248  else
249  type = e.type();
250  }
251  else if(type.id()==ID_unassigned)
252  {
253  // ignore, for template parameter guessing
254  }
255  else if(type.id()==ID_template_class_instance)
256  {
257  // ok (internally generated)
258  }
259  else if(type.id()==ID_block_pointer)
260  {
261  // This is an Apple extension for lambda-like constructs.
262  // http://thirdcog.eu/pwcblocks/
263  // we just treat them as references to functions
264  type.id(ID_frontend_pointer);
265  typecheck_type(type);
266  }
267  else if(type.id()==ID_nullptr)
268  {
269  }
270  else if(type.id()==ID_already_typechecked)
271  {
273  }
274  else
275  {
277  error() << "unexpected cpp type: " << type.pretty() << eom;
278  throw 0;
279  }
280 
281  assert(type.is_not_nil());
282 }
typet::subtype
const typet & subtype() const
Definition: type.h:38
cpp_typecheck_fargst
Definition: cpp_typecheck_fargs.h:22
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
c_typecheck_baset::typecheck_vector_type
virtual void typecheck_vector_type(vector_typet &type)
Definition: c_typecheck_type.cpp:658
typet
The type of an expression, extends irept.
Definition: type.h:27
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
exprt
Base class for all expressions.
Definition: expr.h:54
expr2cpp.h
c_typecheck_baset::typecheck_type
virtual void typecheck_type(typet &type)
Definition: c_typecheck_type.cpp:29
messaget::eom
static eomt eom
Definition: message.h:284
c_qualifiers.h
c_typecheck_baset::typecheck_c_bit_field_type
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
Definition: c_typecheck_type.cpp:1376
cpp_typecheck_resolvet::wantt::TYPE
array_typet::size
const exprt & size() const
Definition: std_types.h:1010
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
messaget::error
mstreamt & error() const
Definition: message.h:386
c_qualifierst::is_constant
bool is_constant
Definition: c_qualifiers.h:91
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
typet::source_location
const source_locationt & source_location() const
Definition: type.h:62
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1491
c_qualifierst::write
virtual void write(typet &src) const override
Definition: c_qualifiers.cpp:89
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
cpp_typecheck_resolvet::wantt::BOTH
source_location.h
c_qualifierst
Definition: c_qualifiers.h:60
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::swap
void swap(irept &irep)
Definition: irep.h:303
code_typet
Base type of functions.
Definition: std_types.h:751
cpp_convert_type.h
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
dstringt::empty
bool empty() const
Definition: dstring.h:75
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
cpp_typecheckt::typecheck_compound_type
void typecheck_compound_type(struct_union_typet &) override
Definition: cpp_typecheck_compound_type.cpp:121
cpp_typecheck.h
simplify_expr.h
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2684
cpp_convert_plain_type
void cpp_convert_plain_type(typet &type)
Definition: cpp_convert_type.cpp:585
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
cpp_typecheckt::implicit_typecast
void implicit_typecast(exprt &expr, const typet &type) override
Definition: cpp_typecheck_conversions.cpp:1493
irept::get_sub
subt & get_sub()
Definition: irep.h:317
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
cpp_typecheckt::typecheck_enum_type
void typecheck_enum_type(typet &type)
Definition: cpp_typecheck_enum_type.cpp:85
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
cpp_typecheckt::resolve
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
Definition: cpp_typecheck.h:88
irept::subt
std::vector< irept > subt
Definition: irep.h:160
cpp_namet
Definition: cpp_name.h:16
c_types.h
to_cpp_name
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:144