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 <util/c_types.h>
12 #include <util/lispexpr.h>
13 #include <util/lispirep.h>
14 #include <util/namespace.h>
15 #include <util/pointer_expr.h>
16 #include <util/std_expr.h>
17 
18 #include <ansi-c/c_misc.h>
19 #include <ansi-c/c_qualifiers.h>
20 #include <ansi-c/expr2c_class.h>
21 
22 #include "cpp_name.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();
33  std::string convert_cpp_new(const exprt &src);
34  std::string convert_extractbit(const exprt &src);
35  std::string convert_extractbits(const exprt &src);
36  std::string convert_code_cpp_delete(const exprt &src, unsigned indent);
37  std::string convert_code_cpp_new(const exprt &src, unsigned indent);
38  std::string convert_struct(const exprt &src, unsigned &precedence) override;
39  std::string convert_code(const codet &src, unsigned indent) override;
40  // NOLINTNEXTLINE(whitespace/line_length)
41  std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
42 
43  std::string convert_rec(
44  const typet &src,
45  const qualifierst &qualifiers,
46  const std::string &declarator) override;
47 };
48 
50  const exprt &src,
51  unsigned &precedence)
52 {
53  const typet &full_type=ns.follow(src.type());
54 
55  if(full_type.id()!=ID_struct)
56  return convert_norep(src, precedence);
57 
58  const struct_typet &struct_type=to_struct_type(full_type);
59 
60  std::string dest="{ ";
61 
62  const struct_typet::componentst &components=
63  struct_type.components();
64 
65  assert(components.size()==src.operands().size());
66 
67  exprt::operandst::const_iterator o_it=src.operands().begin();
68 
69  bool first=true;
70  size_t last_size=0;
71 
72  for(const auto &c : components)
73  {
74  if(c.type().id() == ID_code)
75  {
76  }
77  else
78  {
79  std::string tmp=convert(*o_it);
80  std::string sep;
81 
82  if(first)
83  first=false;
84  else
85  {
86  if(last_size+40<dest.size())
87  {
88  sep=",\n ";
89  last_size=dest.size();
90  }
91  else
92  sep=", ";
93  }
94 
95  dest+=sep;
96  dest+='.';
97  dest += c.get_string(ID_pretty_name);
98  dest+='=';
99  dest+=tmp;
100  }
101 
102  o_it++;
103  }
104 
105  dest+=" }";
106 
107  return dest;
108 }
109 
111  const constant_exprt &src,
112  unsigned &precedence)
113 {
114  if(src.type().id() == ID_c_bool)
115  {
116  // C++ has built-in Boolean constants, in contrast to C
117  if(src.is_true())
118  return "true";
119  else if(src.is_false())
120  return "false";
121  }
122 
123  return expr2ct::convert_constant(src, precedence);
124 }
125 
127  const typet &src,
128  const qualifierst &qualifiers,
129  const std::string &declarator)
130 {
131  std::unique_ptr<qualifierst> clone = qualifiers.clone();
132  qualifierst &new_qualifiers = *clone;
133  new_qualifiers.read(src);
134 
135  const std::string d = declarator.empty() ? declarator : (" " + declarator);
136 
137  const std::string q=
138  new_qualifiers.as_string();
139 
140  if(is_reference(src))
141  {
142  return q+convert(src.subtype())+" &"+d;
143  }
144  else if(is_rvalue_reference(src))
145  {
146  return q+convert(src.subtype())+" &&"+d;
147  }
148  else if(!src.get(ID_C_c_type).empty())
149  {
150  const irep_idt c_type=src.get(ID_C_c_type);
151 
152  if(c_type == ID_bool)
153  return q+"bool"+d;
154  else
155  return expr2ct::convert_rec(src, qualifiers, declarator);
156  }
157  else if(src.id() == ID_struct)
158  {
159  std::string dest=q;
160 
161  if(src.get_bool(ID_C_class))
162  dest+="class";
163  else if(src.get_bool(ID_C_interface))
164  dest+="__interface"; // MS-specific
165  else
166  dest+="struct";
167 
168  dest+=d;
169 
170  return dest;
171  }
172  else if(src.id() == ID_struct_tag)
173  {
174  const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(src));
175 
176  std::string dest = q;
177 
178  if(src.get_bool(ID_C_class))
179  dest += "class";
180  else if(src.get_bool(ID_C_interface))
181  dest += "__interface"; // MS-specific
182  else
183  dest += "struct";
184 
185  const irept &tag = struct_type.find(ID_tag);
186  if(!tag.id().empty())
187  {
188  if(tag.id() == ID_cpp_name)
189  dest += " " + to_cpp_name(tag).to_string();
190  else
191  dest += " " + id2string(tag.id());
192  }
193 
194  dest += d;
195 
196  return dest;
197  }
198  else if(src.id() == ID_union_tag)
199  {
200  const union_typet &union_type = ns.follow_tag(to_union_tag_type(src));
201 
202  std::string dest = q + "union";
203 
204  const irept &tag = union_type.find(ID_tag);
205  if(!tag.id().empty())
206  {
207  if(tag.id() == ID_cpp_name)
208  dest += " " + to_cpp_name(tag).to_string();
209  else
210  dest += " " + id2string(tag.id());
211  }
212 
213  dest += d;
214 
215  return dest;
216  }
217  else if(src.id()==ID_constructor)
218  {
219  return "constructor ";
220  }
221  else if(src.id()==ID_destructor)
222  {
223  return "destructor ";
224  }
225  else if(src.id()=="cpp-template-type")
226  {
227  return "typename";
228  }
229  else if(src.id()==ID_template)
230  {
231  std::string dest="template<";
232 
233  const irept::subt &arguments=src.find(ID_arguments).get_sub();
234 
235  for(auto it = arguments.begin(); it != arguments.end(); ++it)
236  {
237  if(it!=arguments.begin())
238  dest+=", ";
239 
240  const exprt &argument=(const exprt &)*it;
241 
242  if(argument.id()==ID_symbol)
243  {
244  dest+=convert(argument.type())+" ";
245  dest+=convert(argument);
246  }
247  else if(argument.id()==ID_type)
248  dest+=convert(argument.type());
249  else
250  {
251  lispexprt lisp;
252  irep2lisp(argument, lisp);
253  dest+="irep(\""+MetaString(lisp.expr2string())+"\")";
254  }
255  }
256 
257  dest+="> "+convert(src.subtype());
258  return dest;
259  }
260  else if(src.id()==ID_pointer && src.subtype().id()==ID_nullptr)
261  {
262  return "std::nullptr_t";
263  }
264  else if(src.id() == ID_pointer && src.find(ID_to_member).is_not_nil())
265  {
266  typet tmp=src;
267  typet member;
268  member.swap(tmp.add(ID_to_member));
269 
270  std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
271 
272  if(src.subtype().id()==ID_code)
273  {
274  const code_typet &code_type = to_code_type(src.subtype());
275  const typet &return_type = code_type.return_type();
276  dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest;
277 
278  const code_typet::parameterst &args = code_type.parameters();
279  dest+="(";
280 
281  for(code_typet::parameterst::const_iterator it=args.begin();
282  it!=args.end();
283  ++it)
284  {
285  if(it!=args.begin())
286  dest+=", ";
287  dest+=convert_rec(it->type(), c_qualifierst(), "");
288  }
289 
290  dest+=")";
291  dest+=d;
292  }
293  else
294  dest=convert_rec(src.subtype(), c_qualifierst(), "")+" "+dest+d;
295 
296  return dest;
297  }
298  else if(src.id()==ID_verilog_signedbv ||
299  src.id()==ID_verilog_unsignedbv)
300  return "sc_lv[" + std::to_string(to_bitvector_type(src).get_width()) + "]" +
301  d;
302  else if(src.id()==ID_unassigned)
303  return "?";
304  else if(src.id()==ID_code)
305  {
306  const code_typet &code_type=to_code_type(src);
307 
308  // C doesn't really have syntax for function types,
309  // so we use C++11 trailing return types!
310 
311  std::string dest="auto";
312 
313  // qualifiers, declarator?
314  if(d.empty())
315  dest+=' ';
316  else
317  dest+=d;
318 
319  dest+='(';
320  const code_typet::parameterst &parameters=code_type.parameters();
321 
322  for(code_typet::parameterst::const_iterator
323  it=parameters.begin();
324  it!=parameters.end();
325  it++)
326  {
327  if(it!=parameters.begin())
328  dest+=", ";
329 
330  dest+=convert(it->type());
331  }
332 
333  if(code_type.has_ellipsis())
334  {
335  if(!parameters.empty())
336  dest+=", ";
337  dest+="...";
338  }
339 
340  dest+=')';
341 
342  const typet &return_type=code_type.return_type();
343  dest+=" -> "+convert(return_type);
344 
345  return dest;
346  }
347  else if(src.id()==ID_initializer_list)
348  {
349  // only really used in error messages
350  return "{ ... }";
351  }
352  else if(src.id() == ID_c_bool)
353  {
354  return q + "bool" + d;
355  }
356  else
357  return expr2ct::convert_rec(src, qualifiers, declarator);
358 }
359 
361 {
362  return id2string(ID_this);
363 }
364 
365 std::string expr2cppt::convert_cpp_new(const exprt &src)
366 {
367  std::string dest;
368 
369  if(src.get(ID_statement)==ID_cpp_new_array)
370  {
371  dest="new";
372 
373  std::string tmp_size=
374  convert(static_cast<const exprt &>(src.find(ID_size)));
375 
376  dest+=' ';
377  dest+=convert(src.type().subtype());
378  dest+='[';
379  dest+=tmp_size;
380  dest+=']';
381  }
382  else
383  dest="new "+convert(src.type().subtype());
384 
385  return dest;
386 }
387 
388 std::string expr2cppt::convert_code_cpp_new(const exprt &src, unsigned indent)
389 {
390  return indent_str(indent) + convert_cpp_new(src) + ";\n";
391 }
392 
394  const exprt &src,
395  unsigned indent)
396 {
397  std::string dest=indent_str(indent)+"delete ";
398 
399  if(src.operands().size()!=1)
400  {
401  unsigned precedence;
402  return convert_norep(src, precedence);
403  }
404 
405  std::string tmp = convert(to_unary_expr(src).op());
406 
407  dest+=tmp+";\n";
408 
409  return dest;
410 }
411 
413  const exprt &src,
414  unsigned &precedence)
415 {
416  if(src.id()=="cpp-this")
417  {
418  precedence = 15;
419  return convert_cpp_this();
420  }
421  if(src.id()==ID_extractbit)
422  {
423  precedence = 15;
424  return convert_extractbit(src);
425  }
426  else if(src.id()==ID_extractbits)
427  {
428  precedence = 15;
429  return convert_extractbits(src);
430  }
431  else if(src.id()==ID_side_effect &&
432  (src.get(ID_statement)==ID_cpp_new ||
433  src.get(ID_statement)==ID_cpp_new_array))
434  {
435  precedence = 15;
436  return convert_cpp_new(src);
437  }
438  else if(src.id()==ID_side_effect &&
439  src.get(ID_statement)==ID_throw)
440  {
441  precedence = 16;
442  return convert_function(src, "throw");
443  }
444  else if(src.is_constant() && src.type().id()==ID_verilog_signedbv)
445  return "'"+id2string(src.get(ID_value))+"'";
446  else if(src.is_constant() && src.type().id()==ID_verilog_unsignedbv)
447  return "'"+id2string(src.get(ID_value))+"'";
448  else if(src.is_constant() && to_constant_expr(src).get_value()==ID_nullptr)
449  return "nullptr";
450  else if(src.id()==ID_unassigned)
451  return "?";
452  else if(src.id() == ID_pod_constructor)
453  return "pod_constructor";
454  else
455  return expr2ct::convert_with_precedence(src, precedence);
456 }
457 
459  const codet &src,
460  unsigned indent)
461 {
462  const irep_idt &statement=src.get(ID_statement);
463 
464  if(statement==ID_cpp_delete ||
465  statement==ID_cpp_delete_array)
466  return convert_code_cpp_delete(src, indent);
467 
468  if(statement==ID_cpp_new ||
469  statement==ID_cpp_new_array)
470  return convert_code_cpp_new(src, indent);
471 
472  return expr2ct::convert_code(src, indent);
473 }
474 
475 std::string expr2cppt::convert_extractbit(const exprt &src)
476 {
477  const auto &extractbit_expr = to_extractbit_expr(src);
478  return convert(extractbit_expr.op0()) + "[" + convert(extractbit_expr.op1()) +
479  "]";
480 }
481 
482 std::string expr2cppt::convert_extractbits(const exprt &src)
483 {
484  const auto &extractbits_expr = to_extractbits_expr(src);
485  return convert(extractbits_expr.src()) + ".range(" +
486  convert(extractbits_expr.upper()) + "," +
487  convert(extractbits_expr.lower()) + ")";
488 }
489 
490 std::string expr2cpp(const exprt &expr, const namespacet &ns)
491 {
492  expr2cppt expr2cpp(ns);
493  expr2cpp.get_shorthands(expr);
494  return expr2cpp.convert(expr);
495 }
496 
497 std::string type2cpp(const typet &type, const namespacet &ns)
498 {
499  expr2cppt expr2cpp(ns);
500  return expr2cpp.convert(type);
501 }
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:95
ANSI-C Misc Utilities.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
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
bool has_ellipsis() const
Definition: std_types.h:611
const parameterst & parameters() const
Definition: std_types.h:655
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
A constant literal expression.
Definition: std_expr.h:2753
std::string to_string() const
Definition: cpp_name.cpp:75
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
std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:412
std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:49
std::string convert_code_cpp_new(const exprt &src, unsigned indent)
Definition: expr2cpp.cpp:388
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:110
expr2cppt(const namespacet &_ns)
Definition: expr2cpp.cpp:27
std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2cpp.cpp:458
std::string convert_extractbits(const exprt &src)
Definition: expr2cpp.cpp:482
std::string convert_extractbit(const exprt &src)
Definition: expr2cpp.cpp:475
std::string convert_cpp_new(const exprt &src)
Definition: expr2cpp.cpp:365
std::string convert_cpp_this()
Definition: expr2cpp.cpp:360
std::string convert_code_cpp_delete(const exprt &src, unsigned indent)
Definition: expr2cpp.cpp:393
std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2cpp.cpp:126
optionalt< std::string > convert_function(const exprt &src)
Returns a string if src is a function with a known conversion, else returns nullopt.
std::string convert_code(const codet &src)
std::string convert_norep(const exprt &src, unsigned &precedence)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:219
static std::string indent_str(unsigned indent)
const namespacet & ns
Definition: expr2c_class.h:48
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:214
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
operandst & operands()
Definition: expr.h:92
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
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
std::string expr2string() const
Definition: lispexpr.cpp:15
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
virtual std::unique_ptr< qualifierst > clone() const =0
virtual std::string as_string() const =0
virtual void read(const typet &src)=0
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
The union type.
Definition: c_types.h:112
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:497
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:490
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
void irep2lisp(const irept &src, lispexprt &dest)
Definition: lispirep.cpp:43
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:129
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:136
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.