cprover
Loading...
Searching...
No Matches
expr2cpp.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
25class expr2cppt:public expr2ct
26{
27public:
28 explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
29
30protected:
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
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 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(to_reference_type(src).base_type()) + " &" + d;
145 }
146 else if(is_rvalue_reference(src))
147 {
148 return q + convert(to_pointer_type(src).base_type()) + " &&" + 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 for(auto it = arguments.begin(); it != arguments.end(); ++it)
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(to_template_type(src).subtype());
260 return dest;
261 }
262 else if(
263 src.id() == ID_pointer &&
264 to_pointer_type(src).base_type().id() == ID_nullptr)
265 {
266 return "std::nullptr_t";
267 }
268 else if(src.id() == ID_pointer && src.find(ID_to_member).is_not_nil())
269 {
270 typet tmp=src;
271 typet member;
272 member.swap(tmp.add(ID_to_member));
273
274 std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
275
276 const auto &base_type = to_pointer_type(src).base_type();
277
278 if(base_type.id() == ID_code)
279 {
280 const code_typet &code_type = to_code_type(base_type);
281 const typet &return_type = code_type.return_type();
282 dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest;
283
284 const code_typet::parameterst &args = code_type.parameters();
285 dest+="(";
286
287 for(code_typet::parameterst::const_iterator it=args.begin();
288 it!=args.end();
289 ++it)
290 {
291 if(it!=args.begin())
292 dest+=", ";
293 dest+=convert_rec(it->type(), c_qualifierst(), "");
294 }
295
296 dest+=")";
297 dest+=d;
298 }
299 else
300 dest = convert_rec(base_type, c_qualifierst(), "") + " " + dest + d;
301
302 return dest;
303 }
304 else if(src.id()==ID_verilog_signedbv ||
305 src.id()==ID_verilog_unsignedbv)
306 return "sc_lv[" + std::to_string(to_bitvector_type(src).get_width()) + "]" +
307 d;
308 else if(src.id()==ID_unassigned)
309 return "?";
310 else if(src.id()==ID_code)
311 {
312 const code_typet &code_type=to_code_type(src);
313
314 // C doesn't really have syntax for function types,
315 // so we use C++11 trailing return types!
316
317 std::string dest="auto";
318
319 // qualifiers, declarator?
320 if(d.empty())
321 dest+=' ';
322 else
323 dest+=d;
324
325 dest+='(';
326 const code_typet::parameterst &parameters=code_type.parameters();
327
328 for(code_typet::parameterst::const_iterator
329 it=parameters.begin();
330 it!=parameters.end();
331 it++)
332 {
333 if(it!=parameters.begin())
334 dest+=", ";
335
336 dest+=convert(it->type());
337 }
338
339 if(code_type.has_ellipsis())
340 {
341 if(!parameters.empty())
342 dest+=", ";
343 dest+="...";
344 }
345
346 dest+=')';
347
348 const typet &return_type=code_type.return_type();
349 dest+=" -> "+convert(return_type);
350
351 return dest;
352 }
353 else if(src.id()==ID_initializer_list)
354 {
355 // only really used in error messages
356 return "{ ... }";
357 }
358 else if(src.id() == ID_c_bool)
359 {
360 return q + "bool" + d;
361 }
362 else
363 return expr2ct::convert_rec(src, qualifiers, declarator);
364}
365
367{
368 return id2string(ID_this);
369}
370
371std::string expr2cppt::convert_cpp_new(const exprt &src)
372{
373 std::string dest;
374
375 if(src.get(ID_statement)==ID_cpp_new_array)
376 {
377 dest="new";
378
379 std::string tmp_size=
380 convert(static_cast<const exprt &>(src.find(ID_size)));
381
382 dest+=' ';
383 dest += convert(to_pointer_type(src.type()).base_type());
384 dest+='[';
385 dest+=tmp_size;
386 dest+=']';
387 }
388 else
389 dest = "new " + convert(to_pointer_type(src.type()).base_type());
390
391 return dest;
392}
393
394std::string expr2cppt::convert_code_cpp_new(const exprt &src, unsigned indent)
395{
396 return indent_str(indent) + convert_cpp_new(src) + ";\n";
397}
398
400 const exprt &src,
401 unsigned indent)
402{
403 std::string dest=indent_str(indent)+"delete ";
404
405 if(src.operands().size()!=1)
406 {
407 unsigned precedence;
408 return convert_norep(src, precedence);
409 }
410
411 std::string tmp = convert(to_unary_expr(src).op());
412
413 dest+=tmp+";\n";
414
415 return dest;
416}
417
419 const exprt &src,
420 unsigned &precedence)
421{
422 if(src.id()=="cpp-this")
423 {
424 precedence = 15;
425 return convert_cpp_this();
426 }
427 if(src.id()==ID_extractbit)
428 {
429 precedence = 15;
430 return convert_extractbit(src);
431 }
432 else if(src.id()==ID_extractbits)
433 {
434 precedence = 15;
435 return convert_extractbits(src);
436 }
437 else if(src.id()==ID_side_effect &&
438 (src.get(ID_statement)==ID_cpp_new ||
439 src.get(ID_statement)==ID_cpp_new_array))
440 {
441 precedence = 15;
442 return convert_cpp_new(src);
443 }
444 else if(src.id()==ID_side_effect &&
445 src.get(ID_statement)==ID_throw)
446 {
447 precedence = 16;
448 return convert_function(src, "throw");
449 }
450 else if(src.is_constant() && src.type().id()==ID_verilog_signedbv)
451 return "'"+id2string(src.get(ID_value))+"'";
452 else if(src.is_constant() && src.type().id()==ID_verilog_unsignedbv)
453 return "'"+id2string(src.get(ID_value))+"'";
454 else if(src.is_constant() && to_constant_expr(src).get_value()==ID_nullptr)
455 return "nullptr";
456 else if(src.id()==ID_unassigned)
457 return "?";
458 else if(src.id() == ID_pod_constructor)
459 return "pod_constructor";
460 else
461 return expr2ct::convert_with_precedence(src, precedence);
462}
463
465 const codet &src,
466 unsigned indent)
467{
468 const irep_idt &statement=src.get(ID_statement);
469
470 if(statement==ID_cpp_delete ||
471 statement==ID_cpp_delete_array)
472 return convert_code_cpp_delete(src, indent);
473
474 if(statement==ID_cpp_new ||
475 statement==ID_cpp_new_array)
476 return convert_code_cpp_new(src, indent);
477
478 return expr2ct::convert_code(src, indent);
479}
480
482{
483 const auto &extractbit_expr = to_extractbit_expr(src);
484 return convert(extractbit_expr.op0()) + "[" + convert(extractbit_expr.op1()) +
485 "]";
486}
487
489{
490 const auto &extractbits_expr = to_extractbits_expr(src);
491 return convert(extractbits_expr.src()) + ".range(" +
492 convert(extractbits_expr.upper()) + "," +
493 convert(extractbits_expr.lower()) + ")";
494}
495
496std::string expr2cpp(const exprt &expr, const namespacet &ns)
497{
499 expr2cpp.get_shorthands(expr);
500 return expr2cpp.convert(expr);
501}
502
503std::string type2cpp(const typet &type, const namespacet &ns)
504{
506 return expr2cpp.convert(type);
507}
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
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
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
bool has_ellipsis() const
Definition std_types.h:611
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Definition std_expr.h:2942
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:39
bool empty() const
Definition dstring.h:90
std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition expr2cpp.cpp:418
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:394
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition expr2cpp.cpp:112
expr2cppt(const namespacet &_ns)
Definition expr2cpp.cpp:28
std::string convert_code(const codet &src, unsigned indent) override
Definition expr2cpp.cpp:464
std::string convert_extractbits(const exprt &src)
Definition expr2cpp.cpp:488
std::string convert_extractbit(const exprt &src)
Definition expr2cpp.cpp:481
std::string convert_cpp_new(const exprt &src)
Definition expr2cpp.cpp:371
std::string convert_cpp_this()
Definition expr2cpp.cpp:366
std::string convert_code_cpp_delete(const exprt &src, unsigned indent)
Definition expr2cpp.cpp:399
std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition expr2cpp.cpp:128
static std::string indent_str(unsigned indent)
Definition expr2c.cpp:2544
std::string convert_code(const codet &src)
Definition expr2c.cpp:3430
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1612
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:4069
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:1768
const namespacet & ns
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:3633
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
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
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:372
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
bool is_not_nil() const
Definition irep.h:380
subt & get_sub()
Definition irep.h:456
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
std::string expr2string() const
Definition lispexpr.cpp:15
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
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:91
const typet & base_type() const
The type of the data what we point to.
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:503
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition expr2cpp.cpp:496
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#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 unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474