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
52 dest+=lhs_str;
53 dest+='=';
54 }
55
56 const java_method_typet &method_type =
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);
65 dest+=this_str;
66 dest+=" . "; // extra spaces for readability
67 }
68
69 {
70 unsigned p;
71 std::string function_str=convert_with_precedence(src.function(), p);
72 dest+=function_str;
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+=", ";
95 dest+=arg_str;
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
121 components.size() == src.operands().size(),
122 "inconsistent number of components");
123
124 exprt::operandst::const_iterator o_it=src.operands().begin();
125
126 bool first=true;
127 size_t last_size=0;
128
129 for(const auto &c : components)
130 {
132 c.type().id() != ID_code, "struct member must not be of code type");
133
134 std::string tmp = convert(*o_it);
135 std::string sep;
136
137 if(first)
138 first = false;
139 else
140 {
141 if(last_size + 40 < dest.size())
142 {
143 sep = ",\n ";
144 last_size = dest.size();
145 }
146 else
147 sep = ", ";
148 }
149
150 dest += sep;
151 dest += '.';
152 irep_idt field_name = c.get_pretty_name();
153 if(field_name.empty())
154 field_name = c.get_name();
155 dest += id2string(field_name);
156 dest += '=';
157 dest += tmp;
158
159 o_it++;
160 }
161
162 dest+=" }";
163
164 return dest;
165}
166
168 const constant_exprt &src,
169 unsigned &precedence)
170{
171 if(src.type().id()==ID_c_bool)
172 {
173 if(!src.is_zero())
174 return "true";
175 else
176 return "false";
177 }
178 else if(src.is_boolean())
179 {
180 if(src.is_true())
181 return "true";
182 else if(src.is_false())
183 return "false";
184 }
185 else if(src.type().id()==ID_pointer)
186 {
187 // Java writes 'null' for the null reference
188 if(src.is_zero())
189 return "null";
190 }
191 else if(src.type()==java_char_type())
192 {
193 std::string dest;
194 dest.reserve(char_representation_length);
195
196 const char16_t int_value = numeric_cast_v<char16_t>(src);
197
198 // Character literals in Java have type 'char', thus no cast is needed.
199 // This is different from C, where charater literals have type 'int'.
200 dest += '\'' + utf16_native_endian_to_java(int_value) + '\'';
201 return dest;
202 }
203 else if(src.type()==java_byte_type())
204 {
205 // No byte-literals in Java, so just cast:
206 const mp_integer int_value = numeric_cast_v<mp_integer>(src);
207 std::string dest="(byte)";
208 dest+=integer2string(int_value);
209 return dest;
210 }
211 else if(src.type()==java_short_type())
212 {
213 // No short-literals in Java, so just cast:
214 const mp_integer int_value = numeric_cast_v<mp_integer>(src);
215 std::string dest="(short)";
216 dest+=integer2string(int_value);
217 return dest;
218 }
219 else if(src.type()==java_long_type())
220 {
221 // long integer literals must have 'L' at the end
222 const mp_integer int_value = numeric_cast_v<mp_integer>(src);
223 std::string dest=integer2string(int_value);
224 dest+='L';
225 return dest;
226 }
227 else if((src.type()==java_float_type()) ||
228 (src.type()==java_double_type()))
229 {
230 // This converts NaNs to the canonical NaN
231 const ieee_floatt ieee_repr(to_constant_expr(src));
232 if(ieee_repr.is_double())
233 return floating_point_to_java_string(ieee_repr.to_double());
234 return floating_point_to_java_string(ieee_repr.to_float());
235 }
236
237
238 return expr2ct::convert_constant(src, precedence);
239}
240
242 const typet &src,
243 const qualifierst &qualifiers,
244 const std::string &declarator)
245{
246 std::unique_ptr<qualifierst> clone = qualifiers.clone();
247 qualifierst &new_qualifiers = *clone;
248 new_qualifiers.read(src);
249
250 const std::string d = declarator.empty() ? declarator : (" " + declarator);
251
252 const std::string q=
253 new_qualifiers.as_string();
254
255 if(src==java_int_type())
256 return q+"int"+d;
257 else if(src==java_long_type())
258 return q+"long"+d;
259 else if(src==java_short_type())
260 return q+"short"+d;
261 else if(src==java_byte_type())
262 return q+"byte"+d;
263 else if(src==java_char_type())
264 return q+"char"+d;
265 else if(src==java_float_type())
266 return q+"float"+d;
267 else if(src==java_double_type())
268 return q+"double"+d;
269 else if(src==java_boolean_type())
270 return q+"boolean"+d;
271 else if(src==java_byte_type())
272 return q+"byte"+d;
273 else if(src.id()==ID_code)
274 {
275 const java_method_typet &method_type = to_java_method_type(src);
276
277 // Java doesn't really have syntax for function types,
278 // so we make one up, loosely inspired by the syntax
279 // of lambda expressions.
280
281 std::string dest;
282
283 dest+='(';
284 const java_method_typet::parameterst &parameters = method_type.parameters();
285
286 for(java_method_typet::parameterst::const_iterator it = parameters.begin();
287 it != parameters.end();
288 it++)
289 {
290 if(it!=parameters.begin())
291 dest+=", ";
292
293 dest+=convert(it->type());
294 }
295
296 if(method_type.has_ellipsis())
297 {
298 if(!parameters.empty())
299 dest+=", ";
300 dest+="...";
301 }
302
303 dest+=')';
304
305 const typet &return_type = method_type.return_type();
306 dest+=" -> "+convert(return_type);
307
308 return q + dest;
309 }
310 else
311 return expr2ct::convert_rec(src, qualifiers, declarator);
312}
313
315{
316 return id2string(ID_this);
317}
318
320{
321 const auto &instanceof_expr = to_java_instanceof_expr(src);
322
323 return convert(instanceof_expr.tested_expr()) + " instanceof " +
324 convert(instanceof_expr.target_type());
325}
326
327std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)
328{
329 return indent_str(indent) + convert_java_new(src) + ";\n";
330}
331
332std::string expr2javat::convert_java_new(const exprt &src)
333{
334 std::string dest;
335
336 if(src.get(ID_statement)==ID_java_new_array ||
337 src.get(ID_statement)==ID_java_new_array_data)
338 {
339 dest="new";
340
341 std::string tmp_size=
342 convert(static_cast<const exprt &>(src.find(ID_size)));
343
344 dest+=' ';
345 dest += convert(to_pointer_type(src.type()).base_type());
346 dest+='[';
347 dest+=tmp_size;
348 dest+=']';
349 }
350 else
351 dest = "new " + convert(to_pointer_type(src.type()).base_type());
352
353 return dest;
354}
355
357 const exprt &src,
358 unsigned indent)
359{
360 std::string dest=indent_str(indent)+"delete ";
361
362 if(src.operands().size()!=1)
363 {
364 unsigned precedence;
365 return convert_norep(src, precedence);
366 }
367
368 std::string tmp = convert(to_unary_expr(src).op());
369
370 dest+=tmp+";\n";
371
372 return dest;
373}
374
376 const exprt &src,
377 unsigned &precedence)
378{
379 if(src.id()=="java-this")
380 {
381 precedence = 15;
382 return convert_java_this();
383 }
384 if(src.id()==ID_java_instanceof)
385 {
386 precedence = 15;
387 return convert_java_instanceof(src);
388 }
389 else if(src.id()==ID_side_effect &&
390 (src.get(ID_statement)==ID_java_new ||
391 src.get(ID_statement)==ID_java_new_array ||
392 src.get(ID_statement)==ID_java_new_array_data))
393 {
394 precedence = 15;
395 return convert_java_new(src);
396 }
397 else if(src.id()==ID_side_effect &&
398 src.get(ID_statement)==ID_throw)
399 {
400 precedence = 16;
401 return convert_function(src, "throw");
402 }
403 else if(src.id()==ID_code &&
404 to_code(src).get_statement()==ID_exception_landingpad)
405 {
406 const exprt &catch_expr=
408 return "catch_landingpad("+
409 convert(catch_expr.type())+
410 ' '+
411 convert(catch_expr)+
412 ')';
413 }
414 else if(src.id()==ID_unassigned)
415 return "?";
416 else if(src.id()=="pod_constructor")
417 return "pod_constructor";
418 else if(src.id()==ID_virtual_function)
419 {
420 const class_method_descriptor_exprt &virtual_function =
422 return "CLASS_METHOD_DESCRIPTOR(" + id2string(virtual_function.class_id()) +
423 "." + id2string(virtual_function.mangled_method_name()) + ")";
424 }
425 else if(
426 const auto &literal = expr_try_dynamic_cast<java_string_literal_exprt>(src))
427 {
428 return '"' + MetaString(id2string(literal->value())) + '"';
429 }
430 else if(src.is_constant())
431 return convert_constant(to_constant_expr(src), precedence=16);
432 else
433 return expr2ct::convert_with_precedence(src, precedence);
434}
435
437 const codet &src,
438 unsigned indent)
439{
440 const irep_idt &statement=src.get(ID_statement);
441
442 if(statement==ID_java_new ||
443 statement==ID_java_new_array)
444 return convert_code_java_new(src, indent);
445
446 if(statement==ID_function_call)
448
449 return expr2ct::convert_code(src, indent);
450}
451
452std::string expr2java(const exprt &expr, const namespacet &ns)
453{
455 expr2java.get_shorthands(expr);
456 return expr2java.convert(expr);
457}
458
459std::string type2java(const typet &type, const namespacet &ns)
460{
462 return expr2java.convert(type);
463}
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
std::string MetaString(const std::string &in)
Definition c_misc.cpp:95
ANSI-C Misc Utilities.
An expression describing a method on a class.
Definition std_expr.h:3448
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition std_expr.h:3485
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
Definition std_expr.h:3493
goto_instruction_codet representation of a function call statement.
const exprt & catch_expr() const
Definition std_code.h:1948
bool has_this() const
Definition std_types.h:616
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
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
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
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:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
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
bool is_double() const
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
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
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
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
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:32
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
const code_function_callt & to_code_function_call(const goto_instruction_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
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
BigInt mp_integer
Definition smt_terms.h:18
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
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:3538
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 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