cprover
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/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/config.h>
17 #include <util/invariant.h>
18 #include <util/std_types.h>
19 
21 #include <ansi-c/gcc_types.h>
22 
23 #include "cpp_declaration.h"
24 #include "cpp_name.h"
25 
27 {
28 public:
29  // The following types exist in C11 and later, but are implemented as
30  // typedefs. In C++, they are keywords and thus required explicit handling in
31  // here.
33 
34  void write(typet &type) override;
35 
38  {
39  read(type);
40  }
41 
42 protected:
43  void clear() override
44  {
45  wchar_t_count = 0;
46  char16_t_count = 0;
47  char32_t_count = 0;
48 
50  }
51 
52  void read_rec(const typet &type) override;
53  void read_function_type(const typet &type);
54  void read_template(const typet &type);
55 };
56 
58 {
59  #if 0
60  std::cout << "cpp_convert_typet::read_rec: "
61  << type.pretty() << '\n';
62  #endif
63 
64  if(type.id() == ID_gcc_float80)
66  else if(type.id()==ID_wchar_t)
67  ++wchar_t_count;
68  else if(type.id()==ID_char16_t)
70  else if(type.id()==ID_char32_t)
72  else if(type.id()==ID_constexpr)
74  else if(type.id()==ID_function_type)
75  {
76  read_function_type(type);
77  }
78  else if(type.id()==ID_identifier)
79  {
80  // from parameters
81  }
82  else if(type.id()==ID_cpp_name)
83  {
84  // from typedefs
85  other.push_back(type);
86  }
87  else if(type.id()==ID_array)
88  {
89  other.push_back(type);
91  }
92  else if(type.id()==ID_template)
93  {
94  read_template(type);
95  }
96  else if(type.id()==ID_frontend_pointer)
97  {
98  // add width and turn into ID_pointer
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 
130  irept &arguments=t.add(ID_arguments);
131 
132  for(auto &argument : arguments.get_sub())
133  {
134  exprt &decl = static_cast<exprt &>(argument);
135 
136  // may be type or expression
137  bool is_type=decl.get_bool(ID_is_type);
138 
139  if(is_type)
140  {
141  }
142  else
143  {
145  }
146 
147  // TODO: initializer
148  }
149 }
150 
152 {
153  other.push_back(type);
154  other.back().id(ID_code);
155 
156  code_typet &t = to_code_type(other.back());
157 
158  // change subtype to return_type
159  typet &return_type = t.return_type();
160 
161  return_type.swap(t.subtype());
162  t.remove_subtype();
163 
164  if(return_type.is_not_nil())
166 
167  // take care of parameter types
168  code_typet::parameterst &parameters = t.parameters();
169 
170  // see if we have an ellipsis
171  if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
172  {
173  t.make_ellipsis();
174  parameters.pop_back();
175  }
176 
177  for(auto &parameter_expr : parameters)
178  {
179  if(parameter_expr.id()==ID_cpp_declaration)
180  {
181  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
182  source_locationt type_location=declaration.type().source_location();
183 
185 
186  // there should be only one declarator
187  assert(declaration.declarators().size()==1);
188 
189  cpp_declaratort &declarator=
190  declaration.declarators().front();
191 
192  // do we have a declarator?
193  if(declarator.is_nil())
194  {
195  parameter_expr = code_typet::parametert(declaration.type());
196  parameter_expr.add_source_location()=type_location;
197  }
198  else
199  {
200  const cpp_namet &cpp_name=declarator.name();
201  typet final_type=declarator.merge_type(declaration.type());
202 
203  // see if it's an array type
204  if(final_type.id()==ID_array)
205  {
206  // turn into pointer type
207  final_type=pointer_type(final_type.subtype());
208  }
209 
210  code_typet::parametert new_parameter(final_type);
211 
212  if(cpp_name.is_nil())
213  {
214  new_parameter.add_source_location()=type_location;
215  }
216  else if(cpp_name.is_simple_name())
217  {
218  irep_idt base_name=cpp_name.get_base_name();
219  assert(!base_name.empty());
220  new_parameter.set_identifier(base_name);
221  new_parameter.set_base_name(base_name);
222  new_parameter.add_source_location()=cpp_name.source_location();
223  }
224  else
225  {
226  throw "expected simple name as parameter";
227  }
228 
229  if(declarator.value().is_not_nil())
230  new_parameter.default_value().swap(declarator.value());
231 
232  parameter_expr.swap(new_parameter);
233  }
234  }
235  else if(parameter_expr.id()==ID_ellipsis)
236  {
237  throw "ellipsis only allowed as last parameter";
238  }
239  else
240  UNREACHABLE;
241  }
242 
243  // if we just have one parameter of type void, remove it
244  if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
245  parameters.clear();
246 }
247 
249 {
250  if(!other.empty())
251  {
253  {
255  error() << "illegal type modifier for defined type" << eom;
256  throw 0;
257  }
258 
260  }
261  else if(c_bool_cnt)
262  {
263  if(
267  ptr32_cnt || ptr64_cnt)
268  {
269  throw "illegal type modifier for C++ bool";
270  }
271 
273  }
274  else if(wchar_t_count)
275  {
276  // This is a distinct type, and can't be made signed/unsigned.
277  // This is tolerated by most compilers, however.
278 
279  if(
282  ptr32_cnt || ptr64_cnt)
283  {
284  throw "illegal type modifier for wchar_t";
285  }
286 
287  type=wchar_t_type();
290  }
291  else if(char16_t_count)
292  {
293  // This is a distinct type, and can't be made signed/unsigned.
294  if(
298  {
299  throw "illegal type modifier for char16_t";
300  }
301 
302  type=char16_t_type();
305  }
306  else if(char32_t_count)
307  {
308  // This is a distinct type, and can't be made signed/unsigned.
309  if(int_cnt || short_cnt || char_cnt || long_cnt ||
310  int8_cnt || int16_cnt || int32_cnt ||
311  int64_cnt || ptr32_cnt || ptr64_cnt ||
313  {
314  throw "illegal type modifier for char32_t";
315  }
316 
317  type=char32_t_type();
320  }
321  else
322  {
324  }
325 }
326 
327 void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
328 {
329  if(
330  type.id() == ID_cpp_name || type.id() == ID_struct ||
331  type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
332  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
333  type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
334  type.id() == ID_constructor || type.id() == ID_destructor)
335  {
336  }
337  else if(type.id()==ID_c_enum)
338  {
339  // add width -- we use int, but the standard
340  // doesn't guarantee that
341  type.set(ID_width, config.ansi_c.int_width);
342  }
343  else if(type.id() == ID_c_bool)
344  {
345  type.set(ID_width, config.ansi_c.bool_width);
346  }
347  else
348  {
349  cpp_convert_typet cpp_convert_type(message_handler, type);
350  cpp_convert_type.write(type);
351  }
352 }
353 
355  typet &dest,
356  const typet &src,
357  message_handlert &message_handler)
358 {
359  if(dest.id() != ID_merged_type && dest.has_subtype())
360  {
361  cpp_convert_auto(dest.subtype(), src, message_handler);
362  return;
363  }
364 
365  cpp_convert_typet cpp_convert_type(message_handler, dest);
366  for(auto &t : cpp_convert_type.other)
367  if(t.id() == ID_auto)
368  t = src;
369 
370  cpp_convert_type.write(dest);
371 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cpp_convert_typet::char32_t_count
std::size_t char32_t_count
Definition: cpp_convert_type.cpp:32
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:113
typet::subtype
const typet & subtype() const
Definition: type.h:47
ansi_c_convert_typet::int8_cnt
unsigned int8_cnt
Definition: ansi_c_convert_type.h:31
ansi_c_convert_typet::clear
virtual void clear()
Definition: ansi_c_convert_type.h:67
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:613
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:746
char32_t_type
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:175
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
to_cpp_declaration
cpp_declarationt & to_cpp_declaration(irept &irep)
Definition: cpp_declaration.h:146
ansi_c_convert_type.h
ANSI-C Language Conversion.
gcc_types.h
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
ansi_c_convert_typet::write
virtual void write(typet &type)
Definition: ansi_c_convert_type.cpp:252
ansi_c_convert_typet::source_location
source_locationt source_location
Definition: ansi_c_convert_type.h:57
code_typet::parametert::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:785
ansi_c_convert_typet::vector_size
exprt vector_size
Definition: ansi_c_convert_type.h:44
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
ansi_c_convert_typet::c_qualifiers
c_qualifierst c_qualifiers
Definition: ansi_c_convert_type.h:52
cpp_declaratort::name
cpp_namet & name()
Definition: cpp_declarator.h:36
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
invariant.h
cpp_declaration.h
C++ Language Type Checking.
ansi_c_convert_typet::int_cnt
unsigned int_cnt
Definition: ansi_c_convert_type.h:26
exprt
Base class for all expressions.
Definition: expr.h:54
ansi_c_convert_typet::signed_cnt
unsigned signed_cnt
Definition: ansi_c_convert_type.h:25
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:35
configt::ansi_c
struct configt::ansi_ct ansi_c
char16_t_type
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:165
cpp_convert_typet::read_function_type
void read_function_type(const typet &type)
Definition: cpp_convert_type.cpp:151
cpp_convert_typet::write
void write(typet &type) override
Definition: cpp_convert_type.cpp:248
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:32
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
ansi_c_convert_typet::int64_cnt
unsigned int64_cnt
Definition: ansi_c_convert_type.h:31
cpp_convert_typet::read_rec
void read_rec(const typet &type) override
Definition: cpp_convert_type.cpp:57
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
messaget::error
mstreamt & error() const
Definition: message.h:399
c_qualifierst::is_constant
bool is_constant
Definition: c_qualifiers.h:91
ansi_c_convert_typet::c_bool_cnt
unsigned c_bool_cnt
Definition: ansi_c_convert_type.h:27
ansi_c_convert_typet::gcc_int128_cnt
unsigned gcc_int128_cnt
Definition: ansi_c_convert_type.h:37
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:31
code_typet::parametert::default_value
const exprt & default_value() const
Definition: std_types.h:767
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
ansi_c_convert_typet::char_cnt
unsigned char_cnt
Definition: ansi_c_convert_type.h:25
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:149
ansi_c_convert_typet::proper_bool_cnt
unsigned proper_bool_cnt
Definition: ansi_c_convert_type.h:28
std_types.h
Pre-defined types.
ansi_c_convert_typet::short_cnt
unsigned short_cnt
Definition: ansi_c_convert_type.h:26
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
typet::remove_subtype
void remove_subtype()
Definition: type.h:68
irept::swap
void swap(irept &irep)
Definition: irep.h:452
code_typet
Base type of functions.
Definition: std_types.h:744
cpp_convert_type.h
C++ Language Conversion.
cpp_declarationt
Definition: cpp_declaration.h:22
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
dstringt::empty
bool empty() const
Definition: dstring.h:88
ansi_c_convert_typet::other
std::list< typet > other
Definition: ansi_c_convert_type.h:59
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
cpp_convert_typet::cpp_convert_typet
cpp_convert_typet(message_handlert &message_handler, const typet &type)
Definition: cpp_convert_type.cpp:36
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
code_typet::parametert::set_base_name
void set_base_name(const irep_idt &name)
Definition: std_types.h:790
config
configt config
Definition: config.cpp:24
ansi_c_convert_typet::long_cnt
unsigned long_cnt
Definition: ansi_c_convert_type.h:26
cpp_convert_plain_type
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
Definition: cpp_convert_type.cpp:327
source_locationt
Definition: source_location.h:20
cpp_convert_typet::char16_t_count
std::size_t char16_t_count
Definition: cpp_convert_type.cpp:32
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
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:593
ansi_c_convert_typet::unsigned_cnt
unsigned unsigned_cnt
Definition: ansi_c_convert_type.h:25
ansi_c_convert_typet::int16_cnt
unsigned int16_cnt
Definition: ansi_c_convert_type.h:31
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
code_typet::make_ellipsis
void make_ellipsis()
Definition: std_types.h:840
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
irept::get_sub
subt & get_sub()
Definition: irep.h:466
code_typet::parametert
Definition: std_types.h:761
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:354
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
ansi_c_convert_typet::read
virtual void read(const typet &type)
Definition: ansi_c_convert_type.cpp:24
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
cpp_convert_typet
Definition: cpp_convert_type.cpp:27
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:117
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
ansi_c_convert_typet::ptr32_cnt
unsigned ptr32_cnt
Definition: ansi_c_convert_type.h:32
cpp_namet::get_base_name
irep_idt get_base_name() const
Definition: cpp_name.cpp:16
cpp_namet
Definition: cpp_name.h:17
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:111
c_types.h
ansi_c_convert_typet::read_rec
virtual void read_rec(const typet &type)
Definition: ansi_c_convert_type.cpp:31
cpp_declaratort
Definition: cpp_declarator.h:20
cpp_convert_typet::clear
void clear() override
Definition: cpp_convert_type.cpp:43
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:32
cpp_name.h