CBMC
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 #include "cpp_template_type.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(to_reference_type(src).base_type()) + " &" + d;
144  }
145  else if(is_rvalue_reference(src))
146  {
147  return q + convert(to_pointer_type(src).base_type()) + " &&" + 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(to_template_type(src).subtype());
259  return dest;
260  }
261  else if(
262  src.id() == ID_pointer &&
263  to_pointer_type(src).base_type().id() == ID_nullptr)
264  {
265  return "std::nullptr_t";
266  }
267  else if(src.id() == ID_pointer && src.find(ID_to_member).is_not_nil())
268  {
269  typet tmp=src;
270  typet member;
271  member.swap(tmp.add(ID_to_member));
272 
273  std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
274 
275  const auto &base_type = to_pointer_type(src).base_type();
276 
277  if(base_type.id() == ID_code)
278  {
279  const code_typet &code_type = to_code_type(base_type);
280  const typet &return_type = code_type.return_type();
281  dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest;
282 
283  const code_typet::parameterst &args = code_type.parameters();
284  dest+="(";
285 
286  for(code_typet::parameterst::const_iterator it=args.begin();
287  it!=args.end();
288  ++it)
289  {
290  if(it!=args.begin())
291  dest+=", ";
292  dest+=convert_rec(it->type(), c_qualifierst(), "");
293  }
294 
295  dest+=")";
296  dest+=d;
297  }
298  else
299  dest = convert_rec(base_type, c_qualifierst(), "") + " " + dest + d;
300 
301  return dest;
302  }
303  else if(src.id()==ID_verilog_signedbv ||
304  src.id()==ID_verilog_unsignedbv)
305  return "sc_lv[" + std::to_string(to_bitvector_type(src).get_width()) + "]" +
306  d;
307  else if(src.id()==ID_unassigned)
308  return "?";
309  else if(src.id()==ID_code)
310  {
311  const code_typet &code_type=to_code_type(src);
312 
313  // C doesn't really have syntax for function types,
314  // so we use C++11 trailing return types!
315 
316  std::string dest="auto";
317 
318  // qualifiers, declarator?
319  if(d.empty())
320  dest+=' ';
321  else
322  dest+=d;
323 
324  dest+='(';
325  const code_typet::parameterst &parameters=code_type.parameters();
326 
327  for(code_typet::parameterst::const_iterator
328  it=parameters.begin();
329  it!=parameters.end();
330  it++)
331  {
332  if(it!=parameters.begin())
333  dest+=", ";
334 
335  dest+=convert(it->type());
336  }
337 
338  if(code_type.has_ellipsis())
339  {
340  if(!parameters.empty())
341  dest+=", ";
342  dest+="...";
343  }
344 
345  dest+=')';
346 
347  const typet &return_type=code_type.return_type();
348  dest+=" -> "+convert(return_type);
349 
350  return dest;
351  }
352  else if(src.id()==ID_initializer_list)
353  {
354  // only really used in error messages
355  return "{ ... }";
356  }
357  else if(src.id() == ID_c_bool)
358  {
359  return q + "bool" + d;
360  }
361  else
362  return expr2ct::convert_rec(src, qualifiers, declarator);
363 }
364 
366 {
367  return id2string(ID_this);
368 }
369 
370 std::string expr2cppt::convert_cpp_new(const exprt &src)
371 {
372  std::string dest;
373 
374  if(src.get(ID_statement)==ID_cpp_new_array)
375  {
376  dest="new";
377 
378  std::string tmp_size=
379  convert(static_cast<const exprt &>(src.find(ID_size)));
380 
381  dest+=' ';
382  dest += convert(to_pointer_type(src.type()).base_type());
383  dest+='[';
384  dest+=tmp_size;
385  dest+=']';
386  }
387  else
388  dest = "new " + convert(to_pointer_type(src.type()).base_type());
389 
390  return dest;
391 }
392 
393 std::string expr2cppt::convert_code_cpp_new(const exprt &src, unsigned indent)
394 {
395  return indent_str(indent) + convert_cpp_new(src) + ";\n";
396 }
397 
399  const exprt &src,
400  unsigned indent)
401 {
402  std::string dest=indent_str(indent)+"delete ";
403 
404  if(src.operands().size()!=1)
405  {
406  unsigned precedence;
407  return convert_norep(src, precedence);
408  }
409 
410  std::string tmp = convert(to_unary_expr(src).op());
411 
412  dest+=tmp+";\n";
413 
414  return dest;
415 }
416 
418  const exprt &src,
419  unsigned &precedence)
420 {
421  if(src.id()=="cpp-this")
422  {
423  precedence = 15;
424  return convert_cpp_this();
425  }
426  if(src.id()==ID_extractbit)
427  {
428  precedence = 15;
429  return convert_extractbit(src);
430  }
431  else if(src.id()==ID_extractbits)
432  {
433  precedence = 15;
434  return convert_extractbits(src);
435  }
436  else if(src.id()==ID_side_effect &&
437  (src.get(ID_statement)==ID_cpp_new ||
438  src.get(ID_statement)==ID_cpp_new_array))
439  {
440  precedence = 15;
441  return convert_cpp_new(src);
442  }
443  else if(src.id()==ID_side_effect &&
444  src.get(ID_statement)==ID_throw)
445  {
446  precedence = 16;
447  return convert_function(src, "throw");
448  }
449  else if(src.is_constant() && src.type().id()==ID_verilog_signedbv)
450  return "'"+id2string(src.get(ID_value))+"'";
451  else if(src.is_constant() && src.type().id()==ID_verilog_unsignedbv)
452  return "'"+id2string(src.get(ID_value))+"'";
453  else if(src.is_constant() && to_constant_expr(src).get_value()==ID_nullptr)
454  return "nullptr";
455  else if(src.id()==ID_unassigned)
456  return "?";
457  else if(src.id() == ID_pod_constructor)
458  return "pod_constructor";
459  else
460  return expr2ct::convert_with_precedence(src, precedence);
461 }
462 
464  const codet &src,
465  unsigned indent)
466 {
467  const irep_idt &statement=src.get(ID_statement);
468 
469  if(statement==ID_cpp_delete ||
470  statement==ID_cpp_delete_array)
471  return convert_code_cpp_delete(src, indent);
472 
473  if(statement==ID_cpp_new ||
474  statement==ID_cpp_new_array)
475  return convert_code_cpp_new(src, indent);
476 
477  return expr2ct::convert_code(src, indent);
478 }
479 
480 std::string expr2cppt::convert_extractbit(const exprt &src)
481 {
482  const auto &extractbit_expr = to_extractbit_expr(src);
483  return convert(extractbit_expr.op0()) + "[" + convert(extractbit_expr.op1()) +
484  "]";
485 }
486 
487 std::string expr2cppt::convert_extractbits(const exprt &src)
488 {
489  const auto &extractbits_expr = to_extractbits_expr(src);
490  return convert(extractbits_expr.src()) + ".range(" +
491  convert(extractbits_expr.upper()) + "," +
492  convert(extractbits_expr.lower()) + ")";
493 }
494 
495 std::string expr2cpp(const exprt &expr, const namespacet &ns)
496 {
497  expr2cppt expr2cpp(ns);
498  expr2cpp.get_shorthands(expr);
499  return expr2cpp.convert(expr);
500 }
501 
502 std::string type2cpp(const typet &type, const namespacet &ns)
503 {
504  expr2cppt expr2cpp(ns);
505  return expr2cpp.convert(type);
506 }
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:202
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:147
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:36
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:611
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: bitvector_expr.h:429
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:361
expr2cppt::convert_extractbit
std::string convert_extractbit(const exprt &src)
Definition: expr2cpp.cpp:480
expr2cppt::convert_code_cpp_new
std::string convert_code_cpp_new(const exprt &src, unsigned indent)
Definition: expr2cpp.cpp:393
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:541
irept::find
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
expr2ct::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1769
exprt
Base class for all expressions.
Definition: expr.h:55
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
expr2cpp.h
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:58
expr2ct::convert_code
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3425
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:34
c_qualifiers.h
expr2cpp
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:495
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:150
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:43
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
lispexpr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:380
expr2ct
Definition: expr2c_class.h:30
expr2cppt::convert_code_cpp_delete
std::string convert_code_cpp_delete(const exprt &src, unsigned indent)
Definition: expr2cpp.cpp:398
expr2ct::convert
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:214
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
lispexprt::expr2string
std::string expr2string() const
Definition: lispexpr.cpp:15
expr2cppt
Definition: expr2cpp.cpp:25
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:47
expr2ct::indent_str
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2539
type2cpp
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:502
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:417
expr2cppt::convert_constant
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:111
pointer_expr.h
c_misc.h
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
c_qualifierst
Definition: c_qualifiers.h:61
to_reference_type
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:148
irept::swap
void swap(irept &irep)
Definition: irep.h:442
code_typet
Base type of functions.
Definition: std_types.h:538
expr2c_class.h
irept::id
const irep_idt & id() const
Definition: irep.h:396
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:474
dstringt::empty
bool empty() const
Definition: dstring.h:88
union_typet
The union type.
Definition: c_types.h:124
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
expr2cppt::convert_cpp_new
std::string convert_cpp_new(const exprt &src)
Definition: expr2cpp.cpp:370
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::subt
typename dt::subt subt
Definition: irep.h:160
expr2ct::convert_norep
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1613
lispexprt
Definition: lispexpr.h:73
expr2ct::ns
const namespacet & ns
Definition: expr2c_class.h:51
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:143
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:230
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:27
pointer_typet::base_type
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
irept::get_sub
subt & get_sub()
Definition: irep.h:456
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: bitvector_expr.h:517
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:645
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
exprt::operands
operandst & operands()
Definition: expr.h:94
expr2ct::convert_rec
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:219
qualifierst::as_string
virtual std::string as_string() const =0
expr2cppt::convert_extractbits
std::string convert_extractbits(const exprt &src)
Definition: expr2cpp.cpp:487
to_template_type
template_typet & to_template_type(typet &type)
Definition: cpp_template_type.h:40
constant_exprt
A constant literal expression.
Definition: std_expr.h:2941
expr2ct::convert_with_precedence
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3552
std_expr.h
expr2cppt::convert_rec
std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2cpp.cpp:127
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.
Definition: expr2c.cpp:3969
c_types.h
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
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:463
expr2cppt::convert_cpp_this
std::string convert_cpp_this()
Definition: expr2cpp.cpp:365
cpp_template_type.h
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:28
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2992
cpp_name.h