cprover
expr2cpp.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 #include "expr2cpp.h"
10 
11 #include <cassert>
12 
13 #include <util/std_types.h>
14 #include <util/std_expr.h>
15 #include <util/symbol.h>
16 #include <util/lispirep.h>
17 #include <util/lispexpr.h>
18 #include <util/namespace.h>
19 
20 #include <ansi-c/c_misc.h>
21 #include <ansi-c/c_qualifiers.h>
22 #include <ansi-c/expr2c_class.h>
23 
24 class expr2cppt:public expr2ct
25 {
26 public:
27  explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
28 
29 protected:
30  std::string convert_with_precedence(
31  const exprt &src, unsigned &precedence) override;
32  std::string convert_cpp_this(const exprt &src, unsigned precedence);
33  std::string convert_cpp_new(const exprt &src, unsigned precedence);
34  std::string convert_extractbit(const exprt &src, unsigned precedence);
35  std::string convert_extractbits(const exprt &src, unsigned precedence);
36  std::string convert_code_cpp_delete(const exprt &src, unsigned precedence);
37  std::string convert_struct(const exprt &src, unsigned &precedence) override;
38  std::string convert_code(const codet &src, unsigned indent) override;
39  // NOLINTNEXTLINE(whitespace/line_length)
40  std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
41 
42  std::string convert_rec(
43  const typet &src,
44  const c_qualifierst &qualifiers,
45  const std::string &declarator) override;
46 
47  typedef std::unordered_set<std::string, string_hash> id_sett;
48 };
49 
51  const exprt &src,
52  unsigned &precedence)
53 {
54  const typet &full_type=ns.follow(src.type());
55 
56  if(full_type.id()!=ID_struct)
57  return convert_norep(src, precedence);
58 
59  const struct_typet &struct_type=to_struct_type(full_type);
60 
61  std::string dest="{ ";
62 
63  const struct_typet::componentst &components=
64  struct_type.components();
65 
66  assert(components.size()==src.operands().size());
67 
68  exprt::operandst::const_iterator o_it=src.operands().begin();
69 
70  bool first=true;
71  size_t last_size=0;
72 
73  for(struct_typet::componentst::const_iterator
74  c_it=components.begin();
75  c_it!=components.end();
76  c_it++)
77  {
78  if(c_it->type().id()==ID_code)
79  {
80  }
81  else
82  {
83  std::string tmp=convert(*o_it);
84  std::string sep;
85 
86  if(first)
87  first=false;
88  else
89  {
90  if(last_size+40<dest.size())
91  {
92  sep=",\n ";
93  last_size=dest.size();
94  }
95  else
96  sep=", ";
97  }
98 
99  dest+=sep;
100  dest+='.';
101  dest+=c_it->get_string(ID_pretty_name);
102  dest+='=';
103  dest+=tmp;
104  }
105 
106  o_it++;
107  }
108 
109  dest+=" }";
110 
111  return dest;
112 }
113 
115  const constant_exprt &src,
116  unsigned &precedence)
117 {
118  if(src.type().id()==ID_bool)
119  {
120  // C++ has built-in Boolean constants, in contrast to C
121  if(src.is_true())
122  return "true";
123  else if(src.is_false())
124  return "false";
125  }
126 
127  return expr2ct::convert_constant(src, precedence);
128 }
129 
131  const typet &src,
132  const c_qualifierst &qualifiers,
133  const std::string &declarator)
134 {
135  c_qualifierst new_qualifiers(qualifiers);
136  new_qualifiers.read(src);
137 
138  const std::string d=
139  declarator==""?declarator:(" "+declarator);
140 
141  const std::string q=
142  new_qualifiers.as_string();
143 
144  if(is_reference(src))
145  {
146  return q+convert(src.subtype())+" &"+d;
147  }
148  else if(is_rvalue_reference(src))
149  {
150  return q+convert(src.subtype())+" &&"+d;
151  }
152  else if(!src.get(ID_C_c_type).empty())
153  {
154  const irep_idt c_type=src.get(ID_C_c_type);
155 
156  if(c_type==ID_signed_char)
157  return q+"signed char"+d;
158  else if(c_type==ID_unsigned_char)
159  return q+"unsigned char"+d;
160  else if(c_type==ID_char)
161  return q+"char"+d;
162  else if(c_type==ID_signed_short_int)
163  return q+"short"+d;
164  else if(c_type==ID_unsigned_short_int)
165  return q+"unsigned short"+d;
166  else if(c_type==ID_signed_int)
167  return q+"int"+d;
168  else if(c_type==ID_unsigned_int)
169  return q+"unsigned"+d;
170  else if(c_type==ID_signed_long_int)
171  return q+"long"+d;
172  else if(c_type==ID_unsigned_long_int)
173  return q+"unsigned long"+d;
174  else if(c_type==ID_signed_long_long_int)
175  return q+"long long"+d;
176  else if(c_type==ID_unsigned_long_long_int)
177  return q+"unsigned long long"+d;
178  else if(c_type==ID_wchar_t)
179  return q+"wchar_t"+d;
180  else if(c_type==ID_float)
181  return q+"float"+d;
182  else if(c_type==ID_double)
183  return q+"double"+d;
184  else if(c_type==ID_long_double)
185  return q+"long double"+d;
186  else if(c_type==ID_bool)
187  return q+"bool"+d;
188  else
189  return expr2ct::convert_rec(src, qualifiers, declarator);
190  }
191  else if(src.id()==ID_symbol)
192  {
193  const irep_idt &identifier=
195 
196  const symbolt &symbol=ns.lookup(identifier);
197 
198  if(symbol.type.id()==ID_struct ||
199  symbol.type.id()==ID_incomplete_struct)
200  {
201  std::string dest=q;
202 
203  if(symbol.type.get_bool(ID_C_class))
204  dest+="class";
205  else if(symbol.type.get_bool(ID_C_interface))
206  dest+="__interface"; // MS-specific
207  else
208  dest+="struct";
209 
210  if(!symbol.pretty_name.empty())
211  dest+=" "+id2string(symbol.pretty_name);
212 
213  dest+=d;
214 
215  return dest;
216  }
217  else if(symbol.type.id()==ID_c_enum)
218  {
219  std::string dest=q;
220 
221  dest+="enum";
222 
223  if(!symbol.pretty_name.empty())
224  dest+=" "+id2string(symbol.pretty_name);
225 
226  dest+=d;
227 
228  return dest;
229  }
230  else
231  return expr2ct::convert_rec(src, qualifiers, declarator);
232  }
233  else if(src.id()==ID_struct ||
234  src.id()==ID_incomplete_struct)
235  {
236  std::string dest=q;
237 
238  if(src.get_bool(ID_C_class))
239  dest+="class";
240  else if(src.get_bool(ID_C_interface))
241  dest+="__interface"; // MS-specific
242  else
243  dest+="struct";
244 
245  dest+=d;
246 
247  return dest;
248  }
249  else if(src.id()==ID_constructor)
250  {
251  return "constructor ";
252  }
253  else if(src.id()==ID_destructor)
254  {
255  return "destructor ";
256  }
257  else if(src.id()=="cpp-template-type")
258  {
259  return "typename";
260  }
261  else if(src.id()==ID_template)
262  {
263  std::string dest="template<";
264 
265  const irept::subt &arguments=src.find(ID_arguments).get_sub();
266 
267  forall_irep(it, arguments)
268  {
269  if(it!=arguments.begin())
270  dest+=", ";
271 
272  const exprt &argument=(const exprt &)*it;
273 
274  if(argument.id()==ID_symbol)
275  {
276  dest+=convert(argument.type())+" ";
277  dest+=convert(argument);
278  }
279  else if(argument.id()==ID_type)
280  dest+=convert(argument.type());
281  else
282  {
283  lispexprt lisp;
284  irep2lisp(argument, lisp);
285  dest+="irep(\""+MetaString(lisp.expr2string())+"\")";
286  }
287  }
288 
289  dest+="> "+convert(src.subtype());
290  return dest;
291  }
292  else if(src.id()==ID_pointer && src.subtype().id()==ID_nullptr)
293  {
294  return "std::nullptr_t";
295  }
296  else if(src.id()==ID_pointer &&
297  src.find("to-member").is_not_nil())
298  {
299  typet tmp=src;
300  typet member;
301  member.swap(tmp.add("to-member"));
302 
303  std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
304 
305  if(src.subtype().id()==ID_code)
306  {
307  const code_typet &code_type = to_code_type(src.subtype());
308  const typet &return_type = code_type.return_type();
309  dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest;
310 
311  const code_typet::parameterst &args = code_type.parameters();
312  dest+="(";
313 
314  for(code_typet::parameterst::const_iterator it=args.begin();
315  it!=args.end();
316  ++it)
317  {
318  if(it!=args.begin())
319  dest+=", ";
320  dest+=convert_rec(it->type(), c_qualifierst(), "");
321  }
322 
323  dest+=")";
324  dest+=d;
325  }
326  else
327  dest=convert_rec(src.subtype(), c_qualifierst(), "")+" "+dest+d;
328 
329  return dest;
330  }
331  else if(src.id()==ID_verilog_signedbv ||
332  src.id()==ID_verilog_unsignedbv)
333  return "sc_lv["+id2string(src.get(ID_width))+"]"+d;
334  else if(src.id()==ID_unassigned)
335  return "?";
336  else if(src.id()==ID_code)
337  {
338  const code_typet &code_type=to_code_type(src);
339 
340  // C doesn't really have syntax for function types,
341  // so we use C++11 trailing return types!
342 
343  std::string dest="auto";
344 
345  // qualifiers, declarator?
346  if(d.empty())
347  dest+=' ';
348  else
349  dest+=d;
350 
351  dest+='(';
352  const code_typet::parameterst &parameters=code_type.parameters();
353 
354  for(code_typet::parameterst::const_iterator
355  it=parameters.begin();
356  it!=parameters.end();
357  it++)
358  {
359  if(it!=parameters.begin())
360  dest+=", ";
361 
362  dest+=convert(it->type());
363  }
364 
365  if(code_type.has_ellipsis())
366  {
367  if(!parameters.empty())
368  dest+=", ";
369  dest+="...";
370  }
371 
372  dest+=')';
373 
374  const typet &return_type=code_type.return_type();
375  dest+=" -> "+convert(return_type);
376 
377  return dest;
378  }
379  else if(src.id()==ID_initializer_list)
380  {
381  // only really used in error messages
382  return "{ ... }";
383  }
384  else
385  return expr2ct::convert_rec(src, qualifiers, declarator);
386 }
387 
389  const exprt &src,
390  unsigned precedence)
391 {
392  return "this";
393 }
394 
396  const exprt &src,
397  unsigned precedence)
398 {
399  std::string dest;
400 
401  if(src.get(ID_statement)==ID_cpp_new_array)
402  {
403  dest="new";
404 
405  std::string tmp_size=
406  convert(static_cast<const exprt &>(src.find(ID_size)));
407 
408  dest+=' ';
409  dest+=convert(src.type().subtype());
410  dest+='[';
411  dest+=tmp_size;
412  dest+=']';
413  }
414  else
415  dest="new "+convert(src.type().subtype());
416 
417  return dest;
418 }
419 
421  const exprt &src,
422  unsigned indent)
423 {
424  std::string dest=indent_str(indent)+"delete ";
425 
426  if(src.operands().size()!=1)
427  {
428  unsigned precedence;
429  return convert_norep(src, precedence);
430  }
431 
432  std::string tmp=convert(src.op0());
433 
434  dest+=tmp+";\n";
435 
436  return dest;
437 }
438 
440  const exprt &src,
441  unsigned &precedence)
442 {
443  if(src.id()=="cpp-this")
444  return convert_cpp_this(src, precedence=15);
445  if(src.id()==ID_extractbit)
446  return convert_extractbit(src, precedence=15);
447  else if(src.id()==ID_extractbits)
448  return convert_extractbits(src, precedence=15);
449  else if(src.id()==ID_side_effect &&
450  (src.get(ID_statement)==ID_cpp_new ||
451  src.get(ID_statement)==ID_cpp_new_array))
452  return convert_cpp_new(src, precedence=15);
453  else if(src.id()==ID_side_effect &&
454  src.get(ID_statement)==ID_throw)
455  return convert_function(src, "throw", precedence=16);
456  else if(src.is_constant() && src.type().id()==ID_verilog_signedbv)
457  return "'"+id2string(src.get(ID_value))+"'";
458  else if(src.is_constant() && src.type().id()==ID_verilog_unsignedbv)
459  return "'"+id2string(src.get(ID_value))+"'";
460  else if(src.is_constant() && to_constant_expr(src).get_value()==ID_nullptr)
461  return "nullptr";
462  else if(src.id()==ID_unassigned)
463  return "?";
464  else if(src.id()=="pod_constructor")
465  return "pod_constructor";
466  else
467  return expr2ct::convert_with_precedence(src, precedence);
468 }
469 
471  const codet &src,
472  unsigned indent)
473 {
474  const irep_idt &statement=src.get(ID_statement);
475 
476  if(statement==ID_cpp_delete ||
477  statement==ID_cpp_delete_array)
478  return convert_code_cpp_delete(src, indent);
479 
480  if(statement==ID_cpp_new ||
481  statement==ID_cpp_new_array)
482  return convert_cpp_new(src, indent);
483 
484  return expr2ct::convert_code(src, indent);
485 }
486 
488  const exprt &src,
489  unsigned precedence)
490 {
491  assert(src.operands().size()==2);
492  return convert(src.op0())+"["+convert(src.op1())+"]";
493 }
494 
496  const exprt &src,
497  unsigned precedence)
498 {
499  assert(src.operands().size()==3);
500  return
501  convert(src.op0())+".range("+convert(src.op1())+ ","+
502  convert(src.op2())+")";
503 }
504 
505 std::string expr2cpp(const exprt &expr, const namespacet &ns)
506 {
507  expr2cppt expr2cpp(ns);
508  expr2cpp.get_shorthands(expr);
509  return expr2cpp.convert(expr);
510 }
511 
512 std::string type2cpp(const typet &type, const namespacet &ns)
513 {
514  expr2cppt expr2cpp(ns);
515  return expr2cpp.convert(type);
516 }
The type of an expression.
Definition: type.h:20
std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:50
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
Base type of functions.
Definition: std_types.h:734
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
Symbol table entry.
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1180
exprt & op0()
Definition: expr.h:84
std::string convert_extractbit(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:487
std::vector< irept > subt
Definition: irep.h:91
std::string expr2string() const
Definition: lispexpr.cpp:13
bool has_ellipsis() const
Definition: std_types.h:803
std::vector< componentt > componentst
Definition: std_types.h:240
bool is_false() const
Definition: expr.cpp:140
const irep_idt & get_value() const
Definition: std_expr.h:3702
std::vector< parametert > parameterst
Definition: std_types.h:829
std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2cpp.cpp:130
const componentst & components() const
Definition: std_types.h:242
ANSI-C Misc Utilities.
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3269
bool is_true() const
Definition: expr.cpp:133
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:158
std::string convert_cpp_new(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:395
subt & get_sub()
Definition: irep.h:245
std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2cpp.cpp:470
std::string convert_extractbits(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:495
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1704
void read(const typet &src)
const irep_idt & id() const
Definition: irep.h:189
std::string convert_code_cpp_delete(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:420
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:505
std::string convert_cpp_this(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:388
API to expression classes.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::unordered_set< std::string, string_hash > id_sett
Definition: expr2cpp.cpp:47
const namespacet & ns
Definition: expr2c_class.h:35
void irep2lisp(const irept &src, lispexprt &dest)
Definition: lispirep.cpp:43
expr2cppt(const namespacet &_ns)
Definition: expr2cpp.cpp:27
std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:439
bool is_constant() const
Definition: expr.cpp:128
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:163
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1580
std::string as_string() const
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:114
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:512
Base class for all expressions.
Definition: expr.h:46
bool is_rvalue_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:111
const parameterst & parameters() const
Definition: std_types.h:841
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3363
irept & add(const irep_namet &name)
Definition: irep.cpp:306
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void swap(irept &irep)
Definition: irep.h:231
exprt & op2()
Definition: expr.h:90
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:104
A statement in a programming language.
Definition: std_code.h:19
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
bool empty() const
Definition: dstring.h:61
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const typet & return_type() const
Definition: std_types.h:831
const irep_idt & get_identifier() const
Definition: std_types.h:126
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2377
#define forall_irep(it, irep)
Definition: irep.h:62