CBMC
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 <util/c_types.h>
13 #include <util/simplify_expr.h>
14 #include <util/source_location.h>
15 
16 #include <ansi-c/c_qualifiers.h>
17 #include <ansi-c/merged_type.h>
18 
19 #include "cpp_convert_type.h"
20 #include "cpp_typecheck.h"
21 #include "cpp_typecheck_fargs.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(to_pointer_type(type).base_type());
86 
87  // Check if it is a pointer-to-member
88  if(type.find(ID_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(ID_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(to_pointer_type(type).base_type().id() == ID_code)
105  {
106  code_typet::parameterst &parameters =
107  to_code_type(to_pointer_type(type).base_type()).parameters();
108 
109  if(parameters.empty() || !parameters.front().get_this())
110  {
111  // Add 'this' to the parameters
112  code_typet::parametert a0(pointer_type(class_object));
113  a0.set_base_name(ID_this);
114  a0.set_this();
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(to_array_type(type).element_type());
136 
137  if(to_array_type(type).element_type().get_bool(ID_C_constant))
138  type.set(ID_C_constant, true);
139 
140  if(to_array_type(type).element_type().get_bool(ID_C_volatile))
141  type.set(ID_C_volatile, true);
142  }
143  else if(type.id()==ID_vector)
144  {
145  // already done
146  }
147  else if(type.id() == ID_frontend_vector)
148  {
149  typecheck_vector_type(type);
150  }
151  else if(type.id()==ID_code)
152  {
153  code_typet &code_type=to_code_type(type);
154  typecheck_type(code_type.return_type());
155 
156  code_typet::parameterst &parameters=code_type.parameters();
157 
158  for(auto &param : parameters)
159  {
160  typecheck_type(param.type());
161 
162  // see if there is a default value
163  if(param.has_default_value())
164  {
165  typecheck_expr(param.default_value());
166  implicit_typecast(param.default_value(), param.type());
167  }
168  }
169  }
170  else if(type.id()==ID_template)
171  {
172  typecheck_type(to_template_type(type).subtype());
173  }
174  else if(type.id()==ID_c_enum)
175  {
176  typecheck_enum_type(type);
177  }
178  else if(type.id()==ID_c_enum_tag)
179  {
180  }
181  else if(type.id()==ID_c_bit_field)
182  {
184  }
185  else if(
186  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
187  type.id() == ID_bool || type.id() == ID_c_bool || type.id() == ID_floatbv ||
188  type.id() == ID_fixedbv || type.id() == ID_empty)
189  {
190  }
191  else if(type.id() == ID_struct_tag)
192  {
193  }
194  else if(type.id() == ID_union_tag)
195  {
196  }
197  else if(type.id()==ID_constructor ||
198  type.id()==ID_destructor)
199  {
200  }
201  else if(type.id()=="cpp-cast-operator")
202  {
203  }
204  else if(type.id()=="cpp-template-type")
205  {
206  }
207  else if(type.id()==ID_typeof)
208  {
209  exprt e=static_cast<const exprt &>(type.find(ID_expr_arg));
210 
211  if(e.is_nil())
212  {
213  typet tmp_type=
214  static_cast<const typet &>(type.find(ID_type_arg));
215 
216  if(tmp_type.id()==ID_cpp_name)
217  {
218  // this may be ambiguous -- it can be either a type or
219  // an expression
220 
221  cpp_typecheck_fargst fargs;
222 
223  exprt symbol_expr=resolve(
224  to_cpp_name(static_cast<const irept &>(tmp_type)),
226  fargs);
227 
228  type=symbol_expr.type();
229  }
230  else
231  {
232  typecheck_type(tmp_type);
233  type=tmp_type;
234  }
235  }
236  else
237  {
238  typecheck_expr(e);
239  type=e.type();
240  }
241  }
242  else if(type.id()==ID_decltype)
243  {
244  exprt e=static_cast<const exprt &>(type.find(ID_expr_arg));
245  typecheck_expr(e);
246 
247  if(e.type().id() == ID_c_bit_field)
249  else
250  type = e.type();
251  }
252  else if(type.id()==ID_unassigned)
253  {
254  // ignore, for template parameter guessing
255  }
256  else if(type.id()==ID_template_class_instance)
257  {
258  // ok (internally generated)
259  }
260  else if(type.id()==ID_block_pointer)
261  {
262  // This is an Apple extension for lambda-like constructs.
263  // http://thirdcog.eu/pwcblocks/
264  // we just treat them as references to functions
265  type.id(ID_frontend_pointer);
266  typecheck_type(type);
267  }
268  else if(type.id()==ID_nullptr)
269  {
270  }
271  else if(type.id()==ID_already_typechecked)
272  {
274  }
275  else if(type.id() == ID_gcc_attribute_mode)
276  {
277  PRECONDITION(type.has_subtype());
278  merged_typet as_parsed;
279  as_parsed.move_to_subtypes(to_type_with_subtype(type).subtype());
280  type.get_sub().clear();
281  as_parsed.move_to_subtypes(type);
282  type.swap(as_parsed);
283 
285  }
286  else if(type.id() == ID_complex)
287  {
288  // already done
289  }
290  else
291  {
293  error() << "unexpected cpp type: " << type.pretty() << eom;
294  throw 0;
295  }
296 
297  assert(type.is_not_nil());
298 }
c_typecheck_baset::typecheck_vector_type
virtual void typecheck_vector_type(typet &type)
Definition: c_typecheck_type.cpp:667
cpp_typecheck_fargst
Definition: cpp_typecheck_fargs.h:21
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:214
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:541
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
irept::find
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
typet::has_subtype
bool has_subtype() const
Definition: type.h:82
cpp_typecheck_fargs.h
merged_type.h
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:193
exprt
Base class for all expressions.
Definition: expr.h:55
c_typecheck_baset::typecheck_type
virtual void typecheck_type(typet &type)
Definition: c_typecheck_type.cpp:35
messaget::eom
static eomt eom
Definition: message.h:297
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:1490
cpp_typecheck_resolvet::wantt::TYPE
@ TYPE
array_typet::size
const exprt & size() const
Definition: std_types.h:800
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:380
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
messaget::error
mstreamt & error() const
Definition: message.h:399
c_qualifierst::is_constant
bool is_constant
Definition: c_qualifiers.h:92
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
typet::source_location
const source_locationt & source_location() const
Definition: type.h:90
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:2926
type_with_subtypest::move_to_subtypes
void move_to_subtypes(typet &type)
Move the provided type to the subtypes of this type.
Definition: type.cpp:25
cpp_typecheck_resolvet::wantt::BOTH
@ BOTH
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
source_location.h
c_qualifierst
Definition: c_qualifiers.h:61
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
irept::swap
void swap(irept &irep)
Definition: irep.h:442
code_typet
Base type of functions.
Definition: std_types.h:538
cpp_convert_type.h
irept::is_nil
bool is_nil() const
Definition: irep.h:376
irept::id
const irep_idt & id() const
Definition: irep.h:396
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
cpp_typecheckt::typecheck_compound_type
void typecheck_compound_type(struct_union_typet &) override
Definition: cpp_typecheck_compound_type.cpp:126
cpp_typecheck.h
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:585
code_typet::parametert::set_this
void set_this()
Definition: std_types.h:605
c_bit_field_typet::underlying_type
const typet & underlying_type() const
Definition: c_types.h:30
cpp_convert_plain_type
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
Definition: cpp_convert_type.cpp:328
simplify_expr.h
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: c_types.h:58
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2263
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
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:456
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:844
code_typet::parametert
Definition: std_types.h:555
merged_typet
holds a combination of types
Definition: merged_type.h:15
cpp_typecheckt::typecheck_enum_type
void typecheck_enum_type(typet &type)
Definition: cpp_typecheck_enum_type.cpp:87
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:645
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
to_template_type
template_typet & to_template_type(typet &type)
Definition: cpp_template_type.h:40
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:83
cpp_namet
Definition: cpp_name.h:16
c_types.h
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
to_cpp_name
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148