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 class expr2cppt:public expr2ct
25 {
26 public:
27  explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
28 
29 protected:
30  std::string convert_with_precedence(
31  const exprt &src, unsigned &precedence) override;
32  std::string convert_cpp_this(const exprt &src, unsigned precedence);
33  std::string convert_cpp_new(const exprt &src, unsigned precedence);
34  std::string convert_extractbit(const exprt &src, unsigned precedence);
35  std::string convert_extractbits(const exprt &src, unsigned precedence);
36  std::string convert_code_cpp_delete(const exprt &src, unsigned precedence);
37  std::string convert_struct(const exprt &src, unsigned &precedence) override;
38  std::string convert_code(const codet &src, unsigned indent) override;
39  // NOLINTNEXTLINE(whitespace/line_length)
40  std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
41 
42  std::string convert_rec(
43  const typet &src,
44  const qualifierst &qualifiers,
45  const std::string &declarator) override;
46 };
47 
49  const exprt &src,
50  unsigned &precedence)
51 {
52  const typet &full_type=ns.follow(src.type());
53 
54  if(full_type.id()!=ID_struct)
55  return convert_norep(src, precedence);
56 
57  const struct_typet &struct_type=to_struct_type(full_type);
58 
59  std::string dest="{ ";
60 
61  const struct_typet::componentst &components=
62  struct_type.components();
63 
64  assert(components.size()==src.operands().size());
65 
66  exprt::operandst::const_iterator o_it=src.operands().begin();
67 
68  bool first=true;
69  size_t last_size=0;
70 
71  for(const auto &c : components)
72  {
73  if(c.type().id() == ID_code)
74  {
75  }
76  else
77  {
78  std::string tmp=convert(*o_it);
79  std::string sep;
80 
81  if(first)
82  first=false;
83  else
84  {
85  if(last_size+40<dest.size())
86  {
87  sep=",\n ";
88  last_size=dest.size();
89  }
90  else
91  sep=", ";
92  }
93 
94  dest+=sep;
95  dest+='.';
96  dest += c.get_string(ID_pretty_name);
97  dest+='=';
98  dest+=tmp;
99  }
100 
101  o_it++;
102  }
103 
104  dest+=" }";
105 
106  return dest;
107 }
108 
110  const constant_exprt &src,
111  unsigned &precedence)
112 {
113  if(src.type().id() == ID_c_bool)
114  {
115  // C++ has built-in Boolean constants, in contrast to C
116  if(src.is_true())
117  return "true";
118  else if(src.is_false())
119  return "false";
120  }
121 
122  return expr2ct::convert_constant(src, precedence);
123 }
124 
126  const typet &src,
127  const qualifierst &qualifiers,
128  const std::string &declarator)
129 {
130  std::unique_ptr<qualifierst> clone = qualifiers.clone();
131  qualifierst &new_qualifiers = *clone;
132  new_qualifiers.read(src);
133 
134  const std::string d=
135  declarator==""?declarator:(" "+declarator);
136 
137  const std::string q=
138  new_qualifiers.as_string();
139 
140  if(is_reference(src))
141  {
142  return q+convert(src.subtype())+" &"+d;
143  }
144  else if(is_rvalue_reference(src))
145  {
146  return q+convert(src.subtype())+" &&"+d;
147  }
148  else if(!src.get(ID_C_c_type).empty())
149  {
150  const irep_idt c_type=src.get(ID_C_c_type);
151 
152  if(c_type == ID_bool)
153  return q+"bool"+d;
154  else
155  return expr2ct::convert_rec(src, qualifiers, declarator);
156  }
157  else if(src.id() == ID_symbol_type)
158  {
159  const irep_idt &identifier=
161 
162  const symbolt &symbol=ns.lookup(identifier);
163 
164  if(symbol.type.id()==ID_struct ||
165  symbol.type.id()==ID_incomplete_struct)
166  {
167  std::string dest=q;
168 
169  if(symbol.type.get_bool(ID_C_class))
170  dest+="class";
171  else if(symbol.type.get_bool(ID_C_interface))
172  dest+="__interface"; // MS-specific
173  else
174  dest+="struct";
175 
176  if(!symbol.pretty_name.empty())
177  dest+=" "+id2string(symbol.pretty_name);
178 
179  dest+=d;
180 
181  return dest;
182  }
183  else if(symbol.type.id()==ID_c_enum)
184  {
185  std::string dest=q;
186 
187  dest+="enum";
188 
189  if(!symbol.pretty_name.empty())
190  dest+=" "+id2string(symbol.pretty_name);
191 
192  dest+=d;
193 
194  return dest;
195  }
196  else
197  return expr2ct::convert_rec(src, qualifiers, declarator);
198  }
199  else if(src.id()==ID_struct ||
200  src.id()==ID_incomplete_struct)
201  {
202  std::string dest=q;
203 
204  if(src.get_bool(ID_C_class))
205  dest+="class";
206  else if(src.get_bool(ID_C_interface))
207  dest+="__interface"; // MS-specific
208  else
209  dest+="struct";
210 
211  dest+=d;
212 
213  return dest;
214  }
215  else if(src.id()==ID_constructor)
216  {
217  return "constructor ";
218  }
219  else if(src.id()==ID_destructor)
220  {
221  return "destructor ";
222  }
223  else if(src.id()=="cpp-template-type")
224  {
225  return "typename";
226  }
227  else if(src.id()==ID_template)
228  {
229  std::string dest="template<";
230 
231  const irept::subt &arguments=src.find(ID_arguments).get_sub();
232 
233  forall_irep(it, arguments)
234  {
235  if(it!=arguments.begin())
236  dest+=", ";
237 
238  const exprt &argument=(const exprt &)*it;
239 
240  if(argument.id()==ID_symbol)
241  {
242  dest+=convert(argument.type())+" ";
243  dest+=convert(argument);
244  }
245  else if(argument.id()==ID_type)
246  dest+=convert(argument.type());
247  else
248  {
249  lispexprt lisp;
250  irep2lisp(argument, lisp);
251  dest+="irep(\""+MetaString(lisp.expr2string())+"\")";
252  }
253  }
254 
255  dest+="> "+convert(src.subtype());
256  return dest;
257  }
258  else if(src.id()==ID_pointer && src.subtype().id()==ID_nullptr)
259  {
260  return "std::nullptr_t";
261  }
262  else if(src.id()==ID_pointer &&
263  src.find("to-member").is_not_nil())
264  {
265  typet tmp=src;
266  typet member;
267  member.swap(tmp.add("to-member"));
268 
269  std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
270 
271  if(src.subtype().id()==ID_code)
272  {
273  const code_typet &code_type = to_code_type(src.subtype());
274  const typet &return_type = code_type.return_type();
275  dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest;
276 
277  const code_typet::parameterst &args = code_type.parameters();
278  dest+="(";
279 
280  for(code_typet::parameterst::const_iterator it=args.begin();
281  it!=args.end();
282  ++it)
283  {
284  if(it!=args.begin())
285  dest+=", ";
286  dest+=convert_rec(it->type(), c_qualifierst(), "");
287  }
288 
289  dest+=")";
290  dest+=d;
291  }
292  else
293  dest=convert_rec(src.subtype(), c_qualifierst(), "")+" "+dest+d;
294 
295  return dest;
296  }
297  else if(src.id()==ID_verilog_signedbv ||
298  src.id()==ID_verilog_unsignedbv)
299  return "sc_lv["+id2string(src.get(ID_width))+"]"+d;
300  else if(src.id()==ID_unassigned)
301  return "?";
302  else if(src.id()==ID_code)
303  {
304  const code_typet &code_type=to_code_type(src);
305 
306  // C doesn't really have syntax for function types,
307  // so we use C++11 trailing return types!
308 
309  std::string dest="auto";
310 
311  // qualifiers, declarator?
312  if(d.empty())
313  dest+=' ';
314  else
315  dest+=d;
316 
317  dest+='(';
318  const code_typet::parameterst &parameters=code_type.parameters();
319 
320  for(code_typet::parameterst::const_iterator
321  it=parameters.begin();
322  it!=parameters.end();
323  it++)
324  {
325  if(it!=parameters.begin())
326  dest+=", ";
327 
328  dest+=convert(it->type());
329  }
330 
331  if(code_type.has_ellipsis())
332  {
333  if(!parameters.empty())
334  dest+=", ";
335  dest+="...";
336  }
337 
338  dest+=')';
339 
340  const typet &return_type=code_type.return_type();
341  dest+=" -> "+convert(return_type);
342 
343  return dest;
344  }
345  else if(src.id()==ID_initializer_list)
346  {
347  // only really used in error messages
348  return "{ ... }";
349  }
350  else if(src.id() == ID_c_bool)
351  {
352  return q + "bool" + d;
353  }
354  else
355  return expr2ct::convert_rec(src, qualifiers, declarator);
356 }
357 
359  const exprt &src,
360  unsigned precedence)
361 {
362  return "this";
363 }
364 
366  const exprt &src,
367  unsigned precedence)
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 
391  const exprt &src,
392  unsigned indent)
393 {
394  std::string dest=indent_str(indent)+"delete ";
395 
396  if(src.operands().size()!=1)
397  {
398  unsigned precedence;
399  return convert_norep(src, precedence);
400  }
401 
402  std::string tmp=convert(src.op0());
403 
404  dest+=tmp+";\n";
405 
406  return dest;
407 }
408 
410  const exprt &src,
411  unsigned &precedence)
412 {
413  if(src.id()=="cpp-this")
414  return convert_cpp_this(src, precedence=15);
415  if(src.id()==ID_extractbit)
416  return convert_extractbit(src, precedence=15);
417  else if(src.id()==ID_extractbits)
418  return convert_extractbits(src, precedence=15);
419  else if(src.id()==ID_side_effect &&
420  (src.get(ID_statement)==ID_cpp_new ||
421  src.get(ID_statement)==ID_cpp_new_array))
422  return convert_cpp_new(src, precedence=15);
423  else if(src.id()==ID_side_effect &&
424  src.get(ID_statement)==ID_throw)
425  return convert_function(src, "throw", precedence=16);
426  else if(src.is_constant() && src.type().id()==ID_verilog_signedbv)
427  return "'"+id2string(src.get(ID_value))+"'";
428  else if(src.is_constant() && src.type().id()==ID_verilog_unsignedbv)
429  return "'"+id2string(src.get(ID_value))+"'";
430  else if(src.is_constant() && to_constant_expr(src).get_value()==ID_nullptr)
431  return "nullptr";
432  else if(src.id()==ID_unassigned)
433  return "?";
434  else if(src.id() == ID_pod_constructor)
435  return "pod_constructor";
436  else
437  return expr2ct::convert_with_precedence(src, precedence);
438 }
439 
441  const codet &src,
442  unsigned indent)
443 {
444  const irep_idt &statement=src.get(ID_statement);
445 
446  if(statement==ID_cpp_delete ||
447  statement==ID_cpp_delete_array)
448  return convert_code_cpp_delete(src, indent);
449 
450  if(statement==ID_cpp_new ||
451  statement==ID_cpp_new_array)
452  return convert_cpp_new(src, indent);
453 
454  return expr2ct::convert_code(src, indent);
455 }
456 
458  const exprt &src,
459  unsigned precedence)
460 {
461  assert(src.operands().size()==2);
462  return convert(src.op0())+"["+convert(src.op1())+"]";
463 }
464 
466  const exprt &src,
467  unsigned precedence)
468 {
469  assert(src.operands().size()==3);
470  return
471  convert(src.op0())+".range("+convert(src.op1())+ ","+
472  convert(src.op2())+")";
473 }
474 
475 std::string expr2cpp(const exprt &expr, const namespacet &ns)
476 {
477  expr2cppt expr2cpp(ns);
478  expr2cpp.get_shorthands(expr);
479  return expr2cpp.convert(expr);
480 }
481 
482 std::string type2cpp(const typet &type, const namespacet &ns)
483 {
484  expr2cppt expr2cpp(ns);
485  return expr2cpp.convert(type);
486 }
expr2cppt::expr2cppt
expr2cppt(const namespacet &_ns)
Definition: expr2cpp.cpp:27
MetaString
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:95
expr2cppt::convert_extractbits
std::string convert_extractbits(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:465
exprt::op2
exprt & op2()
Definition: expr.h:90
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
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:35
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:849
typet::subtype
const typet & subtype() const
Definition: type.h:38
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
typet
The type of an expression, extends irept.
Definition: type.h:27
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
expr2cppt::convert_code_cpp_delete
std::string convert_code_cpp_delete(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:390
expr2cppt::convert_cpp_this
std::string convert_cpp_this(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:358
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
expr2ct::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1787
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
exprt::op0
exprt & op0()
Definition: expr.h:84
expr2cpp.h
expr2ct::convert_code
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3334
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
c_qualifiers.h
expr2cpp
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:475
qualifierst::read
virtual void read(const typet &src)=0
symbol_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:75
qualifierst
Definition: c_qualifiers.h:18
namespace.h
expr2cppt::convert_extractbit
std::string convert_extractbit(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:457
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
lispexpr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
expr2ct
Definition: expr2c_class.h:25
expr2ct::convert
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:183
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
lispexprt::expr2string
std::string expr2string() const
Definition: lispexpr.cpp:15
expr2cppt
Definition: expr2cpp.cpp:24
lispirep.h
expr2cppt::convert_struct
std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:48
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:2458
type2cpp
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:482
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:409
expr2cppt::convert_constant
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2cpp.cpp:109
std_types.h
c_misc.h
exprt::op1
exprt & op1()
Definition: expr.h:87
c_qualifierst
Definition: c_qualifiers.h:60
irept::swap
void swap(irept &irep)
Definition: irep.h:303
code_typet
Base type of functions.
Definition: std_types.h:751
expr2c_class.h
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:259
dstringt::empty
bool empty() const
Definition: dstring.h:75
expr2ct::convert_function
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1263
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
to_symbol_type
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
expr2ct::convert_norep
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1663
lispexprt
Definition: lispexpr.h:74
expr2ct::ns
const namespacet & ns
Definition: expr2c_class.h:46
forall_irep
#define forall_irep(it, irep)
Definition: irep.h:62
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt
Symbol table entry.
Definition: symbol.h:27
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
irept::get_sub
subt & get_sub()
Definition: irep.h:317
is_rvalue_reference
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:139
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
expr2cppt::convert_cpp_new
std::string convert_cpp_new(const exprt &src, unsigned precedence)
Definition: expr2cpp.cpp:365
exprt::operands
operandst & operands()
Definition: expr.h:78
expr2ct::convert_rec
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:188
qualifierst::as_string
virtual std::string as_string() const =0
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
expr2ct::convert_with_precedence
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3428
irept::subt
std::vector< irept > subt
Definition: irep.h:160
std_expr.h
expr2cppt::convert_rec
std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2cpp.cpp:125
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
expr2cppt::convert_code
std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2cpp.cpp:440
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423