CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
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 = src.type().id() == ID_struct_tag
109 ? ns.follow_tag(to_struct_tag_type(src.type()))
110 : src.type();
111
112 if(full_type.id()!=ID_struct)
113 return convert_norep(src, precedence);
114
115 const struct_typet &struct_type=to_struct_type(full_type);
116
117 std::string dest="{ ";
118
119 const struct_typet::componentst &components=
120 struct_type.components();
121
123 components.size() == src.operands().size(),
124 "inconsistent number of components");
125
126 exprt::operandst::const_iterator o_it=src.operands().begin();
127
128 bool first=true;
129 size_t last_size=0;
130
131 for(const auto &c : components)
132 {
134 c.type().id() != ID_code, "struct member must not be of code type");
135
136 std::string tmp = convert(*o_it);
137 std::string sep;
138
139 if(first)
140 first = false;
141 else
142 {
143 if(last_size + 40 < dest.size())
144 {
145 sep = ",\n ";
146 last_size = dest.size();
147 }
148 else
149 sep = ", ";
150 }
151
152 dest += sep;
153 dest += '.';
154 irep_idt field_name = c.get_pretty_name();
155 if(field_name.empty())
156 field_name = c.get_name();
157 dest += id2string(field_name);
158 dest += '=';
159 dest += tmp;
160
161 o_it++;
162 }
163
164 dest+=" }";
165
166 return dest;
167}
168
170 const constant_exprt &src,
171 unsigned &precedence)
172{
173 if(src.type().id()==ID_c_bool)
174 {
175 if(!src.is_zero())
176 return "true";
177 else
178 return "false";
179 }
180 else if(src.is_boolean())
181 {
182 if(src.is_true())
183 return "true";
184 else if(src.is_false())
185 return "false";
186 }
187 else if(src.type().id()==ID_pointer)
188 {
189 // Java writes 'null' for the null reference
190 if(src.is_zero())
191 return "null";
192 }
193 else if(src.type()==java_char_type())
194 {
195 std::string dest;
196 dest.reserve(char_representation_length);
197
198 const char16_t int_value = numeric_cast_v<char16_t>(src);
199
200 // Character literals in Java have type 'char', thus no cast is needed.
201 // This is different from C, where charater literals have type 'int'.
202 dest += '\'' + utf16_native_endian_to_java(int_value) + '\'';
203 return dest;
204 }
205 else if(src.type()==java_byte_type())
206 {
207 // No byte-literals in Java, so just cast:
209 std::string dest="(byte)";
211 return dest;
212 }
213 else if(src.type()==java_short_type())
214 {
215 // No short-literals in Java, so just cast:
217 std::string dest="(short)";
219 return dest;
220 }
221 else if(src.type()==java_long_type())
222 {
223 // long integer literals must have 'L' at the end
225 std::string dest=integer2string(int_value);
226 dest+='L';
227 return dest;
228 }
229 else if((src.type()==java_float_type()) ||
230 (src.type()==java_double_type()))
231 {
232 // This converts NaNs to the canonical NaN
234 if(ieee_repr.is_double())
235 return floating_point_to_java_string(ieee_repr.to_double());
236 return floating_point_to_java_string(ieee_repr.to_float());
237 }
238
239
241}
242
244 const typet &src,
246 const std::string &declarator)
247{
248 std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
250 new_qualifiers.read(src);
251
252 const std::string d = declarator.empty() ? declarator : (" " + declarator);
253
254 const std::string q=
255 new_qualifiers.as_string();
256
257 if(src==java_int_type())
258 return q+"int"+d;
259 else if(src==java_long_type())
260 return q+"long"+d;
261 else if(src==java_short_type())
262 return q+"short"+d;
263 else if(src==java_byte_type())
264 return q+"byte"+d;
265 else if(src==java_char_type())
266 return q+"char"+d;
267 else if(src==java_float_type())
268 return q+"float"+d;
269 else if(src==java_double_type())
270 return q+"double"+d;
271 else if(src==java_boolean_type())
272 return q+"boolean"+d;
273 else if(src==java_byte_type())
274 return q+"byte"+d;
275 else if(src.id()==ID_code)
276 {
278
279 // Java doesn't really have syntax for function types,
280 // so we make one up, loosely inspired by the syntax
281 // of lambda expressions.
282
283 std::string dest;
284
285 dest+='(';
286 const java_method_typet::parameterst &parameters = method_type.parameters();
287
288 for(java_method_typet::parameterst::const_iterator it = parameters.begin();
289 it != parameters.end();
290 it++)
291 {
292 if(it!=parameters.begin())
293 dest+=", ";
294
295 dest+=convert(it->type());
296 }
297
298 if(method_type.has_ellipsis())
299 {
300 if(!parameters.empty())
301 dest+=", ";
302 dest+="...";
303 }
304
305 dest+=')';
306
307 const typet &return_type = method_type.return_type();
308 dest+=" -> "+convert(return_type);
309
310 return q + dest;
311 }
312 else
313 return expr2ct::convert_rec(src, qualifiers, declarator);
314}
315
317{
318 return id2string(ID_this);
319}
320
322{
323 const auto &instanceof_expr = to_java_instanceof_expr(src);
324
325 return convert(instanceof_expr.tested_expr()) + " instanceof " +
326 convert(instanceof_expr.target_type());
327}
328
329std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)
330{
331 return indent_str(indent) + convert_java_new(src) + ";\n";
332}
333
334std::string expr2javat::convert_java_new(const exprt &src)
335{
336 std::string dest;
337
340 {
341 dest="new";
342
343 std::string tmp_size=
344 convert(static_cast<const exprt &>(src.find(ID_size)));
345
346 dest+=' ';
347 dest += convert(to_pointer_type(src.type()).base_type());
348 dest+='[';
349 dest+=tmp_size;
350 dest+=']';
351 }
352 else
353 dest = "new " + convert(to_pointer_type(src.type()).base_type());
354
355 return dest;
356}
357
359 const exprt &src,
360 unsigned indent)
361{
362 std::string dest=indent_str(indent)+"delete ";
363
364 if(src.operands().size()!=1)
365 {
366 unsigned precedence;
367 return convert_norep(src, precedence);
368 }
369
370 std::string tmp = convert(to_unary_expr(src).op());
371
372 dest+=tmp+";\n";
373
374 return dest;
375}
376
378 const exprt &src,
379 unsigned &precedence)
380{
381 if(src.id()=="java-this")
382 {
383 precedence = 15;
384 return convert_java_this();
385 }
386 if(src.id()==ID_java_instanceof)
387 {
388 precedence = 15;
389 return convert_java_instanceof(src);
390 }
391 else if(src.id()==ID_side_effect &&
395 {
396 precedence = 15;
397 return convert_java_new(src);
398 }
399 else if(src.id()==ID_side_effect &&
401 {
402 precedence = 16;
403 return convert_function(src, "throw");
404 }
405 else if(src.id()==ID_code &&
406 to_code(src).get_statement()==ID_exception_landingpad)
407 {
408 const exprt &catch_expr=
409 to_code_landingpad(to_code(src)).catch_expr();
410 return "catch_landingpad("+
411 convert(catch_expr.type())+
412 ' '+
413 convert(catch_expr)+
414 ')';
415 }
416 else if(src.id()==ID_unassigned)
417 return "?";
418 else if(src.id()=="pod_constructor")
419 return "pod_constructor";
420 else if(src.id()==ID_virtual_function)
421 {
424 return "CLASS_METHOD_DESCRIPTOR(" + id2string(virtual_function.class_id()) +
425 "." + id2string(virtual_function.mangled_method_name()) + ")";
426 }
427 else if(
429 {
430 return '"' + MetaString(id2string(literal->value())) + '"';
431 }
432 else if(src.is_constant())
434 else
436}
437
439 const codet &src,
440 unsigned indent)
441{
442 const irep_idt &statement=src.get(ID_statement);
443
444 if(statement==ID_java_new ||
445 statement==ID_java_new_array)
446 return convert_code_java_new(src, indent);
447
448 if(statement==ID_function_call)
450
451 return expr2ct::convert_code(src, indent);
452}
453
454std::string expr2java(const exprt &expr, const namespacet &ns)
455{
457 expr2java.get_shorthands(expr);
458 return expr2java.convert(expr);
459}
460
461std::string type2java(const typet &type, const namespacet &ns)
462{
464 return expr2java.convert(type);
465}
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:562
An expression describing a method on a class.
Definition std_expr.h:3633
goto_instruction_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:3117
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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
std::string convert_code_java_new(const exprt &src, unsigned precedence)
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)
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator) override
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:224
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:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
An IEEE 754 floating-point value, including specificiation.
Definition ieee_float.h:117
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
bool is_not_nil() const
Definition irep.h:372
const irep_idt & id() const
Definition irep.h:388
std::vector< parametert > parameterst
Definition std_types.h:586
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
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
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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:183
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.
#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:3723
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 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
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:316