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