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_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 c_qualifierst &qualifiers,
46  const std::string &declarator) override;
47 };
48 
50  const exprt &src,
51  unsigned &precedence)
52 {
53  if(src.type().id() != ID_struct && src.type().id() != ID_struct_tag)
54  return convert_norep(src, precedence);
55 
56  const struct_typet &struct_type =
57  src.type().id() == ID_struct_tag
59  : to_struct_type(src.type());
60 
61  std::string dest="{ ";
62 
63  const struct_typet::componentst &components=
64  struct_type.components();
65 
67  components.size() == src.operands().size(), "component count mismatch");
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  if(!c.get_pretty_name().empty())
100  dest += id2string(c.get_pretty_name());
101  else
102  dest += id2string(c.get_name());
103  dest+='=';
104  dest+=tmp;
105  }
106 
107  o_it++;
108  }
109 
110  dest+=" }";
111 
112  return dest;
113 }
114 
116  const constant_exprt &src,
117  unsigned &precedence)
118 {
119  if(src.type().id() == ID_c_bool)
120  {
121  // C++ has built-in Boolean constants, in contrast to C
122  if(src.is_true())
123  return "true";
124  else if(src.is_false())
125  return "false";
126  }
127 
128  return expr2ct::convert_constant(src, precedence);
129 }
130 
132  const typet &src,
133  const c_qualifierst &qualifiers,
134  const std::string &declarator)
135 {
136  std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
137  c_qualifierst &new_qualifiers = *clone;
138  new_qualifiers.read(src);
139 
140  const std::string d = declarator.empty() ? declarator : (" " + declarator);
141 
142  const std::string q=
143  new_qualifiers.as_string();
144 
145  if(is_reference(src))
146  {
147  return q + convert(to_reference_type(src).base_type()) + " &" + d;
148  }
149  else if(is_rvalue_reference(src))
150  {
151  return q + convert(to_pointer_type(src).base_type()) + " &&" + d;
152  }
153  else if(!src.get(ID_C_c_type).empty())
154  {
155  const irep_idt c_type=src.get(ID_C_c_type);
156 
157  if(c_type == ID_bool)
158  return q+"bool"+d;
159  else
160  return expr2ct::convert_rec(src, qualifiers, declarator);
161  }
162  else if(src.id() == ID_struct)
163  {
164  std::string dest=q;
165 
166  if(src.get_bool(ID_C_class))
167  dest+="class";
168  else if(src.get_bool(ID_C_interface))
169  dest+="__interface"; // MS-specific
170  else
171  dest+="struct";
172 
173  dest+=d;
174 
175  return dest;
176  }
177  else if(src.id() == ID_struct_tag)
178  {
179  const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(src));
180 
181  std::string dest = q;
182 
183  if(src.get_bool(ID_C_class))
184  dest += "class";
185  else if(src.get_bool(ID_C_interface))
186  dest += "__interface"; // MS-specific
187  else
188  dest += "struct";
189 
190  const irept &tag = struct_type.find(ID_tag);
191  if(!tag.id().empty())
192  {
193  if(tag.id() == ID_cpp_name)
194  dest += " " + to_cpp_name(tag).to_string();
195  else
196  dest += " " + id2string(tag.id());
197  }
198 
199  dest += d;
200 
201  return dest;
202  }
203  else if(src.id() == ID_union_tag)
204  {
205  const union_typet &union_type = ns.follow_tag(to_union_tag_type(src));
206 
207  std::string dest = q + "union";
208 
209  const irept &tag = union_type.find(ID_tag);
210  if(!tag.id().empty())
211  {
212  if(tag.id() == ID_cpp_name)
213  dest += " " + to_cpp_name(tag).to_string();
214  else
215  dest += " " + id2string(tag.id());
216  }
217 
218  dest += d;
219 
220  return dest;
221  }
222  else if(src.id()==ID_constructor)
223  {
224  return "constructor ";
225  }
226  else if(src.id()==ID_destructor)
227  {
228  return "destructor ";
229  }
230  else if(src.id()=="cpp-template-type")
231  {
232  return "typename";
233  }
234  else if(src.id()==ID_template)
235  {
236  std::string dest="template<";
237 
238  const irept::subt &arguments=src.find(ID_arguments).get_sub();
239 
240  for(auto it = arguments.begin(); it != arguments.end(); ++it)
241  {
242  if(it!=arguments.begin())
243  dest+=", ";
244 
245  const exprt &argument=(const exprt &)*it;
246 
247  if(argument.id()==ID_symbol)
248  {
249  dest+=convert(argument.type())+" ";
250  dest+=convert(argument);
251  }
252  else if(argument.id()==ID_type)
253  dest+=convert(argument.type());
254  else
255  {
256  lispexprt lisp;
257  irep2lisp(argument, lisp);
258  dest+="irep(\""+MetaString(lisp.expr2string())+"\")";
259  }
260  }
261 
262  dest += "> " + convert(to_template_type(src).subtype());
263  return dest;
264  }
265  else if(
266  src.id() == ID_pointer &&
267  to_pointer_type(src).base_type().id() == ID_nullptr)
268  {
269  return "std::nullptr_t";
270  }
271  else if(src.id() == ID_pointer && src.find(ID_to_member).is_not_nil())
272  {
273  typet tmp=src;
274  typet member;
275  member.swap(tmp.add(ID_to_member));
276 
277  std::string dest = "(" + convert(member) + ":: *)";
278 
279  const auto &base_type = to_pointer_type(src).base_type();
280 
281  if(base_type.id() == ID_code)
282  {
283  const code_typet &code_type = to_code_type(base_type);
284  const typet &return_type = code_type.return_type();
285  dest = convert(return_type) + " " + dest;
286 
287  const code_typet::parameterst &args = code_type.parameters();
288  dest+="(";
289 
290  for(code_typet::parameterst::const_iterator it=args.begin();
291  it!=args.end();
292  ++it)
293  {
294  if(it!=args.begin())
295  dest+=", ";
296  dest += convert(it->type());
297  }
298 
299  dest+=")";
300  dest+=d;
301  }
302  else
303  dest = convert(base_type) + " " + dest + d;
304 
305  return dest;
306  }
307  else if(src.id()==ID_verilog_signedbv ||
308  src.id()==ID_verilog_unsignedbv)
309  return "sc_lv[" + std::to_string(to_bitvector_type(src).get_width()) + "]" +
310  d;
311  else if(src.id()==ID_unassigned)
312  return "?";
313  else if(src.id()==ID_code)
314  {
315  const code_typet &code_type=to_code_type(src);
316 
317  // C doesn't really have syntax for function types,
318  // so we use C++11 trailing return types!
319 
320  std::string dest="auto";
321 
322  // qualifiers, declarator?
323  if(d.empty())
324  dest+=' ';
325  else
326  dest+=d;
327 
328  dest+='(';
329  const code_typet::parameterst &parameters=code_type.parameters();
330 
331  for(code_typet::parameterst::const_iterator
332  it=parameters.begin();
333  it!=parameters.end();
334  it++)
335  {
336  if(it!=parameters.begin())
337  dest+=", ";
338 
339  dest+=convert(it->type());
340  }
341 
342  if(code_type.has_ellipsis())
343  {
344  if(!parameters.empty())
345  dest+=", ";
346  dest+="...";
347  }
348 
349  dest+=')';
350 
351  const typet &return_type=code_type.return_type();
352  dest+=" -> "+convert(return_type);
353 
354  return dest;
355  }
356  else if(src.id()==ID_initializer_list)
357  {
358  // only really used in error messages
359  return "{ ... }";
360  }
361  else if(src.id() == ID_c_bool)
362  {
363  return q + "bool" + d;
364  }
365  else
366  return expr2ct::convert_rec(src, qualifiers, declarator);
367 }
368 
370 {
371  return id2string(ID_this);
372 }
373 
374 std::string expr2cppt::convert_cpp_new(const exprt &src)
375 {
376  std::string dest;
377 
378  if(src.get(ID_statement)==ID_cpp_new_array)
379  {
380  dest="new";
381 
382  std::string tmp_size=
383  convert(static_cast<const exprt &>(src.find(ID_size)));
384 
385  dest+=' ';
386  dest += convert(to_pointer_type(src.type()).base_type());
387  dest+='[';
388  dest+=tmp_size;
389  dest+=']';
390  }
391  else
392  dest = "new " + convert(to_pointer_type(src.type()).base_type());
393 
394  return dest;
395 }
396 
397 std::string expr2cppt::convert_code_cpp_new(const exprt &src, unsigned indent)
398 {
399  return indent_str(indent) + convert_cpp_new(src) + ";\n";
400 }
401 
403  const exprt &src,
404  unsigned indent)
405 {
406  std::string dest=indent_str(indent)+"delete ";
407 
408  if(src.operands().size()!=1)
409  {
410  unsigned precedence;
411  return convert_norep(src, precedence);
412  }
413 
414  std::string tmp = convert(to_unary_expr(src).op());
415 
416  dest+=tmp+";\n";
417 
418  return dest;
419 }
420 
422  const exprt &src,
423  unsigned &precedence)
424 {
425  if(src.id()=="cpp-this")
426  {
427  precedence = 15;
428  return convert_cpp_this();
429  }
430  if(src.id()==ID_extractbit)
431  {
432  precedence = 15;
433  return convert_extractbit(src);
434  }
435  else if(src.id()==ID_side_effect &&
436  (src.get(ID_statement)==ID_cpp_new ||
437  src.get(ID_statement)==ID_cpp_new_array))
438  {
439  precedence = 15;
440  return convert_cpp_new(src);
441  }
442  else if(src.id()==ID_side_effect &&
443  src.get(ID_statement)==ID_throw)
444  {
445  precedence = 16;
446  return convert_function(src, "throw");
447  }
448  else if(src.is_constant() && src.type().id()==ID_verilog_signedbv)
449  return "'"+id2string(src.get(ID_value))+"'";
450  else if(src.is_constant() && src.type().id()==ID_verilog_unsignedbv)
451  return "'"+id2string(src.get(ID_value))+"'";
452  else if(src.is_constant() && to_constant_expr(src).get_value()==ID_nullptr)
453  return "nullptr";
454  else if(src.id()==ID_unassigned)
455  return "?";
456  else if(src.id() == ID_pod_constructor)
457  return "pod_constructor";
458  else
459  return expr2ct::convert_with_precedence(src, precedence);
460 }
461 
463  const codet &src,
464  unsigned indent)
465 {
466  const irep_idt &statement=src.get(ID_statement);
467 
468  if(statement==ID_cpp_delete ||
469  statement==ID_cpp_delete_array)
470  return convert_code_cpp_delete(src, indent);
471 
472  if(statement==ID_cpp_new ||
473  statement==ID_cpp_new_array)
474  return convert_code_cpp_new(src, indent);
475 
476  return expr2ct::convert_code(src, indent);
477 }
478 
479 std::string expr2cppt::convert_extractbit(const exprt &src)
480 {
481  const auto &extractbit_expr = to_extractbit_expr(src);
482  return convert(extractbit_expr.op0()) + "[" + convert(extractbit_expr.op1()) +
483  "]";
484 }
485 
486 std::string expr2cpp(const exprt &expr, const namespacet &ns)
487 {
488  expr2cppt expr2cpp(ns);
489  expr2cpp.get_shorthands(expr);
490  return expr2cpp.convert(expr);
491 }
492 
493 std::string type2cpp(const typet &type, const namespacet &ns)
494 {
495  expr2cppt expr2cpp(ns);
496  return expr2cpp.convert(type);
497 }
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_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:224
virtual void read(const typet &src)
virtual std::unique_ptr< c_qualifierst > clone() const
virtual std::string as_string() const
Base type of functions.
Definition: std_types.h:583
std::vector< parametert > parameterst
Definition: std_types.h:585
const typet & return_type() const
Definition: std_types.h:689
bool has_ellipsis() const
Definition: std_types.h:655
const parameterst & parameters() const
Definition: std_types.h:699
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
A constant literal expression.
Definition: std_expr.h:3000
std::string to_string() const
Definition: cpp_name.cpp:73
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:421
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:397
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:115
expr2cppt(const namespacet &_ns)
Definition: expr2cpp.cpp:28
std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2cpp.cpp:462
std::string convert_extractbit(const exprt &src)
Definition: expr2cpp.cpp:479
std::string convert_cpp_new(const exprt &src)
Definition: expr2cpp.cpp:374
std::string convert_cpp_this()
Definition: expr2cpp.cpp:369
std::string convert_code_cpp_delete(const exprt &src, unsigned indent)
Definition: expr2cpp.cpp:402
std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2cpp.cpp:131
std::optional< 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:4080
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:218
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2547
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3433
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1615
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1771
const namespacet & ns
Definition: expr2c_class.h:55
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3645
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:213
Base class for all expressions.
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:448
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
irept & add(const irep_idt &name)
Definition: irep.cpp:103
std::string expr2string() const
Definition: lispexpr.cpp:15
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:94
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
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:29
The union type.
Definition: c_types.h:147
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148
template_typet & to_template_type(typet &type)
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:493
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:486
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:145
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:152
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:162
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3055
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
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:788
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.