CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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_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,
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
57 src.type().id() == ID_struct_tag
58 ? ns.follow_tag(to_struct_tag_type(src.type()))
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
129}
130
132 const typet &src,
134 const std::string &declarator)
135{
136 std::unique_ptr<c_qualifierst> clone = 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 {
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 ||
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 {
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
374std::string expr2cppt::convert_cpp_new(const exprt &src)
375{
376 std::string dest;
377
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
397std::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 ||
438 {
439 precedence = 15;
440 return convert_cpp_new(src);
441 }
442 else if(src.id()==ID_side_effect &&
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
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
480{
481 const auto &extractbit_expr = to_extractbit_expr(src);
482 return convert(extractbit_expr.op0()) + "[" + convert(extractbit_expr.op1()) +
483 "]";
484}
485
486std::string expr2cpp(const exprt &expr, const namespacet &ns)
487{
489 expr2cpp.get_shorthands(expr);
490 return expr2cpp.convert(expr);
491}
492
493std::string type2cpp(const typet &type, const namespacet &ns)
494{
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base type of functions.
Definition std_types.h:583
std::vector< parametert > parameterst
Definition std_types.h:586
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Definition std_expr.h:3117
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
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
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
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
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:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
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
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Structure type, corresponds to C style structs.
Definition std_types.h:231
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.
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:426
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
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:518