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