cprover
Loading...
Searching...
No Matches
expr2java.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
9#include "expr2java.h"
10
11#include <util/namespace.h>
12#include <util/std_expr.h>
13#include <util/unicode.h>
14#include <util/arith_tools.h>
15#include <util/ieee_float.h>
16
17#include <ansi-c/c_misc.h>
18#include <ansi-c/expr2c_class.h>
19
20#include "java_expr.h"
21#include "java_qualifiers.h"
23#include "java_types.h"
24
25std::string expr2javat::convert(const typet &src)
26{
27 return convert_rec(src, java_qualifierst(ns), "");
28}
29
30std::string expr2javat::convert(const exprt &src)
31{
32 return expr2ct::convert(src);
33}
34
36 const code_function_callt &src,
37 unsigned indent)
38{
39 if(src.operands().size()!=3)
40 {
41 unsigned precedence;
42 return convert_norep(src, precedence);
43 }
44
45 std::string dest=indent_str(indent);
46
47 if(src.lhs().is_not_nil())
48 {
49 unsigned p;
50 std::string lhs_str=convert_with_precedence(src.lhs(), p);
51
53 dest+='=';
54 }
55
58
59 bool has_this = method_type.has_this() && !src.arguments().empty();
60
61 if(has_this)
62 {
63 unsigned p;
64 std::string this_str=convert_with_precedence(src.arguments()[0], p);
66 dest+=" . "; // extra spaces for readability
67 }
68
69 {
70 unsigned p;
71 std::string function_str=convert_with_precedence(src.function(), p);
73 }
74
75 dest+='(';
76
77 const exprt::operandst &arguments=src.arguments();
78
79 bool first=true;
80
81 forall_expr(it, arguments)
82 {
83 if(has_this && it==arguments.begin())
84 {
85 }
86 else
87 {
88 unsigned p;
89 std::string arg_str=convert_with_precedence(*it, p);
90
91 if(first)
92 first=false;
93 else
94 dest+=", ";
96 }
97 }
98
99 dest+=");";
100
101 return dest;
102}
103
105 const exprt &src,
106 unsigned &precedence)
107{
108 const typet &full_type=ns.follow(src.type());
109
110 if(full_type.id()!=ID_struct)
111 return convert_norep(src, precedence);
112
113 const struct_typet &struct_type=to_struct_type(full_type);
114
115 std::string dest="{ ";
116
117 const struct_typet::componentst &components=
118 struct_type.components();
119
120 assert(components.size()==src.operands().size());
121
122 exprt::operandst::const_iterator o_it=src.operands().begin();
123
124 bool first=true;
125 size_t last_size=0;
126
127 for(const auto &c : components)
128 {
129 if(c.type().id() != ID_code)
130 {
131 std::string tmp=convert(*o_it);
132 std::string sep;
133
134 if(first)
135 first=false;
136 else
137 {
138 if(last_size+40<dest.size())
139 {
140 sep=",\n ";
141 last_size=dest.size();
142 }
143 else
144 sep=", ";
145 }
146
147 dest+=sep;
148 dest+='.';
149 irep_idt field_name = c.get_pretty_name();
150 if(field_name.empty())
151 field_name = c.get_name();
153 dest+='=';
154 dest+=tmp;
155 }
156
157 o_it++;
158 }
159
160 dest+=" }";
161
162 return dest;
163}
164
166 const constant_exprt &src,
167 unsigned &precedence)
168{
169 if(src.type().id()==ID_c_bool)
170 {
171 if(!src.is_zero())
172 return "true";
173 else
174 return "false";
175 }
176 else if(src.type().id()==ID_bool)
177 {
178 if(src.is_true())
179 return "true";
180 else if(src.is_false())
181 return "false";
182 }
183 else if(src.type().id()==ID_pointer)
184 {
185 // Java writes 'null' for the null reference
186 if(src.is_zero())
187 return "null";
188 }
189 else if(src.type()==java_char_type())
190 {
191 std::string dest;
193
194 const char16_t int_value = numeric_cast_v<char16_t>(src);
195
196 // Character literals in Java have type 'char', thus no cast is needed.
197 // This is different from C, where charater literals have type 'int'.
199 return dest;
200 }
201 else if(src.type()==java_byte_type())
202 {
203 // No byte-literals in Java, so just cast:
205 std::string dest="(byte)";
207 return dest;
208 }
209 else if(src.type()==java_short_type())
210 {
211 // No short-literals in Java, so just cast:
213 std::string dest="(short)";
215 return dest;
216 }
217 else if(src.type()==java_long_type())
218 {
219 // long integer literals must have 'L' at the end
221 std::string dest=integer2string(int_value);
222 dest+='L';
223 return dest;
224 }
225 else if((src.type()==java_float_type()) ||
226 (src.type()==java_double_type()))
227 {
228 // This converts NaNs to the canonical NaN
230 if(ieee_repr.is_double())
231 return floating_point_to_java_string(ieee_repr.to_double());
232 return floating_point_to_java_string(ieee_repr.to_float());
233 }
234
235
237}
238
240 const typet &src,
241 const qualifierst &qualifiers,
242 const std::string &declarator)
243{
244 std::unique_ptr<qualifierst> clone = qualifiers.clone();
245 qualifierst &new_qualifiers = *clone;
246 new_qualifiers.read(src);
247
248 const std::string d = declarator.empty() ? declarator : (" " + declarator);
249
250 const std::string q=
251 new_qualifiers.as_string();
252
253 if(src==java_int_type())
254 return q+"int"+d;
255 else if(src==java_long_type())
256 return q+"long"+d;
257 else if(src==java_short_type())
258 return q+"short"+d;
259 else if(src==java_byte_type())
260 return q+"byte"+d;
261 else if(src==java_char_type())
262 return q+"char"+d;
263 else if(src==java_float_type())
264 return q+"float"+d;
265 else if(src==java_double_type())
266 return q+"double"+d;
267 else if(src==java_boolean_type())
268 return q+"boolean"+d;
269 else if(src==java_byte_type())
270 return q+"byte"+d;
271 else if(src.id()==ID_code)
272 {
274
275 // Java doesn't really have syntax for function types,
276 // so we make one up, loosely inspired by the syntax
277 // of lambda expressions.
278
279 std::string dest;
280
281 dest+='(';
282 const java_method_typet::parameterst &parameters = method_type.parameters();
283
284 for(java_method_typet::parameterst::const_iterator it = parameters.begin();
285 it != parameters.end();
286 it++)
287 {
288 if(it!=parameters.begin())
289 dest+=", ";
290
291 dest+=convert(it->type());
292 }
293
294 if(method_type.has_ellipsis())
295 {
296 if(!parameters.empty())
297 dest+=", ";
298 dest+="...";
299 }
300
301 dest+=')';
302
303 const typet &return_type = method_type.return_type();
304 dest+=" -> "+convert(return_type);
305
306 return q + dest;
307 }
308 else
309 return expr2ct::convert_rec(src, qualifiers, declarator);
310}
311
313{
314 return id2string(ID_this);
315}
316
318{
319 const auto &instanceof_expr = to_java_instanceof_expr(src);
320
321 return convert(instanceof_expr.tested_expr()) + " instanceof " +
322 convert(instanceof_expr.target_type());
323}
324
325std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)
326{
327 return indent_str(indent) + convert_java_new(src) + ";\n";
328}
329
330std::string expr2javat::convert_java_new(const exprt &src)
331{
332 std::string dest;
333
336 {
337 dest="new";
338
339 std::string tmp_size=
340 convert(static_cast<const exprt &>(src.find(ID_size)));
341
342 dest+=' ';
343 dest+=convert(src.type().subtype());
344 dest+='[';
345 dest+=tmp_size;
346 dest+=']';
347 }
348 else
349 dest="new "+convert(src.type().subtype());
350
351 return dest;
352}
353
355 const exprt &src,
356 unsigned indent)
357{
358 std::string dest=indent_str(indent)+"delete ";
359
360 if(src.operands().size()!=1)
361 {
362 unsigned precedence;
363 return convert_norep(src, precedence);
364 }
365
366 std::string tmp = convert(to_unary_expr(src).op());
367
368 dest+=tmp+";\n";
369
370 return dest;
371}
372
374 const exprt &src,
375 unsigned &precedence)
376{
377 if(src.id()=="java-this")
378 {
379 precedence = 15;
380 return convert_java_this();
381 }
382 if(src.id()==ID_java_instanceof)
383 {
384 precedence = 15;
385 return convert_java_instanceof(src);
386 }
387 else if(src.id()==ID_side_effect &&
391 {
392 precedence = 15;
393 return convert_java_new(src);
394 }
395 else if(src.id()==ID_side_effect &&
397 {
398 precedence = 16;
399 return convert_function(src, "throw");
400 }
401 else if(src.id()==ID_code &&
402 to_code(src).get_statement()==ID_exception_landingpad)
403 {
404 const exprt &catch_expr=
405 to_code_landingpad(to_code(src)).catch_expr();
406 return "catch_landingpad("+
407 convert(catch_expr.type())+
408 ' '+
409 convert(catch_expr)+
410 ')';
411 }
412 else if(src.id()==ID_unassigned)
413 return "?";
414 else if(src.id()=="pod_constructor")
415 return "pod_constructor";
416 else if(src.id()==ID_virtual_function)
417 {
420 return "CLASS_METHOD_DESCRIPTOR(" + id2string(virtual_function.class_id()) +
421 "." + id2string(virtual_function.mangled_method_name()) + ")";
422 }
423 else if(
425 {
426 return '"' + MetaString(id2string(literal->value())) + '"';
427 }
428 else if(src.id()==ID_constant)
430 else
432}
433
435 const codet &src,
436 unsigned indent)
437{
438 const irep_idt &statement=src.get(ID_statement);
439
440 if(statement==ID_java_new ||
441 statement==ID_java_new_array)
442 return convert_code_java_new(src, indent);
443
444 if(statement==ID_function_call)
446
447 return expr2ct::convert_code(src, indent);
448}
449
450std::string expr2java(const exprt &expr, const namespacet &ns)
451{
453 expr2java.get_shorthands(expr);
454 return expr2java.convert(expr);
455}
456
457std::string type2java(const typet &type, const namespacet &ns)
458{
460 return expr2java.convert(type);
461}
std::string MetaString(const std::string &in)
Definition c_misc.cpp:95
ANSI-C Misc Utilities.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
An expression describing a method on a class.
Definition std_expr.h:3272
codet representation of a function call statement.
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Definition std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
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
std::string convert_code_java_new(const exprt &src, unsigned precedence)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
std::string convert_java_new(const exprt &src)
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
std::string convert_code_java_delete(const exprt &src, unsigned precedence)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition expr2java.cpp:35
const std::size_t char_representation_length
Definition expr2java.h:50
virtual std::string convert_code(const codet &src, unsigned indent) override
std::string convert_java_instanceof(const exprt &src)
virtual std::string convert(const typet &src) override
Definition expr2java.cpp:25
std::string convert_java_this()
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
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_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:64
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
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
const irep_idt & id() const
Definition irep.h:396
std::vector< parametert > parameterst
Definition std_types.h:542
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
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
const typet & subtype() const
Definition type.h:48
std::string type2java(const typet &type, const namespacet &ns)
std::string expr2java(const exprt &expr, const namespacet &ns)
std::string floating_point_to_java_string(float_type value)
Convert floating point number to a string without printing unnecessary zeros.
Definition expr2java.h:60
#define forall_expr(it, expr)
Definition expr.h:30
const code_function_callt & to_code_function_call(const codet &code)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
Java-specific exprt subclasses.
const java_instanceof_exprt & to_java_instanceof_expr(const exprt &expr)
Cast an exprt to a java_instanceof_exprt.
Definition java_expr.h:86
Java-specific type qualifiers.
Representation of a constant Java string.
signedbv_typet java_int_type()
signedbv_typet java_byte_type()
signedbv_typet java_short_type()
floatbv_typet java_double_type()
floatbv_typet java_float_type()
c_bool_typet java_boolean_type()
unsignedbv_typet java_char_type()
signedbv_typet java_long_type()
const java_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:184
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
static code_landingpadt & to_code_landingpad(codet &code)
Definition std_code.h:1972
const codet & to_code(const exprt &expr)
API to expression classes.
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
Definition std_expr.h:3362
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 struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
static void utf16_native_endian_to_java(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
Escapes non-printable characters, whitespace except for spaces, double- and single-quotes and backsla...
Definition unicode.cpp:317