cprover
expr2java.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 #include "expr2java.h"
10 
11 #include <sstream>
12 
13 #include <util/namespace.h>
14 #include <util/std_types.h>
15 #include <util/std_expr.h>
16 #include <util/symbol.h>
17 #include <util/unicode.h>
18 #include <util/arith_tools.h>
19 #include <util/ieee_float.h>
20 
21 #include <ansi-c/c_misc.h>
22 #include <ansi-c/expr2c_class.h>
23 
24 #include "java_expr.h"
25 #include "java_qualifiers.h"
27 #include "java_types.h"
28 
29 std::string expr2javat::convert(const typet &src)
30 {
31  return convert_rec(src, java_qualifierst(ns), "");
32 }
33 
34 std::string expr2javat::convert(const exprt &src)
35 {
36  return expr2ct::convert(src);
37 }
38 
40  const code_function_callt &src,
41  unsigned indent)
42 {
43  if(src.operands().size()!=3)
44  {
45  unsigned precedence;
46  return convert_norep(src, precedence);
47  }
48 
49  std::string dest=indent_str(indent);
50 
51  if(src.lhs().is_not_nil())
52  {
53  unsigned p;
54  std::string lhs_str=convert_with_precedence(src.lhs(), p);
55 
56  dest+=lhs_str;
57  dest+='=';
58  }
59 
60  const java_method_typet &method_type =
62 
63  bool has_this = method_type.has_this() && !src.arguments().empty();
64 
65  if(has_this)
66  {
67  unsigned p;
68  std::string this_str=convert_with_precedence(src.arguments()[0], p);
69  dest+=this_str;
70  dest+=" . "; // extra spaces for readability
71  }
72 
73  {
74  unsigned p;
75  std::string function_str=convert_with_precedence(src.function(), p);
76  dest+=function_str;
77  }
78 
79  dest+='(';
80 
81  const exprt::operandst &arguments=src.arguments();
82 
83  bool first=true;
84 
85  forall_expr(it, arguments)
86  {
87  if(has_this && it==arguments.begin())
88  {
89  }
90  else
91  {
92  unsigned p;
93  std::string arg_str=convert_with_precedence(*it, p);
94 
95  if(first)
96  first=false;
97  else
98  dest+=", ";
99  dest+=arg_str;
100  }
101  }
102 
103  dest+=");";
104 
105  return dest;
106 }
107 
109  const exprt &src,
110  unsigned &precedence)
111 {
112  const typet &full_type=ns.follow(src.type());
113 
114  if(full_type.id()!=ID_struct)
115  return convert_norep(src, precedence);
116 
117  const struct_typet &struct_type=to_struct_type(full_type);
118 
119  std::string dest="{ ";
120 
121  const struct_typet::componentst &components=
122  struct_type.components();
123 
124  assert(components.size()==src.operands().size());
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  {
133  if(c.type().id() != ID_code)
134  {
135  std::string tmp=convert(*o_it);
136  std::string sep;
137 
138  if(first)
139  first=false;
140  else
141  {
142  if(last_size+40<dest.size())
143  {
144  sep=",\n ";
145  last_size=dest.size();
146  }
147  else
148  sep=", ";
149  }
150 
151  dest+=sep;
152  dest+='.';
153  irep_idt field_name = c.get_pretty_name();
154  if(field_name.empty())
155  field_name = c.get_name();
156  dest += id2string(field_name);
157  dest+='=';
158  dest+=tmp;
159  }
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.type().id()==ID_bool)
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:
208  const mp_integer int_value = numeric_cast_v<mp_integer>(src);
209  std::string dest="(byte)";
210  dest+=integer2string(int_value);
211  return dest;
212  }
213  else if(src.type()==java_short_type())
214  {
215  // No short-literals in Java, so just cast:
216  const mp_integer int_value = numeric_cast_v<mp_integer>(src);
217  std::string dest="(short)";
218  dest+=integer2string(int_value);
219  return dest;
220  }
221  else if(src.type()==java_long_type())
222  {
223  // long integer literals must have 'L' at the end
224  const mp_integer int_value = numeric_cast_v<mp_integer>(src);
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
233  const ieee_floatt ieee_repr(to_constant_expr(src));
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 
240  return expr2ct::convert_constant(src, precedence);
241 }
242 
244  const typet &src,
245  const qualifierst &qualifiers,
246  const std::string &declarator)
247 {
248  std::unique_ptr<qualifierst> clone = qualifiers.clone();
249  qualifierst &new_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  {
277  const java_method_typet &method_type = to_java_method_type(src);
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 
329 std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)
330 {
331  return indent_str(indent) + convert_java_new(src) + ";\n";
332 }
333 
334 std::string expr2javat::convert_java_new(const exprt &src)
335 {
336  std::string dest;
337 
338  if(src.get(ID_statement)==ID_java_new_array ||
339  src.get(ID_statement)==ID_java_new_array_data)
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(src.type().subtype());
348  dest+='[';
349  dest+=tmp_size;
350  dest+=']';
351  }
352  else
353  dest="new "+convert(src.type().subtype());
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 &&
392  (src.get(ID_statement)==ID_java_new ||
393  src.get(ID_statement)==ID_java_new_array ||
394  src.get(ID_statement)==ID_java_new_array_data))
395  {
396  precedence = 15;
397  return convert_java_new(src);
398  }
399  else if(src.id()==ID_side_effect &&
400  src.get(ID_statement)==ID_throw)
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=
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  {
422  const class_method_descriptor_exprt &virtual_function =
424  return "CLASS_METHOD_DESCRIPTOR(" + id2string(virtual_function.class_id()) +
425  "." + id2string(virtual_function.mangled_method_name()) + ")";
426  }
427  else if(
428  const auto &literal = expr_try_dynamic_cast<java_string_literal_exprt>(src))
429  {
430  return '"' + MetaString(id2string(literal->value())) + '"';
431  }
432  else if(src.id()==ID_constant)
433  return convert_constant(to_constant_expr(src), precedence=16);
434  else
435  return expr2ct::convert_with_precedence(src, precedence);
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 
454 std::string expr2java(const exprt &expr, const namespacet &ns)
455 {
456  expr2javat expr2java(ns);
457  expr2java.get_shorthands(expr);
458  return expr2java.convert(expr);
459 }
460 
461 std::string type2java(const typet &type, const namespacet &ns)
462 {
463  expr2javat expr2java(ns);
464  return expr2java.convert(type);
465 }
MetaString
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:95
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ieee_floatt::is_double
bool is_double() const
Definition: ieee_float.cpp:1174
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:816
ieee_floatt
Definition: ieee_float.h:120
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
typet::subtype
const typet & subtype() const
Definition: type.h:47
expr2javat::convert_java_new
std::string convert_java_new(const exprt &src)
Definition: expr2java.cpp:334
class_method_descriptor_exprt::mangled_method_name
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:3148
arith_tools.h
expr2javat::convert_java_this
std::string convert_java_this()
Definition: expr2java.cpp:316
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:28
java_long_type
signedbv_typet java_long_type()
Definition: java_types.cpp:44
expr2javat::convert
virtual std::string convert(const typet &src) override
Definition: expr2java.cpp:29
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
expr2ct::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1693
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
ieee_floatt::to_float
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
Definition: ieee_float.cpp:1217
java_string_literal_expr.h
Representation of a constant Java string.
java_method_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:746
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
java_expr.h
Java-specific exprt subclasses.
expr2ct::convert_code
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3295
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
qualifierst::read
virtual void read(const typet &src)=0
qualifierst
Definition: c_qualifiers.h:19
namespace.h
expr2javat::convert_java_instanceof
std::string convert_java_instanceof(const exprt &src)
Definition: expr2java.cpp:321
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:3111
expr2javat::convert_with_precedence
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:377
ieee_floatt::to_double
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
Definition: ieee_float.cpp:1186
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
expr2ct::convert
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:187
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
expr2ct::indent_str
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2408
expr2ct::convert_function
std::string convert_function(const exprt &src, const std::string &symbol)
Definition: expr2c.cpp:1188
qualifierst::clone
virtual std::unique_ptr< qualifierst > clone() const =0
expr2javat::convert_code_function_call
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2java.cpp:39
std_types.h
Pre-defined types.
c_misc.h
ANSI-C Misc Utilities.
expr2javat::convert_rec
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2java.cpp:243
expr2c_class.h
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
expr2javat::convert_code_java_delete
std::string convert_code_java_delete(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:358
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
floating_point_to_java_string
std::string floating_point_to_java_string(float_type value)
Convert floating point number to a string without printing unnecessary zeros.
Definition: expr2java.h:62
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
expr2javat
Definition: expr2java.h:22
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
java_short_type
signedbv_typet java_short_type()
Definition: java_types.cpp:50
code_landingpadt::catch_expr
const exprt & catch_expr() const
Definition: std_code.h:2396
expr2javat::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:169
code_typet::has_this
bool has_this() const
Definition: std_types.h:821
expr2javat::convert_struct
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:108
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
java_qualifierst
Definition: java_qualifiers.h:13
expr2ct::convert_norep
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1580
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
expr2ct::ns
const namespacet & ns
Definition: expr2c_class.h:49
to_code_landingpad
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:2420
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
java_double_type
floatbv_typet java_double_type()
Definition: java_types.cpp:74
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
to_class_method_descriptor_expr
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:3201
to_java_instanceof_expr
const java_instanceof_exprt & to_java_instanceof_expr(const exprt &expr)
Cast an exprt to a java_instanceof_exprt.
Definition: java_expr.h:86
expr2javat::convert_code
virtual std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2java.cpp:438
ieee_float.h
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:461
unicode.h
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:454
class_method_descriptor_exprt::class_id
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:3156
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
exprt::operands
operandst & operands()
Definition: expr.h:96
expr2java.h
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:30
java_types.h
expr2ct::convert_rec
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:192
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
utf16_native_endian_to_java
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:318
qualifierst::as_string
virtual std::string as_string() const =0
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
expr2ct::convert_with_precedence
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3381
expr2javat::char_representation_length
const std::size_t char_representation_length
Definition: expr2java.h:52
std_expr.h
API to expression classes.
java_method_typet
Definition: java_types.h:103
java_qualifiers.h
Java-specific type qualifiers.
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
java_float_type
floatbv_typet java_float_type()
Definition: java_types.cpp:68
expr2javat::convert_code_java_new
std::string convert_code_java_new(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:329
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106