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