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
97  pointer_typet tmp(
100  if(type.get_bool(ID_C_reference))
101  tmp.set(ID_C_reference, true);
102  if(type.get_bool(ID_C_rvalue_reference))
103  tmp.set(ID_C_rvalue_reference, true);
104  const irep_idt typedef_identifier = type.get(ID_C_typedef);
105  if(!typedef_identifier.empty())
106  tmp.set(ID_C_typedef, typedef_identifier);
107  other.push_back(tmp);
108  }
109  else if(type.id()==ID_pointer)
110  {
111  // ignore, we unfortunately convert multiple times
112  other.push_back(type);
113  }
114  else if(type.id() == ID_frontend_vector)
115  vector_size = static_cast<const exprt &>(type.find(ID_size));
116  else
117  {
119  }
120 }
121 
123 {
124  other.push_back(type);
125  typet &t=other.back();
126 
128 
129  irept &arguments=t.add(ID_arguments);
130 
131  for(auto &argument : arguments.get_sub())
132  {
133  exprt &decl = static_cast<exprt &>(argument);
134 
135  // may be type or expression
136  bool is_type=decl.get_bool(ID_is_type);
137 
138  if(is_type)
139  {
140  }
141  else
142  {
144  }
145 
146  // TODO: initializer
147  }
148 }
149 
151 {
152  other.push_back(type);
153  other.back().id(ID_code);
154 
155  code_typet &t = to_code_type(other.back());
156 
157  // change subtype to return_type
158  typet &return_type = t.return_type();
159 
160  return_type.swap(t.subtype());
161  t.remove_subtype();
162 
163  if(return_type.is_not_nil())
165 
166  // take care of parameter types
167  code_typet::parameterst &parameters = t.parameters();
168 
169  // see if we have an ellipsis
170  if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
171  {
172  t.make_ellipsis();
173  parameters.pop_back();
174  }
175 
176  for(auto &parameter_expr : parameters)
177  {
178  if(parameter_expr.id()==ID_cpp_declaration)
179  {
180  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
181  source_locationt type_location=declaration.type().source_location();
182 
184 
185  // there should be only one declarator
186  assert(declaration.declarators().size()==1);
187 
188  cpp_declaratort &declarator=
189  declaration.declarators().front();
190 
191  // do we have a declarator?
192  if(declarator.is_nil())
193  {
194  parameter_expr = code_typet::parametert(declaration.type());
195  parameter_expr.add_source_location()=type_location;
196  }
197  else
198  {
199  const cpp_namet &cpp_name=declarator.name();
200  typet final_type=declarator.merge_type(declaration.type());
201 
202  // see if it's an array type
203  if(final_type.id()==ID_array)
204  {
205  // turn into pointer type
206  final_type=pointer_type(final_type.subtype());
207  }
208 
209  code_typet::parametert new_parameter(final_type);
210 
211  if(cpp_name.is_nil())
212  {
213  new_parameter.add_source_location()=type_location;
214  }
215  else if(cpp_name.is_simple_name())
216  {
217  irep_idt base_name=cpp_name.get_base_name();
218  assert(!base_name.empty());
219  new_parameter.set_identifier(base_name);
220  new_parameter.set_base_name(base_name);
221  new_parameter.add_source_location()=cpp_name.source_location();
222  }
223  else
224  {
225  throw "expected simple name as parameter";
226  }
227 
228  if(declarator.value().is_not_nil())
229  new_parameter.default_value().swap(declarator.value());
230 
231  parameter_expr.swap(new_parameter);
232  }
233  }
234  else if(parameter_expr.id()==ID_ellipsis)
235  {
236  throw "ellipsis only allowed as last parameter";
237  }
238  else
239  UNREACHABLE;
240  }
241 
242  // if we just have one parameter of type void, remove it
243  if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
244  parameters.clear();
245 }
246 
248 {
249  if(!other.empty())
250  {
252  {
254  error() << "illegal type modifier for defined type" << eom;
255  throw 0;
256  }
257 
259  }
260  else if(c_bool_cnt)
261  {
262  if(
266  ptr32_cnt || ptr64_cnt)
267  {
268  throw "illegal type modifier for C++ bool";
269  }
270 
272  }
273  else if(wchar_t_count)
274  {
275  // This is a distinct type, and can't be made signed/unsigned.
276  // This is tolerated by most compilers, however.
277 
278  if(
281  ptr32_cnt || ptr64_cnt)
282  {
283  throw "illegal type modifier for wchar_t";
284  }
285 
286  type=wchar_t_type();
289  }
290  else if(char16_t_count)
291  {
292  // This is a distinct type, and can't be made signed/unsigned.
293  if(
297  {
298  throw "illegal type modifier for char16_t";
299  }
300 
301  type=char16_t_type();
304  }
305  else if(char32_t_count)
306  {
307  // This is a distinct type, and can't be made signed/unsigned.
308  if(int_cnt || short_cnt || char_cnt || long_cnt ||
309  int8_cnt || int16_cnt || int32_cnt ||
310  int64_cnt || ptr32_cnt || ptr64_cnt ||
312  {
313  throw "illegal type modifier for char32_t";
314  }
315 
316  type=char32_t_type();
319  }
320  else
321  {
323  }
324 }
325 
326 void cpp_convert_plain_type(typet &type, message_handlert &message_handler)
327 {
328  if(
329  type.id() == ID_cpp_name || type.id() == ID_struct ||
330  type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
331  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
332  type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
333  type.id() == ID_constructor || type.id() == ID_destructor)
334  {
335  }
336  else if(type.id()==ID_c_enum)
337  {
338  // add width -- we use int, but the standard
339  // doesn't guarantee that
340  type.set(ID_width, config.ansi_c.int_width);
341  }
342  else if(type.id() == ID_c_bool)
343  {
344  type.set(ID_width, config.ansi_c.bool_width);
345  }
346  else
347  {
348  cpp_convert_typet cpp_convert_type(message_handler, type);
349  cpp_convert_type.write(type);
350  }
351 }
352 
354  typet &dest,
355  const typet &src,
356  message_handlert &message_handler)
357 {
358  if(dest.id() != ID_merged_type && dest.has_subtype())
359  {
360  cpp_convert_auto(dest.subtype(), src, message_handler);
361  return;
362  }
363 
364  cpp_convert_typet cpp_convert_type(message_handler, dest);
365  for(auto &t : cpp_convert_type.other)
366  if(t.id() == ID_auto)
367  t = src;
368 
369  cpp_convert_type.write(dest);
370 }
ANSI-C Language Conversion.
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:185
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
bitvector_typet wchar_t_type()
Definition: c_types.cpp:159
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:175
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:372
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
subt & get_sub()
Definition: irep.h:456
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
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:29
const source_locationt & source_location() const
Definition: type.h:74
const typet & subtype() const
Definition: type.h:48
bool has_subtype() const
Definition: type.h:66
void remove_subtype()
Definition: type.h:71
source_locationt & add_source_location()
Definition: type.h:79
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:115
std::size_t bool_width
Definition: config.h:111
std::size_t int_width
Definition: config.h:109
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177