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/message.h>
18 #include <util/std_types.h>
19 
21 
22 #include "cpp_declaration.h"
23 #include "cpp_name.h"
24 
26 {
27 public:
28  // The following types exist in C11 and later, but are implemented as
29  // typedefs. In C++, they are keywords and thus required explicit handling in
30  // here.
32 
33  void write(typet &type) override;
34 
37  wchar_t_count(0),
38  char16_t_count(0),
40  {
42  read_rec(type);
43  }
44 
45 protected:
46  void read_rec(const typet &type) override;
47  void read_function_type(const typet &type);
48  void read_template(const typet &type);
49 };
50 
52 {
53  #if 0
54  std::cout << "cpp_convert_typet::read_rec: "
55  << type.pretty() << '\n';
56  #endif
57 
58  if(type.id() == ID_gcc_float80)
60  else if(type.id()==ID_wchar_t)
61  ++wchar_t_count;
62  else if(type.id()==ID_char16_t)
64  else if(type.id()==ID_char32_t)
66  else if(type.id()==ID_constexpr)
68  else if(type.id()==ID_function_type)
69  {
70  read_function_type(type);
71  }
72  else if(type.id()==ID_identifier)
73  {
74  // from parameters
75  }
76  else if(type.id()==ID_cpp_name)
77  {
78  // from typedefs
79  other.push_back(type);
80  }
81  else if(type.id()==ID_array)
82  {
83  other.push_back(type);
86  }
87  else if(type.id()==ID_template)
88  {
89  read_template(type);
90  }
91  else if(type.id()==ID_frontend_pointer)
92  {
93  // add width and turn into ID_pointer
94  pointer_typet tmp(
97  if(type.get_bool(ID_C_reference))
98  tmp.set(ID_C_reference, true);
99  if(type.get_bool(ID_C_rvalue_reference))
100  tmp.set(ID_C_rvalue_reference, true);
101  const irep_idt typedef_identifier = type.get(ID_C_typedef);
102  if(!typedef_identifier.empty())
103  tmp.set(ID_C_typedef, typedef_identifier);
104  other.push_back(tmp);
105  }
106  else if(type.id()==ID_pointer)
107  {
108  // ignore, we unfortunately convert multiple times
109  other.push_back(type);
110  }
111  else if(type.id() == ID_frontend_vector)
112  vector_size = static_cast<const exprt &>(type.find(ID_size));
113  else
114  {
116  }
117 }
118 
120 {
121  other.push_back(type);
122  typet &t=other.back();
123 
125 
126  irept &arguments=t.add(ID_arguments);
127 
128  for(auto &argument : arguments.get_sub())
129  {
130  exprt &decl = static_cast<exprt &>(argument);
131 
132  // may be type or expression
133  bool is_type=decl.get_bool(ID_is_type);
134 
135  if(is_type)
136  {
137  }
138  else
139  {
141  }
142 
143  // TODO: initializer
144  }
145 }
146 
148 {
149  other.push_back(type);
150  other.back().id(ID_code);
151 
152  code_typet &t = to_code_type(other.back());
153 
154  // change subtype to return_type
155  typet &return_type = t.return_type();
156 
157  return_type.swap(to_type_with_subtype(t).subtype());
158  t.remove_subtype();
159 
160  if(return_type.is_not_nil())
162 
163  // take care of parameter types
164  code_typet::parameterst &parameters = t.parameters();
165 
166  // see if we have an ellipsis
167  if(!parameters.empty() && parameters.back().id() == ID_ellipsis)
168  {
169  t.make_ellipsis();
170  parameters.pop_back();
171  }
172 
173  for(auto &parameter_expr : parameters)
174  {
175  if(parameter_expr.id()==ID_cpp_declaration)
176  {
177  cpp_declarationt &declaration=to_cpp_declaration(parameter_expr);
178  source_locationt type_location=declaration.type().source_location();
179 
181 
183  declaration.declarators().size() == 1,
184  "there should be only one declarator");
185 
186  cpp_declaratort &declarator=
187  declaration.declarators().front();
188 
189  // do we have a declarator?
190  if(declarator.is_nil())
191  {
192  parameter_expr = code_typet::parametert(declaration.type());
193  parameter_expr.add_source_location()=type_location;
194  }
195  else
196  {
197  const cpp_namet &cpp_name=declarator.name();
198  typet final_type=declarator.merge_type(declaration.type());
199 
200  // see if it's an array type
201  if(final_type.id()==ID_array)
202  {
203  // turn into pointer type
204  final_type = pointer_type(to_array_type(final_type).element_type());
205  }
206 
207  code_typet::parametert new_parameter(final_type);
208 
209  if(cpp_name.is_nil())
210  {
211  new_parameter.add_source_location()=type_location;
212  }
213  else if(cpp_name.is_simple_name())
214  {
215  irep_idt base_name=cpp_name.get_base_name();
216  CHECK_RETURN(!base_name.empty());
217  new_parameter.set_identifier(base_name);
218  new_parameter.set_base_name(base_name);
219  new_parameter.add_source_location()=cpp_name.source_location();
220  }
221  else
222  {
223  throw "expected simple name as parameter";
224  }
225 
226  if(declarator.value().is_not_nil())
227  new_parameter.default_value().swap(declarator.value());
228 
229  parameter_expr.swap(new_parameter);
230  }
231  }
232  else if(parameter_expr.id()==ID_ellipsis)
233  {
234  throw "ellipsis only allowed as last parameter";
235  }
236  else
237  UNREACHABLE;
238  }
239 
240  // if we just have one parameter of type void, remove it
241  if(parameters.size() == 1 && parameters.front().type().id() == ID_empty)
242  parameters.clear();
243 }
244 
246 {
247  if(!other.empty())
248  {
250  {
252  log.error().source_location = source_location;
253  log.error() << "illegal type modifier for defined type" << messaget::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  type.id() == ID_c_enum)
334  {
335  }
336  else if(type.id() == ID_c_bool)
337  {
338  type.set(ID_width, config.ansi_c.bool_width);
339  }
340  else
341  {
342  cpp_convert_typet cpp_convert_type(message_handler, type);
343  cpp_convert_type.write(type);
344  }
345 }
346 
348  typet &dest,
349  const typet &src,
350  message_handlert &message_handler)
351 {
352  if(dest.id() != ID_merged_type && dest.has_subtype())
353  {
355  to_type_with_subtype(dest).subtype(), src, message_handler);
356  return;
357  }
358 
359  cpp_convert_typet cpp_convert_type(message_handler, dest);
360  for(auto &t : cpp_convert_type.other)
361  if(t.id() == ID_auto)
362  t = src;
363 
364  cpp_convert_type.write(dest);
365 }
ANSI-C Language Conversion.
configt config
Definition: config.cpp:25
unsignedbv_typet char32_t_type()
Definition: c_types.cpp:167
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
bitvector_typet wchar_t_type()
Definition: c_types.cpp:141
unsignedbv_typet char16_t_type()
Definition: c_types.cpp:157
virtual void read_rec(const typet &type)
virtual void write(typet &type)
message_handlert & message_handler
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 typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & default_value() const
Definition: std_types.h:606
void set_base_name(const irep_idt &name)
Definition: std_types.h:629
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:624
Base type of functions.
Definition: std_types.h:583
std::vector< parametert > parameterst
Definition: std_types.h:585
const typet & return_type() const
Definition: std_types.h:689
void make_ellipsis()
Definition: std_types.h:679
const parameterst & parameters() const
Definition: std_types.h:699
struct configt::ansi_ct ansi_c
std::size_t char32_t_count
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:14
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:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:236
typet & type()
Return the type of the expression.
Definition: expr.h:84
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:444
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
bool is_not_nil() const
Definition: irep.h:368
const irep_idt & id() const
Definition: irep.h:384
void swap(irept &irep)
Definition: irep.h:430
irept & add(const irep_idt &name)
Definition: irep.cpp:103
bool is_nil() const
Definition: irep.h:364
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
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:72
bool has_subtype() const
Definition: type.h:64
void remove_subtype()
Definition: type.h:69
source_locationt & add_source_location()
Definition: type.h:77
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)
double log(double x)
Definition: math.c:2776
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
std::size_t pointer_width
Definition: config.h:143
std::size_t bool_width
Definition: config.h:139
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208