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/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);
89  }
90  else if(type.id()==ID_template)
91  {
92  read_template(type);
93  }
94  else if(type.id()==ID_frontend_pointer)
95  {
96  // add width and turn into ID_pointer
99  if(type.get_bool(ID_C_reference))
100  tmp.set(ID_C_reference, true);
101  if(type.get_bool(ID_C_rvalue_reference))
102  tmp.set(ID_C_rvalue_reference, true);
103  const irep_idt typedef_identifier = type.get(ID_C_typedef);
104  if(!typedef_identifier.empty())
105  tmp.set(ID_C_typedef, typedef_identifier);
106  other.push_back(tmp);
107  }
108  else if(type.id()==ID_pointer)
109  {
110  // ignore, we unfortunately convert multiple times
111  other.push_back(type);
112  }
113  else if(type.id() == ID_frontend_vector)
114  vector_size = static_cast<const exprt &>(type.find(ID_size));
115  else
116  {
118  }
119 }
120 
122 {
123  other.push_back(type);
124  typet &t=other.back();
125 
127 
128  irept &arguments=t.add(ID_arguments);
129 
130  for(auto &argument : arguments.get_sub())
131  {
132  exprt &decl = static_cast<exprt &>(argument);
133 
134  // may be type or expression
135  bool is_type=decl.get_bool(ID_is_type);
136 
137  if(is_type)
138  {
139  }
140  else
141  {
143  }
144 
145  // TODO: initializer
146  }
147 }
148 
150 {
151  other.push_back(type);
152  other.back().id(ID_code);
153 
154  code_typet &t = to_code_type(other.back());
155 
156  // change subtype to return_type
157  typet &return_type = t.return_type();
158 
159  return_type.swap(t.subtype());
160  t.remove_subtype();
161 
162  if(return_type.is_not_nil())
164 
165  // take care of parameter types
166  code_typet::parameterst &parameters = t.parameters();
167 
168  // see if we have an ellipsis
169  if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
170  {
171  t.make_ellipsis();
172  parameters.pop_back();
173  }
174 
175  for(auto &parameter_expr : parameters)
176  {
177  if(parameter_expr.id()==ID_cpp_declaration)
178  {
179  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
180  source_locationt type_location=declaration.type().source_location();
181 
183 
184  // there should be only one declarator
185  assert(declaration.declarators().size()==1);
186 
187  cpp_declaratort &declarator=
188  declaration.declarators().front();
189 
190  // do we have a declarator?
191  if(declarator.is_nil())
192  {
193  parameter_expr = code_typet::parametert(declaration.type());
194  parameter_expr.add_source_location()=type_location;
195  }
196  else
197  {
198  const cpp_namet &cpp_name=declarator.name();
199  typet final_type=declarator.merge_type(declaration.type());
200 
201  // see if it's an array type
202  if(final_type.id()==ID_array)
203  {
204  // turn into pointer type
205  final_type=pointer_type(final_type.subtype());
206  }
207 
208  code_typet::parametert new_parameter(final_type);
209 
210  if(cpp_name.is_nil())
211  {
212  new_parameter.add_source_location()=type_location;
213  }
214  else if(cpp_name.is_simple_name())
215  {
216  irep_idt base_name=cpp_name.get_base_name();
217  assert(!base_name.empty());
218  new_parameter.set_identifier(base_name);
219  new_parameter.set_base_name(base_name);
220  new_parameter.add_source_location()=cpp_name.source_location();
221  }
222  else
223  {
224  throw "expected simple name as parameter";
225  }
226 
227  if(declarator.value().is_not_nil())
228  new_parameter.default_value().swap(declarator.value());
229 
230  parameter_expr.swap(new_parameter);
231  }
232  }
233  else if(parameter_expr.id()==ID_ellipsis)
234  {
235  throw "ellipsis only allowed as last parameter";
236  }
237  else
238  UNREACHABLE;
239  }
240 
241  // if we just have one parameter of type void, remove it
242  if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
243  parameters.clear();
244 }
245 
247 {
248  if(!other.empty())
249  {
251  {
253  error() << "illegal type modifier for defined type" << eom;
254  throw 0;
255  }
256 
258  }
259  else if(c_bool_cnt)
260  {
261  if(
265  ptr32_cnt || ptr64_cnt)
266  {
267  throw "illegal type modifier for C++ bool";
268  }
269 
271  }
272  else if(wchar_t_count)
273  {
274  // This is a distinct type, and can't be made signed/unsigned.
275  // This is tolerated by most compilers, however.
276 
277  if(
280  ptr32_cnt || ptr64_cnt)
281  {
282  throw "illegal type modifier for wchar_t";
283  }
284 
285  type=wchar_t_type();
288  }
289  else if(char16_t_count)
290  {
291  // This is a distinct type, and can't be made signed/unsigned.
292  if(
296  {
297  throw "illegal type modifier for char16_t";
298  }
299 
300  type=char16_t_type();
303  }
304  else if(char32_t_count)
305  {
306  // This is a distinct type, and can't be made signed/unsigned.
307  if(int_cnt || short_cnt || char_cnt || long_cnt ||
308  int8_cnt || int16_cnt || int32_cnt ||
309  int64_cnt || ptr32_cnt || ptr64_cnt ||
311  {
312  throw "illegal type modifier for char32_t";
313  }
314 
315  type=char32_t_type();
318  }
319  else
320  {
322  }
323 }
324 
325 void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
326 {
327  if(
328  type.id() == ID_cpp_name || type.id() == ID_struct ||
329  type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
330  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
331  type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
332  type.id() == ID_constructor || type.id() == ID_destructor)
333  {
334  }
335  else if(type.id()==ID_c_enum)
336  {
337  // add width -- we use int, but the standard
338  // doesn't guarantee that
339  type.set(ID_width, config.ansi_c.int_width);
340  }
341  else if(type.id() == ID_c_bool)
342  {
343  type.set(ID_width, config.ansi_c.bool_width);
344  }
345  else
346  {
347  cpp_convert_typet cpp_convert_type(message_handler, type);
348  cpp_convert_type.write(type);
349  }
350 }
351 
353  typet &dest,
354  const typet &src,
355  message_handlert &message_handler)
356 {
357  if(dest.id() != ID_merged_type && dest.has_subtype())
358  {
359  cpp_convert_auto(dest.subtype(), src, message_handler);
360  return;
361  }
362 
363  cpp_convert_typet cpp_convert_type(message_handler, dest);
364  for(auto &t : cpp_convert_type.other)
365  if(t.id() == ID_auto)
366  t = src;
367 
368  cpp_convert_type.write(dest);
369 }
ANSI-C Language Conversion.
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:175
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
bitvector_typet wchar_t_type()
Definition: c_types.cpp:149
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:165
virtual void read_rec(const typet &type)
virtual void read(const typet &type)
virtual void write(typet &type)
virtual void set_attributes(typet &type) const
Add qualifiers and GCC attributes onto type.
source_locationt source_location
virtual void build_type_with_subtype(typet &type) const
Build a vector or complex type with type as subtype.
std::list< typet > other
const exprt & default_value() const
Definition: std_types.h:562
void set_base_name(const irep_idt &name)
Definition: std_types.h:585
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:580
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const typet & return_type() const
Definition: std_types.h:645
void make_ellipsis()
Definition: std_types.h:635
const parameterst & parameters() const
Definition: std_types.h:655
struct configt::ansi_ct ansi_c
std::size_t char32_t_count
void clear() override
void write(typet &type) override
cpp_convert_typet(message_handlert &message_handler, const typet &type)
std::size_t char16_t_count
void read_rec(const typet &type) override
std::size_t wchar_t_count
void read_template(const typet &type)
void read_function_type(const typet &type)
const declaratorst & declarators() const
cpp_namet & name()
typet merge_type(const typet &declaration_type) const
irep_idt get_base_name() const
Definition: cpp_name.cpp:16
const source_locationt & source_location() const
Definition: cpp_name.h:73
bool is_simple_name() const
Definition: cpp_name.h:89
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
source_locationt & add_source_location()
Definition: expr.h:235
typet & type()
Return the type of the expression.
Definition: expr.h:82
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
subt & get_sub()
Definition: irep.h:467
irept & add(const irep_namet &name)
Definition: irep.cpp:116
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
bool is_nil() const
Definition: irep.h:387
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
message_handlert * message_handler
Definition: message.h:439
message_handlert & get_message_handler()
Definition: message.h:184
static eomt eom
Definition: message.h:297
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The type of an expression, extends irept.
Definition: type.h:28
const source_locationt & source_location() const
Definition: type.h:71
const typet & subtype() const
Definition: type.h:47
bool has_subtype() const
Definition: type.h:65
void remove_subtype()
Definition: type.h:68
source_locationt & add_source_location()
Definition: type.h:76
configt config
Definition: config.cpp:25
void cpp_convert_auto(typet &dest, const typet &src, message_handlert &message_handler)
void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
C++ Language Conversion.
C++ Language Type Checking.
cpp_declarationt & to_cpp_declaration(irept &irep)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
std::size_t pointer_width
Definition: config.h:116
std::size_t bool_width
Definition: config.h:112
std::size_t int_width
Definition: config.h:110