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