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 <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/invariant.h>
20 #include <util/std_types.h>
21 
23 #include <ansi-c/gcc_types.h>
24 
25 #include "cpp_declaration.h"
26 #include "cpp_name.h"
27 
29 {
30 public:
31  // The following types exist in C11 and later, but are implemented as
32  // typedefs. In C++, they are keywords and thus required explicit handling in
33  // here.
35 
36  void write(typet &type) override;
37 
40  {
41  read(type);
42  }
43 
44 protected:
45  void clear() override
46  {
47  wchar_t_count = 0;
48  char16_t_count = 0;
49  char32_t_count = 0;
50 
52  }
53 
54  void read_rec(const typet &type) override;
55  void read_function_type(const typet &type);
56  void read_template(const typet &type);
57 };
58 
60 {
61  #if 0
62  std::cout << "cpp_convert_typet::read_rec: "
63  << type.pretty() << '\n';
64  #endif
65 
66  if(type.id() == ID_gcc_float80)
68  else if(type.id()==ID_wchar_t)
69  ++wchar_t_count;
70  else if(type.id()==ID_char16_t)
72  else if(type.id()==ID_char32_t)
74  else if(type.id()==ID_constexpr)
76  else if(type.id()==ID_function_type)
77  {
78  read_function_type(type);
79  }
80  else if(type.id()==ID_identifier)
81  {
82  // from parameters
83  }
84  else if(type.id()==ID_cpp_name)
85  {
86  // from typedefs
87  other.push_back(type);
88  }
89  else if(type.id()==ID_array)
90  {
91  other.push_back(type);
93  }
94  else if(type.id()==ID_template)
95  {
96  read_template(type);
97  }
98  else if(type.id()==ID_frontend_pointer)
99  {
100  // add width and turn into ID_pointer
103  if(type.get_bool(ID_C_reference))
104  tmp.set(ID_C_reference, true);
105  if(type.get_bool(ID_C_rvalue_reference))
106  tmp.set(ID_C_rvalue_reference, true);
107  const irep_idt typedef_identifier = type.get(ID_C_typedef);
108  if(!typedef_identifier.empty())
109  tmp.set(ID_C_typedef, typedef_identifier);
110  other.push_back(tmp);
111  }
112  else if(type.id()==ID_pointer)
113  {
114  // ignore, we unfortunately convert multiple times
115  other.push_back(type);
116  }
117  else if(type.id() == ID_frontend_vector)
118  vector_size = static_cast<const exprt &>(type.find(ID_size));
119  else
120  {
122  }
123 }
124 
126 {
127  other.push_back(type);
128  typet &t=other.back();
129 
131 
132  irept &arguments=t.add(ID_arguments);
133 
134  Forall_irep(it, arguments.get_sub())
135  {
136  exprt &decl=static_cast<exprt &>(*it);
137 
138  // may be type or expression
139  bool is_type=decl.get_bool(ID_is_type);
140 
141  if(is_type)
142  {
143  }
144  else
145  {
147  }
148 
149  // TODO: initializer
150  }
151 }
152 
154 {
155  other.push_back(type);
156  other.back().id(ID_code);
157 
158  code_typet &t = to_code_type(other.back());
159 
160  // change subtype to return_type
161  typet &return_type = t.return_type();
162 
163  return_type.swap(t.subtype());
164  t.remove_subtype();
165 
166  if(return_type.is_not_nil())
168 
169  // take care of parameter types
170  code_typet::parameterst &parameters = t.parameters();
171 
172  // see if we have an ellipsis
173  if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
174  {
175  t.make_ellipsis();
176  parameters.pop_back();
177  }
178 
179  for(auto &parameter_expr : parameters)
180  {
181  if(parameter_expr.id()==ID_cpp_declaration)
182  {
183  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
184  source_locationt type_location=declaration.type().source_location();
185 
187 
188  // there should be only one declarator
189  assert(declaration.declarators().size()==1);
190 
191  cpp_declaratort &declarator=
192  declaration.declarators().front();
193 
194  // do we have a declarator?
195  if(declarator.is_nil())
196  {
197  parameter_expr = code_typet::parametert(declaration.type());
198  parameter_expr.add_source_location()=type_location;
199  }
200  else
201  {
202  const cpp_namet &cpp_name=declarator.name();
203  typet final_type=declarator.merge_type(declaration.type());
204 
205  // see if it's an array type
206  if(final_type.id()==ID_array)
207  {
208  // turn into pointer type
209  final_type=pointer_type(final_type.subtype());
210  }
211 
212  code_typet::parametert new_parameter(final_type);
213 
214  if(cpp_name.is_nil())
215  {
216  new_parameter.add_source_location()=type_location;
217  }
218  else if(cpp_name.is_simple_name())
219  {
220  irep_idt base_name=cpp_name.get_base_name();
221  assert(!base_name.empty());
222  new_parameter.set_identifier(base_name);
223  new_parameter.set_base_name(base_name);
224  new_parameter.add_source_location()=cpp_name.source_location();
225  }
226  else
227  {
228  throw "expected simple name as parameter";
229  }
230 
231  if(declarator.value().is_not_nil())
232  new_parameter.default_value().swap(declarator.value());
233 
234  parameter_expr.swap(new_parameter);
235  }
236  }
237  else if(parameter_expr.id()==ID_ellipsis)
238  {
239  throw "ellipsis only allowed as last parameter";
240  }
241  else
242  UNREACHABLE;
243  }
244 
245  // if we just have one parameter of type void, remove it
246  if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
247  parameters.clear();
248 }
249 
251 {
252  if(!other.empty())
253  {
255  {
257  error() << "illegal type modifier for defined type" << eom;
258  throw 0;
259  }
260 
262  }
263  else if(c_bool_cnt)
264  {
265  if(
269  ptr32_cnt || ptr64_cnt)
270  {
271  throw "illegal type modifier for C++ bool";
272  }
273 
275  }
276  else if(wchar_t_count)
277  {
278  // This is a distinct type, and can't be made signed/unsigned.
279  // This is tolerated by most compilers, however.
280 
281  if(
284  ptr32_cnt || ptr64_cnt)
285  {
286  throw "illegal type modifier for wchar_t";
287  }
288 
289  type=wchar_t_type();
292  }
293  else if(char16_t_count)
294  {
295  // This is a distinct type, and can't be made signed/unsigned.
296  if(
300  {
301  throw "illegal type modifier for char16_t";
302  }
303 
304  type=char16_t_type();
307  }
308  else if(char32_t_count)
309  {
310  // This is a distinct type, and can't be made signed/unsigned.
311  if(int_cnt || short_cnt || char_cnt || long_cnt ||
312  int8_cnt || int16_cnt || int32_cnt ||
313  int64_cnt || ptr32_cnt || ptr64_cnt ||
315  {
316  throw "illegal type modifier for char32_t";
317  }
318 
319  type=char32_t_type();
322  }
323  else
324  {
326  }
327 }
328 
329 void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
330 {
331  if(
332  type.id() == ID_cpp_name || type.id() == ID_struct ||
333  type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
334  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
335  type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
336  type.id() == ID_constructor || type.id() == ID_destructor)
337  {
338  }
339  else if(type.id()==ID_c_enum)
340  {
341  // add width -- we use int, but the standard
342  // doesn't guarantee that
343  type.set(ID_width, config.ansi_c.int_width);
344  }
345  else if(type.id() == ID_c_bool)
346  {
347  type.set(ID_width, config.ansi_c.bool_width);
348  }
349  else
350  {
351  cpp_convert_typet cpp_convert_type(message_handler, type);
352  cpp_convert_type.write(type);
353  }
354 }
355 
357  typet &dest,
358  const typet &src,
359  message_handlert &message_handler)
360 {
361  if(dest.id() != ID_merged_type && dest.has_subtype())
362  {
363  cpp_convert_auto(dest.subtype(), src, message_handler);
364  return;
365  }
366 
367  cpp_convert_typet cpp_convert_type(message_handler, dest);
368  for(auto &t : cpp_convert_type.other)
369  if(t.id() == ID_auto)
370  t = src;
371 
372  cpp_convert_type.write(dest);
373 }
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:34
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:33
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:615
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
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:488
to_cpp_declaration
cpp_declarationt & to_cpp_declaration(irept &irep)
Definition: cpp_declaration.h:148
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:254
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:782
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:53
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:153
Forall_irep
#define Forall_irep(it, irep)
Definition: irep.h:66
cpp_convert_typet::write
void write(typet &type) override
Definition: cpp_convert_type.cpp:250
ansi_c_convert_typet
Definition: ansi_c_convert_type.h:23
cpp_declarationt::declarators
const declaratorst & declarators() const
Definition: cpp_declaration.h:64
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:81
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:402
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:59
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
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:764
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:463
code_typet
Base type of functions.
Definition: std_types.h:736
cpp_convert_type.h
C++ Language Conversion.
cpp_declarationt
Definition: cpp_declaration.h:24
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:857
cpp_convert_typet::cpp_convert_typet
cpp_convert_typet(message_handlert &message_handler, const typet &type)
Definition: cpp_convert_type.cpp:38
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:787
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:329
source_locationt
Definition: source_location.h:20
cpp_convert_typet::char16_t_count
std::size_t char16_t_count
Definition: cpp_convert_type.cpp:34
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:595
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:837
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
irept::get_sub
subt & get_sub()
Definition: irep.h:477
code_typet::parametert
Definition: std_types.h:753
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:356
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
ansi_c_convert_typet::read
virtual void read(const typet &type)
Definition: ansi_c_convert_type.cpp:26
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
cpp_convert_typet
Definition: cpp_convert_type.cpp:29
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:37
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
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:17
cpp_namet
Definition: cpp_name.h:17
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:31
c_types.h
ansi_c_convert_typet::read_rec
virtual void read_rec(const typet &type)
Definition: ansi_c_convert_type.cpp:33
cpp_declaratort
Definition: cpp_declarator.h:20
cpp_convert_typet::clear
void clear() override
Definition: cpp_convert_type.cpp:45
cpp_convert_typet::read_template
void read_template(const typet &type)
Definition: cpp_convert_type.cpp:125
cpp_declaratort::merge_type
typet merge_type(const typet &declaration_type) const
Definition: cpp_declarator.cpp:28
cpp_convert_typet::wchar_t_count
std::size_t wchar_t_count
Definition: cpp_convert_type.cpp:34
cpp_name.h