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