CBMC
cpp_convert_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Conversion
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_convert_type.h"
13 
14 #include <util/c_types.h>
15 #include <util/config.h>
16 #include <util/invariant.h>
17 #include <util/std_types.h>
18 
20 
21 #include "cpp_declaration.h"
22 #include "cpp_name.h"
23 
25 {
26 public:
27  // The following types exist in C11 and later, but are implemented as
28  // typedefs. In C++, they are keywords and thus required explicit handling in
29  // here.
31 
32  void write(typet &type) override;
33 
36  {
37  read(type);
38  }
39 
40 protected:
41  void clear() override
42  {
43  wchar_t_count = 0;
44  char16_t_count = 0;
45  char32_t_count = 0;
46 
48  }
49 
50  void read_rec(const typet &type) override;
51  void read_function_type(const typet &type);
52  void read_template(const typet &type);
53 };
54 
56 {
57  #if 0
58  std::cout << "cpp_convert_typet::read_rec: "
59  << type.pretty() << '\n';
60  #endif
61 
62  if(type.id() == ID_gcc_float80)
64  else if(type.id()==ID_wchar_t)
65  ++wchar_t_count;
66  else if(type.id()==ID_char16_t)
68  else if(type.id()==ID_char32_t)
70  else if(type.id()==ID_constexpr)
72  else if(type.id()==ID_function_type)
73  {
74  read_function_type(type);
75  }
76  else if(type.id()==ID_identifier)
77  {
78  // from parameters
79  }
80  else if(type.id()==ID_cpp_name)
81  {
82  // from typedefs
83  other.push_back(type);
84  }
85  else if(type.id()==ID_array)
86  {
87  other.push_back(type);
90  }
91  else if(type.id()==ID_template)
92  {
93  read_template(type);
94  }
95  else if(type.id()==ID_frontend_pointer)
96  {
97  // add width and turn into ID_pointer
98  pointer_typet tmp(
101  if(type.get_bool(ID_C_reference))
102  tmp.set(ID_C_reference, true);
103  if(type.get_bool(ID_C_rvalue_reference))
104  tmp.set(ID_C_rvalue_reference, true);
105  const irep_idt typedef_identifier = type.get(ID_C_typedef);
106  if(!typedef_identifier.empty())
107  tmp.set(ID_C_typedef, typedef_identifier);
108  other.push_back(tmp);
109  }
110  else if(type.id()==ID_pointer)
111  {
112  // ignore, we unfortunately convert multiple times
113  other.push_back(type);
114  }
115  else if(type.id() == ID_frontend_vector)
116  vector_size = static_cast<const exprt &>(type.find(ID_size));
117  else
118  {
120  }
121 }
122 
124 {
125  other.push_back(type);
126  typet &t=other.back();
127 
129  to_type_with_subtype(t).subtype(), get_message_handler());
130 
131  irept &arguments=t.add(ID_arguments);
132 
133  for(auto &argument : arguments.get_sub())
134  {
135  exprt &decl = static_cast<exprt &>(argument);
136 
137  // may be type or expression
138  bool is_type=decl.get_bool(ID_is_type);
139 
140  if(is_type)
141  {
142  }
143  else
144  {
146  }
147 
148  // TODO: initializer
149  }
150 }
151 
153 {
154  other.push_back(type);
155  other.back().id(ID_code);
156 
157  code_typet &t = to_code_type(other.back());
158 
159  // change subtype to return_type
160  typet &return_type = t.return_type();
161 
162  return_type.swap(to_type_with_subtype(t).subtype());
163  t.remove_subtype();
164 
165  if(return_type.is_not_nil())
167 
168  // take care of parameter types
169  code_typet::parameterst &parameters = t.parameters();
170 
171  // see if we have an ellipsis
172  if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
173  {
174  t.make_ellipsis();
175  parameters.pop_back();
176  }
177 
178  for(auto &parameter_expr : parameters)
179  {
180  if(parameter_expr.id()==ID_cpp_declaration)
181  {
182  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
183  source_locationt type_location=declaration.type().source_location();
184 
186 
187  // there should be only one declarator
188  assert(declaration.declarators().size()==1);
189 
190  cpp_declaratort &declarator=
191  declaration.declarators().front();
192 
193  // do we have a declarator?
194  if(declarator.is_nil())
195  {
196  parameter_expr = code_typet::parametert(declaration.type());
197  parameter_expr.add_source_location()=type_location;
198  }
199  else
200  {
201  const cpp_namet &cpp_name=declarator.name();
202  typet final_type=declarator.merge_type(declaration.type());
203 
204  // see if it's an array type
205  if(final_type.id()==ID_array)
206  {
207  // turn into pointer type
208  final_type = pointer_type(to_array_type(final_type).element_type());
209  }
210 
211  code_typet::parametert new_parameter(final_type);
212 
213  if(cpp_name.is_nil())
214  {
215  new_parameter.add_source_location()=type_location;
216  }
217  else if(cpp_name.is_simple_name())
218  {
219  irep_idt base_name=cpp_name.get_base_name();
220  assert(!base_name.empty());
221  new_parameter.set_identifier(base_name);
222  new_parameter.set_base_name(base_name);
223  new_parameter.add_source_location()=cpp_name.source_location();
224  }
225  else
226  {
227  throw "expected simple name as parameter";
228  }
229 
230  if(declarator.value().is_not_nil())
231  new_parameter.default_value().swap(declarator.value());
232 
233  parameter_expr.swap(new_parameter);
234  }
235  }
236  else if(parameter_expr.id()==ID_ellipsis)
237  {
238  throw "ellipsis only allowed as last parameter";
239  }
240  else
241  UNREACHABLE;
242  }
243 
244  // if we just have one parameter of type void, remove it
245  if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
246  parameters.clear();
247 }
248 
250 {
251  if(!other.empty())
252  {
254  {
256  error() << "illegal type modifier for defined type" << eom;
257  throw 0;
258  }
259 
261  }
262  else if(c_bool_cnt)
263  {
264  if(
268  ptr32_cnt || ptr64_cnt)
269  {
270  throw "illegal type modifier for C++ bool";
271  }
272 
274  }
275  else if(wchar_t_count)
276  {
277  // This is a distinct type, and can't be made signed/unsigned.
278  // This is tolerated by most compilers, however.
279 
280  if(
283  ptr32_cnt || ptr64_cnt)
284  {
285  throw "illegal type modifier for wchar_t";
286  }
287 
288  type=wchar_t_type();
291  }
292  else if(char16_t_count)
293  {
294  // This is a distinct type, and can't be made signed/unsigned.
295  if(
299  {
300  throw "illegal type modifier for char16_t";
301  }
302 
303  type=char16_t_type();
306  }
307  else if(char32_t_count)
308  {
309  // This is a distinct type, and can't be made signed/unsigned.
310  if(int_cnt || short_cnt || char_cnt || long_cnt ||
311  int8_cnt || int16_cnt || int32_cnt ||
312  int64_cnt || ptr32_cnt || ptr64_cnt ||
314  {
315  throw "illegal type modifier for char32_t";
316  }
317 
318  type=char32_t_type();
321  }
322  else
323  {
325  }
326 }
327 
328 void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
329 {
330  if(
331  type.id() == ID_cpp_name || type.id() == ID_struct ||
332  type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
333  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
334  type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
335  type.id() == ID_constructor || type.id() == ID_destructor ||
336  type.id() == ID_c_enum)
337  {
338  }
339  else if(type.id() == ID_c_bool)
340  {
341  type.set(ID_width, config.ansi_c.bool_width);
342  }
343  else
344  {
345  cpp_convert_typet cpp_convert_type(message_handler, type);
346  cpp_convert_type.write(type);
347  }
348 }
349 
351  typet &dest,
352  const typet &src,
353  message_handlert &message_handler)
354 {
355  if(dest.id() != ID_merged_type && dest.has_subtype())
356  {
358  to_type_with_subtype(dest).subtype(), src, message_handler);
359  return;
360  }
361 
362  cpp_convert_typet cpp_convert_type(message_handler, dest);
363  for(auto &t : cpp_convert_type.other)
364  if(t.id() == ID_auto)
365  t = src;
366 
367  cpp_convert_type.write(dest);
368 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
cpp_convert_typet::char32_t_count
std::size_t char32_t_count
Definition: cpp_convert_type.cpp:30
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:126
ansi_c_convert_typet::int8_cnt
unsigned int8_cnt
Definition: ansi_c_convert_type.h:32
ansi_c_convert_typet::clear
virtual void clear()
Definition: ansi_c_convert_type.h:72
ansi_c_convert_typet::set_attributes
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
Definition: ansi_c_convert_type.cpp:671
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:541
char32_t_type
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:185
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
to_cpp_declaration
cpp_declarationt & to_cpp_declaration(irept &irep)
Definition: cpp_declaration.h:146
ansi_c_convert_type.h
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
ansi_c_convert_typet::write
virtual void write(typet &type)
Definition: ansi_c_convert_type.cpp:292
ansi_c_convert_typet::source_location
source_locationt source_location
Definition: ansi_c_convert_type.h:62
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:580
ansi_c_convert_typet::vector_size
exprt vector_size
Definition: ansi_c_convert_type.h:45
ansi_c_convert_typet::c_qualifiers
c_qualifierst c_qualifiers
Definition: ansi_c_convert_type.h:57
cpp_declaratort::name
cpp_namet & name()
Definition: cpp_declarator.h:36
invariant.h
cpp_declaration.h
ansi_c_convert_typet::int_cnt
unsigned int_cnt
Definition: ansi_c_convert_type.h:27
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
ansi_c_convert_typet::signed_cnt
unsigned signed_cnt
Definition: ansi_c_convert_type.h:26
messaget::eom
static eomt eom
Definition: message.h:297
ansi_c_convert_typet::gcc_float64x_cnt
unsigned gcc_float64x_cnt
Definition: ansi_c_convert_type.h:36
configt::ansi_c
struct configt::ansi_ct ansi_c
char16_t_type
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:175
cpp_convert_typet::read_function_type
void read_function_type(const typet &type)
Definition: cpp_convert_type.cpp:152
cpp_convert_typet::write
void write(typet &type) override
Definition: cpp_convert_type.cpp:249
ansi_c_convert_typet
Definition: ansi_c_convert_type.h:23
cpp_declarationt::declarators
const declaratorst & declarators() const
Definition: cpp_declaration.h:62
ansi_c_convert_typet::ptr64_cnt
unsigned ptr64_cnt
Definition: ansi_c_convert_type.h:33
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:380
ansi_c_convert_typet::int64_cnt
unsigned int64_cnt
Definition: ansi_c_convert_type.h:32
cpp_convert_typet::read_rec
void read_rec(const typet &type) override
Definition: cpp_convert_type.cpp:55
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
ansi_c_convert_typet::c_bool_cnt
unsigned c_bool_cnt
Definition: ansi_c_convert_type.h:28
ansi_c_convert_typet::gcc_int128_cnt
unsigned gcc_int128_cnt
Definition: ansi_c_convert_type.h:38
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
ansi_c_convert_typet::int32_cnt
unsigned int32_cnt
Definition: ansi_c_convert_type.h:32
code_typet::parametert::default_value
const exprt & default_value() const
Definition: std_types.h:562
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
typet::source_location
const source_locationt & source_location() const
Definition: type.h:90
ansi_c_convert_typet::char_cnt
unsigned char_cnt
Definition: ansi_c_convert_type.h:26
cpp_namet::is_simple_name
bool is_simple_name() const
Definition: cpp_name.h:89
wchar_t_type
bitvector_typet wchar_t_type()
Definition: c_types.cpp:159
ansi_c_convert_typet::proper_bool_cnt
unsigned proper_bool_cnt
Definition: ansi_c_convert_type.h:29
std_types.h
ansi_c_convert_typet::short_cnt
unsigned short_cnt
Definition: ansi_c_convert_type.h:27
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
typet::remove_subtype
void remove_subtype()
Definition: type.h:87
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
cpp_declarationt
Definition: cpp_declaration.h:21
irept::is_nil
bool is_nil() const
Definition: irep.h:376
irept::id
const irep_idt & id() const
Definition: irep.h:396
message_handlert
Definition: message.h:27
dstringt::empty
bool empty() const
Definition: dstring.h:88
ansi_c_convert_typet::other
std::list< typet > other
Definition: ansi_c_convert_type.h:64
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
cpp_convert_typet::cpp_convert_typet
cpp_convert_typet(message_handlert &message_handler, const typet &type)
Definition: cpp_convert_type.cpp:34
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:95
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:585
config
configt config
Definition: config.cpp:25
ansi_c_convert_typet::long_cnt
unsigned long_cnt
Definition: ansi_c_convert_type.h:27
cpp_convert_plain_type
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
Definition: cpp_convert_type.cpp:328
source_locationt
Definition: source_location.h:18
cpp_convert_typet::char16_t_count
std::size_t char16_t_count
Definition: cpp_convert_type.cpp:30
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
cpp_namet::source_location
const source_locationt & source_location() const
Definition: cpp_name.h:73
ansi_c_convert_typet::build_type_with_subtype
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
Definition: ansi_c_convert_type.cpp:651
ansi_c_convert_typet::unsigned_cnt
unsigned unsigned_cnt
Definition: ansi_c_convert_type.h:26
ansi_c_convert_typet::int16_cnt
unsigned int16_cnt
Definition: ansi_c_convert_type.h:32
code_typet::make_ellipsis
void make_ellipsis()
Definition: std_types.h:635
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
config.h
cpp_declaratort::value
exprt & value()
Definition: cpp_declarator.h:42
cpp_convert_auto
void cpp_convert_auto(typet &dest, const typet &src, message_handlert &message_handler)
Definition: cpp_convert_type.cpp:350
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:645
ansi_c_convert_typet::read
virtual void read(const typet &type)
Definition: ansi_c_convert_type.cpp:22
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
cpp_convert_typet
Definition: cpp_convert_type.cpp:24
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:130
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:216
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:23
ansi_c_convert_typet::ptr32_cnt
unsigned ptr32_cnt
Definition: ansi_c_convert_type.h:33
cpp_namet::get_base_name
irep_idt get_base_name() const
Definition: cpp_name.cpp:16
cpp_namet
Definition: cpp_name.h:16
c_types.h
ansi_c_convert_typet::read_rec
virtual void read_rec(const typet &type)
Definition: ansi_c_convert_type.cpp:29
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
cpp_declaratort
Definition: cpp_declarator.h:19
array_typet::element_type
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:785
cpp_convert_typet::clear
void clear() override
Definition: cpp_convert_type.cpp:41
cpp_convert_typet::read_template
void read_template(const typet &type)
Definition: cpp_convert_type.cpp:123
cpp_declaratort::merge_type
typet merge_type(const typet &declaration_type) const
Definition: cpp_declarator.cpp:27
cpp_convert_typet::wchar_t_count
std::size_t wchar_t_count
Definition: cpp_convert_type.cpp:30
cpp_name.h